Theorem meredith 922

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 7, where negation and implication are primitive. Here we prove Meredith's axiom from ax-1 4, ax-2 5, and ax-3 6. Then from it we derive the Lukasiewicz axioms luk-1 936, luk-2 937, and luk-3 938. Using these we finally re-derive our axioms as ax1 947, ax2 948, and ax3 949, 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 6	. . . . 5 ⊢ ((¬ χ → ¬ (¬ χ → (¬ φ → ¬ θ))) → ((¬ χ → (¬ φ → ¬ θ)) → χ))
2		pm2.21 76	. . . . . . 7 ⊢ (¬ φ → (φ → ψ))
3	2	imim1i 16	. . . . . 6 ⊢ (((φ → ψ) → (¬ χ → ¬ θ)) → (¬ φ → (¬ χ → ¬ θ)))
4	3	com23 32	. . . . 5 ⊢ (((φ → ψ) → (¬ χ → ¬ θ)) → (¬ χ → (¬ φ → ¬ θ)))
5	1, 4	syl5 21	. . . 4 ⊢ ((¬ χ → ¬ (¬ χ → (¬ φ → ¬ θ))) → (((φ → ψ) → (¬ χ → ¬ θ)) → χ))
6	5	imim1i 16	. . 3 ⊢ (((((φ → ψ) → (¬ χ → ¬ θ)) → χ) → τ) → ((¬ χ → ¬ (¬ χ → (¬ φ → ¬ θ))) → τ))
7	6	con3d 95	. 2 ⊢ (((((φ → ψ) → (¬ χ → ¬ θ)) → χ) → τ) → (¬ τ → ¬ (¬ χ → ¬ (¬ χ → (¬ φ → ¬ θ)))))
8		pm2.27 62	. . . . . . . . 9 ⊢ (¬ χ → ((¬ χ → (¬ φ → ¬ θ)) → (¬ φ → ¬ θ)))
9	8	impi 143	. . . . . . . 8 ⊢ (¬ (¬ χ → ¬ (¬ χ → (¬ φ → ¬ θ))) → (¬ φ → ¬ θ))
10	9	com12 11	. . . . . . 7 ⊢ (¬ φ → (¬ (¬ χ → ¬ (¬ χ → (¬ φ → ¬ θ))) → ¬ θ))
11	10	imim2d 25	. . . . . 6 ⊢ (¬ φ → ((¬ τ → ¬ (¬ χ → ¬ (¬ χ → (¬ φ → ¬ θ)))) → (¬ τ → ¬ θ)))
12	11	com12 11	. . . . 5 ⊢ ((¬ τ → ¬ (¬ χ → ¬ (¬ χ → (¬ φ → ¬ θ)))) → (¬ φ → (¬ τ → ¬ θ)))
13	12	a2d 13	. . . 4 ⊢ ((¬ τ → ¬ (¬ χ → ¬ (¬ χ → (¬ φ → ¬ θ)))) → ((¬ φ → ¬ τ) → (¬ φ → ¬ θ)))
14		con3 94	. . . 4 ⊢ ((τ → φ) → (¬ φ → ¬ τ))
15	13, 14	syl5 21	. . 3 ⊢ ((¬ τ → ¬ (¬ χ → ¬ (¬ χ → (¬ φ → ¬ θ)))) → ((τ → φ) → (¬ φ → ¬ θ)))
16		ax-3 6	. . 3 ⊢ ((¬ φ → ¬ θ) → (θ → φ))
17	15, 16	syl6 22	. 2 ⊢ ((¬ τ → ¬ (¬ χ → ¬ (¬ χ → (¬ φ → ¬ θ)))) → ((τ → φ) → (θ → φ)))
18	7, 17	syl 10	1 ⊢ (((((φ → ψ) → (¬ χ → ¬ θ)) → χ) → τ) → ((τ → φ) → (θ → φ)))

Syntax hints:  ¬ wn 2   → wi 3

This theorem is referenced by:  merlem1 923  merlem2 924  merlem3 925  merlem4 926  merlem5 927  merlem7 929  merlem8 930  merlem9 931  merlem10 932  merlem11 933  merlem13 935  luk-1 936  luk-2 937

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

Copyright terms: Public domain