Theorem luk-2
2 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 (\neg \varphi \rightarrow \varphi) \rightarrow \varphi \)
Proof
l0
merlem5
\( \vdash (\varphi \rightarrow \neg (\neg \varphi \rightarrow \varphi)) \rightarrow \neg \neg \varphi \rightarrow \neg (\neg \varphi \rightarrow \varphi) \)
merlem4
\( \vdash ((\varphi \rightarrow \neg (\neg \varphi \rightarrow \varphi)) \rightarrow \neg \neg \varphi \rightarrow \neg (\neg \varphi \rightarrow \varphi)) \rightarrow (((\varphi \rightarrow \neg (\neg \varphi \rightarrow \varphi)) \rightarrow \neg \neg \varphi \rightarrow \neg (\neg \varphi \rightarrow \varphi)) \rightarrow \neg \varphi) \rightarrow (((\varphi \rightarrow \neg (\neg \varphi \rightarrow \varphi)) \rightarrow \neg \neg \varphi \rightarrow \neg (\neg \varphi \rightarrow \varphi)) \rightarrow \neg \varphi) \rightarrow \neg \varphi \)
l2
ax-mp l0 _
\( \vdash (((\varphi \rightarrow \neg (\neg \varphi \rightarrow \varphi)) \rightarrow \neg \neg \varphi \rightarrow \neg (\neg \varphi \rightarrow \varphi)) \rightarrow \neg \varphi) \rightarrow (((\varphi \rightarrow \neg (\neg \varphi \rightarrow \varphi)) \rightarrow \neg \neg \varphi \rightarrow \neg (\neg \varphi \rightarrow \varphi)) \rightarrow \neg \varphi) \rightarrow \neg \varphi \)
merlem11
\( \vdash ((((\varphi \rightarrow \neg (\neg \varphi \rightarrow \varphi)) \rightarrow \neg \neg \varphi \rightarrow \neg (\neg \varphi \rightarrow \varphi)) \rightarrow \neg \varphi) \rightarrow (((\varphi \rightarrow \neg (\neg \varphi \rightarrow \varphi)) \rightarrow \neg \neg \varphi \rightarrow \neg (\neg \varphi \rightarrow \varphi)) \rightarrow \neg \varphi) \rightarrow \neg \varphi) \rightarrow (((\varphi \rightarrow \neg (\neg \varphi \rightarrow \varphi)) \rightarrow \neg \neg \varphi \rightarrow \neg (\neg \varphi \rightarrow \varphi)) \rightarrow \neg \varphi) \rightarrow \neg \varphi \)
l4
ax-mp l2 _
\( \vdash (((\varphi \rightarrow \neg (\neg \varphi \rightarrow \varphi)) \rightarrow \neg \neg \varphi \rightarrow \neg (\neg \varphi \rightarrow \varphi)) \rightarrow \neg \varphi) \rightarrow \neg \varphi \)
meredith
\( \vdash ((((\varphi \rightarrow \neg (\neg \varphi \rightarrow \varphi)) \rightarrow \neg \neg \varphi \rightarrow \neg (\neg \varphi \rightarrow \varphi)) \rightarrow \neg \varphi) \rightarrow \neg \varphi) \rightarrow (\neg \varphi \rightarrow \varphi) \rightarrow (\neg \varphi \rightarrow \varphi) \rightarrow \varphi \)
l6
ax-mp l4 _
\( \vdash (\neg \varphi \rightarrow \varphi) \rightarrow (\neg \varphi \rightarrow \varphi) \rightarrow \varphi \)
merlem11
\( \vdash ((\neg \varphi \rightarrow \varphi) \rightarrow (\neg \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\neg \varphi \rightarrow \varphi) \rightarrow \varphi \)
ax-mp l6 _