In logic and theoretical computer science, and specifically proof theory and computational complexity theory, proof complexity is the field aiming to understand and analyse the computational resources that are required to prove or refute statements. Research in proof complexity is predominantly concerned with proving proof-length lower and upper bounds in various propositional proof systems. For example, among the major challenges of proof complexity is showing that the Frege system, the usual propositional calculus, does not admit polynomial-size proofs of all tautologies. Here the size of the proof is simply the number of symbols in it, and a proof is said to be of polynomial size if it is polynomial in the size of the tautology it proves.
Systematic study of proof complexity began with the work of Stephen Cook and Robert Reckhow (1979), who provided the basic definition of a propositional proof system from the perspective of computational complexity. Specifically, Cook and Reckhow observed that proving proof size lower bounds on stronger and stronger propositional proof systems can be viewed as a step towards separating NP from co-NP (and thus P from NP), since the existence of a propositional proof system that admits polynomial size proofs for all tautologies is equivalent to NP = co-NP.
Contemporary proof complexity research draws ideas and methods from many areas in computational complexity, algorithms and mathematics. Since many important algorithms and algorithmic techniques can be cast as proof search algorithms for certain proof systems, proving lower bounds on proof sizes in these systems implies run-time lower bounds on the corresponding algorithms. This connects proof complexity to more applied areas such as SAT solving.
Mathematical logic can also serve as a framework to study propositional proof sizes. First-order theories and, in particular, weak fragments of Peano arithmetic, which come under the name of bounded arithmetic, serve as uniform versions of propositional proof systems and provide further background for interpreting short propositional proofs in terms of various levels of feasible reasoning.
Main concepts
Conventions By default, proof theory discussed proof systems for classical propositional logic, using the language of propositional logic with the connectives , and countably many propositional variables . Here, is the set of finite binary strings.
A proof system is denoted with capital letters: . A proof is denoted with lowercase letters .
A formula is denoted with lower Greek letters: . The length of a formula is . Similarly, the length of a proof is .
TAUT is a formal language consisting of the tautological formulas of propositional logic.
Big-O and big-Omega notation are used in the same way as in computational complexity theory.
Proof systems
A proof system is an algorithm that takes two inputs: a formula , and a purported proof . The proof system must satisfy:
runs in time . if and only if there exists some , such that accepts.
Examples of propositional proof systems include sequent calculus, resolution, cutting planes and Frege systems. Strong mathematical theories such as ZFC induce propositional proof systems as well: a proof of a tautology in a propositional interpretation of ZFC is a ZFC-proof of a formalized statement ' is a tautology'.
A proof system can be thought of as a nondeterministic polynomial-time algorithm for proving non-satisfiability. That is, given a formula , is unsatisfiable if and only if there exists some , such that accepts. This shows its close relationship with the co-NP class.
Complexity Ordinary proof theory does not care about what formulas a certain proof system can and cannot prove. Proof complexity is not satisfied with what can be done, but how efficiently it can be done, i.e. the computational complexity of the proof system. In order to measure efficiency, what efficiency is for a proof system must be defined.
In ordinary complexity theory, efficiency can be measured by how many steps are required (time complexity), how much working space is required (space complexity), size of a Boolean circuit needed to implement a boolean function (circuit complexity), etc. In proof complexity theory, there are also more than one way to measure of efficiency.
The size complexity of a proof system denotes the minimal size of proofs possible in the system for a given tautology. In detail, a proof system has (upper bound) size complexity iff given any tautology of length , there is a proof of in this proof system that uses steps. It has (lower bound) size complexity iff given any length , there exists a tautology of length , such that any proof of in the proof system needs steps.
The space complexity of a proof system denotes the memory usage during a proof. A common way to measure "memory usage" is clause complexity: the maximum number of clauses that can appear simultaneously during a resolution proof. Other ways to measure space complexity include:
The number of symbols of a proof. The number of lines of a proof. The maximal complexity of formulas that appears in a proof. The complexity of a formula may be its length, or its number of variables, or its number of quantifiers, etc. The depth of a proof-tree (in the case of natural deduction or sequent calculus). The memory complexity of a proof. One can imagine a proof system as having a memory bank, such that at any point in the proof, only formulas in the bank, or axioms, may be used. A formula may be removed from the memory bank, but if that formula needs to be used again, it must be re-proven. Then, the memory complexity of the proof is the minimal number of memory locations necessary for the proof to go through.
The search complexity of a proof system denotes the computational complexity of a prover, that is, an algorithm for finding a proof of a tautology within a proof system. A proof system with a polynomial-time prover is automatable.
Proof size complexity
p-boundedness A proof system is polynomially bounded (p-bounded) iff for any , if there exists some such that is true, then there exists some such that is true, and . In other words, anything that the system can prove at all, has a polynomially-short proof.
Most nontrivial proof systems are believed to be not p-bounded. To acquire intuition about why this is the case, one consider the following examples.
Graph coloring Given a graph , if there exists a 3-coloring, then this can be proven by simply giving the coloring. Thus, the proof of 3-colorability has length . It can be checked in polynomial time. In contrast, if there does not exist a 3-coloring, then there is no obvious way to prove it succinctly. The naive way to prove it is to explicitly enumerate all possible 3-colorings, and showing that in each case, there are two vertices of the same color sharing an edge. However, such a proof is exponentially large compared to the input size.
The Hajós construction is a sound and complete proof system for graph non-3-colorability: A graph is non-3-colorable if and only if it has a Hajós 4-construction. However, such a construction may require superpolynomially steps.
Polynomial Given a system of polynomials in a finite field , if there exists a root, then this can be proven by simply giving the values for the variables . The proof size is linear in input size. It can be checked in polynomial time.
However, if there is no root, then there is no obvious way to prove it succinctly. The naive way to prove it is to explicitly enumerate all possible values. By Hilbert's Nullstellensatz, there is a sound and complete proof system for non-solvability: There exists some polynomials such that , if and only if the polynomial system is non-solvable. However, the polynomials may contain superpolynomially many terms.
Tautology Given a formula in classical propositional logic with propositional variables , if it is not a tautology, then this can be proven by simply giving the truth-values for the propositional variables , such that evaluates to False. The proof size is linear in input size. However, if it is a tautology, then there is no obvious way to prove it succinctly. The naive way to prove it is to explicitly enumerate the truth table, which has rows.
There are many sound and complete proof systems for proving tautologies of classical propositional logic, but there is no guarantee that any system can prove all tautologies with proof size .
Main results
Because is not a tautology if and only if is satisfiable, is co-NP-complete. Thus, if there exists a proof system for that is p-bounded, then NP = co-NP. Conversely, if NP = co-NP, then , being co-NP, would also be NP, and thus there is a p-bounded proof system for proving tautologies. This was first proven by Cook and Reckhow (1979). This results in an equivalent formulation of the NP = coNP problem:Does there exist a p-bounded proof system for classical propositional tautologies?
Proof system strength Proof complexity compares the strength of proof systems using the notion of efficient simulation. Efficiency is the operative concept here, since proof complexity theory studies not merely whether something can be proven, but in the efficiency of the proof.
Definitions Given two proof systems , simulates , written as , if and only if there is an algorithm that:
given as input, a Q-proof of a tautology, outputs a P-proof of the same tautology, and the size of the P-proof is polynomial in the size of the Q-proof.
We say that p-simulates , written as if and only if there is an algorithm that:
given as input, a Q-proof of a tautology, outputs a P-proof of the same tautology, and runs in polynomial time polynomial in the size of the Q-proof.
Since a polynomial-time algorithm can only produce a polynomial-size output, p-simulation implies simulation. The converse may not hold, i.e. two proof systems may exist such that simulates , but does not p-simulate .
Both simulation and p-simulation relations are reflexive and transitive, thus they are preorders, and induces equivalence relations. If (p-)simulate each other, then they are (p-)equivalent. A proof system is (p-)optimal if it (p-)simulates all other proof systems.
Results Any nonempty set in NP has an optimal proof system. No set outside of NP is known to have an optimal proof system. Any coNE-hard sets and even all coNQP-hard sets is known to have no optimal proof systems.
Sequent calculus is p-equivalent to (every) Frege system.
Every propositional proof system P can be simulated by Extended Frege extended with axioms postulating soundness of P.
An optimal or p-optimal propositional proof system would be ideal in a sense, since it would produce the shortest (up to a polynomial factor) possible proofs for all tautologies. Unfortunately, this question is open.
It is known that:
If E = NE, then there exists of an optimal proof system. If NE = co-NE, then there exists of an optimal proof system.
It has been proven that many weak proof systems cannot simulate certain stronger systems (see below). However, the question remains open if the notion of simulation is relaxed. For example, it is open whether Resolution effectively polynomially simulates Extended Frege.
Automatability The search complexity of proof systems asks:Given a proof system, is there an efficient prover of tautologies in this system?A proof system is automatable if there is an algorithm , called the prover, such that:
If is a tautology, then is true. That is, the algorithm outputs a P-proof of . Note that there is no requirement for what the algorithm should do when is not a tautology. is computable in time , where is the shortest P-proof of .