Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Meta-Mathematics of Computational Complexity Theory

Igor C. Oliveira

Abstract

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.

Meta-Mathematics of Computational Complexity Theory

Abstract

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.

Paper Structure

This paper contains 31 sections, 14 theorems, 34 equations, 2 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Complexity Theory
  4. Theories of Bounded Arithmetic
  5. $\mathsf{PV}_1$
  6. $\mathsf{S}^1_2$, $\mathsf{T}^1_2$, and Beyond
  7. Theory $\mathsf{T}^1_2$.
  8. Theory $\mathsf{S}^1_2$.
  9. $\mathsf{APC}_1$
  10. Auxiliary Definitions and Results
  11. Witnessing Theorems
  12. Bounded Arithmetic and Propositional Proofs
  13. Cook's Translation Coo75.
  14. Cuts of Models of Bounded Arithmetic
  15. The Strength of Bounded Arithmetic
  16. ...and 16 more sections

Key Result

Theorem 3.1

Let $T$ be a universal theory over a vocabulary $\mathcal{L}$. Let $\varphi(x,y)$ be a quantifier-free $\mathcal{L}$-formula, and suppose that $T \vdash \forall x\,\exists y\,\varphi(x,y)\,.$ There is a constant $k \geq 1$ and $\mathcal{L}$-terms $t_1(x), \ldots, t_k(x)$ such that

Theorems & Definitions (24)

  • Theorem 3.1: Herbrand's Theorem (see, e.g., DBLP:conf/lcc/Buss94mckinley2010sequent)
  • Theorem 3.2: KPT Theorem KrajicekPT91
  • Definition 3.3: Cut in a Model of Arithmetic
  • Claim 3.4
  • Lemma 3.5
  • Lemma 3.6
  • proof
  • Definition 3.7: Cofinal extension
  • Theorem 4.1: CKKOT24
  • proof
  • ...and 14 more