Theorem dn1
A single axiom for Boolean algebra known as DN1. See McCune, Veroff,
Fitelson, Harris, Feist, Wos, Short single axioms for Boolean algebra,
Journal of Automated Reasoning, 29(1):1--16, 2002.
( https://www.cs.unm.edu/~mccune/papers/basax/v12.pdf ). (Contributed
by Jeff Hankins, 3-Jul-2009.) (Proof shortened by Andrew Salmon,
13-May-2011.) (Proof shortened by Wolf Lammen, 6-Jan-2013.)
Conclusion
\( \vdash \neg (\neg (\neg (\varphi \vee \psi) \vee \chi) \vee \neg (\varphi \vee \neg (\neg \chi \vee \neg (\chi \vee \theta)))) \leftrightarrow \chi \)
Proof
l0
pm2.45
\( \vdash \neg (\varphi \vee \psi) \rightarrow \neg \varphi \)
imnan
\( \vdash \neg (\varphi \vee \psi) \rightarrow \neg \varphi \leftrightarrow \neg (\neg (\varphi \vee \psi) \wedge \varphi) \)
mpbi l0 _
l3
biorfri _
\( \vdash \chi \leftrightarrow \chi \vee \neg (\varphi \vee \psi) \wedge \varphi \)
l4
orcom
\( \vdash \chi \vee \neg (\varphi \vee \psi) \wedge \varphi \leftrightarrow \neg (\varphi \vee \psi) \wedge \varphi \vee \chi \)
ordir
\( \vdash \neg (\varphi \vee \psi) \wedge \varphi \vee \chi \leftrightarrow (\neg (\varphi \vee \psi) \vee \chi) \wedge (\varphi \vee \chi) \)
l6
3bitri l3 l4 _
\( \vdash \chi \leftrightarrow (\neg (\varphi \vee \psi) \vee \chi) \wedge (\varphi \vee \chi) \)
l7
pm4.45
\( \vdash \chi \leftrightarrow \chi \wedge (\chi \vee \theta) \)
anor
\( \vdash \chi \wedge (\chi \vee \theta) \leftrightarrow \neg (\neg \chi \vee \neg (\chi \vee \theta)) \)
bitri l7 _
orbi2i _
l11
anbi2i _
\( \vdash (\neg (\varphi \vee \psi) \vee \chi) \wedge (\varphi \vee \chi) \leftrightarrow (\neg (\varphi \vee \psi) \vee \chi) \wedge (\varphi \vee \neg (\neg \chi \vee \neg (\chi \vee \theta))) \)
anor
\( \vdash (\neg (\varphi \vee \psi) \vee \chi) \wedge (\varphi \vee \neg (\neg \chi \vee \neg (\chi \vee \theta))) \leftrightarrow \neg (\neg (\neg (\varphi \vee \psi) \vee \chi) \vee \neg (\varphi \vee \neg (\neg \chi \vee \neg (\chi \vee \theta)))) \)
3bitrri l6 l11 _