Theorem meredith 1635

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 1649, luk-2 1650, and luk-3 1651. Using these we finally rederive our axioms as ax1 1660, ax2 1661, and ax3 1662, 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

Step	Hyp	Ref	Expression
1		pm2.21 123	. . . . . . 7 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
2		con4 113	. . . . . . 7 ⊢ ((¬ 𝜒 → ¬ 𝜃) → (𝜃 → 𝜒))
3	1, 2	imim12i 62	. . . . . 6 ⊢ (((𝜑 → 𝜓) → (¬ 𝜒 → ¬ 𝜃)) → (¬ 𝜑 → (𝜃 → 𝜒)))
4	3	com13 88	. . . . 5 ⊢ (𝜃 → (¬ 𝜑 → (((𝜑 → 𝜓) → (¬ 𝜒 → ¬ 𝜃)) → 𝜒)))
5	4	con1d 145	. . . 4 ⊢ (𝜃 → (¬ (((𝜑 → 𝜓) → (¬ 𝜒 → ¬ 𝜃)) → 𝜒) → 𝜑))
6	5	com12 32	. . 3 ⊢ (¬ (((𝜑 → 𝜓) → (¬ 𝜒 → ¬ 𝜃)) → 𝜒) → (𝜃 → 𝜑))
7	6	a1d 25	. 2 ⊢ (¬ (((𝜑 → 𝜓) → (¬ 𝜒 → ¬ 𝜃)) → 𝜒) → ((𝜏 → 𝜑) → (𝜃 → 𝜑)))
8		ax-1 6	. . 3 ⊢ (𝜏 → (𝜃 → 𝜏))
9	8	imim1d 82	. 2 ⊢ (𝜏 → ((𝜏 → 𝜑) → (𝜃 → 𝜑)))
10	7, 9	ja 186	1 ⊢ (((((𝜑 → 𝜓) → (¬ 𝜒 → ¬ 𝜃)) → 𝜒) → 𝜏) → ((𝜏 → 𝜑) → (𝜃 → 𝜑)))

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  1636  merlem2  1637  merlem3  1638  merlem4  1639  merlem5  1640  merlem7  1642  merlem8  1643  merlem9  1644  merlem10  1645  merlem11  1646  merlem13  1648  luk-1  1649  luk-2  1650  merco1  1707