×

Forcing with random variables and proof complexity. (English) Zbl 1219.03071

London Mathematical Society Lecture Note Series 382. Cambridge: Cambridge University Press (ISBN 978-0-521-15433-8/pbk). xvi, 247 p. (2011).
The book introduces a new method for building Boolean-valued models of bounded arithmetic which subsumes some of the most important independence results and witnessing theorems in bounded arithmetic and lower bounds in propositional proof complexity in a unified framework (e.g., the exponential lower bound for PHP in bounded-depth Frege systems), with a potential to push the boundaries to obtain new results (the author includes material on constructions of models that would lead to lower bounds on bounded-depth Frege with parity gates, which do not work as such, but show some promise).
Theories of bounded arithmetic, first studied by R. Parikh [J. Symb. Log. 36, 494–508 (1971; Zbl 0243.02037)], are weak fragments of Peano arithmetic which only have induction for bounded formulas. The author mostly works with second-order (two-sorted) theories in a minor modification of the setup introduced by D. Zambella [J. Symb. Log. 61, 942–966 (1996; Zbl 0864.03039)] as a simplification of similar theories presented by S. R. Buss [Bounded arithmetic. Studies in Proof Theory. Lecture Notes, 3. Napoli: Bibliopolis (1986; Zbl 0649.03042)]. An important property of bounded arithmetic is that there is a correspondence between arithmetical theories \(T\) and propositional proof systems \(P\) (in the sense of S. A. Cook and R. A. Reckhow [J. Symb. Log. 44, 36–50 (1979; Zbl 0408.03044)]): the main idea is that, on the one hand, \(T\) proves the reflection principle for \(P\) and, on the other hand, \(P\) admits polynomial-size proofs of propositional translations of theorems of \(T\) of a certain form. One can view an arithmetical theory as a uniform version of the corresponding proof system.
A consequence of the correspondence is that a superpolynomial (or even exponential) lower bound on the length of propositional proofs of a combinatorial principle follows from the existence of a model of the corresponding arithmetical theory of a certain form which refutes a first-order version of the principle. This was already used in M. Ajtai’s lower bound on bounded-depth Frege proofs of PHP [Combinatorica 14, No. 4, 417–433 (1994; Zbl 0811.03042)] (which also employs a forcing argument). The framework presented in the book under review, as well as several particular instances considered in the book, are geared towards construction of models exploiting this correspondence.
The basic idea behind the author’s method works as follows. We fix an \(\aleph_1\)-saturated model \(\mathcal M\) of true arithmetic, and in \(\mathcal M\) we consider a discrete probabilistic measure on a set \(\Omega\in\mathcal M\) (which is \(\mathcal M\)-finite, but externally infinite). By modding out the ideal of infinitesimally small sets from the algebra of subsets of \(\Omega\) coded in \(\mathcal M\), we obtain a complete Boolean algebra \(\mathcal B\) carrying a strictly positive \(\sigma\)-additive probabilistic measure. (This combines the construction of Loeb’s measure in nonstandard analysis and the idea of forcing with a measure algebra as in Solovay’s random real forcing.) Then we define a Boolean \(\mathcal B\)-valued model \(K(F)\) whose domain \(F\) consists of some functions \(\alpha:\Omega\to\mathcal M\) coded in \(\mathcal M\); typically, we take functions of low complexity in some restricted model of computation. By varying \(F\), we can change the theory of the resulting model.
Since the topic of the book is a fairly advanced construction of models of bounded arithmetic with applications to propositional lower bounds, it will only be appreciated by readers familiar with these areas of proof complexity (though a crash course in propositional proof complexity is included in Part V). Moreover, many of the results rely on techniques from circuit complexity, such as Håstad’s switching lemma. Some degree of acquaintance with nonstandard analysis will help the reader, but the author included an appendix presenting the construction of \(\aleph_1\)-saturated models and their basic properties which should be enough to make the book self-contained in this respect. Leaving aside the prerequisites, the book is written in a clear and coherent way with detailed proofs, and the reader is guided smoothly from basic properties of the construction through elementary examples to more advanced applications, thus the book can be used as a textbook to learn the new method.
The book is organized as follows. Part I introduces the construction of models, and explains its basic properties, in particular those related to computation of truth values of complex formulas in the model. Part II generalizes the construction to second-order structures. Part III presents a toy example of a model (the shallow decision tree model) to illustrate the basic techniques, and a model of \(V^0_1\) (the tree model) based on the switching lemma, which is used to derive witnessing theorems and an independence result for \(V^0_1\) and a model-theoretic formulation of the AC\(^0\) lower bound for parity. Part IV introduces the algebraic decision tree model, which is shown to be a model of \(Q_2V^0_1\) (\(V^0_1\) with mod-\(2\) counting quantifiers, equivalent to \(V^0(2)\) of [S. Cook and P. Nguyen, Logical foundations of proof complexity. Perspectives in Logic. Cambridge: Cambridge University Press; Urbana, IL: Association for Symbolic Logic (ASL) (2010; Zbl 1206.03051)]) using the Razborov-Smolensky approximation method. This model is used to prove a witnessing theorem and an independence result for \(Q_2V^0_1\).
Part V provides some background in propositional proof complexity, and explains the derivation of lower bounds from the existence of suitable models of arithmetic. Part VI builds a model of \(V^0_1\) where PHP fails, which is used to prove an exponential lower bound on \(F_d\)-proofs of PHP. It also includes a section tackling the issue of generalizing the construction to a model of \(Q_2V^0_1\), which would imply a lower bound for \(F_d(\oplus)\). Part VII is devoted to single-sorted arithmetical theories (PV and Buss’s theories \(S^i_2\) and \(T^i_2\)). The author’s method is used to give new proofs of witnessing and conditional independence results for these theories. This part also includes two sections on unrelated phenomena (pseudorandom sets, and random oracle results). Part VIII diverts from the main topic of the book. It deals with the complexity of strong proof systems such as Extended Frege. The author presents the machinery of \(\tau\)-formulas and proof complexity generators and some conjectures about their properties. A model (the local witness model) is constructed which shows a statement related to these conjectures. Finally, the book contains an appendix on \(\aleph_1\)-saturated models.

MSC:

03F20 Complexity of proofs
03-02 Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations
03C62 Models of arithmetic and set theory
03F30 First-order arithmetic and fragments
68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
PDFBibTeX XMLCite