FOM: Mathematics as governing intuition by formal methods

[Vladimir Sazonov]

In the previous posting I formulated the following "definition":

   Mathematics (in a wide sense) deals with governing our intuitions
   (abstractions, idealizations, imaginations, illusions, fantasies,
   abilities to foresee and anticipate, etc.) on the base of appropriate
   formal/deductive/axiomatic methods/systems/theories/rules.

(This seems to be in some agreement with the definitions of Moshe' 
Machover and Solomon Feferman also cited there.) 
I also wrote that this definition suggests to consciously *manipulate* 
our intuitions or even illusions instead of canonizing them. Let me 
illustrate this by showing how intuition of natural numbers may be 
changed by a critique of the Induction Axiom (and some related things).

Solomon Feferman wrote:

> I. The positive integers are conceived within the structure of objects
> obtained from an initial object by unlimited iteration of its adjunction,
> e.g. 1, 11, 111, 1111, .... , under the operation of successor.

I have questions. What does it mean "unlimited" explicitly? I.e., what 
are these dots "...."? I think it may be understood in various ways. 
Also, why "unlimited"? Is this a necessary component of any intuition 
on the positive integers? Further, is Induction Axiom which is usually 
attributed to natural numbers inevitable? Is it true that we do not 
loose anything essential by choosing once and for all the traditional 
approach to the natural numbers via Peano Arithmetic?  How to formulate 
this "traditional approach" and corresponding intuition in a clear way 
which is not reduced simply to writing down, say, the axioms of PA (or 
PA + ?)?

Actually, I myself have and present below some answers to some of these 
questions. Not all of this is probably very original. But usually some 
essential points are not taken into account at all at the beginnings of 
arithmetic. So let me fix them. I am also interested in the opinions on 
these considerations of other participants of the FOM list.

First, everybody know that there are resource bounds. And these bounds 
may prevent us to choose or use non-critically the term "unlimited" 
above.  Thus, we could in principle admit existence of the biggest 
natural number which I call Box (and denote as \Box in LaTex or as []) 
to emphasize the idea of something "bounded" like a room bounded by the 
walls. We may consider corresponding version PA_[] (or 
"Box-arithmetic") of Peano Arithmetic (PA) *relativized* (together with 
Induction Axiom) to this indefinitely finite row 0,1,2,...,[]-1,[] of 
natural numbers.  Moreover, it reasonable to consider that this 
"uniformly, or globally bounded" arithmetic PA_[] involves symbols for 
*all* recursive functions relativized to []. (This is a quite 
meaningful notion whose precise definition may be known and clear to 
those acquainted with descriptive complexity theory or with 
corresponding approaches in finite model theory.) Then this 
Box-arithmetic proves to be just an *arithmetic of polynomial time 
computability*. (There exists corresponding theorem about this 
arithmetic.)

Note, that interrelation of the first-order version of this arithmetic 
with the second-order one (both in terms of definability and 
proof-theory) is essentially connected with the problem "P=NP?".  (Here 
a well-known definability result of Ronald Fagin (1974) is implicitly 
used.) 

Let me formulate some problems: Is induction axiom over second-order 
formulas provable in the (first-order) PA_[]? Is second-order version 
of PA_[] conservative over PA_[]? What are corresponding approaches to 
predicativity notions analogous to the ordinary arithmetic. What about 
constructive (second-order) versions of PA_[]? A bit *informally*, are 
all (finite!) functions over the row 0,1,2,...,[]-1,[] of natural 
numbers recursive in the above sense? What about *fixing* [] = 1000, or 
= 2^1000, or = any "nonstandard" number? 

By the way, it seems to me that this approach is sufficiently serious 
reason to consider the problem "P=NP?" as foundational one, in contrast 
to the opposed opinion of Professor Solomon Feferman in his recent 
posting on "P=NP". Note, that even with a *fixed* value of []
corresponding 
analogue of this problem remains interesting and non-trivial. Moreover, 
it looses its traditional asymptotic character. (May be some reasonable 
changing this problem will be fruitful for finding its solution?) 
Actually, we could say that it is a problem on the *nature* of finite 
objects. What are they? Are they *all* ("all"?) recursive, or 
constructive, constructible? (Of course, this reminds Kolmogorov's 
complexity.) 

This is one possibility of formalizing natural numbers, 
alternative to PA.

Another possibility:

Let us postulate that there exists no last natural number (as in the 
ordinary PA), but restrict Induction Axiom (and probably some other 
formal rules) in some way.  Why? Because it is unclear that this axiom 
is necessarily "true". Consider, e.g. its equivalent reformulation as 
the Minimum Principle

	\exists x A(x) => \exists x (A(x) & \forall y < x ~A(y)).

This principle is true for *short* initial segments of natural numbers 
like 0,1,2,...,10 and for *simple* properties A(x).  But, if we are 
dealing with numbers more *abstractly*, we have also another, 
"negative" experience. E.g., what about existence of "the least natural 
number which cannot be denoted by a written phrase containing no more 
than one thousand of symbols"?  I also doubt that Minimum Principle 
should inevitably "hold" for any *pure* arithmetical formula with 
quantifiers over "all" natural numbers. ("All" is something extremely 
indefinite!) 

Yes, it seems reasonable to extrapolate the minimum principle to "all" 
natural numbers, whatever they are, and to all arithmetical formulas 
A(x), especially because this extrapolation in the form of PA does not 
seem to lead to a contradiction. But why we *must* do that? Tradition? 
Intuition?  Some kind of Mathematical Religion? What about other 
possibilities and other intuitions (and even "religions")? Who can say 
without sufficient trials that these possibilities do not exist or are 
fruitless? It seems that such (and may be some other) alternatives 
should be at least formulated explicitly when the nature of natural 
numbers is discussed. 

Note, that intuitionists and constructivists have explicitly 
articulated doubts on meaningfulness of quantification over "all" 
natural numbers.  But they made somewhat different conclusion, just on 
the low of excluded middle, instead of Induction Axiom. 


There exists somewhat different way of approaching Induction Axiom 
(Rule).  If A(n) => A(n+1) is provable then we can prove by using the 
cut rule (or transitivity of implication) that A(0) => A(n*) for any 
fixed numeral n*. Then we *extrapolate* this metatheorem to the 
conclusion A(0) => A(n) where n is a (universally quantified) variable 
ranging over "all" natural numbers. This extrapolation is based on 
identifying abstract, semantical objects (numbers denoted by the 
variable n) with concrete, syntactical ones (numerals and therefore - 
via Goedel numbering - with arbitrary terms, formulas, proofs, etc.).  
Such identification of entities of very different nature (semantical 
and syntactical, abstract and concrete) does not seem in general 
sufficiently convincing.  It makes the (infinite!) row of natural 
numbers much "longer" than it is "intended to be".  (By the way, it 
follows that the sentence Consis_PA does not have precisely the 
intended meaning.) 

With the induction axiom (and also with the cut rule and with other 
tools which also could be criticized; cf. my previous postings to FOM 
starting from 5 NOV 1997) we can prove existence of very big numbers 
(like 2^1000) whose meaning and existence may be considered as doubtful 
or questionable. 

I conclude that in principle there are alternatives to PA and 
corresponding traditional arithmetical intuition. One alternative 
discussed above is PA_[].  Another example is Feasibly Constructive 
Arithmetic of Stephen Cook, and closely related Bounded Arithmetic a 
version of which was considered by Rohit Parikh in 1971. (My 
own interest to BA (and to Bounded Set Theory) started exactly with 
PA_[] whose second-order version is essentially equivalent to BA.) Much 
more unusual, even strange (and, I would like to hope, promising too) 
is also Feasible Arithmetic (feasible - in an essentially stronger 
sense of this word than that of Cook) discussed in my previous postings 
in November 1997.  The first mathematically rigorous approach to 
(almost consistent) Feasible Arithmetic was started also by R.Parikh in 
1971. Let me also mention corresponding ideas of Alternative Set Theory 
of Petr Vopenka. 

All of this is related with paying main attention to resources needed 
in computations on the level of mathematical foundations rather than on 
the level of the traditional complexity theory.

Besides numerous literature on Bounded Arithmetic, cf. also my papers 
related to BA, PA_[], Bounded Set Theory (BST) and Feasible Numbers

[1] "Polynomial computability and recursivity in finite domains".
    Elektronische Informationsverarbeitung und Kybernetik, Vol.16,
    N7, 1980, p.319--323. 
[2] "A logical approach to the problem P=?NP", LNCS 88, 1980.
    (See corrections in [3,4])
[3] "On existence of complete predicate calculus in
    metamathematics without exponentiation", MFCS'81, LNCS, N118,
    Springer, New York, 1981, P.483--490.
[4] Also more late paper essentially subsuming [2]:  
    "On equivalence between polynomial constructivity of Markov's 
    principle and the equality P=NP", 1988 (In Russian). Cf. English 
    translation in Siberian Advances in Math., Allerton Press Inc., 
    1991, Vol. 1, N4, 92-121.
[5] "On bounded set theory" in Logic and Scientific Methods, 1997,
    Kluwer Acad. Publ., 85-103. (Accessible also by my WWW-page)
[6] "On feasible numbers", in: Leivant D., ed., Logic and
    Computational Complexity, LNCS Vol. 960, Springer, 1995,
    pp.30--51. (Accessible also by my WWW-page)

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/