FOM: Topos theory need not be logicism

[Till Mossakowski]

Soren Riis wrote:

>It is quite clear that the axioms as given by McLarty are satisfied
>by a model containing only one point (the terminal category). To make 
>sure I double checked this with McLarty as well as other Cat-people on 
>the list. They agree. To my sheer frustration one person did not see this 
>as problem. His reply: "Of course, you can't get something from nothing.  
>If you want to prove that something exists, you must put in some 
>assumption to that effect".
>
>Aha - they are Anarkists!! Or is it post-modernism showing us its
>ugly face of relativism - in mathematics? I cannot believe what 
>I hear. Choose your own assumptions - everything goes!!

This is not what is proposed in the book by Lambek and Scott.
Let me cite them:
"We believe that type theory is the proper foundation for mathematics.
 We believe that the free topots, constructed linguistically but
 determined uniquely (up to isomorphism) by its universal property,
 is an acceptable universe of mathematics for a moderate intuitionist
 and, therefore, that Platonism, formalism and intuitionism are
 reconcilable philosophies of mathemetics."

A "topos" here means a topos with NNO.

Lambek and Scott call a topos M with the following properties
a "model":

(a) no contradiction holds in M (this rules out the one-point topos)
(b) if p or q holds in M, then either p holds in M or q does
(c) if \exists x:A \phi(x) holds in M, then there is an entity
    a of type A in M (actually an arrow a:1->A) such that \phi(a)
    holds in M

Now the free topos actually is a model.

Thus McLarty's axioms should be extended by the statement:
	"the topos is free"
which is equivalent to some distinctness principles plus
some induction principles (in the same style as the Peano
axioms for natural numbers). The induction principles are not 
expressable in first-order logic, but they are second-order axioms
(as with Peano axioms, a first-order axiom scheme may be
used as an approximation which is strictly weaker).

Till Mossakowski

------------------------------------------------------
Till Mossakowski
Fachbereich 3 - Informatik
Universitaet Bremen
Postfach 330440
D-28334 Bremen
Germany
Phone +49-421-218-2935
Fax +49-421-218-4322
E-mail: till at informatik.uni-bremen.de
www: http://www.informatik.uni-bremen.de/~till
------------------------------------------------------