zbMATH — the first resource for mathematics

Bounded arithmetic. (English) Zbl 0649.03042
Studies in Proof Theory. Lecture Notes, 3. Napoli: Bibliopolis. VII, 221 p. (1986).
This is a reprint, with minor corrections, of the author’s Ph. D. dissertation submitted to the Department of Mathematics at Princeton University in May 1985. The thesis advisor was Simon Kochen.
The main objective of the thesis is to relate the so-called polynomial hierarchy studied in Computer Science to appropriate subsystems of Peano Arithmetic. This is achieved in a quite convincing way. To show that a function definable in such a subsystem of Peano Arithmetic actually belongs to the proper level of the polynomial hierarchy the author uses techniques from proof theory (essentially cut elimination), in the spirit of earlier work by Kreisel. (In a postscript the author notes that Alex Wilkie has reproved this result by a model theoretic method). However, the long-standing open problems concerning the polynomial hierarchy (like $$P=?NP,\quad NP=?coNP)$$ remain open, in spite of the fact that the author obtains some nice equivalent formulations of these problems in proof theoretic terms.
In Chapter 1 the polynomial hierarchy is introduced, first by schemata, the main one being what the author calls limited iteration (a version of Grzegorczyk’s bounded recursion), then by the usual definition in terms of Turing machines, and finally in a more logical form using bounded formulas of arithmetic. All three definitions are proved to be equivalent. (As the author states, these results are originally due to Cobham, Stockmeyer and Wrathall).
Chapter 2, entitled Foundations of bounded arithmetic, introduces the subsystems of Peano Arithmetic referred to above which are to be related to the polynomial hierarchy. Among the basic functions the author has x#y:$$=2^{| x| \cdot | y|}$$, where $$| x|$$ denotes the length of the binary representation of x. The main reason for the introduction of this function is that the author intends to build an analogue $$\Sigma^ b_ i$$ of the usual arithmetic hierarchy: unbounded quantifiers of the arithmetic hierarchy are to be replaced by bounded ones, i.e. $$\forall x\leq t$$, and bounded quantifiers of the arithmetical hierarchy (which can be disregarded there) are to be replaced by “sharply bounded” ones, i.e. $$\forall x\leq | t|$$ (which can also be disregarded in his hierarchy). Now to achieve this, it must be possible to replace a quantifier combination ($$\forall x\leq | s|)(\exists y\leq t)$$ by ($$\exists w\leq r)(\forall x\leq | s|)$$ with a suitable r built from s and t; this r requires an order of magnitude provided by the #-function.
Denote by bounded arithmetic the subsystem of Peano Arithmetic obtained by restricting the induction axioms to bounded formulae. The author introduces the following subsystems of bounded arithmetic: $$S^ i_ 2$$ consists of some simple open axioms concerning the basic functions and the induction axioms. $\Sigma^ b_ i-PIND\quad A(0)\quad \wedge \quad (\forall x)(A(\lfloor x\rfloor)\quad \to \quad A(x))\quad \supset \quad (\forall x)A(x)$ with $$A\in \Sigma^ b_ i$$, $$T^ i_ 2$$ contains the usual $$\Sigma^ b_ i$$ induction axioms instead. It is proved that $$S^{i+1}\vdash T^ i_ 2\vdash S^ i_ 2$$ for $$i\geq 0.$$
The author then heads for the proof of his main result, that the functions at the i-th level $$\square^ p_ i$$ of the polynomial hierarchy are exactly the $$\Sigma^ b_ i$$-definable functions in $$S^ i_ 2$$. The easy direction (definability of the $$\square^ p_ i$$- functions) is proved in Chapter 3. For the other direction the author wants to apply proof theoretic methods; hence he takes care of the necessary machinery in Chapter 4, entitled “First-order natural deduction systems”. Mainly following Takeuti’s well-known book he proves Gentzen’s cut elimination theorem in a form adapted to bounded arithmetic.
Chapter 5 then gives the proof of his main result, essentially by applying cut-elimination to a given derivation of an existential formula in $$S^ 0_ 2$$, then reading off a witness for the existential quantifier and finally estimating the computational complexity of this process.
Chapter 6 proves the equivalence of $$S^ 1_ 2$$ to Cook’s equational theory PV [see S. A. Cook, Proc. 7th Ann. ACM Symp. on Theory of Computing, 83-97 (1975; Zbl 0357.68061)]; a slight sharpening of the proof in Chapter 5 is needed to achieve this.
In Chapter 7 it is shown in detail that the first and second Gödel incompleteness theorems hold in $$S^ 1_ 2$$. At the end (in 7.6) the author reports some unsuccessful attempts to use the techniques developed for the completeness theorems to prove $$S_ 2^{i+1}\nvdash S^ i_ 2$$; this remains to be an open question.
In Chapter 8 the author gives a very pretty proof-theoretic statement equivalent to $$NP=coNP$$; he again discusses some unsuccessful attempts to use this for a proof of NP$$\neq coNP.$$
Finally in Chapters 9 and 10 second order systems $$V^ 1_ 2$$ and $$U^ 1_ 2$$ of bounded arithmetic are introduced. It must be stressed (as the author does) that the notion of second order system used here is different from the usual one: all functions are required to have a polynomial growth rate. In particular, his second order systems are not stronger than Peano Arithmetic. The author is able to prove, again by a proof theoretic method similar to the one in Chapter 1, that a function f is $$\Sigma_ 1^{1,b}$$-definable in $$U^ 1_ 2$$ (resp. in $$V^ 1_ 2)$$ iff $$f\in PSPACE$$ (resp. $$f\in EXPTIME).$$
To conclude, this is a carefully written dissertation, which will be a basic reference for the subject for some time to come. It is good to have it published in this more accessible form.
Reviewer: H.Schwichtenberg

MSC:
 03F30 First-order arithmetic and fragments 03F35 Second- and higher-order arithmetic and fragments 03D15 Complexity of computation (including implicit computational complexity) 03-02 Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations 68Q25 Analysis of algorithms and problem complexity 03D20 Recursive functions and relations, subrecursive hierarchies 03F05 Cut-elimination and normal-form theorems