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 , 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 rederive 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." (Contributed by NM, 14-Dec-2002) (Proof shortened by Andrew Salmon, 25-Jul-2011) (Proof shortened by Wolf Lammen, 28-May-2013)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | meredith | |- ( ( ( ( ( ph -> ps ) -> ( -. ch -> -. th ) ) -> ch ) -> ta ) -> ( ( ta -> ph ) -> ( th -> ph ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pm2.21 | |- ( -. ph -> ( ph -> ps ) ) |
|
| 2 | con4 | |- ( ( -. ch -> -. th ) -> ( th -> ch ) ) |
|
| 3 | 1 2 | imim12i | |- ( ( ( ph -> ps ) -> ( -. ch -> -. th ) ) -> ( -. ph -> ( th -> ch ) ) ) |
| 4 | 3 | com13 | |- ( th -> ( -. ph -> ( ( ( ph -> ps ) -> ( -. ch -> -. th ) ) -> ch ) ) ) |
| 5 | 4 | con1d | |- ( th -> ( -. ( ( ( ph -> ps ) -> ( -. ch -> -. th ) ) -> ch ) -> ph ) ) |
| 6 | 5 | com12 | |- ( -. ( ( ( ph -> ps ) -> ( -. ch -> -. th ) ) -> ch ) -> ( th -> ph ) ) |
| 7 | 6 | a1d | |- ( -. ( ( ( ph -> ps ) -> ( -. ch -> -. th ) ) -> ch ) -> ( ( ta -> ph ) -> ( th -> ph ) ) ) |
| 8 | ax-1 | |- ( ta -> ( th -> ta ) ) |
|
| 9 | 8 | imim1d | |- ( ta -> ( ( ta -> ph ) -> ( th -> ph ) ) ) |
| 10 | 7 9 | ja | |- ( ( ( ( ( ph -> ps ) -> ( -. ch -> -. th ) ) -> ch ) -> ta ) -> ( ( ta -> ph ) -> ( th -> ph ) ) ) |