meredith Show Code edit
## Meredith's sole axiom for propositional calculus
##
## 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]], where negation and
## implication are primitive. Here we prove Meredith's axiom from [[ax-1]],
## [[ax-2]], and [[ax-3]]. Then from it we derive the Lukasiewicz axioms
## [[luk-1]], [[luk-2]], and [[luk-3]]. Using these we finally re-derive our
## axioms as [[ax1]], [[ax2]], and [[ax3]], 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."
##
thm (meredith () () (-> (-> (-> (-> (-> ph ps) (-> (-. ch) (-. th))) ch) ta) (-> (-> ta ph) (-> th ph))) ch (-> (-. ch) (-> (-. ph) (-. th))) ax-3 ph ps pm2.21 (-> (-. ch) (-. th)) imim1i com23 syl5 ta imim1i con3d (-. ch) (-> (-. ph) (-. th)) pm2.27 impi com12 (-. ta) imim2d com12 a2d ta ph con3 syl5 ph th ax-3 syl6 syl)
(-> (-> (-> (-> (-> ph ps) (-> (-. ch) (-. th))) ch) ta) (-> (-> ta ph) (-> th ph)))
edit