Theorem meredith 1674

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 1688, luk-2 1689, and luk-3 1690. Using these we finally rederive our axioms as ax1 1699, ax2 1700, and ax3 1701, 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 124	. . . . . . 7 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
2		con4 114	. . . . . . 7 ⊢ ((¬ 𝜒 → ¬ 𝜃) → (𝜃 → 𝜒))
3	1, 2	imim12i 63	. . . . . 6 ⊢ (((𝜑 → 𝜓) → (¬ 𝜒 → ¬ 𝜃)) → (¬ 𝜑 → (𝜃 → 𝜒)))
4	3	com13 89	. . . . 5 ⊢ (𝜃 → (¬ 𝜑 → (((𝜑 → 𝜓) → (¬ 𝜒 → ¬ 𝜃)) → 𝜒)))
5	4	con1d 146	. . . 4 ⊢ (𝜃 → (¬ (((𝜑 → 𝜓) → (¬ 𝜒 → ¬ 𝜃)) → 𝜒) → 𝜑))
6	5	com12 33	. . 3 ⊢ (¬ (((𝜑 → 𝜓) → (¬ 𝜒 → ¬ 𝜃)) → 𝜒) → (𝜃 → 𝜑))
7	6	a1d 26	. 2 ⊢ (¬ (((𝜑 → 𝜓) → (¬ 𝜒 → ¬ 𝜃)) → 𝜒) → ((𝜏 → 𝜑) → (𝜃 → 𝜑)))
8		ax-1 6	. . 3 ⊢ (𝜏 → (𝜃 → 𝜏))
9	8	imim1d 83	. 2 ⊢ (𝜏 → ((𝜏 → 𝜑) → (𝜃 → 𝜑)))
10	7, 9	ja 188	1 ⊢ (((((𝜑 → 𝜓) → (¬ 𝜒 → ¬ 𝜃)) → 𝜒) → 𝜏) → ((𝜏 → 𝜑) → (𝜃 → 𝜑)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  merlem1  1675  merlem2  1676  merlem3  1677  merlem4  1678  merlem5  1679  merlem7  1681  merlem8  1682  merlem9  1683  merlem10  1684  merlem11  1685  merlem13  1687  luk-1  1688  luk-2  1689  merco1  1746