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.


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 the hidden choice made by f, but we compensate by this by hiding our knowledge.

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 quotient types should be the language of a Predicative Topos. I don't see in the moment that the setoid model would introduce anything which isn't provable in the Type Theory and at least in the moment I don't see how to prove the countable
axiom of choice in OTT. Bas, could you explain, please?

Assuming that OTT is the internal type theory of a predicative topos, say a PiW-pretopos (which it seems to be the case), it is not possible to prove
countable choice in OTT. The simple reason is that every topos is a
PiW-pretopos and that countable choice(CAC) does not hold in the topos of sheaves over the reals. Therefore CAC can not hold in the internal type
theory (i.e. OTT).

Now consider the setoid model. The crucial observation is that the setoid
Nat=(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 function on the
underlying types f:N->X' such that
        forall n, (R n (f n))
because Nat carries the finest equality f lifts to a function on the setoid
level 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's treatment of sets lead to the development of setoids by Hofmann. The lecture notes of the TYPES summer school in Chalmers by Erik Palmgren give a nice
presentation 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.

Reply via email to