[FOM] A formalism for Ultrafinitism
Helene.Boucher at wanadoo.fr
Tue May 25 00:59:13 EDT 2004
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
However (Y) cannot be provable in W, because sp might equal the top
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.
More information about the FOM