FOM: IHOL vs topos theory

[Carsten Butz]

Intuitionistic higher order logic (IHOL) vs topos theory.

I apologize for this delayed posting, but I am currently very busy. 

I didn't quite understand some comments from Harvey Friedman and
Stephen Simpson on intuitionistic higher order logic (which is claimed
to be foundation) and topos theory (which is claimed not to be
foundation).
This puzzles me a little (and I guess other categorical logicians
too), so let me describe in some detail the connection, and then see
where we get. For a detailed account I refer to [Lambek-Scott:
Introduction to higher order categorical logic] II.1,II.3,II.11,II.14 etc.

The claim is: IHOL and topos theory are the same.

Of course, this is not completely true, and it needs some explanation.
In the sequel I will use the adjective small to refer to sets instead
of classes. What I say can be proven in a meta-theory which is
sufficiently strong (but weaker than ZF) and which does not
need the law of excluded middle. In particular, all I say is true in
ZF.

Now, IHOL is a type theory (I would prefer, a type language) in which
you have (at least) the basic type \Omega (for the truth-values) and
the type forming operations (-)\times(-) (for product types) and
\power(-) for the power-type. The axioms and rules of inference are
exactly those that you would expect from an intuitionistic higher
order type theory. By a theory, I will mean this "basic" language
enriched with some more basic sorts, some (typed) constants, function
and relation symbols, and a set of axioms in this enriched language. 

Given such a theory  T formulated in intuitionistic higher-order
logic, you can construct a (small) topos E(T), in which exactly the
axioms of T become true. In fact, E(T) comes equipped with some
universal property in the sense that it is minimal with the property
that it makes the axioms of T true.

Conversely, given a (small) topos F there exists a unique language and a
unique theory formulated in this language such that F is equivalent
(as a category) to E(T). I should say that there are many such
theories with this property, but to be sure that one extracts a unique
type theory from the topos F one can chose the maximal such theory,
formulated in the signature with basic sorts the objects of the topos
(category) F.

These two "constructions" are mutually inverse in the following sense:
Starting with a topos F, constructing T (depending on F) and then
building up E(T) gives a topos that is equivalent to F, i.e., 
 F \cong E( T_F ).
Starting with a theory T formulated in the language L 
we first get E(T) and then the theory T' that
we extract from E(T). The underlying language L' of T' is always
bigger than the one we started with, but there is a canonical
interpretation of L in L', and in fact, L' is an extension of L by
definitions. (The situation is similar as on a much lower level
similar as to the situation of vector spaces over a field, which you
can formulate as a one-sorted theory or as a two-sorted theory, but
there is no real difference between the two axiomatizations. 

The whole business can even be made into an equivalence of (large)
categories, where on one side you have (small) toposes and so called
logical functors between them, and on the other side type theories
with "interpretations" as morphisms between them. 

Now what categorical logicians are puzzled about is why Simpson and
may be Friedman call IHOL a topic of fom, but topos theory not. 
Possible answers could be the following:
(1) It's a similar situation as with set-theory: studying models of ZF
is the topic of (formal) set-theory, but not of fom.
Similar with topos theory: studying a model (or the models) of a
higher-order type theory is topos-theory, but not fom.

Discussion: In our writings we
often use the following phrases: "We work in a base-topos called ..."
we then use S to denote this base topos if we want to emphasize the 
intuitionistic character of our proofs, but we write very often for 
simplicity Sets for this base-topos.

Question: Would Harvey Friedman and Stephen Simpson say that there is
something like THE one base topos, and figuring out the properties of this
base-topos is the real question of fom?

(2) Sorry about the confusion we caused, topos theory is fom.

Discussion: No discussion, although I doubt that I will get this
response. 

(3) [Simpson in a private mail to me:] But they [IHOL and topos
theory] aren't the same thing.  The primitives are different.  The
motivation is completely different.  Topos theory is motivated by some
technical problems in algebraic geometry (I think, but let the topos
theorists explain that).  IHOL is motivated by an analysis of
Brouwer's intuitionistic ideas for f.o.m.

Discussion: Well, I don't care too much about the "original"
motivation, in particular, since it is only partly true what you
proposed. 
Grothendieck topos theory was invented to solve some problems in algebraic
geometry, but the theory of (elementary) toposes was done in parallel
and for different reasons. In fact, one of the motivations was to
axiomatize the properties of the base-topos Sets !!

{My apologies to Stephen Simpson for bringing something up from a very
short private discussion with him. If "his" statement causes confusion
this is caused by me, since I took his statement out of the context.}


Let me make another remark by quoting from [MacLane-Moerdijk], p. 275,
l. 10 (the paragraph starting after the proof of Proposition VI.1.6):
"A next property which (according to the authors) the category {\bf
Sets} enjoys is the {\em axiom of choice\/}."

This suggests very much that some people (like maybe Mac Lane and
Moerdijk) think there IS something like THE base-topos. 

I am not sure whether I would sign such a statement but that's another
story, and in fact, this does not affect too much the claims made earlier. 
Instead of reading the quote as a capitulation of the topos theorists
you should read it as the flexibility of the foundational views of
topos theorists.


Regards,

  Carsten Butz


Carsten Butz
Research Associate
Department of Computer Science, University of Aarhus (Denmark)
Research interests: Categorical logic, topos theory, homological algebra
WWW: http://www.brics.dk/~butz/