Source-linked AI summary
Meta-Mathematics of Computational Complexity Theory
Igor C. Oliveira
TL;DR
The paper surveys how bounded arithmetic formalizes complexity-theoretic results and frames provability questions about major open problems. It synthesizes recent techniques and results linking proofs to algorithms, circuit lower bounds, and propositional proof systems, while remaining non-exhaustive.
Problem
Major complexity questions remain open, motivating a logical framework that can formalize known results and determine whether central statements are provable or unprovable.
Method
The survey synthesizes bounded-arithmetic theories, witnessing techniques, formalization results, and connections to propositional proof systems.
Results
PV1-provable circuit lower bounds yield polynomial-time refuters, while stronger or weaker formalizations have correspondingly different witnessing and unprovability implications.
Takeaways & Limitations
Provability analysis in bounded arithmetic provides progress toward understanding the power and limits of feasible computations and proofs, even without resolving the major open problems.
Takeaways & Limitations
The survey is not exhaustive and omits some references and recent developments because of space constraints.
Abstract
from arXiv · showhide
We survey results on the formalization and independence of mathematical statements related to major open problems in computational complexity theory. Our primary focus is on recent findings concerning the (un)provability of complexity bounds within theories of bounded arithmetic. This includes the techniques employed and related open problems, such as the (non)existence of a feasible proof that P = NP.
1 Introduction
The survey studies whether bounded-arithmetic theories can formalize major complexity results and determine the provability or unprovability of central open problems. It emphasizes recent progress while noting that the survey is necessarily selective.
- Major unresolved questions include P versus NP, the power of non-uniform Boolean circuits, and proof-length bounds for Frege and extended Frege.
- The broader goal is to identify a logical theory capturing known algorithms and complexity results, then classify major statements as provable or unprovable within it.
- Bounded arithmetic theories are fragments of Peano Arithmetic designed to formalize reasoning about specified complexity classes, including induction whose hypotheses can be NP predicates.
- These theories already formalize results such as the PCP Theorem, circuit lower bounds, expander constructions, and randomized polynomial-time matching algorithms.
- Determining complexity-bound provability in bounded arithmetic advances understanding of feasible computations and proofs even without resolving the field’s largest open problems.
- The survey focuses on recent developments and omits some references and developments because of space limitations.
2 Preliminaries
This section introduces the computational and logical foundations used to relate bounded arithmetic to complexity classes. It defines the relevant theories through bounded formulas and induction principles, emphasizing their connections to polynomial-time computation and proof complexity.
- 2.1 Complexity Theory: SIZE[s] denotes languages computed by Boolean circuits of size s(n), while FP denotes polynomial-time functions over binary-encoded integers.
- 2.1 Complexity Theory: Cobham’s characterization identifies FP as the least class containing basic functions and closed under composition and limited recursion on notation.
- 2.2 Theories of Bounded Arithmetic: PV1 formalizes polynomial-time functions and admits induction over quantifier-free, hence polynomial-time, predicates.
- 2.2 Theories of Bounded Arithmetic: Sharply bounded formulas define polynomial-time predicates, whereas bounded quantifiers express predicates in NP, coNP, and higher complexity classes.
- 2.2 Theories of Bounded Arithmetic: Alternations of bounded quantifiers define the Σb_i hierarchy, which corresponds over N to levels Σp_i of the polynomial hierarchy.
- 2.2 Theories of Bounded Arithmetic: Buss’s theories share BASIC axioms and differ in their induction schemes, with induction formulas tied to corresponding complexity classes.
- 2.2 Theories of Bounded Arithmetic: Polynomial induction reaches the base case in polynomially many steps for binary inputs and supports translations to polynomial-size propositional proofs.
3 Auxiliary Definitions and Results
The section develops witnessing, propositional-translation, and model-theoretic tools for extracting computational content from bounded-arithmetic proofs. These tools connect provability with algorithms, proof systems, and structured submodels.
- 3.1 Witnessing Theorems: Herbrand’s Theorem extracts finitely many terms from a universal-theory proof of ∀x ∃y φ(x,y), yielding a witness for each input.
- 3.1 Witnessing Theorems: The KPT Theorem handles ∀w ∃u ∀v statements by producing terms whose successive outputs can be interpreted as a finite Student-Teacher interaction.
- 3.1 Witnessing Theorems: Higher quantifier alternations lack a straightforward KPT analogue and require more general witnessing formulations.
- 3.1 Witnessing Theorems: For ∀Σb_1 sentences, Buss’s Theorem transfers provability from S1_2(LPV) to PV1, enabling polynomial-time algorithm extraction and convenient proofs in the richer theory.
- 3.2 Bounded Arithmetic and Propositional Proofs: Cook’s translation maps a universal PV1 theorem to polynomial-size propositional tautologies with polynomial-size extended-Frege proofs, encoding the theorem over n-bit inputs.
- 3.3 Model-Theoretic Techniques: A cut closed under the relevant arithmetic operations satisfies bounded-formula elementarity and can itself model S1_2, supporting model-theoretic constructions.
- 3.3 Model-Theoretic Techniques: A nonstandard countable model of S1_2 has a countable cut containing a nonstandard length n such that every element has length at most n^k for some standard k.
- 3.3 Model-Theoretic Techniques: A cofinal extension is one in which every element of the larger model is bounded by an element of the smaller model.
4 The Strength of Bounded Arithmetic
Bounded arithmetic formalizes established results in algorithms and complexity theory while enabling the study of which complexity bounds are provable or unprovable. The survey illustrates these ideas through PCP formalization and constructive parity formula lower bounds in PV1.
- Research directions: Research progresses on both formalizing established complexity results and proving complexity bounds unprovable in bounded arithmetic, often conditionally.These are complementary directions for understanding feasible computations and proofs.
- Formalization challenges: Formalization may require either adapting existing frameworks or developing new proofs whose concepts and properties fit the theory's inductive axioms.Razborov's formalization of the Switching Lemma is an example of the latter approach.
- Formalization examples: PV1 formalizes the PCP Theorem, yielding an NP-hardness result for approximating the value of suitable k-SAT instances.The formalization uses a function symbol whose behavior as a gap-inducing reduction is proved in PV1.
- Circuit lower-bound formulations: Log and LogLog formalizations differ in parameter scaling: Log uses n as the length of N, whereas LogLog uses n as the length of the length of N.Log formalization is stronger; its witnessing refuters run in polynomial time in n, while LogLog refuters may run in poly(2^n).
- Circuit lower bounds: PV1 can prove the parity formula lower bound Size(F) ≥ n^3/2 by recursively constructing an n-bit witness that a small formula does not compute parity.The argument repeatedly restricts formulas, obtaining Size(F_l) ≤ Size(F) · (k/n)^3/2 before setting l = n − 1.
- Circuit lower bounds: More advanced circuit lower bounds are known with additional axioms extending PV1, while their provability in PV1 remains less clear.The survey identifies proving depth-d circuit lower bounds of size n^ell in PV1 as an open problem.
5 Unprovability of Complexity Bounds
The survey develops unprovability results for complexity bounds in bounded arithmetic, linking logical provability to circuit lower bounds, learning protocols, and propositional proof complexity. These results rule out selected feasible proofs and connect lower-bound unprovability with the consistency of P ≠ NP.
- Upper bounds: Unprovability of NP ⊆ SIZE[n^k] corresponds to consistency of NP ⊈ SIZE[n^k] and constitutes progress toward unconditional lower bounds.The consistency result holds in a nonstandard model where complexity theory resembles the standard model.
- Upper bounds: For every integer k ≥ 1, PV1 does not prove P ⊆ SIZE[n^k], an unconditional result for a theory formalizing advanced complexity results.The result contrasts with earlier conditional negative results for NP ⊆ SIZE[poly].
- LEARN-uniform circuits: Learning-theoretic witnessing reduces upper-bound unprovability to unconditional lower bounds against LEARN-uniform circuits, where a P language lies outside LEARN-uniformEQ[O(1)] SIZE[O(n^k)].The framework uses a bounded-round student-teacher protocol in which counterexamples refine successive candidate solutions.
- Propositional proof complexity: A super-polynomial eF proof lower bound implies that PV1 cannot prove a corresponding P = NP statement, while model constructions establish unprovability of the sentence ΨeF.The argument uses models of PV1 in which every tautology has an eF-proof, contradicting a claimed super-polynomial lower bound.
- P = NP: If PV1 fails to prove nk-size lower bounds for a language in P, then P ≠ NP is consistent with PV1, under a hypothesis weaker than unprovability of NP ⊈ SIZE[n^k].This connects circuit lower-bound unprovability with the formal weakening of the P versus NP conjecture.
6 Additional Recent Developments
Recent work extends bounded-arithmetic meta-mathematics through new unprovability results, reverse-mathematics equivalences, and proof-complexity analyses, while leaving several developments outside this survey.
- Bounded-arithmetic unprovability: dWPHP unprovability in PV1 has been established under circuit-size, or under cryptographic and complexity, assumptions.These results connect dWPHP with exponential circuit lower bounds and use different assumptions.
- Bounded-arithmetic unprovability: NEXP ⊆SIZE[poly] is unprovable in bounded arithmetic V0 via a method that avoids witnessing theorems.The approach simulates a comprehension axiom scheme and uses a lower bound on pigeonhole-principle provability.
- Reverse mathematics: Reverse-mathematics work shows that lower bounds in communication complexity, error-correcting codes, and Turing machines are equivalent to variants of polynomial-time weak pigeonhole principles.These equivalences support viewing complexity lower bounds as axioms with broader combinatorial implications.
- Circuit-size hierarchy: The circuit-size hierarchy is provable in T2^2, while stronger provability in T1^2 would imply P^NP ⊈SIZE[n^(1+ε)] for some ε > 0.Thus proof-complexity upper bounds for the hierarchy can yield circuit lower bounds.
- Bounded-arithmetic unprovability: NP ≠ PSPACE is unprovable in APC1 under a strong average-case hardness assumption using a LogLog formalization.This adds an unprovability result for a major complexity-class separation.
- Related developments: Recent related work also studies proof-complexity generators and weak proof-system non-automatability, while space constraints prevent comprehensive coverage of all developments.The survey explicitly identifies omitted directions and papers.