Theorem luklem4
Used to rederive standard propositional axioms from Lukasiewicz'.
(Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.)
(New usage is discouraged.)
Conclusion
\( \vdash (((\neg \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi) \rightarrow \psi \)
Proof
l0
luk-2
\( \vdash (\neg ((\neg \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\neg \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\neg \varphi \rightarrow \varphi) \rightarrow \varphi \)
l1
luk-2
\( \vdash (\neg \varphi \rightarrow \varphi) \rightarrow \varphi \)
luklem3
\( \vdash ((\neg \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow ((\neg ((\neg \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\neg \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\neg \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \neg \psi \rightarrow (\neg \varphi \rightarrow \varphi) \rightarrow \varphi \)
ax-mp l1 _
\( \vdash ((\neg ((\neg \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\neg \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\neg \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \neg \psi \rightarrow (\neg \varphi \rightarrow \varphi) \rightarrow \varphi \)
l4
ax-mp l0 _
\( \vdash \neg \psi \rightarrow (\neg \varphi \rightarrow \varphi) \rightarrow \varphi \)
luk-1
\( \vdash (\neg \psi \rightarrow (\neg \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow (((\neg \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi) \rightarrow \neg \psi \rightarrow \psi \)
l6
ax-mp l4 _
\( \vdash (((\neg \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow \psi) \rightarrow \neg \psi \rightarrow \psi \)
luk-2
\( \vdash (\neg \psi \rightarrow \psi) \rightarrow \psi \)
luklem1 l6 _