Metamath Proof Explorer


Theorem meredith

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 , where negation and implication are primitive. Here we prove Meredith's axiom from ax-1 , ax-2 , and ax-3 . Then from it we derive the Lukasiewicz axioms luk-1 , luk-2 , and luk-3 . Using these we finally rederive our axioms as ax1 , ax2 , and ax3 , 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)

Ref Expression
Assertion meredith φψ¬χ¬θχττφθφ

Proof

Step Hyp Ref Expression
1 pm2.21 ¬φφψ
2 con4 ¬χ¬θθχ
3 1 2 imim12i φψ¬χ¬θ¬φθχ
4 3 com13 θ¬φφψ¬χ¬θχ
5 4 con1d θ¬φψ¬χ¬θχφ
6 5 com12 ¬φψ¬χ¬θχθφ
7 6 a1d ¬φψ¬χ¬θχτφθφ
8 ax-1 τθτ
9 8 imim1d ττφθφ
10 7 9 ja φψ¬χ¬θχττφθφ