avewright/proofwiki-math huggingface dataset:
Theorem: Rule of Addition/Sequent Form

The '''rule of addition''' can be symbolised by the sequents:
{{begin-eqn}}
{{eqn | n = 1
      | l = p
      | o = 
}}
{{eqn | ll= \vdash 
      | l = p \lor q
      | o = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | n = 2
      | l = q
      | o = 
}}
{{eqn | ll= \vdash 
      | l = p \lor q
      | o = 
}}
{{end-eqn}}

Proof:
{{BeginTableau|p \implies \paren {p \lor q}|Instance 2 of the Hilbert-style systems}}
{{TableauLine
 | n = 1
 | f = q \implies \paren {p \lor q}
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Axiom $\text A 2$
}}
{{TableauLine
 | n = 2
 | f = p \implies \paren {q \lor p}
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Rule $\text {RST} 1$
 | dep  = 1
 | c    = $p \,/\, q, q \,/\, p$
}}
{{TableauLine
 | n = 3
 | f = \paren {p \lor q} \implies \paren {q \lor p}
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Axiom $\text A 3$
}}
{{TableauLine
 | n = 4
 | f = \paren {q \lor p} \implies \paren {p \lor q}
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Rule $\text {RST} 1$
 | dep  = 3
 | c    = $p \,/\, q, q \,/\, p$
}}
{{TableauLine
 | n = 5
 | f = p \implies \paren {p \lor q}
 | rlnk = Hypothetical Syllogism/Formulation 1/Proof 2
 | rtxt = Hypothetical Syllogism
 | dep  = 2, 4
}}
{{EndTableau}}
{{Qed}}
Theorem: Rule of Addition/Sequent Form

The '''rule of addition''' can be symbolised by the sequents:
{{begin-eqn}}
{{eqn | n = 1
      | l = p
      | o = 
}}
{{eqn | ll= \vdash 
      | l = p \lor q
      | o = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | n = 2
      | l = q
      | o = 
}}
{{eqn | ll= \vdash 
      | l = p \lor q
      | o = 
}}
{{end-eqn}}

Proof:
{{BeginTableau|q \implies \paren {p \lor q} }}
{{Premise|1|q}}
{{Addition|2|1|p \lor q|1|2}}
{{Implication|3||q \implies \paren {p \lor q}|1|3}}
{{EndTableau}}
{{Qed}}
Theorem: Rule of Addition/Sequent Form

The '''rule of addition''' can be symbolised by the sequents:
{{begin-eqn}}
{{eqn | n = 1
      | l = p
      | o = 
}}
{{eqn | ll= \vdash 
      | l = p \lor q
      | o = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | n = 2
      | l = q
      | o = 
}}
{{eqn | ll= \vdash 
      | l = p \lor q
      | o = 
}}
{{end-eqn}}

Proof:
=== Form 1 ===
{{:Rule of Addition/Sequent Form/Formulation 2/Proof 1/Form 1}}
=== Form 2 ===
{{:Rule of Addition/Sequent Form/Formulation 2/Proof 1/Form 2}}
Theorem: Rule of Addition/Sequent Form

The '''rule of addition''' can be symbolised by the sequents:
{{begin-eqn}}
{{eqn | n = 1
      | l = p
      | o = 
}}
{{eqn | ll= \vdash 
      | l = p \lor q
      | o = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | n = 2
      | l = q
      | o = 
}}
{{eqn | ll= \vdash 
      | l = p \lor q
      | o = 
}}
{{end-eqn}}

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connectives are $T$ for all boolean interpretations.
:<nowiki>$\begin{array}{|c|c|ccccc|ccccc|} \hline
p & q & p & \implies & (p & \lor & q) & q & \implies & (p & \lor & q) \\
\hline
\F & \F & \F & \T & \F & \F & \F & \F & \T & \F & \F & \F \\
\F & \T & \F & \T & \F & \T & \T & \T & \T & \F & \T & \T \\
\T & \F & \T & \T & \T & \T & \F & \F & \T & \T & \T & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Rule of Addition/Sequent Form

The '''rule of addition''' can be symbolised by the sequents:
{{begin-eqn}}
{{eqn | n = 1
      | l = p
      | o = 
}}
{{eqn | ll= \vdash 
      | l = p \lor q
      | o = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | n = 2
      | l = q
      | o = 
}}
{{eqn | ll= \vdash 
      | l = p \lor q
      | o = 
}}
{{end-eqn}}

Proof:
=== Form 1 ===
{{:Rule of Addition/Sequent Form/Proof 1/Form 1}}
=== Form 2 ===
{{:Rule of Addition/Sequent Form/Proof 1/Form 2}}
Theorem: Rule of Addition/Sequent Form

The '''rule of addition''' can be symbolised by the sequents:
{{begin-eqn}}
{{eqn | n = 1
      | l = p
      | o = 
}}
{{eqn | ll= \vdash 
      | l = p \lor q
      | o = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | n = 2
      | l = q
      | o = 
}}
{{eqn | ll= \vdash 
      | l = p \lor q
      | o = 
}}
{{end-eqn}}

Proof:
We apply the Method of Truth Tables.
:<nowiki>$\begin{array}{|c|c||ccc|} \hline
p & q & p & \lor & q\\
\hline
\F & \F & \F & \F & \F \\
\F & \T & \F & \T & \T \\
\T & \F & \T & \T & \F \\
\T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
As can be seen, whenever either $p$ or $q$ (or both) are true, then so is $p \lor q$.
{{qed}}
Theorem: Rule of Addition/Sequent Form/Proof 1

The Rule of Addition can be symbolised by the sequents:
:$(1): \quad p \vdash p \lor q$
:$(2): \quad q \vdash p \lor q$

Proof:
=== Form 1 ===
{{:Rule of Addition/Sequent Form/Proof 1/Form 1}}
=== Form 2 ===
{{:Rule of Addition/Sequent Form/Proof 1/Form 2}}
Theorem: Proof by Cases/Sequent Form

Proof by Cases can be symbolised by the sequent:
:$p \lor q, \paren {p \vdash r}, \paren {q \vdash r} \vdash r$

Proof:
{{BeginTableau|p \lor q, \paren {p \vdash r}, \paren {q \vdash r} \vdash r}}
{{Premise | 1 | p \lor q}}
{{Assumption | 2 | p}}
{{TableauLine | n    = 3
              | pool = 2
              | f    = r
              | rlnk = Definition:By Hypothesis
              | rtxt = By hypothesis
              | dep  = 2 
              | c    = as $p \vdash r$
}}
{{Assumption  | 4 | q }}
{{TableauLine | n    = 5
              | pool = 4
              | f    = r
              | rlnk = Definition:By Hypothesis
              | rtxt = By hypothesis
              | dep  = 4 
              | c    = as $q \vdash r$
}}
{{ProofByCases | 6 | 1 | r | 1 | 2 | 3 | 4 | 5}}
{{EndTableau}}
{{qed}}
Theorem: Proof by Cases/Sequent Form

Proof by Cases can be symbolised by the sequent:
:$p \lor q, \paren {p \vdash r}, \paren {q \vdash r} \vdash r$

Proof:
We apply the Method of Truth Tables.
:<nowiki>$\begin{array}{|ccc|ccc|ccc||c|} \hline
p & \lor & q & p & \implies & r & q & \implies & r & r \\
\hline
\F & \F & \F & \F & \T & \F & \F & \T & \F & \F \\
\F & \F & \F & \F & \T & \T & \F & \T & \T & \T \\
\F & \T & \T & \F & \T & \F & \T & \F & \F & \F \\
\F & \T & \T & \F & \T & \T & \T & \T & \T & \T \\
\T & \T & \F & \T & \F & \F & \F & \T & \F & \F \\
\T & \T & \F & \T & \T & \T & \F & \T & \T & \T \\
\T & \T & \T & \T & \F & \F & \T & \F & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
As can be seen, when $p \lor q$, $p \implies r$ and $q \implies r$ are all true, then so is $r$.
{{qed}}
Theorem: Modus Ponendo Ponens/Sequent Form

{{begin-eqn}}
{{eqn | l = p
      | o = \implies
      | r = q
}}
{{eqn | l = p
      | o = 
}}
{{eqn | ll= \vdash
      | l = q
      | o = 
}}
{{end-eqn}}

Proof:
{{BeginTableau|p \implies q, p \vdash q}}
{{Premise|1|p \implies q}}
{{Premise|2|p}}
{{ModusPonens|3|1, 2|q|1|2}}
{{EndTableau|qed}}
Theorem: Modus Ponendo Ponens/Sequent Form

{{begin-eqn}}
{{eqn | l = p
      | o = \implies
      | r = q
}}
{{eqn | l = p
      | o = 
}}
{{eqn | ll= \vdash
      | l = q
      | o = 
}}
{{end-eqn}}

Proof:
{{BeginTableau|p \implies q, p \vdash q}}
{{Premise|1|p \implies q}}
{{Premise|2|p}}
{{Assumption|3|p}}
{{ModusPonens|4|1, 3|q|1|3}}
{{Assumption|5|\lnot p}}
{{NonContradiction|6|2, 5|2|5}}
{{Explosion|7|2, 5|q|6}}
{{ExcludedMiddle|8|p \lor \lnot p}}
{{ProofByCases|9|1, 2|q|8|3|4|5|7}}
{{EndTableau|qed}}
Theorem: Modus Ponendo Ponens/Sequent Form

{{begin-eqn}}
{{eqn | l = p
      | o = \implies
      | r = q
}}
{{eqn | l = p
      | o = 
}}
{{eqn | ll= \vdash
      | l = q
      | o = 
}}
{{end-eqn}}

Proof:
We apply the Method of Truth Tables.
:<nowiki>$\begin{array}{|c|ccc||c|} \hline
p & p & \implies & q & q\\
\hline
\F & \F & \T & \F & \F \\
\F & \F & \T & \T & \T \\
\T & \T & \F & \F & \F \\
\T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
As can be seen, when $p$ is true, and so is $p \implies q$, then $q$ is also true.
{{qed}}
Theorem: Logarithm of Power/Natural Logarithm

Let $x \in \R$ be a strictly positive real number.
Let $a \in \R$ be a real number such that $a > 1$.
Let $r \in \R$ be any real number.
Let $\ln x$ be the natural logarithm of $x$.
Then:
:$\map \ln {x^r} = r \ln x$

Proof:
Consider the function $\map f x = \map \ln {x^r} - r \ln x$.
Then from:
:The definition of the natural logarithm
:The Fundamental Theorem of Calculus
:The Power Rule for Derivatives
:The Chain Rule for Derivatives:
:$\forall x > 0: \map {f'} x = \dfrac 1 {x^r} r x^{r-1} - \dfrac r x = 0$
Thus from Zero Derivative implies Constant Function, $f$ is constant:
:$\forall x > 0: \map \ln {x^r} - r \ln x = c$
To determine the value of $c$, put $x = 1$.
From Logarithm of 1 is 0:
:$\ln 1 = 0$
Thus:
:$c = \ln 1 - r \ln 1 = 0$
{{qed}}
Theorem: Logarithm of Power/Natural Logarithm

Let $x \in \R$ be a strictly positive real number.
Let $a \in \R$ be a real number such that $a > 1$.
Let $r \in \R$ be any real number.
Let $\ln x$ be the natural logarithm of $x$.
Then:
:$\map \ln {x^r} = r \ln x$

Proof:
{{begin-eqn}}
{{eqn | l = \ln a
      | r = b
}}
{{eqn | ll= \leadstoandfrom
      | l = e^b
      | r = a
}}
{{eqn | ll= \leadsto
      | l = \paren {e^b}^c
      | r = a^c
}}
{{eqn | ll= \leadsto
      | l = e^{c b}
      | r = a^c
      | c = Exponential of Product
}}
{{eqn | ll= \leadsto
      | l = \ln e^{c b}
      | r = \ln a^c
}}   
{{eqn | ll= \leadsto
      | l = c b
      | r = \ln a^c
      | c = Exponential of Natural Logarithm
}}
{{end-eqn}}
By hypothesis, $\ln a = b$.
Multiplying both sides by $c$:
:$c \ln a = c b$
But we proved above that:
:$c b = \ln a^c$
{{qed}}
Theorem: Logarithm of Power/Natural Logarithm

Let $x \in \R$ be a strictly positive real number.
Let $a \in \R$ be a real number such that $a > 1$.
Let $r \in \R$ be any real number.
Let $\ln x$ be the natural logarithm of $x$.
Then:
:$\map \ln {x^r} = r \ln x$

Proof:
Here we adopt the definition of $\ln x$ to be:
:$\ds \ln x := \int_1^x \dfrac {\d t} t$
{{begin-eqn}}
{{eqn | l = \map \ln {x^r}
      | r = \int_1^{x^r} \dfrac {\d t} t
      | c = {{Defof|Natural Logarithm}}
}}
{{eqn | r = \int_1^x \dfrac {r t^{r - 1} \rd t} {t^r}
      | c = Integration by Substitution: $t \mapsto t^r$, $\d t \mapsto r t^{r - 1} \rd t$, $1 \mapsto 1$, $x^r \mapsto x$
}}
{{eqn | r = r \int_1^x \dfrac {\d t} t
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = r \ln x
      | c = {{Defof|Natural Logarithm}}
}}
{{end-eqn}}
{{qed}}
Theorem: Logarithm of Power/General Logarithm

Let $x \in \R$ be a strictly positive real number.
Let $a \in \R$ be a real number such that $a > 1$.
Let $r \in \R$ be any real number.
Let $\log_a x$ be the logarithm to the base $a$ of $x$.
Then:
:$\map {\log_a} {x^r} = r \log_a x$

Proof:
Let $y = r \log_a x$.
Then:
{{begin-eqn}}
{{eqn | l = a^y
      | r = a^{r \log_a x}
      | c = 
}}
{{eqn | r = \paren {a^{\log_a x} }^r
      | c = Exponent Combination Laws
}}
{{eqn | r = x^r
      | c = {{Defof|General Logarithm|Logarithm base $a$}}
}}
{{end-eqn}}
The result follows by taking logs base $a$ of both sides.
{{qed}}
Theorem: Power Set with Union and Intersection forms Boolean Algebra

Let $S$ be a set, and let $\powerset S$ be its power set.
Denote with $\cup$, $\cap$ and $\complement$ the operations of union, intersection and complement on $\powerset S$, respectively.
Then $\struct {\powerset S, \cup, \cap, \complement}$ is a Boolean algebra.

Proof:
Taking the criteria for definition 1 of a Boolean algebra in turn:
Theorem: Rule of Implication/Sequent Form

The '''rule of implication''' can be symbolised by the sequent:
{{begin-eqn}}
{{eqn | l = \paren {p \vdash q}
      | o = 
}}
{{eqn | ll= \vdash
      | l = p \implies q
      | o = 
}}
{{end-eqn}}

Proof:
* {{BookReference|Symbolic Logic|1973|Irving M. Copi|ed = 4th|edpage = Fourth Edition|prev = Rule of Simplification/Sequent Form/Formulation 1/Form 2|next = Indirect Proof}}: $3$: The Method of Deduction: $3.5$: The Rule of Conditional Proof
Category:Rule of Implication
sok3mffh8m5eu15dn2enblza3f6myp6
Theorem: Rule of Implication/Sequent Form

The '''rule of implication''' can be symbolised by the sequent:
{{begin-eqn}}
{{eqn | l = \paren {p \vdash q}
      | o = 
}}
{{eqn | ll= \vdash
      | l = p \implies q
      | o = 
}}
{{end-eqn}}

Proof:
{{BeginTableau|\paren {p \vdash q} \vdash p \implies q}}
{{Premise|1|p}}
{{TableauLine | n    = 2
              | pool = 1
              | f    = q
              | rlnk = Definition:By Hypothesis
              | rtxt = By hypothesis
              | dep  = 1
              | c    = as $p \vdash q$
}}
{{Implication|3|1|p \implies q|1|2}}
{{EndTableau}}
{{Qed}}
Theorem: Rule of Implication/Sequent Form

The '''rule of implication''' can be symbolised by the sequent:
{{begin-eqn}}
{{eqn | l = \paren {p \vdash q}
      | o = 
}}
{{eqn | ll= \vdash
      | l = p \implies q
      | o = 
}}
{{end-eqn}}

Proof:
We apply the Method of Truth Tables.
:<nowiki>$\begin{array}{|c|c||ccc|} \hline
p & q & p & \implies & q\\
\hline
\F & \F & \F & \T & \F \\
\F & \T & \F & \T & \T \\
\T & \F & \T & \F & \F \\
\T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
As can be seen by inspection, only when $p$ is true and $q$ is false, then so is $p \implies q$ also false.
{{qed}}
Theorem: Sum of Absolutely Convergent Series

Let $\ds \sum_{n \mathop = 1}^\infty a_n$ and $\ds \sum_{n \mathop = 1}^\infty b_n$ be two real or complex series that are absolutely convergent.
Then the series $\ds \sum_{n \mathop = 1}^\infty \paren {a_n + b_n}$ is absolutely convergent, and:
:$\ds \sum_{n \mathop = 1}^\infty \paren {a_n + b_n} = \sum_{n \mathop = 1}^\infty a_n + \sum_{n \mathop = 1}^\infty b_n$

Proof:
Let $\epsilon \in \R_{>0}$.
From Tail of Convergent Series tends to Zero, it follows that there exists $M \in \N$ such that:
:$\ds \sum_{n \mathop = M + 1}^\infty \cmod {a_n} < \dfrac \epsilon 2$
and:
:$\ds\sum_{n \mathop = M + 1}^\infty \cmod {b_n} < \dfrac \epsilon 2$
For all $m \ge M$, it follows that:
{{begin-eqn}}
{{eqn | l = \cmod {\sum_{n \mathop = 1}^\infty a_n + \sum_{n \mathop = 1}^\infty b_n - \sum_{n \mathop = 1}^m \paren {a_n + b_n} }
      | r = \cmod {\sum_{n \mathop = m + 1}^\infty a_n + \sum_{n \mathop = m + 1}^\infty b_n}
}}
{{eqn | o = \le
      | r = \sum_{n \mathop = m + 1}^\infty \cmod {a_n} + \sum_{n \mathop = m + 1}^\infty \cmod {b_n}
      | c = by Triangle Inequality
}}
{{eqn | o = \le
      | r = \sum_{n \mathop = M + 1}^\infty \cmod {a_n} + \sum_{n \mathop = M + 1}^\infty \cmod {b_n}
}}
{{eqn | o = <
      | r = \epsilon
}}
{{end-eqn}}
By definition of convergent series, it follows that:
{{begin-eqn}}
{{eqn | l = \sum_{n \mathop = 1}^\infty a_n + \sum_{n \mathop = 1}^\infty b_n
      | r = \lim_{m \mathop \to \infty} \sum_{n \mathop = 1}^m \paren {a_n + b_n}
}}
{{eqn | r = \sum_{n \mathop = 1}^\infty \paren {a_n + b_n}
}}
{{end-eqn}}
To show that $\ds \sum_{n \mathop = 1}^\infty \paren {a_n + b_n}$ is absolutely convergent, note that:
{{begin-eqn}}
{{eqn | l = \sum_{n \mathop = 1}^\infty \cmod {a_n} + \sum_{n \mathop = 1}^\infty \cmod {b_n}
      | r = \sum_{n \mathop = 1}^\infty \paren {\cmod {a_n} + \cmod {b_n} }
      | c = as shown above
}}
{{eqn | o = \ge
      | r = \sum_{n \mathop = 1}^\infty \cmod {a_n + b_n}
      | c = by Triangle Inequality
}}
{{end-eqn}}
{{qed}}
Theorem: Rule of Simplification/Sequent Form/Formulation 2

{{begin-eqn}}
{{eqn | n = 1
      | l = \vdash p \land q
      | o = \implies
      | r = p
}}
{{eqn | n = 2
      | l = \vdash p \land q
      | o = \implies
      | r = q
}}
{{end-eqn}}

Proof:
=== Form 1 ===
{{:Rule of Simplification/Sequent Form/Formulation 2/Proof 1/Form 1}}
=== Form 2 ===
{{:Rule of Simplification/Sequent Form/Formulation 2/Proof 1/Form 2}}
Theorem: Rule of Simplification/Sequent Form/Formulation 2

{{begin-eqn}}
{{eqn | n = 1
      | l = \vdash p \land q
      | o = \implies
      | r = p
}}
{{eqn | n = 2
      | l = \vdash p \land q
      | o = \implies
      | r = q
}}
{{end-eqn}}

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connective are true for all boolean interpretations.
:<nowiki>$\begin{array}{|ccc|c|c||c|c|} \hline
p & \land & q & p & q & p \land q \implies p & p \land q \implies q \\
\hline
\F & \F & \F & \F & \F & \T & \T \\
\F & \F & \T & \F & \T & \T & \T \\
\T & \F & \F & \T & \F & \T & \T \\
\T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Rule of Simplification/Sequent Form/Formulation 2/Proof 1/Form 1

:$\vdash p \land q \implies p$

Proof:
{{BeginTableau|\vdash p \land q \implies p}}
{{Assumption|1|p \land q}}
{{Simplification|2|1|p|1|1}}
{{Implication|3||p \land q \implies p|1|2}}
{{EndTableau|qed}}
Theorem: Rule of Simplification/Sequent Form/Formulation 2/Proof 1/Form 2

:$\vdash p \land q \implies q$

Proof:
{{BeginTableau|\vdash p \land q \implies q}}
{{Assumption|1|p \land q}}
{{Simplification|2|1|q|1|2}}
{{Implication|3||p \land q \implies q|1|2}}
{{EndTableau}}
{{Qed}}
Theorem: Complement of Complement in Uniquely Complemented Lattice

Let $\struct {S, \wedge, \vee, \preceq}$ be a uniquely complemented lattice.
For each $x \in S$, let $\neg x$ be the complement of $x$.
Then for each $x \in S$:
:$\neg \neg x = x$

Proof:
By the definition of a complement of $x$:
:$\neg x \vee x = \top$
:$\neg x \wedge x = \bot$
Since $\vee$ and $\wedge$ are commutative:
:$x \vee \neg x = \top$
:$x \wedge \neg x = \bot$
Thus by the definition of complement, $x$ is a complement of $\neg x$.
By the definition of a uniquely complemented lattice, $x = \neg \neg x$.
{{qed}}
Category:Uniquely Complemented Lattices
8kji3yc8f56j2xpqp7h5hyesfp1dvh4
Theorem: De Morgan's Laws imply Uniquely Complemented Lattice is Boolean Lattice

Let $\struct {S, \wedge, \vee, \preceq}$ be a uniquely complemented lattice.
{{TFAE}}
{{begin-itemize}}
{{item|(1):|$\forall p, q \in S: \neg p \vee \neg q {{=}} \neg \paren {p \wedge q}$}}
{{item|(2):|$\forall p, q \in S: \neg p \wedge \neg q {{=}} \neg \paren {p \vee q}$}}
{{item|(3):|$\forall p, q \in S: p \preceq q \iff \neg q \preceq \neg p$}}
{{item|(4):|$\struct {S, \wedge, \vee, \preceq}$ is a distributive lattice}}
{{end-itemize}}
{{explain|So we're equivalencing a distributive lattice, but the page title says Boolean Lattice -- needs to be resolved}}

Proof:
=== $(1)$ implies $(2)$ ===
Suppose:
:$\forall p, q \in S: \neg p \vee \neg q = \neg \paren {p \wedge q}$
Then applying this to $\neg p$ and $\neg q$:
:$\neg \neg p \vee \neg \neg q = \neg \paren {\neg p \wedge \neg q}$
By Complement of Complement in Uniquely Complemented Lattice:
:$\neg \neg p = p$ and $\neg \neg q = q$
Thus:
:$p \vee q = \neg \paren {\neg p \wedge \neg q}$
Taking complements of both sides:
:$\neg \paren {p \vee q} = \neg \neg \paren {\neg p \wedge \neg q}$
Again applying Complement of Complement in Uniquely Complemented Lattice:
:$\neg \paren {p \vee q} = \neg p \wedge \neg q$
{{qed|lemma}}
Theorem: Complement of Bottom/Boolean Algebra

Let $\struct {S, \vee, \wedge, \neg}$ be a Boolean algebra.
Then:
:$\neg \bot = \top$

Proof:
Since $\bot$ is the identity for $\vee$, the first condition for $\neg \bot$:
:$\bot \vee \neg \bot = \top$
implies that $\neg \bot = \top$ is the only possibility.
Since $\top$ is the identity for $\wedge$, it follows that:
:$\bot \wedge \top = \bot$
and we conclude that:
:$\neg \bot = \top$
as desired.
{{qed}}
Theorem: Complement of Bottom/Bounded Lattice

Let $\struct {S, \vee, \wedge, \preceq}$ be a bounded lattice.
Then the bottom $\bot$ has a unique complement, namely $\top$, top.

Proof:
We know that $\bot$ is the identity for $\vee$.
Therefore, from the condition that:
:$\bot \vee a = \top$
for a complement $a$ of $\bot$, it follows that $a = \top$ is the only possibility.
Since also:
:$\bot \wedge \top = \bot$
as $\top$ is the identity for $\wedge$, the result follows.
{{qed}}
Theorem: Complement of Top/Bounded Lattice

Let $\struct {S, \vee, \wedge, \preceq}$ be a bounded lattice.
Then the top $\top$ has a unique complement, namely $\bot$, bottom.

Proof:
By Dual Pairs (Order Theory), $\top$ is dual to $\bot$.
The result follows from the Duality Principle and Complement of Bottom.
{{qed}}
Theorem: Complement of Top/Boolean Algebra

Let $\struct {S, \vee, \wedge, \neg}$ be a Boolean algebra.
Then:
:$\neg \top = \bot$

Proof:
Since $\top$ is the identity for $\wedge$, the second condition for $\neg \top$:
:$\top \wedge \neg \top = \bot$
implies that $\neg \top = \bot$ is the only possibility.
Since $\bot$ is the identity for $\vee$, it follows that:
:$\top \vee \bot = \top$
and we conclude that:
:$\neg \top = \bot$
as desired.
{{qed}}
Theorem: Duality Principle (Boolean Algebras)

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

Proof:
Let us take the axioms of a Boolean algebra $\struct {S, \wedge, \vee, \neg}$:
{{:Axiom:Boolean Algebra/Axioms/Formulation 1}}
It can be seen by inspection that exchanging $\wedge$ and $\vee$, and $\bot$ and $\top$ throughout, does not change the axioms.
Thus, what you get is a Boolean algebra again.
Hence the result.
{{qed}}
Theorem: Identities of Boolean Algebra are also Zeroes

Let $\struct {S, \vee, \wedge, \neg}$ be a Boolean algebra, defined as in Definition 1.
Let the identity for $\vee$ be $\bot$ and the identity for $\wedge$ be $\top$.
Then:
{{begin-eqn}}
{{eqn | n = 1
      | q = \forall x \in S
      | l = x \vee \top
      | r = \top
}}
{{eqn | n = 2
      | q = \forall x \in S
      | l = x \wedge \bot
      | r = \bot
}}
{{end-eqn}}
That is:
:$\bot$ is a zero element for $\wedge$
:$\top$ is a zero element for $\vee$.

Proof:
Let $x \in S$.
Then:
{{begin-eqn}}
{{eqn | l = x \vee \top
      | r = \paren {x \vee \top} \wedge \top
      | c = {{Boolean-algebra-axiom|1|3}}: $\top$ is the identity of $\wedge$
}}
{{eqn | r = \paren {x \vee \top} \wedge \paren {x \vee \neg x}
      | c = {{Boolean-algebra-axiom|1|4}}: $x \vee x' = \top$
}}
{{eqn | r = x \vee \paren {\top \wedge x'}
      | c = {{Boolean-algebra-axiom|1|2}}: both $\vee$ and $\wedge$ distribute over the other
}}
{{eqn | r = x \vee x'
      | c = {{Boolean-algebra-axiom|1|3}}: $\top$ is the identity of $\wedge$
}}
{{eqn | r = \top
      | c = {{Boolean-algebra-axiom|1|4}}: $x \vee x' = \top$
}}
{{end-eqn}}
So $x \vee \top = \top$.
{{qed|lemma}}
The result $x \wedge \bot = \bot$ follows from the Duality Principle.
{{qed}}
Theorem: Complement of Complement (Boolean Algebras)

Let $\struct {S, \vee, \wedge, \neg}$ be a Boolean algebra.
Then for all $a \in S$:
:$\map \neg {\neg a} = a$

Proof:
Follows directly from Complement in Boolean Algebra is Unique.
{{qed}}