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 coNP (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=coNP.
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.
Proof systems
A propositional proof system is given as a proof-verification algorithm P(A,x) with two inputs. If P accepts the pair (A,x) we say that x is a P-proof of A. P is required to run in polynomial time, and moreover, it must hold that A has a P-proof if and only if A is a tautology.
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'.
Proofs of polynomial size and the NP versus coNP problem
Proof complexity measures the efficiency of the proof system usually in terms of the minimal size of proofs possible in the system for a given tautology. The size of a proof (respectively formula) is the number of symbols needed to represent the proof (respectively formula). A propositional proof system P is polynomially bounded if there exists a constant such that every tautology of size has a P-proof of size . A central question of proof complexity is to understand if tautologies admit polynomial-size proofs. Formally,
Problem (NP vs. coNP) Does there exist a polynomially bounded propositional proof system?
Cook and Reckhow (1979) observed that there exists a polynomially bounded proof system if and only if NP=coNP. Therefore, proving that specific proof systems do not admit polynomial size proofs can be seen as a partial progress towards separating NP and coNP (and thus P and NP).
Optimality and simulations between proof systems
Proof complexity compares the strength of proof systems using the notion of simulation. A proof system P p-simulates a proof system Q if there is a polynomial-time function that given a Q-proof of a tautology outputs a P-proof of the same tautology. If P p-simulates Q and Q p-simulates P, the proof systems P and Q are p-equivalent. There is also a weaker notion of simulation: a proof system P simulates a proof system Q if there is a polynomial p such that for every Q-proof x of a tautology A, there is a P-proof y of A such that the length of y, |y| is at most p(|x|).
For example, sequent calculus is p-equivalent to (every) Frege system.
A proof system is p-optimal if it p-simulates all other proof systems, and it is optimal if it simulates all other proof systems. It is an open problem whether such proof systems exist:
Problem (Optimality) Does there exist a p-optimal or optimal propositional proof system?
