In propositional calculus and proof complexity a propositional proof system (pps), also called a Cook–Reckhow propositional proof system, is system for proving classical propositional tautologies.
Formally a pps is a polynomial-time function P whose range is the set of all propositional tautologies (denoted TAUT). If A is a formula, then any x such that P(x) = A is called a P-proof of A. The condition defining pps can be broken up as follows:
In general, a proof system for a language L is a polynomial-time function whose range is L. Thus, a propositional proof system is a proof system for TAUT.
Sometimes the following alternative definition is considered: a pps 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 it is a tautology.
If P1 is a pps according to the first definition, then P2 defined by P2(A,x) if and only if P1(x) = A is a pps according to the second definition. Conversely, if P2 is a pps according to the second definition, then P1 defined by
(P1 takes pairs as input) is a pps according to the first definition, where is a fixed tautology.
One can view the second definition as a non-deterministic algorithm for solving membership in TAUT. This means that proving a superpolynomial proof size lower-bound for pps would rule out existence of a certain class of polynomial-time algorithms based on that pps.