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 ( ( ( ( ( 𝜑𝜓 ) → ( ¬ 𝜒 → ¬ 𝜃 ) ) → 𝜒 ) → 𝜏 ) → ( ( 𝜏𝜑 ) → ( 𝜃𝜑 ) ) )