On the Deduction Rule and the Number of Proof Lines (Extended 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 these systems compared to lengths in Frege proof systems. As an application we give a near-linear simulation of the propositional Gentzen sequent calculus by Frege proofs. The length of a proof is the number of steps or lines 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(α(n)) where α is the inverse Ackermann function. A nested deduction Frege system can linearly simulate the propositional sequent calculus and hence a Frege proof system can simulate the propositional sequent calculus with proof lengths bounded by O(n · α(n)). As a technical tool, we introduce the serial transitive closure problem: given a directed graph and a list of closure edges in the transitive closure of the graph, the problem is to derive all the closure edges. We give a nearly linear bound on the number of steps in such a derivation when the graph is tree-like.