[FOM] A formalism for Ultrafinitism

Tue May 25 13:20:56 EDT 2004

This is amended and further reconsidered version of my posting to
FOM (sent on 21/05/04), in request of the list moderator because of
excessive quotation of the original posting of Taylor.

W.Taylor at math.canterbury.ac.nz wrote:

 > 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.

I already mentioned such kind of theory with the biggest number
in FOM. See also related parts in

V.Yu.Sazonov, On Bounded Set Theory, 10th International, Congress on
Logic, Methodology and Philosophy of Sciences, Florence, August 1995,
in Volume I: Logic and Scientific Method, Kluwer Academic Publishers,
1997, pp. 85--103
http://www.csc.liv.ac.uk/~sazonov/papers.html

with some proof-theoretic result (related to the problem P=?NP) on
such a theory (actually on its second order version).
Such a theory was also introduced at the end of an earlier paper

V.Yu.Sazonov, A logical approach to the problem `P=?NP',
Proc of MFCS, LNCS 88, 1980, 562-575.

[
Once I presented this reference here, I should mention an
important correction to this paper (not related with the
above arithmetics with the biggest number) given at the
end of

V.Yu.Sazonov, On existence of complete predicate calculus in
metamathematics without exponentiantion,
Proc of MFCS, LNCS 118, 1981, 483-490.
]

Of course, Jan Mycielski: "Analysis without Actual Infinity".
Journal of Symbolic Logic, vol. 46, number 3, 1981, pp. 625-633,
should be mentioned, too. Although I would rather call this paper
"Analysis without Potential Infinity" because postulating the
biggest number is a way to axiomatically reject Potential Infinity.
The abstraction of Potential Infinity consists, at least, in
our ability to always add 1. (Actually, it assumes also
any *iterations* of this ability giving rise to  "+" and
further iterations "*", exp, superexp, primitive recursion,
"and so on". But does anybody know particularly how "and so on"??
I consider this question especially important to realize
that N is a vague concept.)

This nice work of Mycielski deserves a separate discussion.
I would not say that it is about "ultrafinitism" (as I
remember, the biggest number should be sufficiently big,
but not fixed there).  Anyway, a finitistic approach to
(non-standard) Analysis is developed there and it is
shown that consistency of this Finitistic Analysis
can be proved in PRA.

I currently call first-order version of the theory I considered
in op. cit. as PA_Box or Box-Arithmetic with \Box (in Latex
notation just a box symbol) symbolizing the biggest element
whose value is non-determined by the axioms. It can be 7, 1000,...
or some nonstandard number. Box may be considered as a parameter.

Of course, this theory, if considered with successor operation only,
is too weak. Even in the ordinary PA we need + and *. It were
included in the Box-Arithmetic symbols for all (Box-)recursive
functions and their fixed point equations. Box-primitive recursive
functions are there as partial case.

(Global) Box-recursive functions prove to be exactly (natural
representations) of all polynomial time computable functions
[Sazonov 1980, Gurevich 1983]. Thus, PA_Box is just a theory
of polynomial-time computability.

Box-primitive recursive functions = LOGSPACE computable [Gurevich 1983].

In comparison with PA, we cannot diagonalize in PA_Box to show
(i) that there are more recursive functions than primitive recursive
ones,
(ii) that second-order quantifiers cannot be eliminated (what is
essentially the problem P=?NP),
(iii) that second-order version of PA_Box is stronger than PA_Box
itself (another, proof-theoretic analogue of the problem P=?NP).

Thus, *informally*, we do not know here whether recursive functions
are not "all" possible functions. Some independence result was
obtained in the op. cit. (1980) concerning P=?NP via this line
of thought. (We can consider a non-trivial concept of finite
recursive or constructive object vs. arbitrary one and work with
this in precise mathematical terms to check whether it is
*consistent* that they coincide.)

 > 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.

What is the point (except the tradition and believing in Induction
Axiom which I criticized in another posting) that exp and even
multiplication should be total? It makes sense to consider Exp
and multiplication (of numbers in unary notation) as partial
functions because, unlike +, they so easily lead to numbers which
do not correspond to anything existing in our world. Is not this
enough just to try? This can give some new insight... Such kind of
experiments with axioms is quite normal for mathematical thought.

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.

The informal meaning of this top or Box number is a resource
bound which exists in any computer. In our real life we always
deal with bounded resources. This is a good abstraction from reality. 
However, because of Box, the meaning of the ordinary arithmetical
operations changes. So, its role is rather specific (although
interesting!). When we postulate that there is no biggest number,
the convenient intuitive and computational meaning of arithmetical
operations remains essentially the same even if they are allowed to
be partial. We already know very well, that *considering partial
functions is inevitable* in computability theory. It happens that
in practice exp is partial. Let us formalize this *real* fact.
Why not? Consider this as a challenge. What can be formalized
mathematically? Can infinity fit before 2^1000 (like before any
non-standard number)? 2^1000 *is* intuitively non-standard in
the sense that it is an imagined, "non-existing in reality" number.

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

This approach with the biggest number is rather an approach to
descriptive complexity theory although it has some relation to
ideas of feasibility.

I consider the approach via the axiom like
            forall n log log n < 10
more appropriate for the concept of feasibility.

This might look not so much aesthetic, but (i) this experimental
law corresponds to the reality and (ii) a consistent formalization
of numbers (without any Box) satisfying this law is possible, which
is, in a sense, non-trivial (in the ordinary classical logic a
contradiction follows from this axiom) and is also related with
proof theory in an interesting way. (iii) There are also intriguing
consequences of this axiom. See a formalization called FEAS in my
paper "On Feasible Numbers" in the above Web page.

------------------------------------------------------------------------------
 >              And God said

Are you sure? How do you know? Have you a direct contact?

 >              Let there be numbers
[...]

Vladimir Sazonov