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)))