Propositional proof system

Formally a pps is a polynomial-time function P whose range is the set of all propositional tautologies (denoted TAUT).

As an example, exponential proof size lower-bounds in resolution for the pigeon hole principle imply that any algorithm based on resolution cannot decide TAUT or SAT efficiently and will fail on pigeon hole principle tautologies.

The general definition of a propositional proof system is due to Stephen Cook and Robert A. Reckhow (1979).

A propositional proof system P is polynomially bounded (also called super) if every tautology has a short (i.e., polynomial-size) P-proof.

Existence of a polynomially bounded propositional proof system means that there is a verifier with polynomial-size certificates, i.e., TAUT is in NP.

In fact these two statements are equivalent, i.e., there is a polynomially bounded propositional proof system if and only if the complexity classes NP and coNP are equal.

circuit family of subexponential size, many tautologies relating to the pigeonhole principle cannot have subexponential proofs in a proof system based on bounded-depth formulas (and in particular, not by resolution-based systems, since they rely solely on depth 1 formulas).