Hi Bas,

`thank you - indeed this is a very interesting observation. This was`

`the proof I had in mind when I first claimed that the axiom of choice`

`is provable in OTT. However, I was deluded in believing that OTT/`

`predicative topoi exactly characterize the theory of the setoid`

`model. As you clearly point out this is not the case. To me this is`

`an incompleteness of the formal system (OTT/predicative topoi) wrt`

`the intended interpretation. This should be fixable, leading to OTT+X`

`or predicative topoi + X which should be complete wrt the setoid`

`model. More categorically we could say that X characterizes the`

`predicative topoi obtained by an exact completion of an LCCC - I think.`

## Advertising

Indeed, in the setoid model we can construct a function f : A -> [B] ------------------ lift f : [A -> B]

`if the setoid A is "trivial", i.e. has the identity as its`

`equivalence relation. The construction is exactly the one you point`

`out & it actually corresponds to my previous informal explanation why`

`this is "not unreasonable":`

Note that this is not completely unreasonable: we observe thehidden choice made by f, but we compensate by this by hiding ourknowledge.

`Which setoids have a trivial equality? Certainly all first order`

`types. However, if we start with an extensional theory (which can be`

`justified with the setoid model) than also higher types N -> N have a`

`trivial equality (indeed the extensional equality here is the`

`"finest" equality). Hence we certainly get considerable more than`

`countable choice.`

`Actually, instead of using only [..] we can formulate a more general`

`operator for quotient types, given an equivalence relation ~ : B -> B`

`-> Prop, we define ~' : (A -> B) -> (A->B)->Prop as f ~' g = forall`

`a:A.f a ~ g a. We obtain the following generalisation:`

f : A -> B/~ --------------------- lift f : (A -> B)/~'

`But hang on - what stops us from doing a Diaconescu? Excluded middle`

`doesn't hold in the setoid model, even though we only get P \/ not P`

`where A \/ B = [A + B]. But this would still require that we have P`

`+ not P in the underlying set. So what goes wrong?`

We define the type of non-empty subsets of Bool as NE = Sigma Q : Bool-> Prop.Sigma x:Bool.Q x We define the equivalence relation of extensional equality of subsets ~ : NE -> NE -> Prop (Q,_) ~ (R,_) = forall b:Bool.Q b <-> R b Now we derive: h : NE/~ -> [ NE ]

`which is just the indentity on the underlying elements. The point is`

`that obviously ~ implies the trivial equality of [..].`

Now, if we were able to lift h we get lift h : [ NE/~ -> NE] Obviously, NE/~ isn't a setoid with a trivial equality! The Diaconescu argument shows that we can prove for any P:Prop H : NE/~ -> NE ---------------------- Dia H : P \/ not P = [P + not P] and combining the two using bind we get (lift h) >>= Dia : P \/ not P see below for a Epigram 2+n style proof of Dia. We can also see what goes wrong in general: The principle f : A -> B/~ --------------------- lift f : (A -> B)/~'

`fails because given the setoid A = (A0,~A) the premise gives us an`

`underlying function f0:A0 -> B (for simplicity we assume that B is`

`trivial) s.t. a ~A b implies f0 a ~B f0 b, where to use the same`

`function to construct an element of A -> B we need to show that a`

`~A b implies f0 a = f0 b, and there is no reason to believe this -`

`unless ~A is the equality.`

`The main question is how to characterize abstractly the types A for`

`which lift is valid. Syntactically we could say "All types not`

`containing quotients" but this is not very nice. I'd like a semantic`

`condition for the type.`

Cheers, Thorsten P.S.

`For completeness: Dia itself can be constructed as in the COQ script:`

`we use`

T,F : Bool -> Prop T b = (b=true) \/ P F b = (b=false) \/ P

`by applying H to the equivalence classe <T>,<F> and projecting out`

`the components we get`

t,f : Bool t = fst (H <T>) f = fst (H <F>) snd (H <T>) : t=true \/ P snd (H <F>) : f=false \/ P

`By analyzing the cases of the propositional components we get two`

`cases in which we can prove P (hence we are done with P \/ not P) and`

`one where we have`

t=true f=false

`In this case we can prove not P: we assume p:P and using this we can`

`prove T b, F b for any b and hence T b <-> F <b> and therefore`

`<T>=<F> but then t=f and true=false and we have derived a contradiction.`

On 1 Feb 2007, at 03:10, Bas Spitters wrote:

Hi Thorsten and others, On Tuesday 30 January 2007 21:22:53 [EMAIL PROTECTED] wrote:I do indeed think that Observational Type Theory with quotienttypes shouldbe the language of a Predicative Topos. I don't see in the momentthat thesetoid model would introduce anything which isn't provable in theTypeTheory and at least in the moment I don't see how to prove thecountableaxiom of choice in OTT. Bas, could you explain, please?Assuming that OTT is the internal type theory of a predicativetopos, say aPiW-pretopos (which it seems to be the case), it is not possible toprovecountable choice in OTT. The simple reason is that every topos is aPiW-pretopos and that countable choice(CAC) does not hold in thetopos ofsheaves over the reals. Therefore CAC can not hold in the internaltypetheory (i.e. OTT).Now consider the setoid model. The crucial observation is that thesetoidNat=(N,=_Nat) carries the finest possible equality. Let X=(X',=_X) be a setoid. If we know: forall n in Nat there exists x in X such that (R n x),then, by the construction of the setoid model, there is a functionon theunderlying types f:N->X' such that forall n, (R n (f n))because Nat carries the finest equality f lifts to a function onthe setoidlevel since: If n=_Nat m, then (f n)=_X (f m). Write f':Nat => X for this lifted function. Then forall n in Nat, (R n (f' n)). Thus proving countable choice in the setoid model.This is a well-known argument in Bishop's constructive mathematics.Bishop'streatment of sets lead to the development of setoids by Hofmann.The lecturenotes of the TYPES summer school in Chalmers by Erik Palmgren givea nicepresentation of Bishop set theory in type theory. Bas

This message has been checked for viruses but the contents of an attachment may still contain software viruses, which could damage your computer system: you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.