MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  meredith Structured version   Visualization version   GIF version

Theorem meredith 1557
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 1571, luk-2 1572, and luk-3 1573. Using these we finally rederive our axioms as ax1 1582, ax2 1583, and ax3 1584, 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.)

Assertion
Ref Expression
meredith (((((𝜑𝜓) → (¬ 𝜒 → ¬ 𝜃)) → 𝜒) → 𝜏) → ((𝜏𝜑) → (𝜃𝜑)))

Proof of Theorem meredith
StepHypRef Expression
1 pm2.21 119 . . . . . . 7 𝜑 → (𝜑𝜓))
2 con4 111 . . . . . . 7 ((¬ 𝜒 → ¬ 𝜃) → (𝜃𝜒))
31, 2imim12i 60 . . . . . 6 (((𝜑𝜓) → (¬ 𝜒 → ¬ 𝜃)) → (¬ 𝜑 → (𝜃𝜒)))
43com13 86 . . . . 5 (𝜃 → (¬ 𝜑 → (((𝜑𝜓) → (¬ 𝜒 → ¬ 𝜃)) → 𝜒)))
54con1d 138 . . . 4 (𝜃 → (¬ (((𝜑𝜓) → (¬ 𝜒 → ¬ 𝜃)) → 𝜒) → 𝜑))
65com12 32 . . 3 (¬ (((𝜑𝜓) → (¬ 𝜒 → ¬ 𝜃)) → 𝜒) → (𝜃𝜑))
76a1d 25 . 2 (¬ (((𝜑𝜓) → (¬ 𝜒 → ¬ 𝜃)) → 𝜒) → ((𝜏𝜑) → (𝜃𝜑)))
8 ax-1 6 . . 3 (𝜏 → (𝜃𝜏))
98imim1d 80 . 2 (𝜏 → ((𝜏𝜑) → (𝜃𝜑)))
107, 9ja 172 1 (((((𝜑𝜓) → (¬ 𝜒 → ¬ 𝜃)) → 𝜒) → 𝜏) → ((𝜏𝜑) → (𝜃𝜑)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  merlem1  1558  merlem2  1559  merlem3  1560  merlem4  1561  merlem5  1562  merlem7  1564  merlem8  1565  merlem9  1566  merlem10  1567  merlem11  1568  merlem13  1570  luk-1  1571  luk-2  1572  merco1  1629
  Copyright terms: Public domain W3C validator