FOM: cats/sets

[Jaap van Oosten]

I react (belatedly) to Professor Simpson's message of
1/26, the one answering Awodey.

1. For me, toposes belong to the realm of semantics. If
intuitionistic higher order logic is "perfectly respectable
f.o.m. research" then so is the study of its models, i.e.
topos theory.
One of the most illuminating examples of the usefulness of
toposes was, for me, Hyland's "effective topos". I had been
doing some "f.o.m. research" on realizability, that is: a 
recursive interpretation of intuitionistic arithmetic. Hyland's
paper showed that different threads of research (Kleene's 1945
definition, the Russian Markov school of constructivism based
on algorithms, the Kreisel/Troelstra work on formalised realizability
for second order arithmetic) fit very harmoniously into one universe 
of discourse.
One of the great benefits of the topos point of view is that 
although a priori there might be several realizability models for,
say, second order arithmetic, in the topos there is a canonical
one. Similarly there are objects of reals, and there is no problem
with dealing with higher order statements about them, like that
every bounded subset has a least upper bound.
In a paper in APAL 70 (1994), 87-111 I developed axiom systems
which characterize formalized realizability for higher order
arithmetic; this treatment was directly inspired by the effective
topos.

2. The definition of a topos (I don't bother about "fully formal"
because to me it is semantics) may not be simple, but is
comparable to the definitions of forcing models of set theory, or
the "monster model" which is the starting point of stability theory.

> There is no way for the logically disinclined to study IHOL (=
> intuitionistic higher order logic). If you leave out logic, you leave

With all due respect, this is nonsense, as Brouwer himself was
certainly "logically disinclined". It would also discredit model
theory which is the syntax-free study of logic. It is one of the more
fascinating aspects of logic that such a study is possible.

3. Are toposes, or category theory in general, a full-fledged foundation
of mathematics, competing with set theory? At this moment, definitely
not: all treatments of category theory (whether they want to be vague
about it or not) still depend on some primitive idea of "set".
I think that a purely categorical foundation is possible (starting
with an appropriate axiomatization of CAT as a 2-category; work in 
this direction has been done by Ross Street), but one shouldn't claim
results that no one has written down.

4. 
> If it turns out that the fully formal topos axioms have 50 times as
> many bytes as the fully formal set theory axioms, don't you think that
> would be interesting?

Well...Simplicity of a theory, to me, means that I easily understand its
models, or what a model of the theory is. Suppose I add an axiom to the
theory of groups, forcing this theory to have exactly one model. I have
added "bytes", but simplified the theory.

5. 
> If you
> think that there is a coherent conception of the mathematical universe
> underlying your claims of "categorical foundations", please state that
> conception.

Soory, but I find "coherent conception of the mathematical universe"
highfaluting nonsense. We're like Newton, gathering pebbles at the beach,
with an ocean of knowledge, unexplored, before us. We have no idea!

Jaap van Oosten
position: research fellow
Institution: Utrecht University
Research interest: mathematical logic