[FOM] A formalism for Ultrafinitism

[W.Taylor@math.canterbury.ac.nz]

This is a probably naive approach to the matter, but it strikes me
that it could be useful.

It is an attempt to provide a formalism for Ultrafinitism, flexible
enough to allow the option of an unspecified upper bound on numbers,
but not necessarily insisting on it.  It is also designed to be as
close to PA as possible, so as to allow almost all basic theorems
to go through unchanged.

It may merely turn out to be one of the previous formalisms,
such as the clever attempt to demarcate the axiom "ad infinitum",
but it seems a useful alternative viewpoint to me.


We use the usual axioms for FOL and notations for PA.

Axioms.
------
A. All the usual commutative, associative, distributiove axioms
   and special results for 0 and/or 1.

B. Single top number.   E[<=1] x : x = Sx

C. No cycles.           Ax,y  Sx = Sy => [x=y or x=Sx or y=Sy]

D. Induction on normal numbers.
       phi(0) and [phi(x) and x=/=Sx => phi(Sx)]  =>  Ax phi(x) or x=Sx

If it is absolutely required that there BE a top number, (though still
of unspecified magnitude), B can replace the at-most-1 quantifier by E!x

.........

One advantage of this approach is that we apparently do not get
the result that the exp function is only partial; a restriction
I never really saw the point of.  An ultrafinitist who doesn't
want 10^10^10 or whatever, can merely add an axiom that
the top number has certain appropriate properties.

Of course, any additions, multiplications etc that "go above"
the top number merely have the top number as their value. 
AFAICS that leads to no contradictions.

Does this approach have any obvious problems?
It seems a much more "honest" approach to ultrafinitism than others.

------------------------------------------------------------------------------
             Bill Taylor             W.Taylor at math.canterbury.ac.nz
------------------------------------------------------------------------------
             And God said
             Let there be numbers
             And there *were* numbers.
             Odd and even created he them,
             He said to them be fruitful and multiply
             And he commanded them to keep the laws of induction.
------------------------------------------------------------------------------