Subject: toposes vs. sets - some simple minded questions and remarks

From: categories <[email-masked]>
Date: Fri, 29 Mar 1996 16:00:52 -0400 (AST)

Date: Fri, 29 Mar 1996 16:23:38 MEZ
From: Thomas Streicher <[email-masked]>

Dear all,

I have been following the discussion on toposes vs. set theory on the network.
The discussion has reminded me of a more ``pragmatic problem'' that a student 
of mine (B. Reus) had to face when formalising some variant of Synthetic Domain
Theory in a very strong impredicative type theory : Calculus of Constructions
with Inductive Types, Extensionality for Functions and Axiom of Unique Choice.
This is almost topos logic : what is missing is the principle that equivalent
propositions are equal but one has the further assumption of a small internal
complete universe.

Anyway, the ``pragmatic'' problem he had to face when actually working inside
the formal system was HOW TO DEAL WITH SUBTYPES.
Notice that the notion of subtype is not the object-oriented one from Computer
Science but the good old-fashoned one from Logic. I will now explain more
explicitely what I mean.

If A is a type and P is a predicate on A then in everyday mathematics 
one does not hesitate to form the type

   { x : A | P(x) }  .

This, of course, is no problem in set theory BUT it definitely is a problem in
higher order logic (HOL) because in the latter one does not have the 
possibility of ``subtype formation'' 
which allows one to turn a predicate into a type.

Now it seems to me that topos logic is more expressive than type theory in
the sense that it allows subtype formation. When one extends HOL by subtype 
formation then any subtype

  { x : A | P(x) } 

has to be accompanied by an inclusion map

    iota_A,P : { x : A | P(x) } >--->  A
    
(together with some axioms governing its use; actually, the only place 
where I could find them spelled out in detail 
is in some lecture notes by Wesley Phoa).

The ``pragmatic'' problem now is that when  a \in A and  P(a) then 
one is not allowed to state

  a \in { x : A | P(x) }   BUT ONLY  iota_A,P(a) \in { x : A | P(x) } .
  
Now when it comes to formalise arguments in HOL augmented by logical
subtypes then notation gets really clumsy as one has to mention the
subtype inclusions all the time.

(Notice that in dependent type theory one can express

  { x : A | P(x) }  as  (\Sigma x : A) P(x)
  
and  iota_A,P is projection on the first argument (saliently assuming
that propositions are ``proof-irrelevant'', i.e. any proposition considered
as a type contains at most one element)).

Now -- to my opinion the ``pragmatic'' superiority of (naive) set theory
over HOL with subtypes is that one may omit all the ``iotas'' and what one
writes down is much more concise. So it is precisely this notational
convenience which makes naive set theory a better linguistic tool for
communicating mathematical constructions and arguments.

But notice that this sloppiness of omitting subtype inclusions renders the
``type-checking'' undecidable -- when one would insist on staying in a typed
framework because in order to check whether

    7653 \in  { x : N |  P(x) }
    
one has to PROVE

    P(7653)
    
which actually is a problem when P is not semidecidable, e.g. when
P(x) is a  Pi-0-1-formula (which e.g. states the consistency of the
formal system in use).

!! It is precisely this undecidability of type-checking which forces us to
stick to an untyped universe despite the fact that in ordinary mathematical
arguments one almost never exploits the strong comprehension principles
of ZF(C)
!!

I am always puzzled by the following two slogans

(1)   Topos Logic    corresponds to      Set Theory
  
(2)   Topos Logic    corresponds to      Higher Order Logic

which can be found in the topos-theoretic literature.  
It cannot be the case that both slogans are literally true 
as one can prove the consistency of Higher Order Logic inside Set Theory 
and therefore Set Theory must be more expressive than Higher Order Logic 
(unless one renders G"odel's Second Incompleteness Theorem to be wrong).

The slogan I would have in mind would be

  Topos Logic     corresponds to      Higher Order Logic with Subtypes .
  
Of course, from the point of view of proof-theoretic strength nothing is
gained by adding Subtypes to Higher Order Logic 
(as this way one surely cannot prove more algorithms to terminate).

So I can understand the slogan   

    Topos Logic    corresponds to      Higher Order Logic
    
in the sense that the logics are equiconsistent.

I definitely would like to know from the experts in topos theory 
which of the correspondences (1) or (2) above is the intended one.
Please, note that this question is not meant as a provocation 
but it simply is curiosity about what the acting person thought 
when slogans (1) and (2) were promoted (beginning of the 70s I presume).

Finally, I would like to ask whether the following impression of mine
is absolutely misleading : 
the correspondence between BZF and topos theory given in the book of
Mac Lane and Moerdijk is a mere equiconsistency result saying that there
is a nontrivial elementary topos iff there is a consistent model of BZF.
If I remember correctly there are given 2 constructions : one turning a
model of BZF into an elementary topos (easy) and a second more complicated
one constructing a model of BZF from an elementary topos.
But that does NOT give an EQUIVALENCE bewteen toposes and models of BZF
as far as I can see.
When I start with a topos E then I get a model M of BZF which in turn gives
rise to a topos E_new but, in general, E and E_new will not be equivalent 
anymore.
Right ??

Sorry for that lengthy and maybe shallow remarks but it is really this
``what I always wanted to know but never dared to ask'' sort of question(s) 
which I now dare to ask as the arena seems to have been opened already
for ``fluffy'' questions. 

Thomas Streicher