FOM: feasible numbers or? large cardinals and P vs NP

[Vladimir Sazonov]

Mitchell Spector presented some interesting 
considerations on large cardinals and added:
> 
> P.S.  I didn't change the Subject line, but I don't really
> believe that this has anything to do with the P=NP question.

Really, the initial discussion on P vs. NP quickly shifted 
to something completely foreign to this problem. Of course, 
in principle some new set-theoretic axiom could resolve the 
question considered. But I personally do not believe that 
this is a right way of thought.  
Moreover, I even do not believe that the full strength of 
Peano Arithmetic is necessary to resolve (or find a key 
construction for an independence result, if any). Bounded 
Arithmetic, probably with postulated ~EXP (partiality of 
exponential function 2^n) is more appropriate. This also 
corresponds to my belief that mathematics is not only 
finding a final(!?) TRUTH (a wrong impression from the 
success of contemporary set theory), but rather a PLAY WITH 
TRUTH (like that in non-Euclidean geometries in the 19th 
Century or like more recent Cohen's forcing) in the crucial 
moments of the history of mathematics.  Irrationality of 
square root of 2 was also a play with truth: "Let us just 
will play FORMALLY with truth and derive the conclusion". 

Note, that complexity theory arose essentially from 
the problems of REAL computability, i.e. from the problem 
that only so called feasible numbers can arise in real 
computers (as lengths of inputs, outputs and complexity 
measures). As feasible numbers 
were completely undeveloped at that time (and almost 
undeveloped even now) as a rigorous mathematical notion, 
complexity theory used the old asymptotic approach, instead, 
without any radical change of foundations of mathematics 
which was necessary if to start with the completely new 
concept for mathematics of feasible numbers. I consider 
bounded arithmetic (even in traditional logical and 
model-theoretic framework) as a right direction because 
it is a step to feasible numbers. At least TRUTH (in 
corresponding intuitive context) of ~EXP (despite, say, 
PA |- EXP) seems very suitable for complexity theory. 

Let me present some open questions related to P vs. NP 
for some versions of bounded arithmetic (first, of BA 
of finite binary strings). 

Let p1,p2,... be (symbols for) all PTIME computable 
predicates and operations over {0,1}* (binary strings) 
and T_0 consists of all (or some reasonable list of) 
true universal sentences in this language over (the 
standard model) {0,1}*. Note, that there exists PTIME 
computable polynomial-optimal enumeration 

	e:{1}* --> {0,1}* 

(from unary to binary strings; unary strings being 
identified with natural numbers). 

Let DET denote "forall x exists i (x=e(i))". 
This says that all finite binary strings are 
"constructive" in a sense. (This is an analogy 
to Kolmogorov komplexity of finite objects, but 
in the framework presented we need no asymptotic 
or any additive constants, as usually.) 

PROBLEM 1. Is it consistent [T_0 + ~EXP + DET + Bounded 
Induction Axiom] (all quantifiers of induction 
formula have the form forall x < t or exists x < t, 
x is not free in the term t, < is lexicographical 
order over binary strings)?  (If P=NP then this problem 
would have a positive answer.)

If we replace x in bounded induction axiom by the variable 
i ranging only over unary strings then this theory becomes 
consistent. It follows that it is unprovable in T_0 
that NP-complete problems like SAT have super-polynomial 
(say, exponential) lower bound for the time of 
semi-decidability. What about T_0 + Bounded Induction? 

(Cf. my paper in MFCS'80, LNCS N88, where this result was 
demonstrated for the case of unary form of bounded induction 
and even, mistakenly, for the full form of bounded induction. 
The mistake was noticed by me in the next publication in MFCS81.)


PROBLEM 2. What about completeness of logic 
(propositional or first order) when we are "living" 
in a world with ~EXP? (Cf. my paper in MFCS81.)

If P=CoNP then both propositional and first order logic 
may be shown to have complete axiomatization in the above 
framework. 


Specialists in Bounded Arithmetic could add much more 
problems on BA related to P vs.NP. 


Now about feasible numbers instead of asymptotic approach. 

Consider so called \Box-arithmetic which is like Peano 
Arithmetic in the language for primitive recursive 
functions and functionals (not of arbitrary higher types)); 
i.e. second order function 
variables are allowed. \Box denotes the biggest natural 
number. This requires a trivial change in the axioms for 
successor. (First-order) Induction Axiom is as usual. 
Let us also extend the language for primitive recursive 
function(al)s to some new general recursive function(al)s 
so that they would denote all global PTIME computable 
operations over {0,1,...,\Box} with (finite) functional 
arguments. (Recursion over finite domain with second-order 
parameters = PTIME computability.) Note that till now 
there was imposed no axiom on the value of \Box. "Global" 
means that \Box is considered as an implicit argument. 

Now, let as additionally fix \Box to be = 1000 or 2^1000 
(or even 1; this seems  does not matter because we have 
many-place functions and 1000 of variables over {0,1} 
can imitate 2^1000) and consider also second-order 
version of \Box arithmetic (whose language corresponds to 
NP and to the whole polynomial-time hierarchy). Let us 
also agree that 

    -----------------------------------------------------
    ! all proofs and syntactical expressions (in         !
    ! mathematics and in this arithmetic) are only      !
    ! of feasible length. (Did anybody seen non-feasible! 
    ! mathematical proofs??)                            !
    -----------------------------------------------------

PROBLEM 3. Is second-order \Box-arithmetic (in general 
and in the case of fixed \Box) stronger (or more expressive 
as a language) than the first-order one? (Only feasible 
syntactic expressions and proofs are allowed in this 
formulations!) Cf. also some considerations on this 
in my paper on Bounded Set Theory for the Congress on 
Logic, Methodology and Philosophy of Sci., Florence, 
1995, published in 1997). This is evidently related to 
the problem P vs. NP (at least informally). 

Note again, that the case of fixed \Box requires involving 
feasible numbers via syntax. (Otherwise the problem is 
uninteresting). This is very unusual concept and I would 
like to believe that it is this concept which might 
(in a future) generate a crucial idea for approaching the 
problem P vs. NP and probably other problems of complexity 
theory. But first we should develop feasible numbers theory 
and corresponding intuition and "TRUTH" as far as possible. 
This is not so easy enterprise (at least psychologically). 
The first essential MATHEMATICAL step have already been 
done by Parikh in 1971. I also have a published paper 
(cf. my Web page) which demonstrates some rather unexpected 
properties of feasible numbers (I omit formulating them) 
which do not hold for Parikh's formalization. 


Finally, as to the traditional to FOM question: 
"Does mathematics need new axioms?" Why to concentrate 
only on extensions of ZFC? For example, look for 
axiomatisation of feasible numbers, it is also interesting 
and very intriguing (and, hopefully, promising) subject. 
For example, it could give completely new perspective 
to Nonstandard Analysis. In the framework of feasible 
numbers Analysis can be only "Nonstandard", unlike the 
ordinary mathematics where epsilon-delta approach 
suffice. Everything is "nonstandard" in feasible numbers. 


-- 
Vladimir Sazonov                        V.Sazonov at csc.liv.ac.uk 
Department of Computer Science          tel: (+44) 0151 794-6792
University of Liverpool                 fax: (+44) 0151 794 3715
Liverpool L69 7ZF, U.K.       http://www.csc.liv.ac.uk/~sazonov