[FOM] A formalism for Ultrafinitism

[Andrew Boucher]

Recall the first-order system of Bill Taylor (Thu May 20).  Call it W.

It might be preferable to have the exponential (and sequential, 
additive, and multiplicative) operators possibly partial rather than 
continually having to put the condition "x = Sx" in the axioms and many 
theorems e.g. the Cancellation Laws.

The main drawback that I see of using FOL is that the existence of 
sequences is not assured in W.  In SOL big letters provide sequences 
automatically , but in FOL they are provided by mechanisms such as the 
Chinese Remainder Theorem, where a sequence of numbers n1,n2,....,nk 
are coded by a much bigger number n.  The existence of n, of course, 
cannot be proven in W (knowing the existence of n1,n2,...,nk).

Without sequences it seems dubious that W can state and prove versions 
of the Euclidean Algorithm or the Fundamental Theorem of Arithmetic 
(existence and uniqueness of prime factorization).  Propositions which 
depend on them may thus be out of reach of W.

Indeed without sequences W does not even seem to have access to 
recursion and e.g. is unable to define the exponentiation relationship 
from addition and multiplication.  Perhaps W just assumes 
exponentiation as primitive?  Or is there something else going on here 
which I am misconstruing?

Finally, consider the following proposition:
	(X)  if a prime p divides xy, then p divides x or p divides y.

This is typically proven as follows.  Suppose p does not divide x.  
Then (we are working in the natural numbers, not the integers):
	(Y) there exist s,t such that 1 = sp - xt.
Then y = spy - xty.  Since p divides both terms on the RHS, it divides 
y.

However (Y) cannot be provable in W, because sp might equal the top 
number.

In SOL the proof can be repaired by appealing directly to the Euclidean 
Algorithm or by using recursion, but these avenues may again not be 
open in W.

So it would be interesting to would be to see whether one can prove (X) 
in W and, if so, what the proof looks like.

I do agree with Bill's assessment that these approaches, by W or in 
SOL, are more "honest" approaches to ultrafinitism.