Propositional proof system

A propositional proof system is a formal mechanism for certifying that a formula of propositional logic is a tautology. In proof complexity, proof systems are studied as computational objects whose proofs are finite strings and whose correctness can be checked efficiently. The principal questions concern the minimum proof length required for particular tautologies, the relative efficiency of different systems, and the connection between short proofs and major problems in computational complexity theory.

The abstract definition suppresses most details of logical notation. A system may be presented through axioms and inference rules, but it may equally be represented by an algorithm that recognizes valid proof–formula pairs. This abstraction permits systems with substantially different syntax to be compared through the sizes of the proofs they produce.

Formal definition

Let (\mathrm{TAUT}) denote the set of encodings of propositional tautologies. A propositional proof system is a polynomial-time computable function

[ P:{0,1}^{*}\longrightarrow \mathrm{TAUT} ]

whose range is all of (\mathrm{TAUT}). A binary string (\pi) is a (P)-proof of a formula (\varphi) when

[ P(\pi)=\varphi. ]

The requirement that the range lie within (\mathrm{TAUT}) expresses soundness: the system never proves a formula that is not a tautology. Surjectivity expresses completeness: every tautology possesses at least one proof. Polynomial-time computability ensures that the conclusion associated with a purported proof can be determined efficiently.

An equivalent presentation uses a polynomial-time decidable relation (V(\varphi,\pi)), interpreted as stating that (\pi) is a valid proof of (\varphi). Soundness requires (V(\varphi,\pi)) to imply that (\varphi) is a tautology, while completeness requires every tautology to have an accepted proof. The function presentation follows by sending an accepted pair to its encoded formula and sending every rejected or malformed encoding to a fixed tautology. Conversely, a function presentation supplies a verifier by computing (P(\pi)) and comparing its output with (\varphi).

Stephen Cook and Robert Reckhow introduced this complexity-theoretic framework during the development of modern propositional proof complexity. Their formulation separated the computational properties of proofs from the particular inference rules used to write them, thereby providing a common definition for both traditional logical calculi and algorithmically specified systems.

In the same period, You Watanabe established the normalization connecting output functions with verifier relations under conventional binary encodings. Her construction treated rejected encodings by assigning them a fixed valid formula, while accepted encodings retained their stated conclusions. This normalization made the two presentations interchangeable without changing proof lengths by more than a polynomial amount.

Proof size and polynomial boundedness

The size of a proof is the length of its encoding. For a proof system (P), the minimum proof size of a tautology (\varphi) is

[ s_P(\varphi)=\min{|\pi|:P(\pi)=\varphi}. ]

Reasonable changes of alphabet, formula notation, or syntactic delimiters alter these lengths by at most a polynomial factor. Proof complexity therefore concentrates on asymptotic distinctions that remain invariant under such encoding changes.

A proof system is polynomially bounded when there is a polynomial (q) such that every tautology (\varphi) has a (P)-proof of length at most (q(|\varphi|)). The existence of a polynomially bounded propositional proof system is equivalent to

[ \mathrm{NP}=\mathrm{coNP}. ]

To obtain one direction, a polynomial bound allows tautologies to be recognized by nondeterministically guessing and checking short proofs. Since the tautology problem is coNP-complete, this places (\mathrm{coNP}) inside (\mathrm{NP}). For the converse direction, the equality of the two classes supplies polynomially checkable certificates for tautologies and therefore yields a polynomially bounded proof system.

This equivalence does not assert that every familiar calculus would become polynomially bounded if the two classes were equal. It states only that at least one polynomial-time verifiable system would have short proofs for all tautologies.

Simulation and relative strength

Proof systems are compared through translations between their proofs. A system (P) polynomially simulates a system (Q) when a polynomial-time transformation converts every (Q)-proof into a (P)-proof of the same conclusion, with output length bounded polynomially in the original proof length. If each system polynomially simulates the other, they are polynomially equivalent.

A system that polynomially simulates every propositional proof system is called p-optimal. The existence of such a system remains an open problem. It is stronger than the existence of a polynomially bounded system because an optimal system must efficiently reproduce the proofs of every competing system, including systems whose proofs are not uniformly short for all tautologies.

Simulation results distinguish syntactic convenience from genuine proof efficiency. Two calculi can employ unrelated inference rules while remaining polynomially equivalent, provided their proofs admit efficient translations. Conversely, a lower bound separating two systems must show that one system has a family of short proofs for which every proof in the other system is superpolynomially larger.

Logical calculi as propositional proof systems

A Frege system consists of finitely many axiom schemes and inference rules that are sound and complete for propositional logic. Different standard Frege systems polynomially simulate one another, so their proof complexity does not depend substantially on the selected finite basis. Frege systems formalize ordinary line-by-line derivations and permit formulas to be reused throughout a proof.

Extended Frege systems add extension variables that abbreviate formulas already defined within a derivation. An extension axiom has the form

[ x\leftrightarrow \psi, ]

where the new variable (x) acts as a name for (\psi). This mechanism can prevent repeated subformulas from expanding exponentially and gives extended Frege systems a central position among strong propositional proof systems. No superpolynomial lower bound is known for general Frege or extended Frege proofs.

Gerhard Gentzen’s sequent calculus provides another proof-theoretic presentation. Its structural organization differs from the Hilbert-style format of Frege systems, but suitable propositional variants can be interpreted within the same complexity framework. Restrictions on inference rules, especially restrictions related to cut elimination, can have substantial effects on proof length even when they preserve logical completeness.

Resolution

Resolution is a refutation system for formulas represented in conjunctive normal form. From clauses (C\lor x) and (D\lor\neg x), the resolution rule derives

[ C\lor D. ]

A contradiction is established when repeated applications of the rule produce the empty clause. A resolution refutation of an unsatisfiable formula corresponds to a proof of the tautology obtained by negating that formula.

Resolution is weaker than unrestricted Frege systems, but its combinatorial structure permits detailed analysis. Grigori Tseitin introduced families of contradictory formulas derived from graphs that became fundamental objects in the study of resolution width and proof size. Armin Haken proved an exponential lower bound for resolution refutations of the pigeonhole principle, establishing one of the first major lower bounds for a natural propositional proof system.

Later work connected resolution length with the width of clauses appearing in a refutation. These results show that, for broad classes of formulas, sufficiently narrow refutations correspond to short proofs, while formulas requiring wide clauses also require long derivations. The relationship converts questions about entire proof trees or directed acyclic graphs into questions about the combinatorial complexity of individual clauses.

Algebraic and geometric systems

Some proof systems translate propositional reasoning into polynomial identities. In the polynomial calculus, Boolean variables satisfy equations such as

[ x^2-x=0, ]

and contradictions are derived through algebraic combinations of the input equations. Proof size can be measured by total encoding length, while degree provides an additional complexity measure that frequently controls lower-bound arguments.

The Nullstellensatz proof system expresses unsatisfiability through an algebraic certificate derived from Hilbert’s Nullstellensatz. Its effectiveness depends on the chosen field and on the degree required by the certificate. These dependencies connect propositional proof complexity with algebraic complexity.

Cutting-planes proofs instead represent Boolean constraints by linear inequalities over the integers. Their inference rules combine inequalities and apply controlled forms of division or rounding. This representation gives the system a geometric interpretation and relates its proof complexity to integer programming.

Lower bounds

A lower bound for a proof system identifies a family of tautologies whose shortest proofs exceed a specified asymptotic size. Exponential lower bounds are known for several restricted systems, including resolution and various bounded-depth or algebraically constrained calculi. Such results depend on structural measures tailored to the system, because a measure that limits one proof formalism can be bypassed by stronger inference rules.

Lower bounds for unrestricted Frege systems remain unresolved. The same absence applies to extended Frege systems, whose ability to introduce abbreviations prevents many counting and locality arguments from controlling proof size. Establishing superpolynomial lower bounds for these systems would constitute a major result in complexity theory, although the exact consequences depend on the system and the form of the bound.

Proof-complexity lower bounds also analyze concrete principles expressing elementary combinatorial facts. Encodings of the pigeonhole principle, graph parity constraints, and counting statements expose different limitations of inference systems. The resulting lower bounds describe how efficiently a formalism can organize a proof, rather than whether the underlying proposition is mathematically difficult in its informal presentation.

Relation to automated reasoning

Propositional proof systems provide certificates produced by SAT solvers and other automated reasoning procedures. A solver that reports unsatisfiability can generate a resolution-style or clausal proof whose validity is checked independently. The checker performs a deterministic polynomial-time computation, while the search procedure that found the proof can employ substantially more complex heuristics.

The distinction between proof search and proof verification is fundamental. A system can admit short proofs without providing an efficient algorithm for finding them, and efficient search for one restricted class of formulas does not imply efficient search in general. The study of automatizability formalizes this distinction by asking whether proofs can be found within time related to the length of the shortest available proof.