Quantified propositional logic and the number of lines of tree-like proofs (Q1577358)

Rules for quantifiers over propositions are added to the sequent calculus for propositional logic. The rules are formulated in the obvious way and they are similar to the usual rules for first-order quantification. In contrast, Substitution Frege systems are formulated in the sequent calculus for propositional logic as well; however, instead of the quantifier rules they feature a rule that allows for uniform substitution of propositional parameters by arbitrary propositional formulas. The introduction of the propositional quantifiers induces an exponential speed-up of proofs of propositional tautologies (with respect to the number of lines in a proof) over Substitution Frege systems.