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.
