meredith

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	$⊢ ((((φ \to ψ) \to (\neg χ \to \neg θ)) \to χ) \to τ) \to ((τ \to φ) \to (θ \to φ))$

Proof

Step	Hyp	Ref	Expression
1		pm2.21	$⊢ \neg φ \to (φ \to ψ)$
2		con4	$⊢ (\neg χ \to \neg θ) \to (θ \to χ)$
3	1 2	imim12i	$⊢ ((φ \to ψ) \to (\neg χ \to \neg θ)) \to (\neg φ \to (θ \to χ))$
4	3	com13	$⊢ θ \to (\neg φ \to (((φ \to ψ) \to (\neg χ \to \neg θ)) \to χ))$
5	4	con1d	$⊢ θ \to (\neg (((φ \to ψ) \to (\neg χ \to \neg θ)) \to χ) \to φ)$
6	5	com12	$⊢ \neg (((φ \to ψ) \to (\neg χ \to \neg θ)) \to χ) \to (θ \to φ)$
7	6	a1d	$⊢ \neg (((φ \to ψ) \to (\neg χ \to \neg θ)) \to χ) \to ((τ \to φ) \to (θ \to φ))$
8		ax-1	$⊢ τ \to (θ \to τ)$
9	8	imim1d	$⊢ τ \to ((τ \to φ) \to (θ \to φ))$
10	7 9	ja	$⊢ ((((φ \to ψ) \to (\neg χ \to \neg θ)) \to χ) \to τ) \to ((τ \to φ) \to (θ \to φ))$

Metamath Proof Explorer

Theorem meredith

Proof