 The ideas behind these rules seem to have no intrinsic connection with natural deduction: they do not use subproofs (they replace the subproof-involving quantifier rules of more standard systems), and they could be used in conjunction with a purely axiomatic system of propositional logic. Their association with natural deduction is a matter of historical accident: the textbooks introducing them presented systems with other features of natural deduction. Still, they have some practical value: proofs employing (a correctly restricted version of) them, in the context of a system for classical logic, can be shorter and simpler than the proofs in systems with the standard natural deduction rules. (The classically valid schemes