The Complexity of Propositional Proofs with the Substitution Rule
Alasdair Urquhart · Logic Journal of IGPL · 2005
We prove that for sufficiently large N, there are tautologies of size O(N) that require proofs containing Ω(N) lines in axiomatic systems of propositional logic based on axioms and the rule of substitution for single variables. These tautologies have proofs with O(log2N) lines in systems with the multiple substitution rule.