| Description: Carew Meredith's sole
axiom for propositional calculus. This amazing
formula is thought to be the shortest possible single axiom for
propositional calculus with inference rule ax-mp 5,
where negation and
implication are primitive. Here we prove Meredith's axiom from ax-1 6,
ax-2 7, and ax-3 8. Then from it we derive the Lukasiewicz
axioms
luk-1 1420, luk-2 1421, and luk-3 1422. Using these we finally re-derive our
axioms as ax1 1431, ax2 1432, and ax3 1433,
thus proving the equivalence of all
three systems. C. A. Meredith, "Single Axioms for the Systems (C,N),
(C,O) and (A,N) of the Two-Valued Propositional Calculus," The
Journal of
Computing Systems vol. 1 (1953), pp. 155-164. Meredith claimed to be
close to a proof that this axiom is the shortest possible, but the proof
was apparently never completed.
An obscure Irish lecturer, Meredith (1904-1976) became enamored with logic
somewhat late in life after attending talks by Lukasiewicz and produced
many remarkable results such as this axiom. From his obituary: "He
did
logic whenever time and opportunity presented themselves, and he did it on
whatever materials came to hand: in a pub, his favored pint of porter
within reach, he would use the inside of cigarette packs to write proofs
for logical colleagues." (Contributed by NM, 14-Dec-2002.) (Proof
shortened by Andrew Salmon, 25-Jul-2011.) (Proof shortened by Wolf
Lammen, 28-May-2013.) |
