Theorem tbwlem4
Used to rederive the Lukasiewicz axioms from Tarski-Bernays-Wajsberg'.
(Contributed by Anthony Hart, 16-Aug-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
Conclusion
\( \vdash ((\varphi \rightarrow \bot) \rightarrow \psi) \rightarrow (\psi \rightarrow \bot) \rightarrow \varphi \)
Proof
l0
tbw-ax4
\( \vdash \bot \rightarrow \bot \)
l1
tbw-ax1
\( \vdash (\psi \rightarrow \bot) \rightarrow (\bot \rightarrow \bot) \rightarrow \psi \rightarrow \bot \)
tbwlem1
\( \vdash ((\psi \rightarrow \bot) \rightarrow (\bot \rightarrow \bot) \rightarrow \psi \rightarrow \bot) \rightarrow (\bot \rightarrow \bot) \rightarrow (\psi \rightarrow \bot) \rightarrow \psi \rightarrow \bot \)
ax-mp l1 _
\( \vdash (\bot \rightarrow \bot) \rightarrow (\psi \rightarrow \bot) \rightarrow \psi \rightarrow \bot \)
l4
ax-mp l0 _
\( \vdash (\psi \rightarrow \bot) \rightarrow \psi \rightarrow \bot \)
tbwlem1
\( \vdash ((\psi \rightarrow \bot) \rightarrow \psi \rightarrow \bot) \rightarrow \psi \rightarrow (\psi \rightarrow \bot) \rightarrow \bot \)
l6
ax-mp l4 _
\( \vdash \psi \rightarrow (\psi \rightarrow \bot) \rightarrow \bot \)
l7
tbw-ax1
\( \vdash ((\varphi \rightarrow \bot) \rightarrow \psi) \rightarrow (\psi \rightarrow (\psi \rightarrow \bot) \rightarrow \bot) \rightarrow (\varphi \rightarrow \bot) \rightarrow (\psi \rightarrow \bot) \rightarrow \bot \)
tbwlem1
\( \vdash (((\varphi \rightarrow \bot) \rightarrow \psi) \rightarrow (\psi \rightarrow (\psi \rightarrow \bot) \rightarrow \bot) \rightarrow (\varphi \rightarrow \bot) \rightarrow (\psi \rightarrow \bot) \rightarrow \bot) \rightarrow (\psi \rightarrow (\psi \rightarrow \bot) \rightarrow \bot) \rightarrow ((\varphi \rightarrow \bot) \rightarrow \psi) \rightarrow (\varphi \rightarrow \bot) \rightarrow (\psi \rightarrow \bot) \rightarrow \bot \)
ax-mp l7 _
\( \vdash (\psi \rightarrow (\psi \rightarrow \bot) \rightarrow \bot) \rightarrow ((\varphi \rightarrow \bot) \rightarrow \psi) \rightarrow (\varphi \rightarrow \bot) \rightarrow (\psi \rightarrow \bot) \rightarrow \bot \)
l10
ax-mp l6 _
\( \vdash ((\varphi \rightarrow \bot) \rightarrow \psi) \rightarrow (\varphi \rightarrow \bot) \rightarrow (\psi \rightarrow \bot) \rightarrow \bot \)
l11
tbwlem2
\( \vdash ((\varphi \rightarrow \bot) \rightarrow (\psi \rightarrow \bot) \rightarrow \bot) \rightarrow (((\varphi \rightarrow \bot) \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\psi \rightarrow \bot) \rightarrow \varphi \)
tbwlem3
\( \vdash ((((\varphi \rightarrow \bot) \rightarrow \varphi) \rightarrow \varphi) \rightarrow (\psi \rightarrow \bot) \rightarrow \varphi) \rightarrow (\psi \rightarrow \bot) \rightarrow \varphi \)
tbwsyl l11 _
\( \vdash ((\varphi \rightarrow \bot) \rightarrow (\psi \rightarrow \bot) \rightarrow \bot) \rightarrow (\psi \rightarrow \bot) \rightarrow \varphi \)
tbwsyl l10 _