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.
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.
A propositional proof system P is polynomially bounded if there exists a constant
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.
Every propositional proof system P can be simulated by Extended Frege extended with axioms postulating soundness of P.[3] The existence of an optimal (respectively p-optimal) proof system is known to follow from the assumption that NE=coNE (respectively E=NE).
For example, it is open whether Resolution effectively polynomially simulates Extended Frege.
It is not known if the weak automatability of Resolution would break any standard complexity-theoretic hardness assumptions.
On the positive side, Propositional proof systems can be interpreted as nonuniform equivalents of theories of higher order.
For example, the Extended Frege system corresponds to Cook's theory
formalizing polynomial-time reasoning and the Frege system corresponds to the theory
The correspondence was introduced by Stephen Cook (1975), who showed that coNP theorems, formally
translate to sequences of tautologies with polynomial-size proofs in Extended Frege.
It is possible to derive lower bounds on size of proofs in a proof system P by constructing suitable models of a theory T corresponding to the system P. This allows to prove complexity lower bounds via model-theoretic constructions, an approach known as Ajtai's method.
[22] Propositional proof systems can be interpreted as nondeterministic algorithms for recognizing tautologies.
Proving a superpolynomial lower bound on a proof system P thus rules out the existence of a polynomial-time algorithm for SAT based on P. For example, runs of the DPLL algorithm on unsatisfiable instances correspond to tree-like Resolution refutations.
Therefore, exponential lower bounds for tree-like Resolution (see below) rule out the existence of efficient DPLL algorithms for SAT.
Proving lower bounds on lengths of propositional proofs is generally very difficult.
Nevertheless, several methods for proving lower bounds for weak proof systems have been discovered.
It is a long-standing open problem to derive a nontrivial lower bound for the Frege system.
Some proof systems such as Resolution and Cutting Planes admit feasible interpolation or its variants.
In fact, for many proof systems, such as Extended Frege, feasible interpolation is equivalent to weak automatability.
Therefore, an efficient interpolant resulting from short P-proofs of soundness of P would decide whether a given formula
Such an interpolant can be used to define a proof system R witnessing that P is weakly automatable.
[30] On the other hand, weak automatability of a proof system P implies that P admits feasible interpolation.
However, if a proof system P does not prove efficiently its own soundness, then it might not be weakly automatable even if it admits feasible interpolation.
Many non-automatability results provide evidence against feasible interpolation in the respective systems.
Hrubeš (2007–2009) proved exponential lower bounds on size of proofs in the Extended Frege system in some modal logics and in intuitionistic logic using a version of monotone feasible interpolation.