No subject

Soren Riis sriis at
Sun Feb 1 11:30:13 EST 1998

Categorical foundation axioms needs the touch of infinity

First let me thank Colin McLarty for clarifying some 
concrete questions to his axioms. Also I would like 
to thank Vaughan Pratt (as well as others) for their 
answer to a question I asked [Soren Riis, Tue 27 Jan 1998]. 
Not only did they answer my question, but they made me 
want to learn more Category Theory. 

I might be mistaken, but I think Colin McLarty's axioms
needs some addition. It might be a good idea to clarify
this before Friedman and other starts looking at the axioms.
All functions in McLarty's system are essentially got by 
iterating basic operations like projections, embeddings, 
quotient maps and pullbacks etc. - starting with N and a 
few constant maps. These are the only kind of functions 
McLarty's axioms seems to introduce. I think McLarty's 
axioms needs some modification, otherwise we do not get 
enough functions. 
It also puzzles me that McLarty can do with only finitely 
many axioms. Let me explain why I think this is a problem:

Any axiom-system which is strong enough to do analysis 
must have a deductive strength at least that of ACA_0.
Now Peano's Arithmetic (the usual first order axiomatization 
of N) do not have any extension which is finitely axiomatizable. 
Thus ACA_0 (or any other system for analysis) must as far as 
I can see contain infinitely many axioms.
Sometimes this fact is somewhat disguised because one is using 
higher order logic and thus have smuggled in an infinite 
axiom-schema in the underlying rules. McLarty did not specify 
any rules for his system (so unlike the axioms for set-theory
[Harvey Friedman, Fri 23 Jan 1998] a computer wouldn't quite know 
what to do with McLarty's axioms).  I think we need to add some 
sort of rule for set-formation to McLarty's axioms.
Any constructive suggestions?
McLarty's system still haven't got this little touch of 

Soren Riis

More information about the FOM mailing list