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 | ⊢ ( ( ( ( ( 𝜑 → 𝜓 ) → ( ¬ 𝜒 → ¬ 𝜃 ) ) → 𝜒 ) → 𝜏 ) → ( ( 𝜏 → 𝜑 ) → ( 𝜃 → 𝜑 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pm2.21 | ⊢ ( ¬ 𝜑 → ( 𝜑 → 𝜓 ) ) | |
| 2 | con4 | ⊢ ( ( ¬ 𝜒 → ¬ 𝜃 ) → ( 𝜃 → 𝜒 ) ) | |
| 3 | 1 2 | imim12i | ⊢ ( ( ( 𝜑 → 𝜓 ) → ( ¬ 𝜒 → ¬ 𝜃 ) ) → ( ¬ 𝜑 → ( 𝜃 → 𝜒 ) ) ) |
| 4 | 3 | com13 | ⊢ ( 𝜃 → ( ¬ 𝜑 → ( ( ( 𝜑 → 𝜓 ) → ( ¬ 𝜒 → ¬ 𝜃 ) ) → 𝜒 ) ) ) |
| 5 | 4 | con1d | ⊢ ( 𝜃 → ( ¬ ( ( ( 𝜑 → 𝜓 ) → ( ¬ 𝜒 → ¬ 𝜃 ) ) → 𝜒 ) → 𝜑 ) ) |
| 6 | 5 | com12 | ⊢ ( ¬ ( ( ( 𝜑 → 𝜓 ) → ( ¬ 𝜒 → ¬ 𝜃 ) ) → 𝜒 ) → ( 𝜃 → 𝜑 ) ) |
| 7 | 6 | a1d | ⊢ ( ¬ ( ( ( 𝜑 → 𝜓 ) → ( ¬ 𝜒 → ¬ 𝜃 ) ) → 𝜒 ) → ( ( 𝜏 → 𝜑 ) → ( 𝜃 → 𝜑 ) ) ) |
| 8 | ax-1 | ⊢ ( 𝜏 → ( 𝜃 → 𝜏 ) ) | |
| 9 | 8 | imim1d | ⊢ ( 𝜏 → ( ( 𝜏 → 𝜑 ) → ( 𝜃 → 𝜑 ) ) ) |
| 10 | 7 9 | ja | ⊢ ( ( ( ( ( 𝜑 → 𝜓 ) → ( ¬ 𝜒 → ¬ 𝜃 ) ) → 𝜒 ) → 𝜏 ) → ( ( 𝜏 → 𝜑 ) → ( 𝜃 → 𝜑 ) ) ) |