Preprint:
Sam Buss
Substitution and Propositional Proof Complexity
In Alasdair Urquhart on Nonclassical
and Algebraic Logic and Complexity of Proofs
Springer, 2022, pp. 477-496.
Download
preprint.
Abstract: We discuss substitution rules that allow the substitution of formulas for formula variables. A substitution rule was first introduced by Frege. More recently, substitution is studied in the setting of propositional logic. We state theorems of Urquhart's giving lower bounds on the number of steps in the substitution Frege system for propositional logic. We give the first superlinear lower bounds on the number of symbols in substitution Frege and multi-substitution Frege proofs.