Propositional calculus in implication and non-equivalence.
Arthur N. Prior · Notre Dame Journal of Formal Logic · 1969
If we use C for implication, 0 for a false constant, and J for nonequivalence, Jaβ is definable as CCaβCCβaQ.Hence the full classical calculus in C-O-J is obtainable by substitution and detachment fromHere 1 is Lukasiewicz's single axiom for C-pure; 2 with this is known to give full C-0, and 3 and 4 are jointly equivalent to the above definition.Moreover, we have CJppQ from 3 q/p and Cpp, and CJppq from this and 2; from this in turn we have CJppJqq, showing that Jpp is a constant and can take the place of 0 in the above postulates to give a full set for C-J. 2 and 3 can then be replaced by CJpqCCpqCCqpr, which yields 3 by r/Jpp, and 2 by q/p and Cpp.Hence 1.CCCpqrCCrpCsp, 2\ CJpqCCpqCCqpr and 3 T .CCCpqCCqpJppJpq suffice for C-J.This set somewhat abridges that given by Shukla in "A set of axioms for the propositional calculus with implication and non-equivalence", Notre Dame Journal of Formal Logic, Vol. 7 (1966), pp.281-6.Similar considerations show that if we use B for non-implication and axiomatise in C-B (as suggested by C. S. Peirce, Collected Papers 3.386), we need only 1, CBpqCCpqr and CCCpqBppBpq.Indeed, we can give a similar proof of an old result, the adequacy of 1, CNpCpq and CCpNpNp for C-N, thus: 5. CNCppCCppq {CNpCpq) *6.CNCppq (1, 5) *7.CNCppNCqq (6) 8. CCpNCppCpq (1, 6) *9.CCpNCppNp (1, 8 q/Np, CCpNpNp) *10.CNpCpNCpp (CNpCpq)