Theorem meredith 644

Description: Carew Meredith's sole axiom for propositional calculus. This amazing formula is thought to be the shortest possible single axiom for propositional calculus using negation, implication, and inference rule ax-mp 6. Here we prove Meredith's axiom from ax-1 3, ax-2 4, and ax-3 5. Then from it we derive the Lukasiewicz axioms luk-1 658, luk-2 659, and luk-3 660. Using these we finally re-derive our axioms as ax1 669, ax2 670, and ax3 671, 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. 3 (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."

Assertion

Ref	Expression
meredith	⊢ (((((φ → ψ) → (¬ χ → ¬ θ)) → χ) → τ) → ((τ → φ) → (θ → φ)))

Proof of Theorem meredith

Step	Hyp	Ref	Expression
1		ax-3 5	. . . . 5 ⊢ ((¬ χ → ¬ (¬ χ → (¬ φ → ¬ θ))) → ((¬ χ → (¬ φ → ¬ θ)) → χ))
2		pm2.21 71	. . . . . . 7 ⊢ (¬ φ → (φ → ψ))
3	2	syl4 19	. . . . . 6 ⊢ (((φ → ψ) → (¬ χ → ¬ θ)) → (¬ φ → (¬ χ → ¬ θ)))
4	3	com23 32	. . . . 5 ⊢ (((φ → ψ) → (¬ χ → ¬ θ)) → (¬ χ → (¬ φ → ¬ θ)))
5	1, 4	syl5 22	. . . 4 ⊢ ((¬ χ → ¬ (¬ χ → (¬ φ → ¬ θ))) → (((φ → ψ) → (¬ χ → ¬ θ)) → χ))
6	5	syl4 19	. . 3 ⊢ (((((φ → ψ) → (¬ χ → ¬ θ)) → χ) → τ) → ((¬ χ → ¬ (¬ χ → (¬ φ → ¬ θ))) → τ))
7	6	con3d 87	. 2 ⊢ (((((φ → ψ) → (¬ χ → ¬ θ)) → χ) → τ) → (¬ τ → ¬ (¬ χ → ¬ (¬ χ → (¬ φ → ¬ θ)))))
8		pm2.27 30	. . . . . . . . 9 ⊢ (¬ χ → ((¬ χ → (¬ φ → ¬ θ)) → (¬ φ → ¬ θ)))
9	8	impi 124	. . . . . . . 8 ⊢ (¬ (¬ χ → ¬ (¬ χ → (¬ φ → ¬ θ))) → (¬ φ → ¬ θ))
10	9	com12 13	. . . . . . 7 ⊢ (¬ φ → (¬ (¬ χ → ¬ (¬ χ → (¬ φ → ¬ θ))) → ¬ θ))
11	10	syl3d 26	. . . . . 6 ⊢ (¬ φ → ((¬ τ → ¬ (¬ χ → ¬ (¬ χ → (¬ φ → ¬ θ)))) → (¬ τ → ¬ θ)))
12	11	com12 13	. . . . 5 ⊢ ((¬ τ → ¬ (¬ χ → ¬ (¬ χ → (¬ φ → ¬ θ)))) → (¬ φ → (¬ τ → ¬ θ)))
13	12	a2d 15	. . . 4 ⊢ ((¬ τ → ¬ (¬ χ → ¬ (¬ χ → (¬ φ → ¬ θ)))) → ((¬ φ → ¬ τ) → (¬ φ → ¬ θ)))
14		con3 86	. . . 4 ⊢ ((τ → φ) → (¬ φ → ¬ τ))
15	13, 14	syl5 22	. . 3 ⊢ ((¬ τ → ¬ (¬ χ → ¬ (¬ χ → (¬ φ → ¬ θ)))) → ((τ → φ) → (¬ φ → ¬ θ)))
16		ax-3 5	. . 3 ⊢ ((¬ φ → ¬ θ) → (θ → φ))
17	15, 16	syl6 23	. 2 ⊢ ((¬ τ → ¬ (¬ χ → ¬ (¬ χ → (¬ φ → ¬ θ)))) → ((τ → φ) → (θ → φ)))
18	7, 17	syl 12	1 ⊢ (((((φ → ψ) → (¬ χ → ¬ θ)) → χ) → τ) → ((τ → φ) → (θ → φ)))

Syntax hints:  ¬ wn 1   → wi 2

This theorem is referenced by:  merlem1 645  merlem2 646  merlem3 647  merlem4 648  merlem5 649  merlem7 651  merlem8 652  merlem9 653  merlem10 654  merlem11 655  merlem13 657  luk-1 658  luk-2 659

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

metamath.org