[FOM] PA with few symbols.

[Vladimir Sazonov]

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

Does anyone know of any work done on representing PA
> with a fixed finite number of variables, as well as the finite number
> of everything else?

I can understand that this may be considered. But if we have
unbounded number of formulas or formal proofs, why to bother
on unbounded number of variables? (By "unbounded" I mean that
there is no precise bound, say, no longest variable or no biggest
number, etc. - quite a weak version of potential infinity.)

> ------------------------------------------------------------------------------
>         Ultra-finitism: Math done on a computer with limited CPU space
> ------------------------------------------------------------------------------

Actually all mathematical theorems, definitions and proofs
(even on large cardinals or anything else) are of feasible
size and therefore can be done on contemporary or future computers.
There is a technical problem how to do this in a completely
formalized way. People are working on this and this does not
seem impossible. But I do not think they would call their activity
as ultra-finitism. I believe that ultra-finitism or strict finitism
is on formalizing what is feasibly finite - a related but rather
different enterprise which requires reconsidering even the first order
logic as it proves to be inappropriate (at least for a particular
approach to feasibility when no biggest number is allowed).
In particular, feasible mathematics (say, Analysis, if it can be
reformulated in such a framework) might be more appropriate for
more straightforward and efficient implementation in computers.
This may be considered as a possible practical goal of ultra-finitism.
This is also related ideologically with complexity theory.


Vladimir Sazonov