FOM: feasibility

[Vladimir Sazonov]

I am sorry for the late reply. Also note, that some of the
following have been presented in my postings to fom.

Harvey Friedman wrote:
>
> I have no quarrel with Sazonov that investigating the notion or notions of
> feasibility sounds interesting and promising. The only issue might be: what
> kind of results would make this into a serious ongoing subject, with deep
> and surprising results? I'm not sure we are there yet.
>
> I would like to come back to the kind of thing you said Parikh did. Let
> PA(F) be Peano arithemtic formulated without the unary predicate F for
> feasible, together with the single axioms:
>
> F(0).
> (forall x)(F(x) implies F(x+1)).
>
> We also allow abbreviations; i.e., we can introduce new predicates by
> explicit definition. This shortens formulas, and hence proofs.
>
> Let 2^[n] be an exponential stack of n 2's.

Alternatively, it can be used the notation 2_n^m for the
exponential tower

			      m
			     2
			    .
			   .
			  .		n times "2"
			 2
			2

> Obviously, we can prove in
> PA(F) that F(2^[n]). A question is: how many symbols in such a proof? The
> answer is: linear in n with a small constant. Also, it appears that you
> need only a tiny fragment of PA for this. Just standard quantifier free
> information about 0,S,+,x,exp. Conversely, how many symbols are required
> for such a proof? Again, the answer seems to be: linear in n with a small
> constant.
>
> How explicit are the known estimates?


There are the following issues which may be discussed in
connection with formalizing feasibility:

1. The aspect of length of proofs, lower and upper bounds.
2. The intended *informal* interpretation of a theory of feasibility.
3. What are deep and surprising results?
4. Using abbreviations in proofs.
5. Which are possible applications and perspectives?

Let me consider these in turn.

1&2. According to the paper of Parikh let PA(F) also contain
symbols for all primitive recursive functions and corresponding
recursive equations. Postulate also closure of F under 0,
successor and <. Finally, include that axiom \neg F(\theta) for
some primitive recursive constant term denoting a big number.
For the case of your above question, let \theta = 2_m (or 2^[m]
in your notation) for m another prim. rec. term, desirably
rather short, say 1000 or 2^1000).

Let P be any tree-like Hilbert-style proof in PA(F) (say, of a
contradiction 0 = 1 which, by reductio ad absurdum, would the
proof the statement F(\theta) from the rest of axioms). Let also

c = c(P) = the number of quantifier axioms A(t) => Ex A(x) in P
where F occurs in A;

r = r(P) = the largest number of quantifiers in these formulas A
and

n = n(P) = the number of occurrences in P of the axiom F(x) =>
F(succ(x)).

Theorem 2.2a [Parikh, JSL, 1971] Let P be a proof in PA(F) of a
closed formula B [say 0 = 1, - V.S.] which does not contain F
and, moreover, let

		\theta > n*2_r^{c(c+1)/2}.

Then the pure PA also proves B.


In particular, the above inequality holds for

	\theta = 2_{2^1000}

(or = 2^[2^1000] in your notation), and arbitrary n, r, k <
2^995.  This guarantees *feasible consistency* of PA(F) with
such \theta (or *almost consistency* in terms of Parikh himself). 
This \theta serves as concrete *upper bound* for the "set" of
"feasible" numbers F. (Note that taking \theta = 2_1000 instead
of 2_{2^1000} will not suffice to get almost consistency of
PA(F) in this way!)

The proof of Th.2.2a is based on translating PA(F) and any proof
P into a Hilbert's epsilon-calculus and then on eliminating
epsilon symbols with estimating the growth of proof length.
Alternatively it can be used cut elimination technique as it was
done later by Albert Dragalin. We know that an upper bound of
cut elimination or elimination of epsilon symbol is
non-elementary. This is why the above expression with growing
tower n*2_r^{c(c+1)/2} arise and why we should take above the
upper bound \theta on feasible numbers to be "non-elementary"
natural number 2_{2^1000}.

I included above the word 'feasible' in quotes because this
formalization of feasibility is still rather far from the
desired ideal.  Indeed, as you have actually noted yourself, 
there exists a feasible (without quotes!) proof in PA(F) of the 
statement F(2_1000).  Note that the latter is based on a short 
proof in the classical predicate calculus (with abbreviations) 
of a specific formula which asserts in a sense existence of the 
number 2_1000. Such kind of proof in PC is the crucial step in 
obtaining e.g. by V.P.Orevkov (1979) or R.Statman (1978, 1979), 
a lower non-elementary lower bound of cut-elimination in 
predicate calculus.

Thus, we have a formal (feasibly) consistent theory PA(F) of
feasible numbers *closed under successor* in which

	F(2_1000) & \neg F(2_{2^1000}) holds.

Here 2_1000 and 2_{2^1000}) play the role of lower and,
respectively, upper bounds for the "borderline" between
feasible and infeasible *according to* formalization of
feasibility given by Parikh.

We see that there are *two important aspects* here.

One is estimating length of proofs (related with eliminating
epsilon symbol).  *Technically* this was the main point
of Parikh's paper. (I do not mention here his other, also
pioneering results related with Bounded Arithmetic.)

But from the point of view of *foundations of mathematics* the 
most crucial point was discovering completely new possibility to 
describe *formally* a naive intuition on feasible numbers. Note 
that this intuition cannot be formalized in the ordinary 
mathematics. Such almost consistent theories cannot have models 
in the sense of the ordinary model theory because from the 
ordinary point of view such theories are contradictory. My 
opinion is that INDEPENDENTLY ON TECHNICALITIES ON LENGTH OF 
PROOFS INVOLVED (which are, no doubts, very important in itself) 
THE MERE FORMALIZATION OF FEASIBILITY IS THE MAIN FUNDAMENTAL 
AND FOUNDATIONAL VALUE OF THIS PARIKH's RESULT.


3. "Deep and surprising"?

Of course in this state of affairs it is probably prematurely to 
give any highest evaluation of such an approach to feasibility.  
But let us look what we have and what we could probably have.

Troelstra and van Dalen wrote in 1988 in their book (when
describing various "trends in constructive mathematics"):
"There are considerable obstacles to overcome for a coherent and
systematic development of ultra-finitism, and in our opinion no
satisfactory development exists at present." "The program
indicated in Esenin-Vol'pin (1961,1970,1981) so far has not
progressed beyound the initial stage. There are, however,
certain researches into the possibility of introducing *feasible
numbers*, e.g. by Parikh (1971) which tie up with considerations
concerning complexity."

In any case this citations (actually asking for a reasonable 
formalization) witness that the problem of feasibility is a very 
serious one and therefore the first essential step in its 
"resolving", even of a preliminary character, should be 
evaluated appropriately.

I would also add that the notion of almost or feasible 
consitency on which the approach of Parikh is based may somewhat 
change or influence our views on f.o.m.  and on mathematics.  
Even if this is debatable, it is worth to think more about such 
possibilty. Say, taking into account feasibly consistent 
theories, should we still consider that mathematics in general 
is reducible to ZFC or its extensions? Has mathematics a unique 
foundation? Which one, if any? 

It seems that many of us know not so much on the recent proof of
the FLT. But we evaluate very high the mere existence of such a
proof. Here we know that such unusual for mathematics notion
from our everyday naive experience as feasibility was formalized
in *some reasonable and radically new way*.  It seems that this
should be especially interesting at least to peoples working on
f.o.m.  It is the business of f.o.m. to formalize fundamental
concepts especially those completely new for mathematics.
This is just a new kind of (more "realistic") infinity.


4. Using abbreviations in mathematical proofs and some further
step in formalizing feasibility.

First note that abbreviation of terms (unlike formulas) in a
proof should be *forbidden* in the case of formalizing feasibility
because it has strong and undesirable consequences on existence
of infeasible numbers. This is the *key idea* for the following.

In the above formalization of feasibility notion by Parikh there 
was nothing mentioned about using abbreviations. Proofs in PA(F) 
were considered in the ordinary (Hilbert-style) predicate 
calculus AS IT IS. However, it seems that the theorem of Parikh 
on feasible consistency of PA(F) will be preserved if 
abbreviations (say, of formulas only) will be allowed. I did not 
check the details.  Then we can prove the "lower bound" 2_1000 
(i.e. that F(2_1000) holds) on the base of some abbreviations of 
formulas as it was mentioned by Friedman above (cf. the details, 
e.g. in my paper "On feasible numbers" accessible online). Also, 
at least F(2^1000) can be feasibly proved directly in PA(F) 
without any specially introduced abbreviations. (This 
essentially follows from Facts 3 and 4 below. Cf. corresponding 
real, feasible inferences in my paper.) Thus, provability of 
F(2^1000) allows to say that formalism PA(F) is not sufficiently 
satisfactory, because 2^1000 is intuitively infeasible.

The issue of abbreviations (of terms!) becomes unavoidable if we 
decide to replace the above lower and upper bounds for feasible 
numbers 2_1000 (or 2^1000) and, respectively, 2_{2^1000}), say, 
by 1000 and, respectively, by 2^1000. I.e., let us postulate 
that F contains 0, 1 and is closed under x+y and therefore

	0,1,2,3,...,1000,1001,...2000,... are in F,

but 2^1000 is not in F.

The latter axiom may be formulated alternatively as "double
logarithm of feasible numbers is always bounded by 10".
Strictly speaking we need not have PA and the predicate F in 
axioms.  Just postulate some universal properties of + and 
logarithm.

This is much closer to our intuition on F than in the above 
formalization. Unfortunately, doing this in the framework of the 
ordinary classical first-order logic is impossible.  The 
resulting theory will be feasibly *inconsistent*. The reason is 
that the logic *implicitly* contains some kind of abbreviating 
mechanism.

Thus, take the natural deduction rule of elimination of 
existential quantification. Having proved Ex A(x), say, by 
proving previously A(t) for some term t, we may continue:  
"let x be such that A(x) holds", etc.  This is the place 
where abbreviation x for t is actually introduced (and used!).  
Without going into further details, note that by an appropriate 
restricting the classical logic we can make abbreviations of 
terms to be forbidden, completely or partially.  E.g. this may 
be done in terms of the requirement to consider only normal 
proofs or only cut-free proofs, or in some other way. Then we 
may get (feasibly) consistent theory FEAS of feasible arithmetic 
(based essentially on the above axioms) with more realistic 
upper bound 2^1000 for feasible numbers.  This formalization is 
a kind of compromise. We should pay something very essential for 
such a formalization. (Who do not want to pay will not have the 
desired formalization!)

Let me recall in this respect the following sentence from
another posting of Friedman which was said in some different
context.

> mathematics cannot be done *by people* in a cut free
> system.

It is indeed not very convenient to write cut-free or normal
proofs. To work in FEAS we should learn how to do this
practically or, alternatively, we should appropriately weaken
the abovementioned restrictions on proofs to make the work in
FEAS somewhat more comfortable.

But what we will get by this formalization FEAS?


First, this is indeed (feasibly) consistent formalization of the 
intuitive notion of feasibility which is more adequate than that 
of Parikh (as we discussed above).

Second, we may formally deduce in this theory FEAS the following 
simple theorems or just Facts (because they are technically not 
so difficult; however, we should be rather careful!). I omit all 
the details. But they are fully presented in my paper. Let

M(x) := "2^x exists (i.e. is feasible)" and
S(x) := "2^{2^x} exists".

We may also read

S(x) as "x is a small number",
M(x) as "x is a middle (medium?) number" and
\neg M(x) as "x is big (feasible) number".

(I am not sure that this is a good terminology in English. Any
suggestions and comments are appreciated!) Evidently,

S \subseteq M \subseteq All_Numbers_of_FEAS (= Feasible_Numbers).


Fact 1. However FEAS is (feasibly) consistent, introducing to
FEAS new function symbol f with the new axiom f(x) = x + x (f is
multiplication by 2 and actually serves as an abbreviation for
the term x + x) makes this theory formally inconsistent.

(Just apply 1000 of times f to 1. Thus abbreviation of terms is 
indeed dangerous!)


Fact 2. 0,1,2 are small, but 9,10 aren't. There exists a biggest
small number s_0 somewhere between.

It is unclear what exactly is the number s_0 because the proof
of its existence is non-constructive. We can only give lower and
upper bounds for it.


Fact 3. Middle numbers are closed under successor, but,
nevertheless, 1000 is (evidently) not middle (it is a big
feasible)!

This may be considered as a possible rigorous approach to the
Heap Paradox and to the *vague concepts*. It seems quite
interesting that such not very big number as 1000 (or even 100)
may *formally* behave as infinity. And we have numerous examples
of such behaviour in the real world!

However, it might seem that Fact 3 is contradictory. Thus, using
modus ponens 1000 times seemingly would show that 1000 is also a
middle number.  But let me recall that there are some
restrictions on the underlying predicate logic and this proof
actually does not satisfy such restrictions!  We can really show
step by step that 0,1,2,3,... are middle.  But the bigger is
number the longer will be the proof that it is middle so that
even for the case of 100 it will be practically impossible to
write such a proof in the given formalism FEAS. If it is
practically impossible, then why should we conclude that it
exist? Thus there is no formal contradiction.  All of this seems
sufficiently reasonable. We just got a (proof-theoretic) 
mechanism for formalizing vague concepts.


But *especially unexpected*, at least for me personally, was the
following.  In spite of Fact 3, it is possible to prove


Fact 4. There exists a biggest middle number m_0 < 1000 (no
exact value of m_0 is known).

Formally this is again not a contradiction (with Fact 3). In
general, A and \neg A (where the negation is defined formally as
implication A => false) do not imply contradiction because modus
ponens (to get false from A and \neg A) and cut rules are not
applicable in general in FEAS.

Alternatively, we could allow applying the cut rule, or to use 
any abbreviations in proofs, but then we are *obliged* to 
eliminate them (not in our imagination, but really or, if you 
want, by "realistic" imagination!). If we succeeded then modus 
ponens, cut rule or abbreviations used prove to be harmless.

Facts 3 and 4 altogether may be interpreted as reflecting, for
example, the following quite real and well-known situation.

Consider a graphical image on computer display. Is it discrete
or continuous? The answer is that it is BOTH discrete AND
continuous and the reason for that is evidently just our mind,
not only an optical effect. We switch something in our brains
and see the picture in one or other way.

Let me repeat that demonstrating feasible consistency and formal 
proving the above facts in FEAS is technically rather simple, 
simpler than the proof of Parikh's theorem on feasible 
consistency of PA(F). I do not know whether the readers will 
find them "deep and surprising results", but for me personally 
they were very unexpected. The only expected thing (just the 
goal of the approach) was non-feasibility of 2^1000.  Without 
formalization of feasibility it is rather difficult to say 
anything rational and non-dubious on this concept.  The "rules 
of game" are almost completely unknown at the beginning.  We 
should appropriately *create* them some way, and for the case 
of very unusual feasibility concept this is rather difficult 
psychologically.

Now there is some, may be very preliminary formalization with
infeasible 2^1000 and we can investigate this concept
*completely rigorously*.  We may also try to find some other,
better formalizations.


5. Possible applications and perspectives.

We may also try to give some new foundation based on the concept
of feasibility of the notion of continuum which will be
probably somewhat more appropriate for real computer
applications.  Each real number will contain *simultaneously*
finitely (= m_0) and infinitely many digits after the point
(just middle number < 1000 or even < 100 of binary digits!).
What will be the corresponding differential and integral
calculus?  It is interesting what happens with the *feasible
version* of the notion of Euclidean space? What will happen with
corresponding approaches to physics? Is not new approach more
appropriate and natural to come to the ideas of quantum
mechanics, and macro/micro physics etc?  What will be *feasible*
computability theory? (Say, esponential and even multiplication
functions and therefore syntactic substitution operator are
partial recursive here.) Will we have a universal partial
feasibly recursive function?  What is feasibly constructive 
mathematics? Finally, feasible computability theory may be 
considered as a kind of complexity theory on the level of 
foundations of mathematics. 

There is a lot of fantasy here and a lot of work should be done 
to understand how useful (of course, if useful at all!) may be 
feasible numbers.  We cannot assert nothing very definite at 
this state of knowledge except that there is indeed some kind of 
formalization with some specific unusual properties. But we can 
hope on the best and try to do something in this direction.


Vladimir Sazonov
-- 			   | Tel. +7-08535-98945 (Inst.),
Computer Logic Lab.,	   | Tel. +7-08535-98953 (Inst.),
Program Systems Institute, | Tel. +7-08535-98365 (home),
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/