FOM: Challenge axioms

[Colin McLarty]

	Here are my axioms for a topos with classical real analysis. Unlike Harvey
in his challenge of Fri, 23 Jan 1998, I write out all 15 axioms. Harvey only
wrote out the 6 simplest of his for ZF, and described two infinite lists of
more--far more complicated than anything I use. 

        Of course some people will feel that 15 is virtually infinite, for
our purposes, and my use of more primitives will tip the scale to make
Harvey's axioms the simpler ones. Or Harvey could extend his language as in
Goedel-Bernays and get a finitely axiomatized theory, but that needs
considerably more axioms than he has given.

	The axioms use a two sorted language, a sort of objects and a sort of
arrows. I write some universal quantifiers with just parentheses, as (f,g,h)
to say "for every arrow f and arrow g and arrow h". I spell out all
existential quantifiers. I have broken the axioms into stages: category
axioms, product axioms, topos axioms, and the axioms for a wpt with choice
and natural numbers to give classical analysis. In the lists of primitives I
include informal explications. The actual axioms are numbered. You will
notice that many of the primitives are definable in terms of others, here I
axiomatize them.

Primitives for a category:
Id(A) the identity arrow on A
F:A-->B   f is an arrow with domain A and codomain B.
M(g,f;h)  h is the composite of f and g.

Axioms for a category:
1.  (f,A,B)  If  f:A-->B then  M(f,Id(A);f) and M(Id(B),f;f)
2.  (f,g,h)(there exist A,B,C) [ (f:A-->B and g:B-->C) iff  
        (for some h)M(g,f;h)]
3.  (f,g,h,k,i,j) (If (M(g,f;k) & M(h,k;j) & M(h,g;i)) then  M(i,f;j))


Extend to axioms for a category with terminal object and cartesian products.
Use these primitives:
1 the terminal object
_x_  cartesian product of two objects.
_x_  cartesian product of two arrows.
p1(_,_) and p2(_,_) two projection arrows from a product

and these axioms:
4.  (A) (There is a unique f:A-->1 )
5.  (A,B) ( p1(A,B):AxB-->A   &   p2(A,B):AxB-->B )
6.  (f,g,A,B,T) ( If  (f:T-->A & g:T-->B) then 
        (there is a unique u:T-->AxB) such that 
                ( M(p1(A,B),u;f)  & M(p2(A,B),u;g) ) )
7. (f,g,A,B,C,D) If (f:A-->B &  g:C-->D) then  
        [fxg:AxC-->BxD & (h,k) If (M(f,p1(A,B);h) and M(g,p2(A,B);k)
                 then (M(p1(C,D),fxg;h) & M(p2(C,D),fxg;k)) ] 

To extend to the topos axioms use these primitives:
B^A  read "B superscript A", the 'set' of functions from A to B.
ev_A,B  read "ev subscript A,B" the evaluation of a function from A to B at
a         value in A.
m(f)  read f is monic, or one-to-one.
*W*  read "upper case Greek Omega", the subset classifier
t the truth value "true".

Use these axioms:
8.  (A,B) ev_A,B :(B^A)xA-->B
9.  (f,A,B,T) If f:TxA-->B then (there is a unique u:T-->B^A)
        such that  M(ev_A,B,uxId(A); f)
10:   t:1-->*W*
11.  (f)[m(f) if and only if (g,h,k)(If M(f,g;k) and M(f,h;k) then g=h)]
12.  (f,A,B) [If (m(f) & f:A-->B) then (there exists a unique u:B-->*W*) 
        such that (h,k,j)[If (M(k,t;j) & M(u,h;j) then 
                (there exists a unique v such that M(f,v;h))]] 


And to get classical analysis by using natural numbers in a well-pointed
topos with choice.

13.  (there exist N, 0,s) such that [0:1-->N & s:N-->N & 
        (for all A,x,f with x:1-->A and f:A-->A)
                (there is a unique u:N-->A) such that 
                (for some h,k) M(u,0;x) & M(u,s;k) & M(f,u;k) ] 
14.   (f,g,A,B) (If [f:A--B & g:A--B & (for all k and for all h:1-->A) 
        M(f,h;k) iff  M(g,h;k)] Then f=g )
15.   (f,A,B) If [ f:A-->B  & [ for every h:1-->B there exists 
        k:1-->A with M(f,k;h)]] Then (for some g:B-->A)M(f,g;Id(B))