ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  meredith Unicode version

Theorem meredith 1250
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 8, where negation and implication are primitive. Here we prove Meredith's axiom from ax-1 5, ax-2 6, and ax-3 7. Then from it we derive the Lukasiewicz axioms luk-1 1265, luk-2 1266, and luk-3 1267. Using these we finally re-derive our axioms as ax1 1276, ax2 1277, and ax3 1278, 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.) (The proof was shortened by Wolf Lammen, 28-May-2013.)

Assertion
Ref Expression
meredith

Proof of Theorem meredith
StepHypRef Expression
1 pm2.21 530 . . . . . . 7
2 ax-3 7 . . . . . . 7
31, 2imim12i 52 . . . . . 6
43com13 73 . . . . 5
54con1d 720 . . . 4
65com12 26 . . 3
76a1d 21 . 2
8 ax-1 5 . . 3
98imim1d 68 . 2
107, 9ja 738 1
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-in1 527  ax-in2 528
  Copyright terms: Public domain W3C validator