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.