avewright/proofwiki-math huggingface dataset:
Theorem: Extended Completeness Theorem for Propositional Tableaux and Boolean Interpretations

Tableau proofs (in terms of propositional tableaux) are a strongly complete proof system for boolean interpretations.
More precisely, for every countable collection $\mathbf H$ of WFFs of propositional logic and every WFF $\mathbf A$:
:$\mathbf H \models_{\mathrm{BI} } \mathbf A$ implies $\mathbf H \vdash_{\mathrm{PT} } \mathbf A$

Proof:
Let $\mathbf A$ be a semantic consequence of $\mathbf H$ for boolean interpretations.
That is, if $v \models_{\mathrm{BI} } \mathbf H$, also $v \models_{\mathrm{BI} } \mathbf A$.
By the truth function for $\neg$, it follows that for such $v$:
:$v \not\models_{\mathrm{BI}} \neg \mathbf A$
Therefore, $\mathbf H' := \mathbf H \cup \set {\mathbf A}$ is unsatisfiable for boolean interpretations.
Since $\mathbf H'$ is countable, it follows from the Compactness Theorem for Boolean Interpretations that:
:Some finite $\mathbf H' ' \subseteq \mathbf H'$ is unsatisfiable.
By the Tableau Extension Lemma, there exists a finite finished tableau $T$ for $\mathbf H''$.
By definition of finished tableau, every branch of $T$ is finished or contradictory.
From {{Corollary|Finished Branch Lemma}}, $\Phi \sqbrk \Gamma$ is satisfiable for any finished branch $\Gamma$.
But since $\mathbf H' ' \subseteq \Phi \sqbrk \Gamma$, this would imply $\mathbf H' '$ is also satisfiable, which is a contradiction.
It follows that every branch of $T$ is contradictory.
Since $\mathbf H' ' \subseteq \mathbf H'$, replacing the hypothesis set $\mathbf H'$ of $T$ with $\mathbf H' '$ yields another propositional tableau $T'$.
Since every branch of $T'$ is contradictory, $T'$ is a tableau confutation of $\mathbf H'$.
Recalling that $\mathbf H' = \mathbf H \cup \set {\neg \mathbf A}$, we conclude that $T'$ is a tableau proof of $\mathbf A$ from $\mathbf H$:
:$\mathbf H \vdash_{\mathrm{PT} } \mathbf A$
{{qed}}
Theorem: Completeness Theorem for Propositional Tableaux and Boolean Interpretations

Tableau proofs (in terms of propositional tableaux) are a complete proof system for boolean interpretations.
That is, for every WFF $\mathbf A$:
:$\models_{\mathrm{BI} } \mathbf A$ implies $\vdash_{\mathrm{PT} } \mathbf A$

Proof:
This is a corollary of the Extended Completeness Theorem for Propositional Tableaux and Boolean Interpretations.
Namely, it is the special case $\mathbf H = \O$.
Hence the result.
{{qed}}
Theorem: König's Tree Lemma

Let $T$ be a rooted tree with an infinite number of nodes, each with a finite number of children.
Then $T$ has a branch of infinite length.

Proof:
We will show that we can choose an infinite sequence of nodes $t_0, t_1, t_2, \ldots$ of $T$ such that:
* $t_0$ is the root node;
* $t_{n + 1}$ is a child of $t_n$;
* Each $t_n$ has infinitely many descendants.
Then the sequence $t_0, t_1, t_2, \ldots$ is such a branch of infinite length.
Take the root node $t_0$.
By definition, it has a finite number of children.
Suppose that all of these childen had a finite number of descendants.
Then that would mean that $t_0$ had a finite number of descendants, and that would mean $T$ was finite.
So $t_0$ has at least one child with infinitely many descendants.
Thus, we may pick $t_1$ as any one of those children.
Now, suppose node $t_k$ has infinitely many descendants. 
As $t_k$ has a finite number of children, by the same argument as above, $t_k$ has at least one child with infinitely many descendants.
Thus we may pick $t_{k+1}$ which has infinitely many descendants.
The assertion follows by the Axiom of Dependent Choice.
{{qed}}
Theorem: König's Tree Lemma

Let $T$ be a rooted tree with an infinite number of nodes, each with a finite number of children.
Then $T$ has a branch of infinite length.

Proof:
We will show that we can choose an infinite sequence of nodes $t_0, t_1, t_2, \ldots$ of $T$ such that:
:$t_0$ is the root node
:$t_{n + 1}$ is a child of $t_n$
Then the sequence $t_0, t_1, t_2, \ldots$ is such a branch of infinite length.
Let $I$ be the set of all nodes in $T$ that have infinitely many descendants.
Define a relation $\RR$ on $I$ by letting $x \mathrel \RR y$ {{iff}} $y$ is a child of $x$.
Since $T$ has infinitely many nodes, its root node is in $I$.
Let $t \in I$.
By the premise, $t$ has a finite number of children.
{{AimForCont}} that all of these children had a finite number of descendants.
Then by Finite Union of Finite Sets is Finite, that would mean that $t$ had a finite number of descendants, contradicting the fact that $t$ is in $I$.
So $t$ has at least one child with infinitely many descendants.
That is, $\map \RR t$ is non-empty for each $t \in I$.
That is, $\RR$ is a left-total relation.
Thus by Dependent Choice for Finite Sets, there is an infinite sequence $\sequence {t_n}$ such that:
:$t_0$ is the root of $T$
:$\forall n \in \N: t_n \mathrel \RR t_{n + 1}$ (that is, $t_{n + 1}$ is a child of $t_n$).
{{qed}}
Theorem: König's Tree Lemma

Let $T$ be a rooted tree with an infinite number of nodes, each with a finite number of children.
Then $T$ has a branch of infinite length.

Proof:
Suppose $T$ is a labeled tree with root $r$.
Let $L_0 = \set r, L_1, L_2, \ldots$ be the levels of $T$.
We construct our path by starting with $r$.
Next we partition all vertices in levels higher then $L_0$ (that is, all vertices in levels $L_i$ where $i > 0$) into as many finite parts as is the cardinality of $L_1$.
In other words if $L_1 = \set {v_1, \ldots, v_n}$ then we partition the vertices (there are infinitely many of them) in $n$ parts:
:$P_1, P_2, \ldots, P_n$
This partitioning is done as follows:
Any vertex $w$ will be connected to $r$ via some $v_i$ owing to connectedness.
We put $w$ in $P_i$. 
Now since we have partitioned infinitely many vertices in finitely many parts, one of the parts will contain infinitely many vertices.
(This is also called the Infinite Pigeonhole Principle).
Let that part be $P_j$.
Choose $w_1 = v_j$ as the next vertex in our under-construction path.
Next we delete the vertex $r$ and consider the component containing $w_1$.
It is also an infinite tree with each level finite and having $w_1$ as its root.
By a similar piece of reasoning, we get a vertex $w_2$ which is adjacent to $w_1$ and has infinitely many vertices corresponding to it.
We continue building our path by choosing $w_2$ as a part of it.
By induction we can continue and get an infinite path $r w_1 w_2 \cdots$.
This proves the theorem.
{{qed}}
Theorem: Compactness Theorem for Boolean Interpretations

Let $\mathbf H$ be a countable set of WFFs of propositional logic.
Suppose $\mathbf H$ is finitely satisfiable for boolean interpretations.
That is, suppose that every finite subset $\mathbf H' \subseteq \mathbf H$ is satisfiable for boolean interpretations.
Then $\mathbf H$ has a model.

Proof:
Suppose $\mathbf H$ does '''not''' have a model.
By the Main Lemma of Propositional Tableaux, $\mathbf H$ has a tableau confutation $T$.
By Tableau Confutation contains Finite Tableau Confutation, $T$ may be assumed to be finite.
Hence the set $\mathbf H'$ of all WFFs in $\mathbf H$ used somewhere in $T$ is finite.
Now, let $T'$ be the labeled tree which is the same as $T$ but with root $\mathbf H'$ instead of $\mathbf H$.
Then $T'$ is a tableau confutation of $\mathbf H'$.
By the Tableau Confutation implies Unsatisfiable, $\mathbf H'$ has no models.
But this contradicts the assumption that all finite subsets of $\mathbf H$ have models.
Hence the result.
{{qed}}
Theorem: Compactness Theorem for Boolean Interpretations

Let $\mathbf H$ be a countable set of WFFs of propositional logic.
Suppose $\mathbf H$ is finitely satisfiable for boolean interpretations.
That is, suppose that every finite subset $\mathbf H' \subseteq \mathbf H$ is satisfiable for boolean interpretations.
Then $\mathbf H$ has a model.

Proof:
If $\mathbf H$ is finite, the result is trivial.
So let $\mathbf H = \set {\mathbf A_n: n \in \N}$ be an enumeration of $\mathbf H$.
Define $\mathbf H_m = \set {\mathbf A_n: n \le m}$.
Let $T_1$ be the propositional tableau consisting of only a root node with hypothesis set $\mathbf H_1$.
For each $m \in \N$, construct $T_{m + 1}$ from $T_m$ by applying the Tableau Extension Lemma to $\mathbf H_{m + 1}$.
This provides us with a sequence $\sequence {T_m}_{m \mathop \in \N}$ of finished propositional tableaus.
The $T_m$ form an exhausting sequence of sets for the infinite propositional tableau $\ds T = \bigcup_{m \mathop = 1}^\infty T_m$.
If $T$ has a finished branch $\Gamma$, then by Finished Branch Lemma: Corollary:
:$\Phi \sqbrk \Gamma$ is satisfiable
and hence $\mathbf H$ is satisfiable (since $\mathbf H \subseteq \Phi \sqbrk \Gamma$).
Suppose $T$ has no finite finished branches.
Let $T'$ be the subtree of $T$ given by:
:$t \in T'$ {{iff}} $t$ is on a finished branch $\Gamma_m$ of every $T_m$ such that $t \in T_m$
Suppose the root node $r_T$ of $T$ were not in $T'$.
Then for some $T_m$, $r_T$ would not be on a finished branch of $T_m$.
But since $T_m$ is finished, every branch of $T_m$ is finished or contradictory.
Hence every branch of $T_m$ is contradictory.
But then $T_m$ is a tableau confutation of $\mathbf H_m$.
By Tableau Confutation implies Unsatisfiable, this contradicts the assumption that $\mathbf H_m$ is satisfiable.
Therefore, $r_T$ is in $T'$.
Suppose $T'$ were finite.
Let $t$ be a leaf of $T'$, which exists by Finite Tree has Leaf Nodes.
Suppose $t$ were a leaf of $T$.
Then $\Gamma_t$, the branch of $T$ identified by Leaf of Rooted Tree is on One Branch, is finished.
For, as any $T_m$ is a subtree of $T$, $\Gamma_t$ is the only branch of $T_m$ such that $t \in \Gamma_t$.
The conclusion follows from the definition of $T'$.
But then $\Gamma_t$ would be a finite finished branch of $T$, a contradiction.
Therefore, $T'$ cannot be finite.
Hence, $T'$ is a finitely branching tree.
By König's Tree Lemma, $T'$ has an infinite branch $\Gamma$.
By definition of $T'$, the branch $\Gamma_m := \Gamma \cap T_m$ of $T_m$ is finished for each $m \in \N$.
If $\Gamma$ were contradictory, then $\mathbf A \in \Gamma$ and $\neg\mathbf A \in \Gamma$ for some WFF $\mathbf A$.
But then $\mathbf A, \neg \mathbf A \in \Gamma_m$ for some $m \in \N$, contradicting that $\Gamma_m$ is finished.
Also, if $\mathbf A$ occurs on $\Gamma$, then it occurs on some $\Gamma_m$.
Since $\Gamma_m$ is finished, it follows that $\mathbf A$ is used on $\Gamma_m$, and hence on $\Gamma$.
In conclusion, $\Gamma$ is finished.
As established above, it follows that $\mathbf H$ is satisfiable for boolean interpretations.
{{qed}}
Theorem: Prefix of WFF of Predicate Logic is not WFF

Let $\mathbf A$ be a WFF of predicate logic.
Let $\mathbf S$ be a prefix of $\mathbf A$.
Then $\mathbf S$ is not a WFF of predicate logic.

Proof:
Let $\map l {\mathbf Q}$ denote the length of a string $\mathbf Q$.
By definition, $\mathbf S$ is a prefix of $\mathbf A$ iff $\mathbf A = \mathbf{ST}$ for some non-null string $\mathbf T$.
Thus we note that $\map l {\mathbf S} < \map l {\mathbf A}$.
The proof proceeds by induction on $\map l {\mathbf A}$.
Theorem: Language of Predicate Logic has Unique Parsability

Each WFF of predicate logic which starts with a left bracket or a negation sign has exactly one main connective.
{{Explain|probably, in the correct formulation of 'main connective', the quantifiers ought to be connectives as well}}

Proof:
We have the following cases:
# $\mathbf A = \neg \mathbf B$, where $\mathbf B$ is a WFF of length $k$.
# $\mathbf A = \paren {\mathbf B \circ \mathbf C}$ where $\circ$ is one of the binary connectives.
# $\mathbf A = \map p {t_1, t_2, \ldots, t_n}$, where $t_1, t_2, \ldots, t_n$ are terms, and $p \in \PP_n$.
# $\mathbf A = \paren {Q x: \mathbf B}$, where $\mathbf B$ is a WFF of length $k - 5$, $Q$ is a quantifier ($\forall$ or $\exists$) and $x$ is a variable.
We deal with these in turn.
Cases 1 and 2 are taken care of by Language of Propositional Logic has Unique Parsability.
Cases 3 and 4 do not start with either a left bracket or a negation sign, so do not have to be investigated. 
{{proof wanted|clearly, under the new, correct formal grammar, case 4 ''does'' need investigation}}
{{qed}}
Theorem: Quantifier has Unique Scope

Let $\mathbf A$ be a WFF of predicate logic.
Let $Q$ be an occurrence of a quantifier in $\mathbf A$.
Then there exists a unique well-formed part of $\mathbf A$ which (omitting outermost parentheses) begins with that occurrence $Q$.
This unique well-formed part of $\mathbf A$ is called the scope of the occurrence of $Q$.

Proof:
=== Existence ===
First, from the rules of formation of predicate logic, we have that whenever a quantifier is included in a WFF, it appears in the form:
:$\paren {Q x: \mathbf B }$
where $\mathbf B$ is itself a WFF.
Hence it is clear that $\paren {Q x: \mathbf B}$ is a well-formed part of $\mathbf A$ which begins with $Q$.
{{qed|lemma}}
Theorem: Restriction of Operation Distributivity

Let $\struct {S, *, \circ}$ be an algebraic structure.
Let $T \subseteq S$.
If the operation $\circ$ is distributive over $*$ in $\struct {S, *, \circ}$, then it is also distributive over $*$ on a restriction $\struct {T, * \restriction_T, \circ \restriction_T}$.

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = T \subseteq S
      | c = 
}}
{{eqn | ll= \leadsto
      | o = 
      | r = \forall a, b, c \in T: a, b, c \in S
      | c = {{Defof|Subset}}
}}
{{eqn | ll= \leadsto
      | o = 
      | r = a \circ_T \paren {b *_T c}
      | c = 
}}
{{eqn | r = a \circ \paren {b * c}
      | c = 
}}
{{eqn | r = \paren {a \circ b} * \paren {a \circ c}
      | c = as $\circ$ is distributive over $*$
}}
{{eqn | r = \paren {a \circ_T b} *_T \paren {a \circ_T c}
      | c = 
}}
{{end-eqn}}
Similarly for $\paren {a *_T b} \circ_T c = \paren {a \circ_T c} *_T \paren {b \circ_T c}$.
{{Qed}}
Category:Abstract Algebra
Category:Distributive Operations
hgc9ngx5b162m5fnffe39r9pr7abrz7
Theorem: Disjunction of Conjunctions

:$\paren {p \land q} \lor \paren {r \land s} \vdash p \lor r$

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, in all cases the truth values under the main connectives match for all boolean interpretations.
:<nowiki>$\begin {array} {|ccc||ccccccccc|} \hline
p & \iff & q & (p & \land & q) & \lor & (\neg & p & \land & \neg & q) \\
\hline
\F & \T & \F & \F & \F & \F & \T & \T & \F & \T & \T & \F \\
\F & \F & \T & \F & \F & \T & \F & \T & \F & \F & \F & \T \\
\T & \F & \F & \T & \F & \F & \F & \F & \T & \F & \T & \F \\
\T & \T & \T & \T & \T & \T & \T & \F & \T & \F & \F & \T \\
\hline
\end {array}$</nowiki>
{{qed}}
Theorem: Disjunction of Conjunctions

:$\paren {p \land q} \lor \paren {r \land s} \vdash p \lor r$

Proof:
{{BeginTableau|\vdash \paren {p \iff q} \iff \paren {\paren {p \land q} \lor \paren {\neg p \land \neg q} } }}
{{Assumption        |1|p \iff q}}
{{SequentIntro      |2|1|\paren {p \land q} \lor \paren {\neg p \land \neg q}|1|Biconditional as Disjunction of Conjunctions: Formulation 1}}
{{Implication       |3| |\paren {p \iff q} \implies \paren {\paren {p \land q} \lor \paren {\neg p \land \neg q} }|1|2}}
{{Assumption        |4|\paren {p \land q} \lor \paren {\neg p \land \neg q} }}
{{SequentIntro      |5|4|p \iff q|4|Biconditional as Disjunction of Conjunctions: Formulation 1}}
{{Implication       |6| |\paren {\paren {p \land q} \lor \paren {\neg p \land \neg q} } \implies \paren {p \iff q}|4|5}}
{{BiconditionalIntro|7| |\paren {p \iff q} \iff \paren {\paren {p \land q} \lor \paren {\neg p \land \neg q} }|3|6}}
{{EndTableau}}
{{qed}}
Theorem: Disjunction of Conjunctions

:$\paren {p \land q} \lor \paren {r \land s} \vdash p \lor r$

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, in all cases the truth values under the main connective is true for all boolean interpretations.
$\begin{array}{|ccc|c|ccccccccc|} \hline
(p & \iff & q) & \iff & ((p & \land & q) & \lor & (\neg & p & \land & \neg & q)) \\
\hline
\F & \T & \F & \T & \F & \F & \F & \T & \T & \F & \T & \T & \F \\
\F & \F & \T & \T & \F & \F & \T & \F & \T & \F & \F & \F & \T \\
\T & \F & \F & \T & \T & \F & \F & \F & \F & \T & \F & \T & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \F & \T & \F & \F & \T \\
\hline
\end{array}$
{{qed}}
Theorem: Disjunction of Conjunctions

:$\paren {p \land q} \lor \paren {r \land s} \vdash p \lor r$

Proof:
{{BeginTableau|\paren {p \land q} \lor \paren {r \land s} \vdash p \lor r}}
{{Premise|1|\paren {p \land q} \lor \paren {r \land s} }}
{{Assumption|2|p \land q}}
{{Simplification|3|2|p|2|1}}
{{Addition|4|2|p \lor r|3|1}}
{{Assumption|5|r \land s}}
{{Simplification|6|5|r|5|1}}
{{Addition|7|5|p \lor r|6|2}}
{{ProofByCases|8|1|p \lor r|1|2|4|5|7}}
{{EndTableau|qed}}
Category:Conjunction
Category:Disjunction
81d3q7moxhydex7m2ygsqr26l8vxt1z
Theorem: Disjunction of Conjunctions

:$\paren {p \land q} \lor \paren {r \land s} \vdash p \lor r$

Proof:
{{begin-eqn}}
{{eqn | l = p \oplus q
      | o = \dashv \vdash
      | r = \neg \left ({p \iff q}\right)
      | c = Exclusive Or is Negation of Biconditional
}}
{{eqn | o = \dashv \vdash
      | r = \left({\neg p \land q}\right) \lor \left({p \land \neg q}\right)
      | c = Non-Equivalence as Disjunction of Conjunctions
}}
{{end-eqn}}
{{qed}}
Theorem: Disjunction of Conjunctions

:$\paren {p \land q} \lor \paren {r \land s} \vdash p \lor r$

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} {|ccc||ccccccccc|} \hline
p & \oplus & q & (\neg & p & \land & q) & \lor & (p & \land & \neg & q) \\
\hline
\F & \F & \F & \T & \F & \F & \F & \F & \F & \F & \T & \F \\
\F & \T & \T & \T & \F & \T & \T & \T & \F & \F & \F & \T \\
\T & \T & \F & \F & \T & \F & \F & \T & \T & \T & \T & \F \\
\T & \F & \T & \F & \T & \F & \T & \F & \T & \F & \F & \T \\
\hline
\end {array}$</nowiki>
{{qed}}
Theorem: Disjunction of Conjunctions

:$\paren {p \land q} \lor \paren {r \land s} \vdash p \lor r$

Proof:
{{BeginTableau|\neg \paren {p \iff q} \vdash \paren {\neg p \land q} \lor \paren {p \land \neg q} }}
{{Premise|1|\neg \paren {p \iff q} }}
{{SequentIntro|2|1|\neg \paren {\paren {p \implies q} \land \paren {q \implies p} }|1
  |Rule of Material Equivalence}}
{{SequentIntro|3|1|\neg \paren {\paren {\neg p \lor q} \land \paren {\neg q \lor p} }|2
  |Rule of Material Implication (twice)}}
{{DeMorgan|4|1|\neg \paren {\neg p \lor q} \lor \neg \paren {\neg q \lor p}|3|Disjunction of Negations}}
{{DeMorgan|5|1|\paren {\neg \neg  p \land \neg q} \lor \paren {\neg \neg q \land \neg p}|4|Conjunction of Negations}}
{{DoubleNegElimination|6|1|\paren {p \land \neg q} \lor \paren {q \land \neg p}|5}}
{{Commutation|7|1|\paren {p \land \neg q} \lor \paren {\neg p \land q}|6|Conjunction}}
{{Commutation|8|1|\paren {\neg p \land q} \lor \paren {p \land \neg q}|7|Disjunction}}
{{EndTableau|qed}}
{{LEM|Double Negation Elimination|3}}
Theorem: Disjunction of Conjunctions

:$\paren {p \land q} \lor \paren {r \land s} \vdash p \lor r$

Proof:
=== Forward Implication: Proof ===
{{:Non-Equivalence as Disjunction of Conjunctions/Formulation 1/Forward Implication/Proof}}
=== Reverse Implication: Proof ===
{{:Non-Equivalence as Disjunction of Conjunctions/Formulation 1/Reverse Implication/Proof}}
Theorem: Disjunction of Conjunctions

:$\paren {p \land q} \lor \paren {r \land s} \vdash p \lor r$

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}{|cccc||ccccccccc|} \hline
\neg & (p & \iff & q) & (\neg & p & \land & q) & \lor & (p & \land & \neg & q) \\
\hline
\F & \F & \T & \F & \T & \F & \F & \F & \F & \F & \F & \T & \F \\
\T & \F & \F & \T & \T & \F & \T & \T & \T & \F & \F & \F & \T \\
\T & \T & \F & \F & \F & \T & \F & \F & \T & \T & \T & \T & \F \\
\F & \T & \T & \T & \F & \T & \F & \T & \F & \T & \F & \F & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Disjunction of Conjunctions

:$\paren {p \land q} \lor \paren {r \land s} \vdash p \lor r$

Proof:
{{BeginTableau|\paren {\neg p \land q} \lor \paren {p \land \neg q} \vdash \neg \paren {p \iff q} }}
{{Premise|1|\paren {\neg p \land q} \lor \paren {p \land \neg q} }}
{{Commutation|2|1|\paren {p \land \neg q} \lor \paren {\neg p \land q}|1|Disjunction}}
{{Commutation|3|1|\paren {p \land \neg q} \lor \paren {q \land \neg p}|2|Conjunction}}
{{DoubleNegIntro|4|1|\paren {\neg \neg  p \land \neg q} \lor \paren {\neg \neg q \land \neg p}|3}}
{{DeMorgan|5|1|\neg \paren {\neg p \lor q} \lor \neg \paren {\neg q \lor p}|4|Conjunction of Negations}}
{{DeMorgan|6|1|\neg \paren {\paren {\neg p \lor q} \land \paren {\neg q \lor p} }|5|Disjunction of Negations}}
{{SequentIntro|7|1 |\neg \paren {\paren {p \implies q} \land \paren {q \implies p} }|6
  |Rule of Material Implication (twice)}}
{{SequentIntro|8|1|\neg \paren {p \iff q}|7|Rule of Material Equivalence}}
{{EndTableau}}
{{qed}}
Theorem: Union of Intersections

:$\paren {S_1 \cap S_2} \cup \paren {T_1 \cap T_2} \subseteq S_1 \cup T_1$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {S_1 \cap S_2} \cup \paren {T_1 \cap T_2}
      | r = \paren {\paren {S_1 \cap S_2} \cup T_1} \cap \paren {\paren {S_1 \cap S_2} \cup T_2}
      | c = Union Distributes over Intersection
}}
{{eqn | r = \paren {S_1 \cup T_1} \cap \paren {S_2 \cup T_1} \cap \paren {\paren {S_1 \cap S_2} \cup T_2}
      | c = Union Distributes over Intersection
}}
{{eqn | o = \subseteq
      | r = S_1 \cup T_1
      | c = Intersection is Subset
}}
{{end-eqn}}
{{qed}}
Theorem: Union of Symmetric Differences

Let $R, S, T$ be sets.
Then:
:$\paren {R \symdif S} \cup \paren {S \symdif T} = \paren {R \cup S \cup T} \setminus \paren {R \cap S \cap T}$
where $R \symdif S$ denotes the symmetric difference between $R$ and $S$.

Proof:
From the definition of symmetric difference, we have:
:$R \symdif S = \paren {R \setminus S} \cup \paren {S \setminus R}$
Thus, expanding:
{{begin-eqn}}
{{eqn | l = \paren {R \symdif S} \cup \paren {S \symdif T}
      | r = \paren {R \setminus S} \cup \paren {S \setminus R} \cup \paren {S \setminus T} \cup \paren {T \setminus S}
}}
{{eqn | r = \paren {\paren {R \setminus S} \cup \paren {T \setminus S} } \cup \paren {\paren {S \setminus R} \cup \paren {S \setminus T} }
}}
{{eqn | r = \paren {\paren {R \cup T} \setminus S} \cup \paren {\paren {S \setminus R} \cup \paren {S \setminus T} }
      | c = Set Difference is Right Distributive over Union
}}
{{eqn | r = \paren {\paren {R \cup T} \setminus S} \cup \paren {S \setminus \paren {R \cap T} }
      | c = De Morgan's Laws: Difference with Intersection
}}
{{eqn | r = \paren {\paren {R \cup S \cup T} \setminus S} \cup \paren {S \setminus \paren {R \cap T} }
      | c = Set Difference with Union is Set Difference
}}
{{eqn | r = \paren {R \cup S \cup T} \setminus \paren {R \cap S \cap T}
      | c = De Morgan's Laws for Difference with Intersection: Corollary
}}
{{end-eqn}}
{{qed}}