FOM: Was sind und was sollen die Zahlen

[Vladimir Sazonov]

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.


Vladimir Sazonov
-- 
Program Systems Institute,  	| Tel. +7-08535-98945 (Inst.), 
Russian Acad. of Sci.		| Fax. +7-08535-20566
Pereslavl-Zalessky,		| e-mail: sazonov at logic.botik.ru 
152140, RUSSIA			| http://www.botik.ru/~logic/SAZONOV/