Proof routines for the propositional calculus.
Hugues Leblanc · Notre Dame Journal of Formal Logic · 1963
I prove in the pages that follow a conjecture of mine, to wit: Any metastatement of the form A v Λ 2 > Ά n h B,where A χ , A 2 , . . ., A n (n > 0), and B are tuffs of PC and f |-' is the customary yields sign, is provable, when valid, by means of the three structural rules in Table I and the intelim rules in Table I for such of the connectives % nJ, % y, '&', V, and '=' as occur in A χ9 A 2 , . . ., A n \-B, and sketch a routine for proving A χ9 A 2 , . . ., A n \-B, when valid, for each one of the 32 cases covered by the conjecture. 1 I also discuss a related conjecture of mine concerning the intuitionist fragment of PC.My thanks go to Nuel D. Belnap, Jr., who should be credited for some of the results of Section II, and to Henry Hiz and Michael D