Replacing Modus Ponens With One-Premiss Rules

摘要

After some motivating remarks in Section 1, in Section 2 we show how to replace an axiomatic basis for any one of a broad range of sentential logics having finitely many axiom schemes and Modus Ponens as the sole proper rule, by a basis with the same axiom schemes and finitely many one-premiss rules. (Indeed, we also show that for the same range of logics, we can replace these axiom schemes by a single scheme, keeping the rules as for the replacement axiomatization just alluded to.) Section 3 mentions some questions arising from this replacement procedure (which works for many familiar sentential logics, including intuitionistic and classical logic), explores another such procedure, and discusses some aspects of the consequence relations associated with the different axiomatizations in play. Several open problems are mentioned. An appendix briefly treats the issue of a similar ‘at most one-premiss rules’ reformulation of proof systems with sequent-to-sequent rules.