Theorem luk-1
1 of 3 axioms for propositional calculus due to Lukasiewicz, derived from
Meredith's sole axiom. (Contributed by NM, 14-Dec-2002.)
(Proof modification is discouraged.) (New usage is discouraged.)
Conclusion
\( \vdash (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
Proof
l0
meredith
\( \vdash ((((\chi \rightarrow \chi) \rightarrow \neg \neg \neg \varphi \rightarrow \neg \varphi) \rightarrow \neg \neg \varphi) \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
l1
merlem13
\( \vdash (\varphi \rightarrow \psi) \rightarrow (((\chi \rightarrow \chi) \rightarrow \neg \neg \neg \varphi \rightarrow \neg \varphi) \rightarrow \neg \neg \varphi) \rightarrow \psi \)
merlem13
\( \vdash ((\varphi \rightarrow \psi) \rightarrow (((\chi \rightarrow \chi) \rightarrow \neg \neg \neg \varphi \rightarrow \neg \varphi) \rightarrow \neg \neg \varphi) \rightarrow \psi) \rightarrow (((((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi) \rightarrow \neg \neg \neg (\varphi \rightarrow \psi) \rightarrow \neg (\varphi \rightarrow \psi)) \rightarrow \neg \neg (\varphi \rightarrow \psi)) \rightarrow (((\chi \rightarrow \chi) \rightarrow \neg \neg \neg \varphi \rightarrow \neg \varphi) \rightarrow \neg \neg \varphi) \rightarrow \psi \)
l3
ax-mp l1 _
\( \vdash (((((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi) \rightarrow \neg \neg \neg (\varphi \rightarrow \psi) \rightarrow \neg (\varphi \rightarrow \psi)) \rightarrow \neg \neg (\varphi \rightarrow \psi)) \rightarrow (((\chi \rightarrow \chi) \rightarrow \neg \neg \neg \varphi \rightarrow \neg \varphi) \rightarrow \neg \neg \varphi) \rightarrow \psi \)
meredith
\( \vdash ((((((\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow \varphi) \rightarrow \neg \neg \neg (\varphi \rightarrow \psi) \rightarrow \neg (\varphi \rightarrow \psi)) \rightarrow \neg \neg (\varphi \rightarrow \psi)) \rightarrow (((\chi \rightarrow \chi) \rightarrow \neg \neg \neg \varphi \rightarrow \neg \varphi) \rightarrow \neg \neg \varphi) \rightarrow \psi) \rightarrow (((((\chi \rightarrow \chi) \rightarrow \neg \neg \neg \varphi \rightarrow \neg \varphi) \rightarrow \neg \neg \varphi) \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l3 _
\( \vdash (((((\chi \rightarrow \chi) \rightarrow \neg \neg \neg \varphi \rightarrow \neg \varphi) \rightarrow \neg \neg \varphi) \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi) \rightarrow (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \chi \)
ax-mp l0 _