FOM: Challenge axioms, final draft

[Colin McLarty]

        Here is a final version of the challenge axioms. First, let me clear
up a misconception Soren Riis and others have about what they accomplish.
They do not test the adequacy to analysis of a well-pointed topos with
natural numbers and choice. The theory of such a topos was given by Lawvere
and Tierney over 25 years ago and has been well known ever since as first
order expressible and adequate to classical analysis--in fact, equivalent to
Zermelo set theory with bounded comprehension and the axiom of choice. All
these axioms do is show my version of first order expression of the theory.
No one I know of has ever actually put it all in formal first order logic
before. That includes me, in my post of 1/30/98, where I meant to do so but
had some mistakes, notably the lack of a non-triviality axiom. Those axioms
are indeed satisfied in a universe with one set (and Vaughan Pratt correctly
describes the resulting ambiguity of this "set", at once empty and a
singleton and more).


Compared to the earlier post: In axioms 2 and 7 I correct typos. Axiom 8 was
redundant, implied by 1 and 9, I eliminated it without changing other
numbers. In axiom 10 I specialize to give Booleanness immediately, I cut out
the general axiom for a subobject classifier, and I add a non-triviality
condition lacking in the earlier posted version. Axiom 12 earlier said every
subset has a characteristic function, the new version adds that every
function to 1+1 is characteristic function to some subset. I thank
especially Soren Riis, Niel Tennant, and Steve Simpson for corrections.
  
	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 existential
quantifiers. I have broken the axioms into stages. In the lists of
primitives I include informal explications. The actual axioms are numbered.

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) [ (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,C);h) and M(g,p2(A,C);k)
                 then (M(p1(B,D),fxg;h) & M(p2(B,D),fxg;k)) ] 

To extend to a non-trivial Boolean topos use these primitives:
1+1 A disjoint union of two copies of 1
i1 and i2 will insert the copies of 1 into 1+1 
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.

Use these axioms:

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:   not-(i1 = i2) & [(f,g,A) If f:1-->A & g:1-->A Then (there is
        a unique u:1-->A such that M(u,i1;g) & M(u,i2;g)]
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-->1+1) 
        such that (h,k,j)[If (M(i1,k;j) & M(u,h;j) then 
                (there exists a unique v such that M(f,v;h))]]
        And (u,h,k,j)[If (u:B-->1+1 & M(i1,k;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))