# Boolean algebra

## Axioms

     sup_commute: ?x $$\sqcup$$ ?y = ?y $$\sqcup$$ ?x
inf_commute: ?x $$\sqcap$$ ?y = ?y $$\sqcap$$ ?x

sup_inf_distrib1: ?x $$\sqcup$$ ?y $$\sqcap$$ ?z = (?x $$\sqcup$$ ?y) $$\sqcap$$ (?x $$\sqcup$$ ?z)
sup_inf_distrib2: ?y $$\sqcap$$ ?z $$\sqcup$$ ?x = (?y $$\sqcup$$ ?x) $$\sqcap$$ (?z $$\sqcup$$ ?x)
inf_sup_distrib1: ?x $$\sqcap$$ (?y $$\sqcup$$ ?z) = ?x $$\sqcap$$ ?y $$\sqcup$$ ?x $$\sqcap$$ ?z
inf_sup_distrib2: (?y $$\sqcup$$ ?z) $$\sqcap$$ ?x = ?y $$\sqcap$$ ?x $$\sqcup$$ ?z $$\sqcap$$ ?x

sup_bot_left: $$\bot$$ $$\sqcup$$ ?x = ?x
sup_bot_right: ?x $$\sqcup$$ $$\bot$$ = ?x
inf_top_left: $$\top$$ $$\sqcap$$ ?x = ?x
inf_top_right: ?x $$\sqcap$$ $$\top$$ = ?x

sup_compl_top: ?x $$\sqcup$$ - ?x = $$\top$$
inf_compl_bot: ?x $$\sqcap$$ - ?x = $$\bot$$

THEOREM

Let $$(S, \vee, \wedge)$$ be a Boolean algebra. Then any theorem in $$(S, \vee, \wedge)$$ remains valid if both $$\vee$$ and $$\wedge$$ are interchanged, and also $$\bot$$ and $$\top$$ are interchanged throughout the whole theorem.

Proof.     ProofWiki
THEOREM    $$- x \sqcap x = \bot$$
Proof 1.     \begin{align} - x \sqcap x &= x \sqcap - x \\ &= \bot \end{align}
Proof 2.
THEOREM    $$- x \sqcup x = \top$$
Proof 1.     \begin{align} - x \sqcup x &= x \sqcup - x \\ &= \top \end{align}
Proof 2.
THEOREM

Top is a right zero of join.

$$x \sqcup \top = \top$$
Proof 1.     ProofWiki
Proof 2.
THEOREM

Bottom is a right zero of meet.

$$x \sqcap \bot = \bot$$
Proof 1.     ProofWiki
Proof 2.
THEOREM

Bottom is the complement of top.

$$- \top = \bot$$
Proof 1.     \begin{align} - \top &= \top \sqcap - \top \\ &= \bot \end{align}
Proof 2.
THEOREM

Top is the complement of bottom.

$$- \bot = \top$$
Proof 1.     \begin{align} - \bot &= \bot \sqcup - \bot \\ &= \top \end{align}
Proof 2.
THEOREM

Join is idempotent.

$$x \sqcup x = x$$
Proof 1.     \begin{align} x &= x \sqcup \bot \\ &= x \sqcup (x \sqcap - x) \\ &= (x \sqcup x) \sqcap (x \sqcup - x) \\ &= (x \sqcup x) \sqcap \top \\ &= x \sqcup x \end{align}
Proof 2.     ProofWiki
Proof 3.
THEOREM

Meet is idempotent.

$$x \sqcap x = x$$
Proof 1.     \begin{align} x &= x \sqcap \top \\ &= x \sqcap (x \sqcup - x) \\ &= (x \sqcap x) \sqcup (x \sqcap - x) \\ &= (x \sqcap x) \sqcup \bot \\ &= x \sqcap x \end{align}
Proof 2.     ProofWiki
Proof 3.
THEOREM

Meet absorbs join.

$$x \sqcap (x \sqcup y)$$
Proof 1.     ProofWiki
Proof 2.     \begin{align} x \sqcap (x \sqcup y) &= (x \sqcup \bot) \sqcap (x \sqcup y) \\ &= x \sqcup \bot \sqcap y \\ &= x \sqcup \bot \\ &= x \end{align}
Proof 3.
THEOREM

Join absorbs meet.

$$x \sqcup (x \sqcap y)$$
Proof 1.     ProofWiki
Proof 2.     \begin{align} x \sqcup (x \sqcap y) &= (x \sqcap \top) \sqcup (x \sqcap y) \\ &= x \sqcap \top \sqcup y \\ &= x \sqcap \top \\ &= x \end{align}
Proof 3.