Theorem rblem5
Used to rederive the Lukasiewicz axioms from Russell-Bernays'.
(Contributed by Anthony Hart, 19-Aug-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
Conclusion
\( \vdash \neg (\neg \neg \varphi \vee \psi) \vee (\neg \neg \psi \vee \varphi) \)
Proof
l0
rb-ax2
\( \vdash \neg (\varphi \vee \neg \neg \psi) \vee (\neg \neg \psi \vee \varphi) \)
l1
rb-ax4
\( \vdash \neg (\varphi \vee \varphi) \vee \varphi \)
rb-ax3
\( \vdash \neg \varphi \vee (\varphi \vee \varphi) \)
l3
rbsyl l1 _
\( \vdash \neg \varphi \vee \varphi \)
l4
rb-ax4
\( \vdash \neg (\neg \neg \varphi \vee \neg \neg \varphi) \vee \neg \neg \varphi \)
rb-ax3
\( \vdash \neg \neg \neg \varphi \vee (\neg \neg \varphi \vee \neg \neg \varphi) \)
l6
rbsyl l4 _
\( \vdash \neg \neg \neg \varphi \vee \neg \neg \varphi \)
rb-ax2
\( \vdash \neg (\neg \neg \neg \varphi \vee \neg \neg \varphi) \vee (\neg \neg \varphi \vee \neg \neg \neg \varphi) \)
anmp l6 _
rblem1 _ l3
\( \vdash \neg (\neg \varphi \vee \varphi) \vee (\neg \neg \neg \varphi \vee \varphi) \)
l10
anmp l3 _
l11
rb-ax4
\( \vdash \neg (\neg \psi \vee \neg \psi) \vee \neg \psi \)
rb-ax3
\( \vdash \neg \neg \psi \vee (\neg \psi \vee \neg \psi) \)
l13
rbsyl l11 _
\( \vdash \neg \neg \psi \vee \neg \psi \)
rb-ax2
\( \vdash \neg (\neg \neg \psi \vee \neg \psi) \vee (\neg \psi \vee \neg \neg \psi) \)
anmp l13 _
rblem1 l10 _
\( \vdash \neg (\neg \neg \varphi \vee \psi) \vee (\varphi \vee \neg \neg \psi) \)
rbsyl l0 _