FOM: Was sind und was sollen die Zahlen

Vladimir Sazonov sazonov at logic.botik.ru
Wed Nov 5 15:56:37 EST 1997

```V. Pratt wrote:

> Those of you who've met and talked with Yessenin-Volpin may have had my
> initial reaction to Vladimir Sazonov's post.  My experience has been
> that it is difficult to see Y-V's point of view.  On rereading it more
> carefully however I see that Vladimir is making the identical point I
> was planning to make in one of my several half-completed on-hold
> replies to Harvey, Martin, etc.  Let me try to develop his (and Rohit
> Parikh's) point in even more detail.

At first reading it was difficult to me to recognize in the
details followed this text the main ideas of that approach.
Note, that the question here is not feasibility notion
as it is but rather its formalizability. If we have nothing to
say on (actual or potential, hypothetical) formalizability then
it hardly has a relation to mathematics.

I also was unable to understand Yessenin-Volpin sufficiently
well.  But I like some of his works on feasibility (I mean those
written in Russian) because they are provocative in the best
sense of this word. Actually I also tried to be somewhat
provocative in my posting. However note again that the main
point of that posting was the fact that feasibility *is
formalizable* like PA or ZFC.  It is this foundational question
which I suggested to discuss.  Moreover, the formalization I
mean is even more rigorous than that of PA or ZFC or FOL because
here we should be much more careful in using formal
abbreviations than in the ordinary mathematics.

Without fixing abbreviation mechanisms allowed we cannot
consider FOL, etc. as completely formalized. A formal proof
should contain all necessary symbols (according to the
definition of what is a proof) like a program in a programming
language (otherwise computer will not `understand' that
program). No, I do not insist that all mathematical proofs in
scientific papers must be formal in this very sense. Let us use
informal (or semiformal) proofs as we like.  The point is that
in some cases as with feasibility we should be much more careful
with the notion of (formal) proof.

Let me illustrate this. I wrote that the `set' of feasible
numbers F is closed under addition (F+F\subseteq F). It cannot
be closed under multiplication because otherwise we could prove
that 2^1000 is feasible (i.e. is in F) by writing the
corresponding (not too long) term 2*2*2*...*2. If we have only
addition operation then it would be completely unrealistic to
write corresponding term having `intended' value 2^1000. We can
only imagine such a term.  But imaginable proof is not a
(genuine formal) proof.

Now, about abbreviations. Traditional mathematical proofs have a
lot of them. E.g. even having no multiplication on F we could
abbreviate x+x as 2*x. Then, as in the previous paragraph, we
would get a proof that 2^1000 is feasible, against our intuition
on F. Therefore, we should prohibit such kind of abbreviations
if we want to formalize F.

On the other hand, if we allow arbitrary abbreviations in the
ordinary mathematics, what the word `arbitrary' does mean here.
We may abbreviate terms, formulas, proofs in various ways (say,
by using some kind of recursion or anything else). It is
possible in principle that some kind of abbreviations is
dangerous and will make, say, ZFC contradictory. Is not Russel's
set {x|x\notin x} (as well as any lambda-term) just such an
abbreviation?

Let us fix those abbreviations which are allowed in the branch
of mathematics we are interesting in and only then call this
branch formalized. Of course, in this case we obliged to use
only completely written proofs (like computer programs) or,
more liberal and comfortable, to give some informal evidence
that such a routine proof may be written. Who can give a guarantee
that recently proved FLT (which is easily formulated so that at
least its very formulation is not a problem) is provable in *pure*
ZFC without any abbreviations.  Which abbreviation schemes are
enough? Will they be enough for the rest of Mathematics? Should
some kind of completeness theorem be proved for FOL + some fixed
abbreviation schemes?

I conclude that abbreviation schemes may serve as essential
mathematical principles (like Choice Axiom or the like) which
must be formulated explicitly. Even if this is not so important
for practical doing the traditional mathematics, it may be
crucial for its hypothetical new branches (such as feasible
numbers). Therefore, this seems to be the subject of f.o.m.

Of course, there have been done numerous researches on abbreviations
(lambda-calculus, etc.) but in somewhat different perspective.