avewright/proofwiki-math huggingface dataset:
Theorem: Self-Distributive Law for Conditional

The following is known as the Self-Distributive Law:
=== Formulation 1 ===
{{:Self-Distributive Law for Conditional/Formulation 1}}
=== Formulation 2 ===
{{:Self-Distributive Law for Conditional/Formulation 2}}

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth value under the main connective is true for all boolean interpretations.
:<nowiki>$\begin{array}{|ccccc|c|ccccccc|}
\hline
(p & \implies & (q & \implies & r)) & \implies & ((p & \implies & q) & \implies & (p & \implies & r)) \\
\hline
\F & \T & \F & \T & \F & \T & \F & \T & \F & \T & \F & \T & \F \\
\F & \T & \F & \T & \T & \T & \F & \T & \F & \T & \F & \T & \T \\
\F & \T & \T & \F & \F & \T & \F & \T & \T & \T & \F & \T & \F \\
\F & \T & \T & \T & \T & \T & \F & \T & \T & \T & \F & \T & \T \\
\T & \T & \F & \T & \F & \T & \T & \F & \F & \T & \T & \F & \F \\
\T & \T & \F & \T & \T & \T & \T & \F & \F & \T & \T & \T & \T \\
\T & \F & \T & \F & \F & \T & \T & \T & \T & \F & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
Theorem: Self-Distributive Law for Conditional

The following is known as the Self-Distributive Law:
=== Formulation 1 ===
{{:Self-Distributive Law for Conditional/Formulation 1}}
=== Formulation 2 ===
{{:Self-Distributive Law for Conditional/Formulation 2}}

Proof:
{{BeginTableau |\vdash \paren {\paren {p \implies q} \implies \paren {p \implies r} } \implies \paren {p \implies \paren {q \implies r} } }}
{{Assumption   |1|\paren {p \implies q} \implies \paren {p \implies r} }}
{{SequentIntro |2|1|p \implies \paren {q \implies r}|1|Self-Distributive Law for Conditional: Formulation 1}}
{{Implication  |3||\paren {\paren {p \implies q} \implies \paren {p \implies r} } \implies \paren {p \implies \paren {q \implies r} }|1|2}}
{{EndTableau}}
{{Qed}}
Theorem: Self-Distributive Law for Conditional

The following is known as the Self-Distributive Law:
=== Formulation 1 ===
{{:Self-Distributive Law for Conditional/Formulation 1}}
=== Formulation 2 ===
{{:Self-Distributive Law for Conditional/Formulation 2}}

Proof:
{{BeginTableau |\vdash \paren {\paren {p \implies q} \implies \paren {p \implies r} } \implies \paren {p \implies \paren {q \implies r} } }}
{{Assumption|1|\paren {p \implies q} \implies \paren {p \implies r} }}
{{Assumption|2|p}}
{{Assumption|3|q}}
{{SequentIntro|4|3|p \implies q|3|True Statement is implied by Every Statement}}
{{ModusPonens|5|1, 3|p \implies r|1|4}}
{{ModusPonens|6|1, 2, 3|r|5|2}}
{{Implication|7|1, 2|q \implies r|3|6}}
{{Implication|8|1|p \implies \paren {q \implies r}|2|7}}
{{Implication|9||\paren {\paren {p \implies q} \implies \paren {p \implies r} } \implies \paren {p \implies \paren {q \implies r} }|1|8}}
{{EndTableau|qed}}
Theorem: Disjunction of Conditional and Converse

:$\vdash \paren {p \implies q} \lor \paren {q \implies p}$

Proof:
{{BeginTableau|\vdash \paren {p \implies q} \lor \paren {q \implies p} }}
{{ExcludedMiddle|1|p \lor \neg p}}
{{Assumption|2|p}}
{{SequentIntro|3|2|q \implies p|2|True Statement is implied by Every Statement}}
{{Addition|4|2|\paren {p \implies q} \lor \paren {q \implies p}|2|2}}
{{Assumption|5|\neg p}}
{{SequentIntro|6|5|p \implies q|5|False Statement implies Every Statement}}
{{Addition|7|5|\paren {p \implies q} \lor \paren {q \implies p}|7|1}}
{{ProofByCases|8||\paren {p \implies q} \lor \paren {q \implies p}|1|2|4|5|7}}
{{EndTableau|qed}}
{{LEM||3}}
Theorem: Disjunction of Conditional and Converse

:$\vdash \paren {p \implies q} \lor \paren {q \implies p}$

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, the truth values under the main connective is true for all boolean interpretations, proving a tautology.
$\begin{array}{|ccccccc|} \hline
(p & \implies & q) & \lor & (q & \implies & p) \\
\hline
\F & \T & \F & \T & \F & \T & \F \\
\F & \T & \T & \T & \T & \F & \F \\
\T & \F & \F & \T & \F & \T & \T \\
\T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$
{{qed}}
Theorem: Characteristics of Eulerian Graph

A finite (undirected) graph is Eulerian {{iff}} it is connected and each vertex is even.

Proof:
Suppose that an (undirected) graph $G$ is connected and its vertices all have even degree.
If there is more than one vertex in $G$, then each vertex must have degree greater than $0$.
Begin at a vertex $v$.
From Graph with Even Vertices Partitions into Cycles, we know that $v$ will be on at least one cycle.
Since $G$ is connected, there must be an edge $\set {v, v_1}$ for some vertex $v_1 \ne v$.
Since $v_1$ has even degree greater than $0$, there is an edge $\set {v_1, v_2}$ where $v_2 \ne v_1$.
These two edges make a trail from $v$ to $v_2$.
Continue this trail, leaving each vertex on an edge that was not previously used, until returning to $v$.
This is always possible, because $v$ is on a cycle.
Call the circuit formed by this process $C_1$.
If $C_1$ covers all the edges of $G$, then the proof is complete.
Otherwise, remove all the edges that contribute to $C_1$ from $G$, leaving the graph $G_0$.
The remaining vertices are still even, and since $G$ is connected there is some vertex $u$ in both $G_0$ and $C_1$.
Repeat the same process as before, beginning at $u$.
The new circuit, $C_2$, can be added to $C_1$ by starting at $v$, moving along $C_1$ to $u$, travelling around $C_2$ back to $u$ and then along the remainder of $C_1$ back to $v$.
Repeat this process, adding each new circuit found to create a larger circuit.
Since $G$ is finite, this process must end at some point, and the resulting circuit will be an Eulerian circuit.
{{qed}}
Theorem: Characteristics of Eulerian Graph

A finite (undirected) graph is Eulerian {{iff}} it is connected and each vertex is even.

Proof:
Suppose that an (undirected) graph $G$ is connected and its vertices all have even degree.
From Graph with Even Vertices Partitions into Cycles, we can split $G$ into a number of cycles $\mathbb S = C_1, C_2, \ldots, C_k$.
Start at any vertex $v$ on cycle $C_1$ and traverse its edges until we encounter a vertex of another cycle of $\mathbb S$, $C_2$ say.
The edges of $C_2$ are then traversed, and then the traversal of $C_1$ is resumed when it is returned to.
As $C_1$ is traversed, the journey is interrupted so as to traverse any other cycles of $\mathbb S$ in the same way that $C_2$ is traversed.
Eventually the beginning of $C_1$ is reached, which is vertex $v$.
Thus there exists a circuit which includes $C_1$ and at least one other cycle (unless $C_1$ is the only cycle), as $G$ is connected.
If this circuit contains all the cycles $C_1, C_2, \ldots, C_k$, the required Eulerian circuit has been found.
If not, then the circuit just generated is traversed.
Because $G$ is connected, other cycles in $\mathbb S$ will be encountered.
These, again, are traversed as they are encountered.
This process is continued till all the cycles have been included in the circuit.
At this stage, the required Eulerian circuit has been found.
Hence $G$ is Eulerian.
{{qed}}
Theorem: Commutativity of Incidence Matrix with its Transpose for Symmetric Design

Let $A$ be the incidence matrix of a symmetric design.
Then:
:$A A^\intercal = A^\intercal A$
where $A^\intercal$ is the transpose of $A$.

Proof:
First note, we have:
:$(1): \quad A J = J A = k J$, so $A^\intercal J = \paren {J A}^\intercal = \paren {k J}^\intercal = k J$, and likewise $J A^\intercal = k J$
:$(2): \quad J^2 = v J$
:$(3): \quad$ If a design is symmetric, then $A A^\intercal = \paren {r - \lambda} I + \lambda J = \paren {k - \lambda} I + \lambda J$
{{explain|We need to establish these three results. We need to confirm that $J$ is the ones matrix (I think it is, from the context) and then make sure of those above results.}}
From $(3)$, we get:
{{begin-eqn}}
{{eqn | l = \paren {A^\intercal - \sqrt {\paren {\frac \lambda v} J} } \paren {A + \sqrt {\paren {\frac \lambda v} J} }
      | r = A^\intercal A + \sqrt {\frac \lambda v} \paren {A^\intercal J - J A} - \frac \lambda v J^2
}}
{{eqn | r = A^\intercal A - \lambda J = \paren {k - \lambda} I
}}
{{end-eqn}}
We now have that:
:$\ds \frac 1 {k - \lambda} \paren {A + \sqrt {\paren {\frac \lambda v} J} }$
is the inverse of:
:$A^\intercal - \sqrt {\paren {\dfrac \lambda v} J}$
which implies that they commute with each other.
{{explain|... why?}}
Thus:
{{begin-eqn}}
{{eqn | l = \paren {k - \lambda} I
      | r = \paren {A + \sqrt {\frac \lambda v} J} \paren {A^\intercal - \sqrt {\frac \lambda v} J}
}}
{{eqn | r = A A^\intercal + \sqrt {\frac \lambda v} \paren {J A^\intercal - A J} - \frac \lambda v J^2
}}
{{eqn | r = A A^\intercal - \lambda J
}}
{{end-eqn}}
{{explain|The above steps need justification}}
whence:
:$A A^\intercal = \paren {k - \lambda} + \lambda J = A^\intercal A$
{{qed}}
Category:Design Theory
ffbni750n3mprbei4e19qaxg8q6f6rx
Theorem: De Morgan's Laws

'''De Morgan's Laws''' are a suite of theorems in logic, which are also applied in set theory, as follows:
=== Propositional Logic ===
{{:De Morgan's Laws (Logic)}}
=== Predicate Logic ===
{{:De Morgan's Laws (Predicate Logic)}}
=== Set Theory ===
{{:De Morgan's Laws (Set Theory)}}
=== Boolean Algebras ===
{{:De Morgan's Laws (Boolean Algebras)}}

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
:<nowiki>$\begin{array}{|ccccc||cccc|} \hline
\neg & p & \land & \neg & q & \neg & (p & \lor & q) \\
\hline
\T & \F & \T & \T & \F & \T & \F & \F & \F \\
\T & \F & \F & \F & \T & \F & \F & \T & \T \\
\F & \T & \F & \T & \F & \F & \T & \T & \F \\
\F & \T & \F & \F & \T & \F & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: De Morgan's Laws

'''De Morgan's Laws''' are a suite of theorems in logic, which are also applied in set theory, as follows:
=== Propositional Logic ===
{{:De Morgan's Laws (Logic)}}
=== Predicate Logic ===
{{:De Morgan's Laws (Predicate Logic)}}
=== Set Theory ===
{{:De Morgan's Laws (Set Theory)}}
=== Boolean Algebras ===
{{:De Morgan's Laws (Boolean Algebras)}}

Proof:
{{BeginTableau|\vdash \paren {\neg p \land \neg q} \iff \paren {\neg \paren {p \lor q} } }}
{{Assumption|1|\neg p \land \neg q}}
{{SequentIntro|2|1|\neg \paren {p \lor q}|1|De Morgan's Laws (Logic): Disjunction of Negations: Formulation 1}}
{{Implication|3||\paren {\neg p \land \neg q} \implies \paren {\neg \paren {p \lor q} }|1|2}}
{{Assumption|4|\neg \paren {p \lor q} }}
{{SequentIntro|5|4|\neg p \land \neg q|4|De Morgan's Laws (Logic): Disjunction of Negations: Formulation 1}}
{{Implication|6||\paren {\neg \paren {p \lor q} } \implies \paren {\neg p \land \neg q}|4|5}}
{{BiconditionalIntro|7||\paren {\neg p \land \neg q} \iff \paren {\neg \paren {p \lor q} }|3|6}}
{{EndTableau|qed}}
Theorem: De Morgan's Laws

'''De Morgan's Laws''' are a suite of theorems in logic, which are also applied in set theory, as follows:
=== Propositional Logic ===
{{:De Morgan's Laws (Logic)}}
=== Predicate Logic ===
{{:De Morgan's Laws (Predicate Logic)}}
=== Set Theory ===
{{:De Morgan's Laws (Set Theory)}}
=== Boolean Algebras ===
{{:De Morgan's Laws (Boolean Algebras)}}

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connective is true for all boolean interpretations.
:<nowiki>$\begin{array}{|ccccc|c|cccc|} \hline
\neg & p & \land & \neg & q & \iff & \neg & (p & \lor & q) \\
\hline
\T & \F & \T & \T & \F & \T & \T & \F & \F & \F \\
\T & \F & \F & \F & \T & \T & \F & \F & \T & \T \\
\F & \T & \F & \T & \F & \T & \F & \T & \T & \F \\
\F & \T & \F & \F & \T & \T & \F & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: De Morgan's Laws

'''De Morgan's Laws''' are a suite of theorems in logic, which are also applied in set theory, as follows:
=== Propositional Logic ===
{{:De Morgan's Laws (Logic)}}
=== Predicate Logic ===
{{:De Morgan's Laws (Predicate Logic)}}
=== Set Theory ===
{{:De Morgan's Laws (Set Theory)}}
=== Boolean Algebras ===
{{:De Morgan's Laws (Boolean Algebras)}}

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
$\begin{array}{|ccc||cccccc|} \hline
p & \land & q & \neg & (\neg & p & \lor & \neg & q)  \\
\hline
\F & \F & \F & \F & \T & \F & \T & \T & \F \\
\F & \F & \T & \F & \T & \F & \T & \F & \T \\
\T & \F & \F & \F & \F & \T & \T & \T & \F \\
\T & \T & \T & \T & \F & \T & \F & \F & \T \\
\hline
\end{array}$
{{qed}}
Theorem: De Morgan's Laws

'''De Morgan's Laws''' are a suite of theorems in logic, which are also applied in set theory, as follows:
=== Propositional Logic ===
{{:De Morgan's Laws (Logic)}}
=== Predicate Logic ===
{{:De Morgan's Laws (Predicate Logic)}}
=== Set Theory ===
{{:De Morgan's Laws (Set Theory)}}
=== Boolean Algebras ===
{{:De Morgan's Laws (Boolean Algebras)}}

Proof:
{{BeginTableau|\vdash \paren {p \land q} \iff \paren {\neg \paren {\neg p \lor \neg q} } }}
{{Assumption|1|p \land q}}
{{SequentIntro|2|1|\neg \paren {\neg p \lor \neg q}|1|De Morgan's Laws (Logic): Conjunction: Formulation 1}}
{{Implication|3||\paren {p \land q} \implies \paren {\neg \paren {\neg p \lor \neg q} }|1|2}}
{{Assumption|4|\neg \paren {\neg p \lor \neg q} }}
{{SequentIntro|5|4|p \land q|4|De Morgan's Laws (Logic): Conjunction: Formulation 1}}
{{Implication|6||\paren {\neg \paren {\neg p \lor \neg q} } \implies \paren {p \land q}|4|5}}
{{BiconditionalIntro|7||\paren {p \land q} \iff \paren {\neg \paren {\neg p \lor \neg q} }|3|6}}
{{EndTableau}}
{{qed}}
Theorem: De Morgan's Laws

'''De Morgan's Laws''' are a suite of theorems in logic, which are also applied in set theory, as follows:
=== Propositional Logic ===
{{:De Morgan's Laws (Logic)}}
=== Predicate Logic ===
{{:De Morgan's Laws (Predicate Logic)}}
=== Set Theory ===
{{:De Morgan's Laws (Set Theory)}}
=== Boolean Algebras ===
{{:De Morgan's Laws (Boolean Algebras)}}

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.
$\begin{array}{|ccc|c|cccccc|} \hline
(p & \land & q) & \iff & (\neg & (\neg & p & \lor & \neg & q))  \\
\hline
\F & \F & \F & \T & \F & \T & \F & \T & \T & \F \\
\F & \F & \T & \T & \F & \T & \F & \T & \F & \T \\
\T & \F & \F & \T & \F & \F & \T & \T & \T & \F \\
\T & \T & \T & \T & \T & \F & \T & \F & \F & \T \\
\hline
\end{array}$
{{qed}}
Theorem: De Morgan's Laws

'''De Morgan's Laws''' are a suite of theorems in logic, which are also applied in set theory, as follows:
=== Propositional Logic ===
{{:De Morgan's Laws (Logic)}}
=== Predicate Logic ===
{{:De Morgan's Laws (Predicate Logic)}}
=== Set Theory ===
{{:De Morgan's Laws (Set Theory)}}
=== Boolean Algebras ===
{{:De Morgan's Laws (Boolean Algebras)}}

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
:<nowiki>$\begin{array}{|ccccc||cccc|} \hline
\neg & p & \lor & \neg & q & \neg & (p & \land & q) \\
\hline
\T & \F & \T & \T & \F & \T & \F & \F & \F \\
\T & \F & \T & \F & \T & \T & \F & \F & \T \\
\F & \T & \T & \T & \F & \T & \T & \F & \F \\
\F & \T & \F & \F & \T & \F & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: De Morgan's Laws

'''De Morgan's Laws''' are a suite of theorems in logic, which are also applied in set theory, as follows:
=== Propositional Logic ===
{{:De Morgan's Laws (Logic)}}
=== Predicate Logic ===
{{:De Morgan's Laws (Predicate Logic)}}
=== Set Theory ===
{{:De Morgan's Laws (Set Theory)}}
=== Boolean Algebras ===
{{:De Morgan's Laws (Boolean Algebras)}}

Proof:
{{BeginTableau|\neg \paren {p \land q} \vdash \neg p \lor \neg q}}
{{Premise|1|\neg \paren {p \land q} }}
{{Assumption|2|\neg \paren {\neg p \lor \neg q} }}
{{Assumption|3|\neg p}}
{{Addition|4|3|\neg p \lor \neg q|3|1}}
{{NonContradiction|5|2, 3|4|2}}
{{Reductio|6|2|p|3|5}}
{{Assumption|7|\neg q}}
{{Addition|8|7|\neg p \lor \neg q|7|2}}
{{NonContradiction|9|2, 7|8|2}}
{{Reductio|10|2|q|7|9}}
{{Conjunction|11|2|p \land q|6|10}}
{{NonContradiction|12|1, 2|11|1}}
{{Reductio|13|1|\neg p \lor \neg q|2|12}}
{{EndTableau|qed}}
{{LEM|Reductio ad Absurdum|3}}
Theorem: De Morgan's Laws

'''De Morgan's Laws''' are a suite of theorems in logic, which are also applied in set theory, as follows:
=== Propositional Logic ===
{{:De Morgan's Laws (Logic)}}
=== Predicate Logic ===
{{:De Morgan's Laws (Predicate Logic)}}
=== Set Theory ===
{{:De Morgan's Laws (Set Theory)}}
=== Boolean Algebras ===
{{:De Morgan's Laws (Boolean Algebras)}}

Proof:
{{BeginTableau|\vdash \paren {\neg p \lor \neg q} \iff \paren {\neg \paren {p \land q} } }}
{{Assumption|1|\neg p \lor \neg q}}
{{SequentIntro|2|1|\neg \paren {p \land q}|1|De Morgan's Laws (Logic): Disjunction of Negations: Formulation 1}}
{{Implication|3||\paren {\neg p \lor \neg q} \implies \paren {\neg \paren {p \land q} }|1|2}}
{{Assumption|4|\neg \paren {p \land q} }}
{{SequentIntro|5|4|\neg p \lor \neg q|4|De Morgan's Laws (Logic): Disjunction of Negations: Formulation 1}}
{{Implication|6||\paren {\neg \paren {p \land q} } \implies \paren {\neg p \lor \neg q}|4|5}}
{{BiconditionalIntro|7||\paren {\neg p \lor \neg q} \iff \paren {\neg \paren {p \land q} }|3|6}}
{{EndTableau}}
{{qed}}
Theorem: De Morgan's Laws

'''De Morgan's Laws''' are a suite of theorems in logic, which are also applied in set theory, as follows:
=== Propositional Logic ===
{{:De Morgan's Laws (Logic)}}
=== Predicate Logic ===
{{:De Morgan's Laws (Predicate Logic)}}
=== Set Theory ===
{{:De Morgan's Laws (Set Theory)}}
=== Boolean Algebras ===
{{:De Morgan's Laws (Boolean Algebras)}}

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connective is true for all boolean interpretations.
:<nowiki>$\begin{array}{|ccccc|c|cccc|} \hline
\neg & p & \lor & \neg & q & \iff & \neg & (p & \land & q) \\
\hline
\T & \F & \T & \T & \F & \T & \T & \F & \F & \F \\
\T & \F & \T & \F & \T & \T & \T & \F & \F & \T \\
\F & \T & \T & \T & \F & \T & \T & \T & \F & \F \\
\F & \T & \F & \F & \T & \T & \F & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: De Morgan's Laws

'''De Morgan's Laws''' are a suite of theorems in logic, which are also applied in set theory, as follows:
=== Propositional Logic ===
{{:De Morgan's Laws (Logic)}}
=== Predicate Logic ===
{{:De Morgan's Laws (Predicate Logic)}}
=== Set Theory ===
{{:De Morgan's Laws (Set Theory)}}
=== Boolean Algebras ===
{{:De Morgan's Laws (Boolean Algebras)}}

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
$\begin{array}{|ccc||cccccc|} \hline
p & \lor & q & \neg & (\neg & p & \land & \neg & q) \\
\hline
\F & \F & \F & \F & \T & \F & \T & \T & \F \\
\F & \T & \T & \T & \T & \F & \F & \F & \T \\
\T & \T & \F & \T & \F & \T & \F & \T & \F \\
\T & \T & \T & \T & \F & \T & \F & \F & \T \\
\hline
\end{array}$
{{qed}}
Theorem: De Morgan's Laws

'''De Morgan's Laws''' are a suite of theorems in logic, which are also applied in set theory, as follows:
=== Propositional Logic ===
{{:De Morgan's Laws (Logic)}}
=== Predicate Logic ===
{{:De Morgan's Laws (Predicate Logic)}}
=== Set Theory ===
{{:De Morgan's Laws (Set Theory)}}
=== Boolean Algebras ===
{{:De Morgan's Laws (Boolean Algebras)}}

Proof:
{{BeginTableau|\vdash \paren {p \lor q} \iff \paren {\neg \paren {\neg p \land \neg q} } }}
{{Assumption|1|p \lor q}}
{{SequentIntro|2|1|\neg \paren {\neg p \land \neg q}|1|De Morgan's Laws (Logic): Disjunction: Formulation 1}}
{{Implication|3||\paren {p \lor q} \implies \paren {\neg \paren {\neg p \land \neg q} }|1|2}}
{{Assumption|4|\neg \paren {\neg p \land \neg q} }}
{{SequentIntro|5|4|p \lor q|4|De Morgan's Laws (Logic): Disjunction: Formulation 1}}
{{Implication|6||\paren {\neg \paren {\neg p \land \neg q} } \implies \paren {p \lor q}|4|5}}
{{BiconditionalIntro|7||\paren {p \lor q} \iff \paren {\neg \paren {\neg p \land \neg q} }|3|6}}
{{EndTableau}}
{{qed}}
Theorem: De Morgan's Laws

'''De Morgan's Laws''' are a suite of theorems in logic, which are also applied in set theory, as follows:
=== Propositional Logic ===
{{:De Morgan's Laws (Logic)}}
=== Predicate Logic ===
{{:De Morgan's Laws (Predicate Logic)}}
=== Set Theory ===
{{:De Morgan's Laws (Set Theory)}}
=== Boolean Algebras ===
{{:De Morgan's Laws (Boolean Algebras)}}

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|cccccc|} \hline
(p & \lor & q) & \iff & (\neg & (\neg & p & \land & \neg & q)) \\
\hline
\F & \F & \F & \T & \F & \T & \F & \T & \T & \F \\
\F & \T & \T & \T & \T & \T & \F & \F & \F & \T \\
\T & \T & \F & \T & \T & \F & \T & \F & \T & \F \\
\T & \T & \T & \T & \T & \F & \T & \F & \F & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: De Morgan's Laws

'''De Morgan's Laws''' are a suite of theorems in logic, which are also applied in set theory, as follows:
=== Propositional Logic ===
{{:De Morgan's Laws (Logic)}}
=== Predicate Logic ===
{{:De Morgan's Laws (Predicate Logic)}}
=== Set Theory ===
{{:De Morgan's Laws (Set Theory)}}
=== Boolean Algebras ===
{{:De Morgan's Laws (Boolean Algebras)}}

Proof:
Let the cardinality $\card I$ of the indexing set $I$ be $n$.
Then by the definition of cardinality, it follows that $I \cong \N^*_n$ and we can express the proposition:
:$\ds S \setminus \bigcap_{i \mathop \in I} T_i = \bigcup_{i \mathop \in I} \paren {S \setminus T_i}$
as:
:$\ds S \setminus \bigcap_{i \mathop = 1}^n T_i = \bigcup_{i \mathop = 1}^n \paren {S \setminus T_i}$
The proof of this is more amenable to proof by Principle of Mathematical Induction.
For all $n \in \N_{>0}$, let $\map P n$ be the proposition:
:$\ds S \setminus \bigcap_{i \mathop = 1}^n T_i = \bigcup_{i \mathop = 1}^n \paren {S \setminus T_i}$
$\map P 1$ is true, as this just says $S \setminus T_1 = S \setminus T_1$.
=== Base Case ===
$\map P 2$ is the case:
:$S \setminus \paren {T_1 \cap T_2} = \paren {S \setminus T_1} \cup \paren {S \setminus T_2}$
which has been proved. 
This is our basis for the induction.
=== Induction Hypothesis ===
Now we need to show that, if $\map P k$ is true, where $k \ge 2$, then it logically follows that $\map P {k + 1}$ is true.
So this is our induction hypothesis:
:$\ds S \setminus \bigcap_{i \mathop = 1}^k T_i = \bigcup_{i \mathop = 1}^k \paren {S \setminus T_i}$
=== Induction Step ===
Now we need to show:
:$\ds S \setminus \bigcap_{i \mathop = 1}^{k + 1} T_i = \bigcup_{i \mathop = 1}^{k + 1} \paren {S \setminus T_i}$
This is our induction step:
{{begin-eqn}}
{{eqn | l = S \setminus \bigcap_{i \mathop = 1}^{k + 1} T_i
      | r = S \setminus \paren {\bigcap_{i \mathop = 1}^k T_i \cap T_{k + 1} }
      | c = Intersection is Associative
}}
{{eqn | r = \paren {S \setminus \bigcap_{i \mathop = 1}^k T_i} \cup \paren {S \setminus T_{k + 1} }
      | c = Base case
}}
{{eqn | r = \paren {\bigcup_{i \mathop = 1}^k \paren {S \setminus T_i} } \cup \paren {S \setminus T_{k + 1} }
      | c = Induction hypothesis
}}
{{eqn | r = \bigcup_{i \mathop = 1}^{k + 1} \paren {S \setminus T_i}
      | c = Union is Associative
}}
{{end-eqn}}
So $\map P k \implies \map P {k + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
:$\ds S \setminus \bigcap_{i \mathop = 1}^n T_i = \bigcup_{i \mathop = 1}^n \paren {S \setminus T_i}$
that is:
:$\ds S \setminus \bigcap_{i \mathop \in I} T_i = \bigcup_{i \mathop \in I} \paren {S \setminus T_i}$
{{qed}}