Journal article:
Maria Luisa Bonet and Samuel R. Buss.
"The deduction rule and linear and near-linear proof
simulations."
Journal of Symbolic Logic 58 (1993) 688-709.
Download article: postscript or PDF.
Abstract: We introduce new proof systems for
propositional logic, simple deduction Frege systems, general deduction Frege
systems and nested deduction Frege systems, which augment Frege systems with
variants of the deduction rule. We give upper bounds on the lengths of proofs in Frege
proof systems compared to lengths in these new systems. As applications we give
near-linear simulations of the propositional Gentzen sequent calculus and the natural
deduction calculus by Frege proofs. The length of a proof is the number of lines (or
formulas) in the proof.
A general deduction Frege proof system provides at most quadratic
speedup over Frege proof systems. A nested deduction Frege proof system provides at most a
nearly linear speedup over Frege system where by ``nearly linear'' is meant the ratio of
proof lengths is $O(\alpha(n))$ where $\alpha$ is the inverse Ackermann function. A nested
deduction Frege system can linearly simulate the propositional sequent calculus, the
tree-like general deduction Frege calculus, and the natural deduction calculus. Hence a
Frege proof system can simulate all those proof systems with proof lengths bounded by
$O(n\cdot\alpha(n))$. Also we show that a Frege proof of $n$ lines can be transformed into
a tree-like Frege proof of $O(n\log n)$ lines and of height $O(\log n)$. As a corollary of
this fact we can prove that natural deduction and sequent calculus tree-like systems
simulate Frege systems with proof lengths bounded by $O(n\log n)$.
Related paper: The serial transitive closure problem, in SIAM J. Comput. 1995.
Earlier conference paper: On the deduction rule and the number of proof lines, in LICS'91.