2.2 Proof Systems

A propositional proof system (Cook and Reckhow, 1977) is a polynomial time computable predicate S such that a propositional formula F is unsatisfiable iff there exists a proof p for which S(F, p) holds. In other words, it is an efficient (in the size of the proof) procedure to check the correctness of proofs presented in a certain format. Finding short proofs, however, may still be difficult. In fact, short proofs may not exist in the proof system if it is too weak. In the rest of this paper, we refer to such systems simply as proof systems and omit the word propositional.

Definition 1   For a proof system S and an unsatisfiable formula F, the complexity of F in S, denoted $\mathcal {C}$_S(F), is the length of the shortest refutation of F in S. For a family {F_n} of formulas over increasing number of variables n, its asymptotic complexity in S, denoted $\mathcal {C}$_S(F_n) with abuse of notation, is measured with respect to the increasing sizes of F_n.

Definition 2   For proof systems S and T, and a function f : $\mathbb {N}$ $\rightarrow$ $\mathbb {N}$,

• S is natural if for any formula F and restriction $\rho$ on its variables, $\mathcal {C}$_S(F|_$\rho$)$\le$$\mathcal {C}$_S(F).

• S is a refinement of T if proofs in S are also (restricted) proofs in T.

• A refinement S of T is f (n)-proper if there exists a witnessing family {F_n} of formulas such that $\mathcal {C}$_S(F_n)$\ge$f (n) ^. $\mathcal {C}$_T(F_n). The refinement is exponentially-proper if f (n) = 2^n$\Omega$(1) and super-polynomially-proper if f (n) = n^$\omega$(1).