Journal article:
Samuel R. Buss.
"Propositional consistency proofs."
Annals of Pure and Applied Logic 52 (1991) 3-29.
Download article: postscript or PDF.
Abstract: Partial consistency statements can be
expressed as polynomial-size propositional formulas. Frege proof systems have
polynomial-size partial self-consistency proofs. Frege proof systems have polynomial-size
proofs of partial consistency of extended Frege proof systems if and only if Frege proof
systems polynomially simulate extended Frege proof systems. We give a new proof of
Reckhow's theorem that any two Frege proof systems p-simulate each other.
The proofs depend on polynomial size propositional formulas defining
the truth of propositional formulas. These are already known to exist since the Boolean
formula value problem is in alternating logarithmic time; this paper presents a proof of
this fact based on a construction which is somewhat simpler than the prior proofs of Buss
and of Buss-Cook-Gupta-Ramachandran.