Theorem rblem4
Used to rederive the Lukasiewicz axioms from Russell-Bernays'.
(Contributed by Anthony Hart, 18-Aug-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
rblem4.1
\( \vdash \neg \varphi \vee \theta \)
rblem4.2
\( \vdash \neg \psi \vee \tau \)
rblem4.3
\( \vdash \neg \chi \vee \eta \)
Conclusion
\( \vdash \neg (\varphi \vee \psi \vee \chi) \vee (\eta \vee \tau \vee \theta) \)
Proof
l0
rblem4.3
rblem4.2
l2
rblem1 l0 _
rblem4.1
l4
rblem1 l2 _
\( \vdash \neg (\chi \vee \psi \vee \varphi) \vee (\eta \vee \tau \vee \theta) \)
l5
rb-ax2
\( \vdash \neg (\varphi \vee (\chi \vee \psi)) \vee (\chi \vee \psi \vee \varphi) \)
l6
rb-ax2
\( \vdash \neg (\psi \vee \chi) \vee (\chi \vee \psi) \)
rb-ax1
\( \vdash \neg (\neg (\psi \vee \chi) \vee (\chi \vee \psi)) \vee (\neg (\varphi \vee (\psi \vee \chi)) \vee (\varphi \vee (\chi \vee \psi))) \)
l8
anmp l6 _
\( \vdash \neg (\varphi \vee (\psi \vee \chi)) \vee (\varphi \vee (\chi \vee \psi)) \)
rb-ax2
\( \vdash \neg (\psi \vee \chi \vee \varphi) \vee (\varphi \vee (\psi \vee \chi)) \)
rbsyl l8 _
\( \vdash \neg (\psi \vee \chi \vee \varphi) \vee (\varphi \vee (\chi \vee \psi)) \)
l11
rbsyl l5 _
\( \vdash \neg (\psi \vee \chi \vee \varphi) \vee (\chi \vee \psi \vee \varphi) \)
l12
rb-ax4
\( \vdash \neg (\psi \vee \chi \vee \varphi \vee (\psi \vee \chi \vee \varphi)) \vee (\psi \vee \chi \vee \varphi) \)
l13
rb-ax2
\( \vdash \neg (\varphi \vee (\psi \vee \chi)) \vee (\psi \vee \chi \vee \varphi) \)
rblem2
\( \vdash \neg (\varphi \vee \psi) \vee (\varphi \vee (\psi \vee \chi)) \)
l15
rbsyl l13 _
l16
rb-ax3
\( \vdash \neg \chi \vee (\psi \vee \chi) \)
rblem2
\( \vdash \neg (\neg \chi \vee (\psi \vee \chi)) \vee (\neg \chi \vee (\psi \vee \chi \vee \varphi)) \)
anmp l16 _
rblem1 l15 _
\( \vdash \neg (\varphi \vee \psi \vee \chi) \vee (\psi \vee \chi \vee \varphi \vee (\psi \vee \chi \vee \varphi)) \)
rbsyl l12 _
\( \vdash \neg (\varphi \vee \psi \vee \chi) \vee (\psi \vee \chi \vee \varphi) \)
rbsyl l11 _
\( \vdash \neg (\varphi \vee \psi \vee \chi) \vee (\chi \vee \psi \vee \varphi) \)
rbsyl l4 _