Bounded Arithmetic, Propositional Logic, and Complexity Theory


Jan Krajicek


Cambridge University Press, 1995.

(Encyclopedia of Mathematics and Its Applications, Vol. 60)



Preface

The central problem of complexity theory is the relation of deterministic and non-deterministic computations: whether $P$ equals $NP$, and generally whether the polynomial time hierarchy $PH$ collapses. The famous {\em $P$ versus $NP$ problem} is often regarded as one of the most important and beautiful open problems in contemporary mathematics, even by non-specialists (see, for example, Smale (1992)).

The central problem of bounded arithmetic is whether it is a finitely axiomatizable theory which amounts to deciding whether there is a model of the theory in which the polynomial time hierarchy does not collapse.

The central problem of propositional logic is whether there is a proof system in which every tautology has a proof of size polynomial in the size of the tautology. In this generality the question is equivalent to asking whether the class \cal NP \rm is closed under complementation. Particular cases of the problem, to establish lower bounds for usual calculi, are analogous to constructing models of associated systems of bounded arithmetic in which $NP \neq coNP$.

Notions, problems and results about complexity (of predicates, functions, proofs, $\dots$) are deep-rooted in mathematical logic and (good) theorems about them belong to the most profound results in the field. Bounded arithmetic and propositional logic are closely interrelated and have several explicit and implicit connections to the computational complexity theory around the {\em $P$ versus $NP$} problem. Central computational notions (Turing machine, boolean circuit) are crucial in metamathematics of the logical systems and models of these systems are natural structures for concepts of computational complexity.

Moreover, the only approach in sight universal enough to have a chance to produce lower bounds to the size of general boolean circuits needed for the first problem is the method of approximations, which is a version of the ultraproduct construction (and of forcing), while forcing bears a relation to the second and the third problems, and a general framework for the last problem is in terms of boolean valuations (sections 3.1, 9.4, 12.7 and 13.3).

Much of the contemporary research in computational complexity theory concentrates on proving weaker versions of $P \neq NP$, for example on proving lower bounds to the size of restricted models of circuits, and some deep results (although telling little about the $P$ versus $NP$ problem) have been obtained.

It is however, possible to approach the same problem differently and to try to prove statement $P \neq NP$ first for other structures than natural numbers {\bf N}, in particular for non-standard models of systems of bounded arithmetic.

Such approach is, in fact, common in mathematics where for example a number-theoretic conjecture about the field of rational numbers is first tested for function fields which share many properties with the rationals. Similarly, we can try to prove that $P \neq NP$ holds in a model of a system of bounded arithmetic. Non-standard models of systems of bounded arithmetic are not some ridiculously pathological structures and a part of the difficulty in constructing them stems exactly from the fact that it is hard to distinguish these structures, by the studied properties, from natural numbers.

Methods (all essentially combinatorial) used for known circuit lower bounds are demonstrably inadequate for the general problem. It is to be expected that a non-trivial combinatorial or algebraic argument will be required for the solution of the $P$ versus $NP$ problem. However, I believe that the close relations of this problem to bounded arithmetic and propositional logic indicates that such solution should also require a non-trivial insight into logic. For example, recent strong lower bounds for constant-depth proof systems needed a reinterpretation of logical validity (section 12.4).

The relations between bounded arithmetic, propositional logic and complexity theory are not \it ad hoc \rm but are reflected in numerous more specific relations, ranging from intertranslability of arithmetic and propositional proofs and computations of machines, to characterizations of provably total functions in various subsystems of bounded arithmetic in terms of familiar computational models, correspondence in definability of predicates by restricted means and their decidability in a particular computational model, to proof methods based on analogous combinatorial backgrounds in all three areas, and finally to formalizability of basic concepts and methods of complexity theory within bounded arithmetic. It is the main aim of this monograph to explain these relations.

The last several years have seen important developments in areas of complexity theory, as well as in bounded arithmetic and complexity of propositional logic, and other deep relations between these areas were established. While there are several monographs on computational complexity theory and very good survey articles covering the main fields of research, many recent results in bounded arithmetic and propositional logic are scattered in research articles and some important facts, like relations between various theorems and methods, are even just a part of unpublished folklore or appeared in a longer but now less significant, and hence less read, work.

To my knowledge there are three published monographs treating, at least partially, bounded arithmetic and its relation to complexity theory: Wilkie (1985), Buss (1986) and the last part of H\'{a}jek and Pudl\'{a}k (1993) (Chapter 5, pp.267-408). While these are very interesting books, the first two contain none of developments of last several years (obviously) and none of the three treats propositional logic.

This book is not intended to be a text-book of either logic or complexity theory. It merely wants to present main parts of contemporary research in bounded arithmetic and complexity of propositional logic in a coherent way and to illustrate topics pointed out at the beginning of this {\em Preface}. It is aimed at research mathematicians, computer scientists and graduate students. No previous knowledge of the topics is required but it is expected that the reader is willing to learn what is needed along the way. My hope is that the book will stimulate more people to contribute to this fascinating area.

Contents