avewright/proofwiki-math huggingface dataset:
Theorem: Hypothetical Syllogism

The '''(rule of the) hypothetical syllogism''' is a valid deduction sequent in propositional logic:
{{begin-itemize}}
{{item||If we can conclude both:
{{begin-itemize}}
{{item||that $p$ implies $q$}}
{{item||that $q$ implies $r$}}
{{end-itemize}} }}
{{item||then we may infer that $p$ implies $r$.}}
{{end-itemize}}

Proof:
We apply the Method of Truth Tables to the propositions in turn.
As can be seen for all boolean interpretations by inspection, where the truth values under the main connective on the {{LHS}} (that is, the rightmost $\land$) is $\T$, that under the instance of $r$ on the {{RHS}} is also $\T$:
:<nowiki>$\begin{array}{|ccccccccc||c|} \hline
((p & \implies & q) & \land & (q & \implies & r)) & \land & p & r \\
\hline
\F & \T & \F & \T & \F & \T & \F & \F & \F & \F \\
\F & \T & \F & \T & \F & \T & \T & \F & \F & \T \\
\F & \T & \T & \F & \T & \F & \F & \F & \F & \F \\
\F & \T & \T & \T & \T & \T & \T & \F & \F & \T \\
\T & \F & \F & \F & \F & \T & \F & \F & \T & \F \\
\T & \F & \F & \F & \F & \T & \T & \F & \T & \T \\
\T & \T & \T & \F & \T & \F & \F & \F & \T & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
Hence the result.
{{qed}}
Theorem: Hypothetical Syllogism

The '''(rule of the) hypothetical syllogism''' is a valid deduction sequent in propositional logic:
{{begin-itemize}}
{{item||If we can conclude both:
{{begin-itemize}}
{{item||that $p$ implies $q$}}
{{item||that $q$ implies $r$}}
{{end-itemize}} }}
{{item||then we may infer that $p$ implies $r$.}}
{{end-itemize}}

Proof:
Let us use the following abbreviations:
{{begin-eqn}}
{{eqn | l = \phi
      | o = \text{ for }
      | r = p \implies q
      | c = 
}}
{{eqn | l = \psi
      | o = \text{ for }
      | r = q \implies r
      | c = 
}}
{{eqn | l = \chi
      | o = \text{ for }
      | r = p \implies r
      | c = 
}}
{{end-eqn}}
{{BeginTableau|\vdash \paren {\phi \land \psi} \implies \chi}}
{{Assumption|1|\phi \land \psi}}
{{Simplification|2|1|\phi|1|1}}
{{Simplification|3|1|\psi|1|2}}
{{SequentIntro|4|1|\chi|2, 3|{{Formulation|Hypothetical Syllogism|1}}}}
{{Implication|5||\paren {\phi \land \psi} \implies \chi|1|4}}
{{EndTableau}}
Expanding the abbreviations leads us back to:
:$\paren {\paren {p \implies q} \land \paren {q \implies r} } \implies \paren {p \implies r}$
{{qed}}
Theorem: Hypothetical Syllogism

The '''(rule of the) hypothetical syllogism''' is a valid deduction sequent in propositional logic:
{{begin-itemize}}
{{item||If we can conclude both:
{{begin-itemize}}
{{item||that $p$ implies $q$}}
{{item||that $q$ implies $r$}}
{{end-itemize}} }}
{{item||then we may infer that $p$ implies $r$.}}
{{end-itemize}}

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}{|ccccccc|c|ccc|} \hline
((p & \implies & q) & \land & (q & \implies & r)) & \implies & (p & \implies & r) \\
\hline
\F & \T & \F & \T & \F & \T & \F & \T & \F & \T & \F \\
\F & \T & \F & \T & \F & \T & \T & \T & \F & \T & \T \\
\F & \T & \T & \T & \T & \F & \F & \T & \F & \T & \F \\
\F & \T & \T & \T & \T & \T & \T & \T & \F & \T & \T \\
\T & \F & \F & \F & \F & \T & \F & \T & \T & \F & \F \\
\T & \F & \F & \T & \F & \T & \T & \T & \T & \T & \T \\
\T & \T & \T & \F & \T & \F & \F & \T & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Hypothetical Syllogism

The '''(rule of the) hypothetical syllogism''' is a valid deduction sequent in propositional logic:
{{begin-itemize}}
{{item||If we can conclude both:
{{begin-itemize}}
{{item||that $p$ implies $q$}}
{{item||that $q$ implies $r$}}
{{end-itemize}} }}
{{item||then we may infer that $p$ implies $r$.}}
{{end-itemize}}

Proof:
Let us use the following abbreviations
{{begin-eqn}}
{{eqn | l = \phi
      | o = \text{ for }
      | r = p \implies q
}}
{{eqn | l = \psi
      | o = \text{ for }
      | r = q \implies r
}}
{{eqn | l = \chi
      | o = \text{ for }
      | r = p \implies r
}}
{{end-eqn}}
{{BeginTableau|\paren {p \implies q} \implies \paren {\paren {q \implies r} \implies \paren {p \implies r} } }}
{{TheoremIntro|1|\paren {\phi \land \psi} \implies \chi|Hypothetical Syllogism: Formulation 3}}
{{SequentIntro|2||\phi \implies \paren {\psi \implies \chi}|1|Rule of Exportation}}
{{EndTableau}}
Expanding the abbreviations leads us back to:
:$\vdash \paren {p \implies q} \implies \paren {\paren {q \implies r} \implies \paren {p \implies r} }$
{{qed}}
Theorem: Hypothetical Syllogism

The '''(rule of the) hypothetical syllogism''' is a valid deduction sequent in propositional logic:
{{begin-itemize}}
{{item||If we can conclude both:
{{begin-itemize}}
{{item||that $p$ implies $q$}}
{{item||that $q$ implies $r$}}
{{end-itemize}} }}
{{item||then we may infer that $p$ implies $r$.}}
{{end-itemize}}

Proof:
{{BeginTableau|\paren {p \implies q} \implies \paren {\paren {q \implies r} \implies \paren {p \implies r} } }}
{{Assumption|1|p \implies q}}
{{Assumption|2|p}}
{{Assumption|3|q \implies r}}
{{ModusPonens|4|1,2|q|1|2}}
{{ModusPonens|5|1,2,3|r|3|4}}
{{Implication|6|1,3|p \implies r|2|5}}
{{Implication|7|1|\paren {q \implies r} \implies \paren {p \implies r}|3|6}}
{{Implication|8||\paren {p \implies q} \implies \paren {\paren {q \implies r} \implies \paren {p \implies r} }|1|7}}
{{EndTableau|qed}}
Theorem: Hypothetical Syllogism

The '''(rule of the) hypothetical syllogism''' is a valid deduction sequent in propositional logic:
{{begin-itemize}}
{{item||If we can conclude both:
{{begin-itemize}}
{{item||that $p$ implies $q$}}
{{item||that $q$ implies $r$}}
{{end-itemize}} }}
{{item||then we may infer that $p$ implies $r$.}}
{{end-itemize}}

Proof:
{{BeginTableau|\vdash \paren {p \implies q} \implies \paren {\paren {q \implies r} \implies \paren {p \implies r} }|instance 1 of a Hilbert proof system}}
{{Assumption|1|p}}
{{Assumption|2|p \implies q}}
{{ModusPonens|3|1, 2|q|1|2}}
{{Assumption|4|q \implies r}}
{{ModusPonens|5|1, 2, 4|r|3|4}}
{{TableauLine|n = 6
  | pool = 2, 4
  | f = p \implies r
  | rlnk = Deduction Theorem
  | rtxt = Deduction Theorem
  | dep  = 1, 5
  | c = Assumption $1$ has been discharged
}}
{{TableauLine|n = 7
  | pool = 2
  | f = \paren {q \implies r} \implies \paren {p \implies r}
  | rlnk = Deduction Theorem
  | rtxt = Deduction Theorem
  | dep  = 4, 6
  | c = Assumption $4$ has been discharged
}}
{{TableauLine|n = 8
  | f = \paren {p \implies q} \implies \paren {\paren {q \implies r} \implies \paren {p \implies r} }
  | rlnk = Deduction Theorem
  | rtxt = Deduction Theorem
  | dep  = 2, 7
  | c = Assumption $2$ has been discharged
}}
{{EndTableau|qed}}
Theorem: Hypothetical Syllogism

The '''(rule of the) hypothetical syllogism''' is a valid deduction sequent in propositional logic:
{{begin-itemize}}
{{item||If we can conclude both:
{{begin-itemize}}
{{item||that $p$ implies $q$}}
{{item||that $q$ implies $r$}}
{{end-itemize}} }}
{{item||then we may infer that $p$ implies $r$.}}
{{end-itemize}}

Proof:
Let us use the following abbreviations
{{begin-eqn}}
{{eqn | l = \phi
      | o = \text{ for }
      | r = p \implies q
      | c = 
}}
{{eqn | l = \psi
      | o = \text{ for }
      | r = q \implies r
      | c = 
}}
{{eqn | l = \chi
      | o = \text{ for }
      | r = p \implies r
      | c = 
}}
{{end-eqn}}
From Hypothetical Syllogism: Formulation 3 we have:
:$(1): \quad \vdash \paren {\paren {p \implies q} \land \paren {q \implies r} } \implies \paren {p \implies r}$
{{BeginTableau|\paren {q \implies r} \implies \paren {\paren {p \implies q} \implies \paren {p \implies r} } }}
{{Assumption|1|\psi \land \phi}}
{{Commutation|2|1|\phi \land \psi|1|Conjunction}}
{{SequentIntro|3|1|\chi|2|Hypothetical Syllogism: Formulation 3 (see $(1)$ above)}}
{{Implication|4||\paren {\psi \land \phi} \implies \chi|1|3}}
{{SequentIntro|5||\psi \implies \paren {\phi \implies \chi}|4|Rule of Exportation}}
{{EndTableau}}
Expanding the abbreviations leads us back to:
:$\vdash \paren {q \implies r} \implies \paren {\paren {p \implies q} \implies \paren {p \implies r} }$
{{qed}}
Theorem: Hypothetical Syllogism

The '''(rule of the) hypothetical syllogism''' is a valid deduction sequent in propositional logic:
{{begin-itemize}}
{{item||If we can conclude both:
{{begin-itemize}}
{{item||that $p$ implies $q$}}
{{item||that $q$ implies $r$}}
{{end-itemize}} }}
{{item||then we may infer that $p$ implies $r$.}}
{{end-itemize}}

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

The '''(rule of the) hypothetical syllogism''' is a valid deduction sequent in propositional logic:
{{begin-itemize}}
{{item||If we can conclude both:
{{begin-itemize}}
{{item||that $p$ implies $q$}}
{{item||that $q$ implies $r$}}
{{end-itemize}} }}
{{item||then we may infer that $p$ implies $r$.}}
{{end-itemize}}

Proof:
{{BeginTableau|\vdash \paren {q \implies r} \implies \paren {\paren {p \implies q} \implies \paren {p \implies r} } }}
{{Assumption|1|q \implies r}}
{{Assumption|2|p \implies q}}
{{Assumption|3|p}}
{{ModusPonens|4|2,3|q|2|3}}
{{ModusPonens|5|1,2,3|r|1|4}}
{{Implication|6|1,2|p \implies r|3|5}}
{{Implication|7|1|\paren {p \implies q} \implies \paren {p \implies r}|2|6}}
{{Implication|8||\paren {q \implies r} \implies \paren {\paren {p \implies q} \implies \paren {p \implies r} }|1|7}}
{{EndTableau|qed}}
Theorem: Extended Rule of Implication

Any sequent can be expressed as a theorem.
That is:
:$P_1, P_2, P_3, \ldots, P_n \vdash Q$
means the same thing as:
:$\vdash P_1 \implies \paren {P_2 \implies \paren {P_3 \implies \paren {\ldots \implies \paren {P_n \implies Q} \ldots} } }$
The latter expression is known as the corresponding conditional of the former.
Thus every sequent containing the symbol $\vdash$ can, if so desired, be expressed in the form of a theorem which has $\implies$.

Proof:
From the Rule of Conjunction, we note the following.
Any sequent:
:$P_1, P_2 \vdash Q$
can be expressed as:
:$P_1 \land p_2 \vdash Q$
Also, from the Rule of Simplification, any sequent:
:$P_1 \land P_2 \vdash Q$
can be expressed as:
:$P_1, P_2 \vdash Q$
Consider the expression:
:$P_1, P_2, P_3, \ldots, P_{n - 1}, P_n \vdash Q$
By repeated application of the above, we can arrive at:
:$P_1 \land \paren {P_2 \land \paren {P_3 \land \paren {\ldots \land \paren {P_{n - 1} \land P_n} \ldots} } } \vdash Q$
For convenience, the Rule of Substitution can be used to substitute $R_1$ for:
:$P_2 \land \paren {P_3 \land \paren {\ldots \land \paren {P_{n - 1} \land P_n} \ldots} }$
to get:
:$P_1 \land R_1 \vdash Q$
From the Rule of Implication:
:$\vdash \paren {P_1 \land R_1} \implies Q$
Using the Rule of Exportation, we then get:
:$\vdash P_1 \implies \paren {R_1 \implies Q}$
Substituting back for $R_1$:
:$\vdash P_1 \implies \paren {\paren {P_2 \land \paren {P_3 \land \paren {\ldots \land \paren {P_{n - 1} \land P_n} \ldots} } } \implies Q}$
Making a substitution of convenience again, substitute $R_2$ for:
:$P_3 \land \paren {\ldots \land \paren {P_{n - 1} \land P_n} \ldots}$
Take the expression:
:$\paren {P_2 \land R_2} \implies Q$
and express it as:
:$P_2 \land R_2 \vdash Q$
and use the Rule of Exportation to get:
:$P_2 \implies \paren {R_2 \implies Q}$
which, substituting back for $R_2$, gives:
:$P_2 \implies \paren {\paren {P_3 \land \paren {\ldots \land \paren {P_{n - 1} \land P_n} \ldots} } \implies Q}$
Similarly:
:$\paren {P_3 \land \paren {\ldots \land \paren {P_{n - 1} \land P_n} \ldots} } \implies Q$
converts to:
:$P_3 \implies \paren {\paren {\ldots \land \paren {P_{n - 1} \land P_n} \ldots} \implies Q}$
The pattern becomes apparent.
Eventually:
:$\paren {P_{n - 1} \land P_n} \implies Q$
which converts to:
:$P_{n - 1} \implies \paren {P_n \implies Q}$
Substituting these back into our original expression:
:$\vdash P_1 \implies \paren {P_2 \implies \paren {P_3 \implies \paren {\ldots \implies \paren {P_n \implies Q} \ldots} } }$
{{qed}}
Theorem: Equivalences are Interderivable

If two propositional formulas are interderivable, they are equivalent:
:$\paren {p \dashv \vdash q} \dashv \vdash \paren {p \iff q}$

Proof:
Let $v$ be an arbitrary interpretation.
Then by definition of interderivable:
:$\map v {p \iff q}$ {{iff}} $\map v p = \map v q$
Since $v$ is arbitrary, $\map v p = \map v q$ holds in all interpretations.
That is:
:$p \dashv \vdash q$
{{qed}}
Theorem: Equivalences are Interderivable

If two propositional formulas are interderivable, they are equivalent:
:$\paren {p \dashv \vdash q} \dashv \vdash \paren {p \iff q}$

Proof:
The result follows directly from the truth table for the biconditional:
:<nowiki>$\begin {array} {|cc||ccc|} \hline
p & q & p & \iff & q \\
\hline
\F & \F & \F & \T & \F \\
\F & \T & \F & \F & \T \\
\T & \F & \T & \F & \F \\
\T & \T & \T & \T & \T \\
\hline
\end {array}$</nowiki>
By inspection, it is seen that $\map \MM {p \iff q} = \T$ {{iff}} $\map \MM p = \map \MM q$.
{{qed}}
Theorem: Union is Commutative

Set union is commutative:
:$S \cup T = T \cup S$

Proof:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \paren {S \cup T}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x \in S
      | o = \lor
      | r = x \in T
      | c = {{Defof|Set Union}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x \in T
      | o = \lor
      | r = x \in S
      | c = Disjunction is Commutative
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = \paren {T \cup S}
      | c = {{Defof|Set Union}}
}}
{{end-eqn}}
{{qed}}
Theorem: Intersection is Commutative

Set intersection is commutative:
:$S \cap T = T \cap S$

Proof:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \paren {S \cap T}
}}
{{eqn | ll= \leadstoandfrom
      | l = x \in S
      | o = \land
      | r = x \in T
      | c = {{Defof|Set Intersection}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x \in T
      | o = \land
      | r = x \in S
      | c = Conjunction is Commutative
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = \paren {T \cap S}
      | c = {{Defof|Set Intersection}}
}}
{{end-eqn}}
{{qed}}
Theorem: Intersection is Commutative

Set intersection is commutative:
:$S \cap T = T \cap S$

Proof:
We have that both $\ds \bigcap_{j \mathop \in J} S_j$ and $\ds \bigcap_{k \mathop \in \relcomp I J} S_k$ are sets.
Hence by Intersection is Commutative we have:
:$\ds \bigcap_{j \mathop \in J} S_j \cap \bigcap_{k \mathop \in \relcomp I J} S_k = \bigcap_{k \mathop \in \relcomp I J} S_k \cap \bigcap_{j \mathop \in J} S_j$
It remains to be demonstrated that $\ds \bigcap_{i \mathop \in I} S_i = \bigcap_{j \mathop \in J} S_j \cap \bigcap_{k \mathop \in \relcomp I J} S_k$.
So:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \bigcap_{i \mathop \in I} S_i
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall i \in I
      | l = x
      | o = \in
      | r = S_i
      | c = {{Defof|Intersection of Family}}
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall j \in J
      | l = x
      | o = \in
      | r = S_j
      | c = {{Defof|Relative Complement}}
}}
{{eqn | lo= \land
      | q = \forall k \in \relcomp I J
      | l = x
      | o = \in
      | r = S_k
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = \bigcap_{j \mathop \in J} S_j
      | c = {{Defof|Intersection of Family}}
}}
{{eqn | lo= \land
      | l = x
      | o = \in
      | r = \bigcap_{k \mathop \in \relcomp I J} S_k
      | c = {{Defof|Intersection of Family}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = \bigcap_{j \mathop \in J} S_j \cap \bigcap_{k \mathop \in \relcomp I J} S_k
      | c = {{Defof|Set Intersection}}
}}
{{end-eqn}}
That is:
:$\ds x \in \bigcap_{i \mathop \in I} S_i \iff x \in \bigcap_{j \mathop \in J} S_j \cap \bigcap_{k \mathop \in \relcomp I J} S_k$
The result follows by definition of set equality.
{{qed}}
Theorem: Intersection is Commutative

Set intersection is commutative:
:$S \cap T = T \cap S$

Proof:
{{begin-eqn}}
{{eqn | l = \bigcap_{j \mathop \in J} S_j \cap \bigcap_{k \mathop \in \relcomp I J} S_k
      | r = \map \complement {\map \complement {\bigcap_{j \mathop \in J} S_j \cap \bigcap_{k \mathop \in \relcomp I J} S_k} }
      | c = Complement of Complement
}}
{{eqn | r = \map \complement {\map \complement {\bigcap_{j \mathop \in J} S_j} \cup \map \complement {\bigcap_{k \mathop \in \relcomp I J} S_k} }
      | c = De Morgan's Laws (Set Theory)/Set Complement/Complement of Intersection
}}
{{eqn | n = 1
      | r = \map \complement {\bigcup_{j \mathop \in J} \map \complement {S_j} \cup \bigcup_{k \mathop \in \relcomp I J} \map \complement {S_k} }
      | c = De Morgan's Laws (Set Theory)/Set Complement/Family of Sets/Complement of Intersection
}}
{{eqn | r = \map \complement {\bigcup_{k \mathop \in \relcomp I J} \map \complement {S_k} \cup \bigcup_{j \mathop \in J} \map \complement {S_j} }
      | c = General Commutativity of Set Union
}}
{{eqn | r = \map \complement {\map \complement {\bigcap_{k \mathop \in \relcomp I J} S_k}\cup \map \complement {\bigcap_{j \mathop \in J} S_j} }
      | c = De Morgan's Laws (Set Theory)/Set Complement/Family of Sets/Complement of Intersection
}}
{{eqn | r = \map \complement {\map \complement {\bigcap_{k \mathop \in \relcomp I J} \cap S_k \bigcap_{j \mathop \in J} S_j} }
      | c = De Morgan's Laws (Set Theory)/Set Complement/Complement of Intersection
}}
{{eqn | r = \bigcap_{k \mathop \in \relcomp I J} S_k \cap \bigcap_{j \mathop \in J} S_j
      | c = Complement of Complement
}}
{{end-eqn}}
Also:
{{begin-eqn}}
{{eqn | l = \bigcap_{i \mathop \in I} S_i
      | r = \map \complement {\map \complement {\bigcap_{i \mathop \in I} S_i} }
      | c = Complement of Complement
}}
{{eqn | r = \map \complement {\bigcup_{i \mathop \in I} \map \complement {S_i} }
      | c = De Morgan's Laws (Set Theory)/Set Complement/Family of Sets/Complement of Intersection
}}
{{eqn | r = \map \complement {\bigcup_{j \mathop \in J} \map \complement {S_j} \cup \bigcup_{k \mathop \in \relcomp I J} \map \complement {S_k} }
      | c = General Commutativity of Set Union
}}
{{eqn | r = \bigcap_{j \mathop \in J} S_j \cap \bigcap_{k \mathop \in \relcomp I J} S_k
      | c = from $(1)$ above
}}
{{end-eqn}}
{{qed}}
Theorem: Russell's Paradox

The {{axiom-link|Abstraction}} leads to a contradiction.

Proof:
{{AimForCont}} there does exist such an $x$.
Let $\RR$ be such that $\map \RR {x, x}$.
Then $\neg \map \RR {x, x}$.
Hence it cannot be the case that $\map \RR {x, x}$.
Now suppose that $\neg \map \RR {x, x}$.
Then by definition of $x$ it follows that $\map \RR {x, x}$.
In both cases a contradiction results.
Hence there can be no such $x$.
{{qed}}
Theorem: Russell's Paradox

The {{axiom-link|Abstraction}} leads to a contradiction.

Proof:
{{AimForCont}}:
:$\exists x: \forall y: \paren {\map \RR {x, y} \iff \neg \map \RR {y, y} }$
By Existential Instantiation:
:$\forall y: \paren {\map \RR {x, y} \iff \neg \map \RR {y, y} }$
By Universal Instantiation:
:$\map \RR {x, x} \iff \neg \map \RR {x, x} $
But this contradicts Biconditional of Proposition and its Negation.
We thus conclude:
:$\not \exists x: \forall y: \paren {\map \RR {x, y} \iff \neg \map \RR {y, y} }$
{{qed}}
Theorem: Russell's Paradox

The {{axiom-link|Abstraction}} leads to a contradiction.

Proof:
Sets have elements.
Some of those elements may themselves be sets.
So, given two sets $S$ and $T$, we can ask the question:
:''Is $S$ an element of $T$?''
The answer will either be ''yes'' or ''no''.
In particular, given any set $S$, we can ask the question:
:''Is $S$ an element of $S$?''
Again, the answer will either be ''yes'' or ''no''.
Recall the definitions for a set to be:
:ordinary {{iff}} it is ''not'' an element of itself
:extraordinary {{iff}} it ''is'' an element of itself.
Thus, $\map P S = S \in S$ is a property on which we can use the {{axiom-link|Abstraction}} to build the set $T$ of all extraordinary:
:$T = \set {S: S \in S}$
which is the set of all sets which contain themselves.
Or we can apply the {{axiom-link|Abstraction}} to build the set $T$ of all ordinary sets:
:$R = \set {S: S \notin S}$
($R$ for {{AuthorRef|Bertrand Russell|Russell}}, of course.)
We ask the question:
:''Is $R$ itself an element of $R$?''
There are two possible answers: ''yes'' or ''no''.
If $R \in R$, then $R$ must satisfy the property that $R \notin R$.
So from that contradiction we know that $R \in R$ does not hold.
So the only other answer, $R \notin R$, must hold instead.
But now we see that $R$ satisfies the conditions of the property that $R \in R$.
So we can see that $R \notin R$ does not hold either.
Thus we have generated a contradiction from the {{axiom-link|Abstraction}}.
{{qed}}
Theorem: Russell's Paradox

The {{axiom-link|Abstraction}} leads to a contradiction.

Proof:
{{AimForCont}} the {{axiom-link|Abstraction}}, that for all predicates $P$ where $S$ is not free:
:$\exists S : \forall x : \paren {x \in S \iff \map P x}$
Since $x \notin x$ is a predicate where $S$ is not free, it follows that:
:$\exists S : \forall x : \paren {x \in S \iff x \notin x}$
is an instance of the {{axiom-link|Abstraction}}.
By Existential Instantiation:
:$\forall x: \paren {x \in S \iff x \notin x}$
By Universal Instantiation:
:$S \in S \iff S \notin S$
But this contradicts Biconditional of Proposition and its Negation.
Thus, the {{axiom-link|Abstraction}} yields a contradiction.
{{qed}}
Theorem: Solution to Quadratic Equation

The quadratic equation of the form $a x^2 + b x + c = 0$ has solutions:
:$x = \dfrac {-b \pm \sqrt {b^2 - 4 a c} } {2 a}$

Proof:
{{begin-eqn}}
{{eqn | l = a x^2 + b x + c
      | r = 0
      | c = {{hypothesis}}
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\paren {2 a x + b}^2 - b^2 + 4 a c} {4 a}
      | r = 0
      | c = Completing the Square
}}
{{eqn | ll= \leadsto
      | l = \paren {2 a x + b}^2
      | r = b^2 - 4 a c
      | c = simplification
}}
{{eqn | ll= \leadsto
      | l = x
      | r = \frac {-b \pm \sqrt {b^2 - 4 a c} } {2 a}
      | c = solving for $x$
}}
{{end-eqn}}
{{qed}}
Theorem: Normal Subgroup Test

Let $G$ be a group and $H \le G$.
Then $H$ is a normal subgroup (by definition 1) of $G$ {{iff}}:
:$\forall x \in G: x H x^{-1} \subseteq H$.

Proof:
Let $H$ be a subgroup of $G$.
Suppose $H$ is normal in $G$.
Then $\forall x \in G, a \in H: \exists b \in H: x a = b x$.
Thus, $x a x^{-1} = b \in H$ implying $x H x^{-1} \subseteq H$.
Conversely, suppose $\forall x \in G: x H x^{-1} \subseteq H$.
Then for $g \in G$, we have $g H g^{-1} \subseteq H$, which implies $g H \subseteq H g$.
Also, for $g^{-1} \in G$, we have $g^{-1} H (g^{-1})^{-1} = g^{-1} H g \subseteq H$ which implies $H g \subseteq g H$.
Therefore, $g H = H g$ meaning $H \lhd G$.
{{qed}}
Category:Normal Subgroups
gymiuxywejymobwt2j5bl16k7hh3q0z
Theorem: Equality of Ordered Pairs

Two ordered pairs are equal {{iff}} corresponding coordinates are equal:
:$\tuple {a, b} = \tuple {c, d} \iff a = c \land b = d$

Proof:
=== Necessary Condition ===
{{:Equality of Ordered Pairs/Necessary Condition}}{{qed|lemma}}