Notes on the axiomatics of the propositional calculus.
C. A. Meredith, Arthur N. Prior · Notre Dame Journal of Formal Logic · 1963
In this paper the proofs, unless otherwise stated, are Meredith's, and the bracketed notes introducing each item or commenting on it, Prior's.The proofs are all compressed by Meredith's device of writing Όmn' for the most general result (i.e.without any unnecessary identification of variables) of detaching the formula n, or some substitution in it, from the formula m, or some substitution in it.1. -Lukasiewicz's Deduction Shortened.(This is a very slight abridgement of -Lukasiewicz's proof that CCCpqrCCrpCsp suffices for classical C. It seems worth including, as Lukasiewicz's own paper [5] is now out of print and not easily obtainable.) 1. CCCpqrCCrpCsp 2. CCCpqpCrp = DDDlDllln 3. CCCpqrCqr = DDDlDlD121n 4. CpCCpqCrq = D31 5. CCCpqCrsCCCqtsCrs = DDDlDlDlD141n 6. CCCpqCrsCCpsCrs = D51 7. CCpCqrCCpsrCqr = D64 8. CCCCCpqrtCspCCrpCsp = D71 9. CCpqCpq = D83 10.CCCCrpCtpCCCpqrsCuCCCpqrs = D18 11.CCCCpqrCsqCCCqtsCpq = DDlO.lO.n 12. CCCCpqrCsqCCCqtpCsq = D5.ll 13.CCCCpqrsCCsqCpq = D12.6 14. CCCpqrCCrpp = D12.9 15.CpCCpqq = D3.14 16.CCpqCCCprqq = D6.15*17.CCpqCCqrCpr = DD.13D.16.16.13