avewright/proofwiki-math huggingface dataset:
Theorem: Subset Product with Identity

Let $\struct {S, \circ}$ be a magma.
Let $\struct {S, \circ}$ have an identity element $e$.
Then $e \circ S = S \circ e = S$, where $\circ$ is understood to be the subset product with singleton.

Proof:
{{begin-eqn}}
{{eqn | l = e \circ S
      | r = \set e \circ S
      | c = {{Defof|Subset Product with Singleton}}
}}
{{eqn | r = \set {x \circ y: x \in \set e, \, y \in S}
      | c = {{Defof|Subset Product}}
}}
{{eqn | r = \set {e \circ y: y \in S}
      | c = 
}}
{{eqn | r = \set {y: y \in S}
      | c = {{Defof|Identity Element}}
}}
{{eqn | r = S
      | c =
}}
{{end-eqn}}
Thus:
:$e \circ S = S$
A similar argument shows that:
:$S \circ e = S$
{{qed}}
Category:Subset Products
jej85vhju65zvnzp2zuywdetfte9243
Theorem: Equivalence of Definitions of Normal Subset/2 implies 3

Let $\left({G, \circ}\right)$ be a group.
Let $S \subseteq G$.
Let $S$ be a normal subset of $G$ by Definition 2.
Then $S$ is a normal subset of $G$ by Definition 3.
That is, if:
:$\forall g \in G: g \circ S \circ g^{-1} = S$
or:
:$\forall g \in G: g^{-1} \circ S \circ g = S$
then:
:$\forall g \in G: g \circ S \circ g^{-1} \subseteq S$
and:
:$\forall g \in G: g^{-1} \circ S \circ g \subseteq S$

Proof:
We have that:
:$\left({\forall g \in G: g \circ S \circ g^{-1} = S}\right) \iff \left({\forall g \in G: g^{-1} \circ S \circ g = S}\right)$
The result follows by definition of set equality.
{{qed}}
Theorem: Superset Relation is Compatible with Subset Product

Let $\struct {S, \circ}$ be a magma.
Let $\circ_\PP$ be the subset product on $\powerset S$, the power set of $S$.
Then the superset relation $\supseteq$ is compatible with $\circ_\PP$.

Proof:
By Subset Relation is Compatible with Subset Product, the subset relation $\subseteq$ is compatible with $\circ_\PP$.
From Inverse of Subset Relation is Superset, the inverse of $\subseteq$ is $\supseteq$.
The result follows from Inverse of Relation Compatible with Operation is Compatible.
{{qed}}
Category:Compatible Relations
kl1zpn01t23uiib7si5niey8lm2yzpk
Theorem: Equivalence of Definitions of Normal Subset/3 iff 4

Let $\struct {G,\circ}$ be a group.
Let $S \subseteq G$.
Then:
: $S$ is a normal subset of $G$ by Definition 3
{{iff}}:
: $S$ is a normal subset of $G$ by Definition 4.
That is, the following conditions are equivalent:
: $(1) \quad \forall g \in G: g \circ S \circ g^{-1} \subseteq S$
: $(2) \quad \forall g \in G: g^{-1} \circ S \circ g \subseteq S$
: $(3) \quad \forall g \in G: S \subseteq g \circ S \circ g^{-1}$
: $(4) \quad \forall g \in G: S \subseteq g^{-1} \circ S \circ g$

Proof:
First note that:
:$(5): \quad \paren {\forall g \in G: g \circ S \circ g^{-1} \subseteq S} \iff \paren {\forall g \in G: g^{-1} \circ S \circ g \subseteq S}$
:$(6): \quad \paren {\forall g \in G: S \subseteq g \circ S \circ g^{-1}} \iff \paren {\forall g \in G: S \subseteq g^{-1} \circ S \circ g}$
which is shown by, for example, setting $h := g^{-1}$ and substituting.
Therefore:
: conditions $(1)$ and $(2)$ are equivalent
and:
: conditions $(3)$ and $(4)$ are equivalent.
It remains to be shown that condition $(1)$ is equivalent to condition $(3)$.
Suppose that $(1)$ holds.
Then:
{{begin-eqn}}
{{eqn | q = \forall g \in G
      | l = g \circ S \circ g^{-1}
      | o = \subseteq
      | r = S
}}
{{eqn | ll= \leadsto
      | l = g^{-1} \circ \paren {g \circ S \circ g^{-1} }
      | o = \subseteq
      | r = g^{-1} \circ S
      | c = Subset Relation is Compatible with Subset Product/Corollary 2
}}
{{eqn | ll= \leadsto
      | l = S \circ g^{-1}
      | o = \subseteq
      | r = g^{-1} \circ S
      | c = Subset Product within Semigroup is Associative/Corollary and the definition of inverse
}}
{{eqn | ll= \leadsto
      | l = \paren {S \circ g^{-1} } \circ g
      | o = \subseteq
      | r = \paren { g^{-1} \circ S} \circ g
      | c = Subset Relation is Compatible with Subset Product/Corollary 2
}}
{{eqn | ll= \leadsto
      | l = S
      | o = \subseteq
      | r = g^{-1} \circ S \circ g
      | c = Subset Product within Semigroup is Associative/Corollary and the definition of inverse
}}
{{end-eqn}}
Thus condition $(1)$ implies condition $(3)$.
The exact same argument, substituting $\supseteq$ for $\subseteq$ and using Superset Relation is Compatible with Subset Product instead of Subset Relation is Compatible with Subset Product proves that $(3)$ implies $(1)$.
{{explain|the necessary corollary is currently only available in subset form, but these arguments are all the same.  Alternatively, the exact same method can be used to move the gs from the right to the left as was used to move them from the left to the right.}}
{{qed}}
Theorem: Equivalence of Definitions of Normal Subset/3 and 4 imply 2

Let $\struct {G, \circ}$ be a group.
Let $S \subseteq G$.
Let $S$ be a normal subset of $G$ by Definition 3 and Definition 4.
Then $S$ is a normal subset of $G$ by Definition 2.

Proof:
By Equivalence of Definitions of Normal Subset: 3 iff 4, $S$ being a normal subset of $G$ by Definition 3 and Definition 4 implies that the following hold:
:$(1)\quad \forall g \in G: g \circ S \circ g^{-1} \subseteq S$
:$(2)\quad \forall g \in G: g^{-1} \circ S \circ g \subseteq S$
:$(3)\quad \forall g \in G: S \subseteq g \circ S \circ g^{-1}$
:$(4)\quad \forall g \in G: S \subseteq g^{-1} \circ S \circ g$
By $(1)$ and $(3)$ and definition of set equality:
:$\forall g \in G: g \circ S \circ g^{-1} = S$
By $(2)$ and $(4)$ and definition of set equality:
:$\forall g \in G: g^{-1} \circ S \circ g = S$
{{qed}}
Theorem: Equivalence of Definitions of Normal Subset/3 iff 5

Let $\struct {G, \circ}$ be a group.
Let $S \subseteq G$.
Then:
: $S$ is a normal subset of $G$ by Definition 3
{{iff}}:
: $S$ is a normal subset of $G$ by Definition 5.

Proof:
==== 3 implies 5 ====
Suppose that $S$ is a normal subset of $G$ by Definition 3.
That is:
:$\forall g \in G: g^{-1} \circ S \circ g \subseteq S$.
Let $x, y \in G$ such that $x \circ y \in S$.
Then:
{{begin-eqn}}
{{eqn | l = y \circ x
      | r = e \circ \paren {y \circ x}
      | c = {{Group-axiom|2}}
}}
{{eqn | r = \paren {x^{-1} \circ x} \circ \paren {y \circ x}
      | c = {{Group-axiom|3}}
}}
{{eqn | r = x^{-1} \circ \paren {x \circ y} \circ x
      | c = {{Group-axiom|1}}
}}
{{eqn | ll= \leadsto
      | l = y \circ x
      | o = \in
      | r = x^{-1} \circ S \circ x
      | c = $x \circ y \in S$
}}
{{eqn | ll= \leadsto
      | l = y \circ x
      | o = \in
      | r = S
      | c = {{hypothesis}}: {{Defof|Normal Subset|index = 3}}
}}
{{end-eqn}}
{{qed|lemma}}
==== 5 implies 3 ====
Suppose that $S$ is a normal subset of $G$ by Definition 5.
That is:
:$\forall x, y \in G: x \circ y \in S \implies y \circ x \in S$
Let $g \in G$.
Then:
{{begin-eqn}}
{{eqn | q = \forall x \in S
      | l = e \circ x \circ e
      | o = \in
      | r = S
      | c = {{Group-axiom|2}}
}}
{{eqn | ll= \leadsto
      | q = \forall x \in S
      | l = \paren {g \circ g^{-1} } \circ x \circ \paren {g \circ g^{-1} }
      | o = \in
      | r = S
      | c = {{Group-axiom|3}}
}}
{{eqn | ll= \leadsto
      | q = \forall x \in S
      | l = g \circ \paren {g^{-1} \circ x \circ g \circ g^{-1} }
      | o = \in
      | r = S
      | c = {{Group-axiom|1}}
}}
{{eqn | ll= \leadsto
      | q = \forall x \in S
      | l = \paren {g^{-1} \circ x \circ g \circ g^{-1} } \circ g
      | o = \in
      | r = S
      | c = {{hypothesis}}: {{Defof|Normal Subset|index = 5}}
}}
{{eqn | ll= \leadsto
      | q = \forall x \in S
      | l = \paren {g^{-1} \circ x \circ g} \circ \paren {g^{-1} \circ g}
      | o = \in
      | r = S
      | c = {{Group-axiom|1}}
}}
{{eqn | ll= \leadsto
      | q = \forall x \in S
      | l = \paren {g^{-1} \circ x \circ g} \circ e
      | o = \in
      | r = S
      | c = {{Defof|Inverse Element}}
}}
{{eqn | ll= \leadsto
      | q = \forall x \in S
      | l = g^{-1} \circ x \circ g
      | o = \in
      | r = S
      | c = {{Defof|Identity Element}}
}}
{{eqn | ll= \leadsto
      | l = g^{-1} \circ S \circ g
      | o = \subseteq
      | r = S
      | c = {{Defof|Subset Product}}
}}
{{end-eqn}}
{{qed}}
Theorem: Subgroup is Normal iff Normal Subset

Let $\left({G, \circ}\right)$ be a group.
Let $N$ be a subgroup of $G$.
Then $N$ is normal in $G$ (by definition 1) {{iff}} it is a normal subset of $G$.

Proof:
=== Necessary Condition ===
Let $N$ be normal in $G$ (by definition 1):
Thus for each $g \in G$:
:$\forall g \in G: g \circ N = N \circ g$
where $g \circ N$ denotes the subset product of $g$ with $N$.
Thus $N$ is a normal subset of $G$ (by definition 1):
:$\forall g \in G: g \circ N = N \circ g$
=== Sufficient Condition ===
Let $N$ be a normal subset of $G$ (by definition 1):
:$\forall g \in G: g \circ N = N \circ g$
Since $N$ is a subgroup, $N$ is a normal subgroup of $G$ (by definition 1).
{{Qed}}
Theorem: Rule of Explosion/Sequent Form

:$\bot \vdash \phi$

Proof:
{{BeginTableau|\bot \vdash \phi}}
{{Premise|1|\bot}}
{{Explosion|2|1|\phi|1}}
{{EndTableau}}
{{Qed}}
Category:Rule of Explosion
qvl3j0govct9cz4i06dono4n38594tf
Theorem: Law of Excluded Middle/Sequent Form

The '''Law of Excluded Middle''' can be symbolised by the sequent:
:$\vdash p \lor \neg p$

Proof:
{{BeginTableau|\vdash p \lor \neg p}}
{{ExcludedMiddle|1|p \lor \neg p}}
{{EndTableau}}
{{Qed}}
Theorem: Law of Excluded Middle/Sequent Form

The '''Law of Excluded Middle''' can be symbolised by the sequent:
:$\vdash p \lor \neg p$

Proof:
{{BeginTableau|\vdash p \lor \neg p|Instance 2 of the Hilbert-style systems}}
{{TheoremIntro|1|\paren {q \implies r} \implies \paren {\paren {p \implies q} \implies \paren {p \implies r} }|Hypothetical Syllogism}}
{{TableauLine
 | n = 2
 | f = \paren {\paren {p \lor p} \implies p} \implies \paren {\paren {p \implies \paren {p \lor p} } \implies \paren {p \implies p} }
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Rule $\text {RST} 1$
 | dep = 1
 | c = $p \lor p \, / \, q$, $p \, / \, r$
}}
{{TableauLine
 | n = 3
 | f = \paren {p \lor p} \implies p
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Axiom $\text A 1$
}}
{{TableauLine
 | n = 4
 | f = \paren {p \implies \paren {p \lor p} } \implies \paren {p \implies p}
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Rule $\text {RST} 3$
 | dep = 2, 3
}}
{{TableauLine
 | n = 5
 | f = p \implies \paren {p \lor p}
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Axiom $\text A 2$, Rule $\text {RST} 1$
 | c = $p \, / \, q$
}}
{{TableauLine
 | n = 6
 | f = p \implies p
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Rule $\text {RST} 3$
 | dep = 4, 5
}}
{{TableauLine
 | n = 7
 | f = \neg p \lor p
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Rule $\text {RST} 2 \, (2)$
 | dep = 6
}}
{{TableauLine
 | n = 8
 | f = \paren {p \lor q} \implies \paren {q \lor p}
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Axiom $\text A 3$
}}
{{TableauLine
 | n = 9
 | f = \paren {\neg p \lor p} \implies \paren {p \lor \neg p}
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Rule $\text {RST} 1$
 | dep = 8
 | c = $p \, / \, q$, $\neg p \, / \, p$
}}
{{TableauLine
 | n = 10
 | f = p \lor \neg p
 | rlnk = Definition:Hilbert Proof System/Instance 2
 | rtxt = Rule $\text {RST} 3$
 | dep = 7, 9
}}
{{EndTableau}}
{{Qed}}
Theorem: Law of Excluded Middle/Sequent Form

The '''Law of Excluded Middle''' can be symbolised by the sequent:
:$\vdash p \lor \neg p$

Proof:
We apply the Method of Truth Tables to the proposition $\vdash p \lor \neg p$.
As can be seen by inspection, the truth value of the main connective, that is $\lor$, is $\T$ for each boolean interpretation for $p$.
:<nowiki>$\begin{array}{|c|c|cc|} \hline
p & \lor & \neg & p \\
\hline
\F & \T & \T & \F \\
\T & \T & \F & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Power Structure of Monoid is Monoid

Let $\struct {G, \circ}$ be a monoid with identity $e$.
Let $\struct {\powerset G, \circ_\PP}$ be the power structure of $\struct {G, \circ}$.
Then $\struct {\powerset G, \circ_\PP}$ is a monoid with identity $\set e$.

Proof:
By definition of a monoid, $\struct {G, \circ}$ is a semigroup.
By Power Structure of Semigroup is Semigroup, $\struct {\powerset G, \circ_\PP}$ is a semigroup.
By Subset Product by Identity Singleton, $\set e$ is an identity for $\struct {\powerset G, \circ_\PP}$.
Thus $\struct {\powerset G, \circ_\PP}$ is a monoid with identity $\set e$.
{{qed}}
Category:Monoids
Category:Power Structures
q9sgpvt3gzedshrhffest4afrx52x3r
Theorem: Principle of Non-Contradiction/Sequent Form/Formulation 2

:$\vdash \neg \paren {p \land \neg p}$

Proof:
{{BeginTableau|\vdash \neg \left({p \land \neg p}\right)}}
{{Assumption|1|p \land \neg p}}
{{Simplification|2|1|p|1|1}}
{{Simplification|3|1|\neg p|1|2}}
{{NonContradiction|4|1|2|3}}
{{Contradiction|5||\neg \left({p \land \neg p}\right)|1|4}}
{{EndTableau|qed}}
Theorem: Principle of Non-Contradiction/Sequent Form/Formulation 2

:$\vdash \neg \paren {p \land \neg p}$

Proof:
We apply the Method of Truth Tables to the proposition $\neg \paren {p \land \neg p}$.
As can be seen by inspection, the truth value of the main connective, that is $\neg$, is $T$ for each boolean interpretation for $p$.
:<nowiki>$\begin {array} {|ccccc|} \hline
\neg & (p & \land & \neg & p)\\
\hline
\T & \F & \F & \T & \F \\
\T & \T & \F & \F & \T \\
\hline
\end {array}$</nowiki>
{{qed}}
Theorem: Power Structure of Semigroup is Semigroup

Let $\struct {S, \circ}$ be a semigroup.
Let $\struct {\powerset S, \circ_\PP}$ be the power structure of $\struct {S, \circ}$.
Then $\struct {\powerset S, \circ_\PP}$ is a semigroup.

Proof:
From Power Structure of Magma is Magma we conclude that $\struct {\powerset S, \circ_\PP}$ is a magma.
It follows from Subset Product within Semigroup is Associative that $\circ_\PP$ is associative in $\struct {\powerset S, \circ_\PP}$.
Thus $\struct {\powerset S, \circ_\PP}$ is a semigroup.
{{qed}}
Category:Semigroups
Category:Power Structures
0bkwr6ovkhrw7hh4yo3d3az59avwx93
Theorem: Power Structure of Group is Monoid

Let $\struct {G, \circ}$ be a group with identity $e$.
Let $\struct {\powerset G, \circ_\PP}$ be the power structure of $\struct {G, \circ}$.
Then $\struct {\powerset G, \circ_\PP}$ is a monoid with identity $\set e$.

Proof:
By definition of a group, $\struct {G, \circ}$ is a monoid.
The result follows from Power Structure of Monoid is Monoid.
{{qed}}
Category:Power Structures
Category:Monoids
Category:Group Theory
4mllzcji74j6twhcs98ka2qafla6gy9
Theorem: Power Structure of Magma is Magma

Let $\struct {S, \circ}$ be a magma.
Let $\struct {\powerset S, \circ_\PP}$ be the power structure of $\struct {S, \circ}$.
Then $\struct {\powerset S, \circ_\PP}$ is a magma.
That is, $\circ_\PP$ is closed in $\powerset S$.

Proof:
Let $\struct {S, \circ}$ be a magma.
Let $A, B \subseteq S$.
{{begin-eqn}}
{{eqn | q = \forall a \in A, b \in B
      | l = a \circ b
      | o = \in
      | r = S
      | c = {{Defof|Magma}}
}}
{{eqn | ll= \leadsto
      | l = A \circ B
      | o = \subseteq
      | r = S
      | c = {{Defof|Subset Product}}
}}
{{eqn | ll= \leadsto
      | l = A \circ_\PP B
      | o = \subseteq
      | r = S
      | c = {{Defof|Subset Product|Operation Induced on $\powerset S$ by $\circ$}}
}}
{{eqn | ll= \leadsto
      | l = A \circ_\PP B
      | o = \in
      | r = \powerset S
      | c = {{Defof|Power Set}}
}}
{{end-eqn}}
Thus $\struct {\powerset S, \circ_\PP}$ is a magma.
{{qed}}
Category:Power Structures
Category:Magmas
m2fjce26sfsgldjb51n4mpkceeuqcjl
Theorem: Element in Left Coset iff Product with Inverse in Subgroup

Let $y H$ denote the left coset of $H$ by $y$.
Then:
:$x \in y H \iff x^{-1} y \in H$

Proof:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = y H
      | c =
}}
{{eqn | ll= \leadstoandfrom
      | q = \exists h \in H
      | l = x
      | r = y h
      | c = {{Defof|Left Coset}}
}}
{{eqn | ll= \leadstoandfrom
      | q = \exists h \in H
      | l = x^{-1}
      | r = h^{-1} y^{-1}
      | c = Inverse of Group Product
}}
{{eqn | ll= \leadstoandfrom
      | q = \exists h \in H
      | l = x^{-1} y
      | r = h^{-1}
      | c = Product with $y$ on the right
}}
{{eqn | ll= \leadstoandfrom
      | l = x^{-1} y
      | o = \in
      | r = H
      | c = $H$ is a subgroup
}}
{{end-eqn}}
{{Qed}}
</onlyinclude>
Theorem: Element in Right Coset iff Product with Inverse in Subgroup

Let $H \circ y$ denote the right coset of $H$ by $y$.
Then:
:$x \in H y \iff x y^{-1} \in H$

Proof:
Let $\struct {G, *}$ be the opposite group of $G$.
Then:
:$x \in H y \iff x \in y * H$
:$x y^{-1} \in H \iff y^{-1} * x \in H$ 
Since $H$ is closed under inverses:
:$x y^{-1} \in H \iff x^{-1} * y \in H$ 
By Element in Left Coset iff Product with Inverse in Subgroup:
:$x \in y * H \iff x^{-1} * y \in H$
Hence the result.
{{Qed}}
Theorem: Inverse of Inverse of Subset of Group

Let $\struct {G, \circ}$ be a group.
Let $X \subseteq G$.
Then:
:$\paren {X^{-1} }^{-1} = X$.
where $X^{-1}$ denotes the inverse of $X$.

Proof:
{{begin-eqn}}
{{eqn | l = \paren {X^{-1} }^{-1}
      | r = \set {x^{-1}: x \in X^{-1} }
      | c = {{Defof|Inverse of Subset of Group}}
}}
{{eqn | r = \set {\paren {x^{-1} }^{-1}: x \in X}
      | c = {{Defof|Inverse of Subset of Group}}
}}
{{eqn | r = \set {x: x \in X}
      | c = Inverse of Group Inverse
}}
{{eqn | r = X
      | c = {{Defof|Set Definition by Predicate}}
}}
{{end-eqn}}
{{qed}}
Category:Group Theory
l14b6b884nvvro00chh4nwp83joss02
Theorem: Exclusive Or is Commutative

: $p \oplus q \dashv \vdash q \oplus p$

Proof:
{{BeginTableau|p \oplus q \vdash q \oplus p}}
{{Premise|1|p \oplus q}}
{{SequentIntro|2|1|\left({p \lor q} \right) \land \neg \left({p \land q}\right)|1|Definition of Exclusive Or}}
{{Commutation|3|1|\left({q \lor p} \right) \land \neg \left({p \land q}\right)|2|Disjunction}}
{{Commutation|4|1|\left({q \lor p} \right) \land \neg \left({q \land p}\right)|3|Conjunction}}
{{SequentIntro|5|1|q \oplus p|4|Definition of Exclusive Or}}
{{EndTableau}}
{{BeginTableau|q \oplus p \vdash p \oplus q}}
{{Premise|1|q \oplus p}}
{{SequentIntro|2|1|\left({q \lor p} \right) \land \neg \left({q \land p}\right)|1|Definition of Exclusive Or}}
{{Commutation|3|1|\left({q \lor p} \right) \land \neg \left({p \land q}\right)|2|Conjunction}}
{{Commutation|4|1|\left({p \lor q} \right) \land \neg \left({p \land q}\right)|3|Disjunction}}
{{SequentIntro|5|1|p \oplus q|4|Definition of Exclusive Or}}
{{EndTableau}}
{{qed}}
Theorem: Exclusive Or is Commutative

: $p \oplus q \dashv \vdash q \oplus p$

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||ccc|} \hline
p & \oplus & q & q & \oplus & p \\
\hline
F & F & F & F & F & F \\
F & T & T & T & T & F \\
T & T & F & F & T & T \\
T & F & T & T & F & T \\
\hline
\end{array}$
{{qed}}
Theorem: Exclusive Or is Associative

Exclusive or is associative:
:$p \oplus \paren {q \oplus r} \dashv \vdash \paren {p \oplus q} \oplus 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.
$\begin{array}{|ccccc||ccccc|} \hline
p & \oplus & (q & \oplus & r) & (p & \oplus & q) & \oplus & r \\
\hline
\F & \F & \F & \F & \F & \F & \F & \F & \F & \F \\
\F & \T & \F & \T & \T & \F & \F & \F & \T & \T \\
\F & \T & \T & \T & \F & \F & \T & \T & \T & \F \\
\F & \F & \T & \F & \T & \F & \T & \T & \F & \T \\
\T & \T & \F & \F & \F & \T & \T & \F & \T & \F \\
\T & \F & \F & \T & \T & \T & \T & \F & \F & \T \\
\T & \F & \T & \T & \F & \T & \F & \T & \F & \F \\
\T & \T & \T & \F & \T & \T & \F & \T & \T & \T \\
\hline
\end{array}$
{{qed}}
Theorem: Exclusive Or with Itself

Exclusive or destroys copies of itself:
:$p \oplus p \dashv \vdash \bot$

Proof:
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connective match for each boolean interpretations.
$\begin{array}{|ccc|} \hline
p & \oplus & p \\
\hline
\F & \F & \F \\
\T & \F & \T \\
\hline
\end{array}$
{{qed}}
Theorem: Non-Equivalence as Disjunction of Conjunctions/Formulation 1/Proof 1

: $\neg \left ({p \iff q}\right) \dashv \vdash \left({\neg p \land q}\right) \lor \left({p \land \neg q}\right)$

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: Non-Equivalence as Disjunction of Conjunctions/Formulation 1

:$\neg \paren {p \iff q} \dashv \vdash \paren {\neg p \land q} \lor \paren {p \land \neg q}$

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: Non-Equivalence as Disjunction of Conjunctions/Formulation 1

:$\neg \paren {p \iff q} \dashv \vdash \paren {\neg p \land q} \lor \paren {p \land \neg q}$

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: Non-Equivalence as Disjunction of Conjunctions/Formulation 1

:$\neg \paren {p \iff q} \dashv \vdash \paren {\neg p \land q} \lor \paren {p \land \neg q}$

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: Non-Equivalence as Disjunction of Conjunctions/Formulation 1

:$\neg \paren {p \iff q} \dashv \vdash \paren {\neg p \land q} \lor \paren {p \land \neg q}$

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: Exclusive Or is Negation of Biconditional

Exclusive or is equivalent to the negation of the biconditional:
:$p \oplus q \dashv \vdash \neg \paren {p \iff q}$

Proof:
{{begin-eqn}}
{{eqn | l = p \oplus q
      | o = \dashv \vdash
      | r = \paren {p \lor q} \land \neg \paren {p \land q}
      | c = {{Defof|Exclusive Or}}
}}
{{eqn | o = \dashv \vdash
      | r = \neg \paren {p \iff q}
      | c = Non-Equivalence as Conjunction of Disjunction with Negation of Conjunction
}}
{{end-eqn}}
{{qed}}