Theorem meredith 1200

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 1215, luk-2 1216, and luk-3 1217. Using these we finally re-derive our axioms as ax1 1226, ax2 1227, and ax3 1228, 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." (The proof was shortened by Andrew Salmon, 25-Jul-2011.)

Assertion

Ref	Expression
meredith	|- (((((ph -> ps) -> (-. ch -> -. th)) -> ch) -> ta) -> ((ta -> ph) -> (th -> ph)))

Proof of Theorem meredith

Step	Hyp	Ref	Expression
1		annim 257	. . . 4 |- ((((ph -> ps) -> (-. ch -> -. th)) /\ -. ch) <-> -. (((ph -> ps) -> (-. ch -> -. th)) -> ch))
2		pm2.21 92	. . . . . . . . 9 |- (-. ph -> (ph -> ps))
3	2	con1i 112	. . . . . . . 8 |- (-. (ph -> ps) -> ph)
4	3	a1d 15	. . . . . . 7 |- (-. (ph -> ps) -> (th -> ph))
5	4	a1d 15	. . . . . 6 |- (-. (ph -> ps) -> (-. ch -> (th -> ph)))
6		pm2.21 92	. . . . . . 7 |- (-. th -> (th -> ph))
7	6	imim2i 11	. . . . . 6 |- ((-. ch -> -. th) -> (-. ch -> (th -> ph)))
8	5, 7	ja 152	. . . . 5 |- (((ph -> ps) -> (-. ch -> -. th)) -> (-. ch -> (th -> ph)))
9	8	imp 377	. . . 4 |- ((((ph -> ps) -> (-. ch -> -. th)) /\ -. ch) -> (th -> ph))
10	1, 9	sylbir 218	. . 3 |- (-. (((ph -> ps) -> (-. ch -> -. th)) -> ch) -> (th -> ph))
11	10	a1d 15	. 2 |- (-. (((ph -> ps) -> (-. ch -> -. th)) -> ch) -> ((ta -> ph) -> (th -> ph)))
12		pm2.27 76	. . 3 |- (ta -> ((ta -> ph) -> ph))
13	12	a1dd 53	. 2 |- (ta -> ((ta -> ph) -> (th -> ph)))
14	11, 13	ja 152	1 |- (((((ph -> ps) -> (-. ch -> -. th)) -> ch) -> ta) -> ((ta -> ph) -> (th -> ph)))

Syntax hints:  -. wn 2   -> wi 3   /\ wa 240

This theorem is referenced by:  merlem1 1202  merlem2 1203  merlem3 1204  merlem4 1205  merlem5 1206  merlem7 1208  merlem8 1209  merlem9 1210  merlem10 1211  merlem11 1212  merlem13 1214  luk-1 1215  luk-2 1216  merco1 14180

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

This theorem depends on definitions:  df-bi 164  df-an 242

Copyright terms: Public domain