Equational logic.
C. A. Meredith, A. N. Prior · Notre Dame Journal of Formal Logic · 1968
PRIOR §1.General Introduction The present section is by A. N. Prior, while those which follow are by C. A. Meredith, except where otherwise indicated.The second section, which is of date 1956, carries further a result which Lukasiewicz published in 1952, 1 namely that if F, T and N be intuitionist implication, conjunction and negation, and Cpq be defined as NTpNq, the classical axioms CCpqCCqrCpr, CCNppp and CpCNpq are provable from the intuitionist basis, and the rule of C-detachment (to infer f-β from ϊ-Caβ, i.e. hNTaNβ, and ha) is provable for formulae in C and N. Meredith's improvement on this is that if Cpq be defined as FFFqppq, the C-classical axioms CCpqCCqrCpr, CCCpqpp, CpCqp are provable from the intuitionist base, and detachment for this C (which unlike Lukasiewicz's is stronger than F) is provable without restriction.The proof which Meredith sketches in his note is not, however, a simple substitution-and-detachment deduction, but the derivation of classical equations for the defined functor (which he writes as G) from intuitionist equations for the undefined (which he writes as C).An early example of an equational axiomatisation of the full propositional calculus is that given by W. E. Johnson in his articles of 1892. 2 Johnson's undefined functors are conjunction, represented by juxtaposition, and negation, represented by a superimposed bar.His axioms are the five equations 1. xy = yx 2. {xy)z = x(yz) 3. xx = x 4. x -x 5. ~x -Icy xyIt might be argued that these involve not only conjunction and negation but also equivalence as a primitive, but the "=" sign is to be thought of rather as on the same level as the assertion sign in ordinary substitution-anddetachment systems.The sole rules Johnson uses are substitution for