Theorem rblem6
Used to rederive the Lukasiewicz axioms from Russell-Bernays'.
(Contributed by Anthony Hart, 19-Aug-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
Hypothesis
rblem6.1
\( \vdash \neg (\neg (\neg \varphi \vee \psi) \vee \neg (\neg \psi \vee \varphi)) \)
Conclusion
\( \vdash \neg \varphi \vee \psi \)
Proof
l0
rblem6.1
\( \vdash \neg (\neg (\neg \varphi \vee \psi) \vee \neg (\neg \psi \vee \varphi)) \)
l1
rb-ax4
\( \vdash \neg (\neg (\neg \varphi \vee \psi) \vee \neg (\neg \varphi \vee \psi)) \vee \neg (\neg \varphi \vee \psi) \)
rb-ax3
\( \vdash \neg \neg (\neg \varphi \vee \psi) \vee (\neg (\neg \varphi \vee \psi) \vee \neg (\neg \varphi \vee \psi)) \)
l3
rbsyl l1 _
\( \vdash \neg \neg (\neg \varphi \vee \psi) \vee \neg (\neg \varphi \vee \psi) \)
rb-ax2
\( \vdash \neg (\neg \neg (\neg \varphi \vee \psi) \vee \neg (\neg \varphi \vee \psi)) \vee (\neg (\neg \varphi \vee \psi) \vee \neg \neg (\neg \varphi \vee \psi)) \)
l5
anmp l3 _
\( \vdash \neg (\neg \varphi \vee \psi) \vee \neg \neg (\neg \varphi \vee \psi) \)
rblem3
\( \vdash \neg (\neg (\neg \varphi \vee \psi) \vee \neg \neg (\neg \varphi \vee \psi)) \vee (\neg (\neg \varphi \vee \psi) \vee \neg (\neg \psi \vee \varphi) \vee \neg \neg (\neg \varphi \vee \psi)) \)
l7
anmp l5 _
\( \vdash \neg (\neg \varphi \vee \psi) \vee \neg (\neg \psi \vee \varphi) \vee \neg \neg (\neg \varphi \vee \psi) \)
rb-ax2
\( \vdash \neg (\neg (\neg \varphi \vee \psi) \vee \neg (\neg \psi \vee \varphi) \vee \neg \neg (\neg \varphi \vee \psi)) \vee (\neg \neg (\neg \varphi \vee \psi) \vee (\neg (\neg \varphi \vee \psi) \vee \neg (\neg \psi \vee \varphi))) \)
l9
anmp l7 _
\( \vdash \neg \neg (\neg \varphi \vee \psi) \vee (\neg (\neg \varphi \vee \psi) \vee \neg (\neg \psi \vee \varphi)) \)
rblem5
\( \vdash \neg (\neg \neg (\neg \varphi \vee \psi) \vee (\neg (\neg \varphi \vee \psi) \vee \neg (\neg \psi \vee \varphi))) \vee (\neg \neg (\neg (\neg \varphi \vee \psi) \vee \neg (\neg \psi \vee \varphi)) \vee (\neg \varphi \vee \psi)) \)
anmp l9 _
\( \vdash \neg \neg (\neg (\neg \varphi \vee \psi) \vee \neg (\neg \psi \vee \varphi)) \vee (\neg \varphi \vee \psi) \)
anmp l0 _