avewright/proofwiki-math huggingface dataset:
Theorem: Reflexive Closure of Relation Compatible with Operation is Compatible

Let $\struct {S, \circ}$ be a magma.
Let $\RR$ be a relation on $S$ which is compatible with $\circ$.
Let $\RR^=$ be the reflexive closure of $\prec$.
That is, $\RR^=$ is defined as the union of $\RR$ with the diagonal relation for $S$.
Then $\RR^=$ is compatible with $\circ$.

Proof:
By Diagonal Relation is Universally Compatible, the diagonal relation is compatible with $\circ$.
Then by Union of Relations Compatible with Operation is Compatible, $\RR^=$ is compatible with $\circ$.
{{qed}}
Theorem: Reflexive Reduction of Relation Compatible with Group Operation is Compatible

Let $\struct {S, \circ}$ be a group.
Let $\RR$ be a relation on $S$ which is compatible with $\circ$.
Let $\RR^\ne$ be the reflexive reduction of $\RR$.
Then $\RR^\ne$ is compatible with $\circ$.

Proof:
From the Cancellation Laws, $\circ$ is a cancellable operation.
The result then follows directly from Reflexive Reduction of Relation Compatible with Cancellable Operation is Compatible.
{{qed}}
Theorem: Double Negation Elimination implies Law of Excluded Middle

Let the Law of Double Negation Elimination be supposed to hold:
:$\neg \neg p \vdash p$
Then the Law of Excluded Middle likewise holds:
:$\vdash p \lor \neg p$

Proof:
{{BeginTableau|p \lor \neg p}}
{{Assumption           |1|\neg \paren {p \lor \neg p}|Assume the contrary}}
{{Assumption           |2|p|Assume one disjunct}}
{{Addition             |3|2|p \lor \neg p|2|1}}
{{NonContradiction     |4|1, 2|3|1}}
{{Contradiction        |5|1|\neg p|2|4|demonstrating a contradiction}}
{{Addition             |6|1|p \lor \neg p|5|2}}
{{NonContradiction     |7|1|6|1|also demonstrating a contradiction}}
{{Contradiction        |8||\neg \neg \paren {p \lor \neg p}|1|7}}
{{DoubleNegElimination |9||p \lor \neg p|8}}
{{EndTableau|qed}}
Theorem: Double Negation Elimination implies Law of Excluded Middle

Let the Law of Double Negation Elimination be supposed to hold:
:$\neg \neg p \vdash p$
Then the Law of Excluded Middle likewise holds:
:$\vdash p \lor \neg p$

Proof:
{{BeginTableau|\vdash p \lor \neg p}}
{{TheoremIntro|1|\neg\neg (p \lor \neg p)|Negation of Excluded Middle is False: Form 2}}
{{DoubleNegElimination|2||p \lor \neg p|1}}
{{EndTableau|qed}}
Theorem: Double Negation/Double Negation Introduction/Sequent Form/Formulation 2

:$\vdash p \implies \neg \neg p$

Proof:
{{BeginTableau|\vdash p \implies \neg \neg p}}
{{Assumption|1|p}}
{{DoubleNegIntro|2|1|\neg \neg p|1}}
{{Implication|3||p \implies \neg \neg p|1|2}}
{{EndTableau|qed}}
Theorem: Dual of Dual Ordering

Let $\struct {S, \preceq}$ be an ordered set.
Let $\struct {S, \succeq}$ be its dual.
Then the dual of $\struct {S, \succeq}$ is again $\struct {S, \preceq}$.

Proof:
Denote with $\preceq'$ the dual of $\succeq$.
By definition of dual ordering, we thus have for all $a, b \in S$:
:$a \preceq b$ {{iff}} $b \succeq a$
:$b \succeq a$ {{iff}} $a \preceq' b$
Hence $a \preceq b$ {{iff}} $a \preceq' b$.
The result follows from Equality of Relations.
{{qed}}
Theorem: Dual of Dual Statement (Order Theory)

Let $\Sigma$ be a statement about ordered sets.
Let $\Sigma^*$ be its dual statement.
Then $\Sigma$ is also the dual statement of $\Sigma^*$.

Proof:
By definition, the dual statement $\Sigma^*$ is formed by replacing the ordering $\preceq$ with its dual $\succeq$.
By Dual of Dual Ordering, applying this operation twice results in the original sentence $\Sigma$ again.
{{qed}}
Category:Order Theory
sgenggbsvmbmw7wypp9g6hrj4lesfpe
Theorem: Double Negation/Double Negation Elimination/Sequent Form/Formulation 2

:$\vdash \neg \neg p \implies p$

Proof:
{{BeginTableau|\vdash \neg \neg p \implies p}}
{{Assumption|1|\neg \neg p}}
{{DoubleNegElimination|2|1|p|1}}
{{Implication|3||\neg \neg p \implies p|1|2}}
{{EndTableau|qed}}
Theorem: Double Negation/Double Negation Elimination

The '''rule of double negation elimination''' is a valid argument in certain types of logic dealing with negation $\neg$.
This includes classical propositional logic and predicate logic, and in particular natural deduction, but for example not intuitionistic propositional logic.

Proof:
{{BeginTableau|\neg \neg p \vdash p}}
{{Premise|1|\neg \neg p}}
{{ExcludedMiddle|2|p \lor \neg p}}
{{Assumption|3|p}}
{{Assumption|4|\neg p}}
{{NonContradiction|5|1, 4|4|1}}
{{Explosion|6|1, 4|p|5}}
{{ProofByCases|7|1|p|2|3|3|4|6}}
{{EndTableau}}
{{Qed}}
Theorem: Double Negation/Formulation 1

:$p \dashv \vdash \neg \neg p$

Proof:
=== Double Negation Introduction ===
{{:Double Negation/Double Negation Introduction/Sequent Form/Formulation 1/Proof}}
=== Double Negation Elimination ===
{{:Double Negation/Double Negation Elimination/Sequent Form/Formulation 1/Proof}}
Theorem: Double Negation/Formulation 1

:$p \dashv \vdash \neg \neg p$

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, appropriate truth values match for both boolean interpretations.
:<nowiki>$\begin {array} {|c||ccc|} \hline
p & \neg & \neg & p \\
\hline
\F & \F & \T & \F \\
\T & \T & \F & \T \\
\hline
\end {array}$</nowiki>
Hence:
:$p \dashv \vdash \neg \neg p$
{{qed}}
Theorem: Double Negation/Formulation 2

:$\vdash p \iff \neg \neg p$

Proof:
{{BeginTableau|\vdash p \iff \neg \neg p}}
{{TheoremIntro|1|p \implies \neg \neg p|Double Negation Introduction: Formulation 2}}
{{TheoremIntro|2|\neg \neg p \implies p|Double Negation Elimination: Formulation 2}}
{{BiconditionalIntro|3||p \iff \neg \neg p|1|2}}
{{EndTableau}}
{{qed}}
Theorem: Double Negation/Formulation 2

:$\vdash p \iff \neg \neg 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 are true for all boolean interpretations.
$\quad \begin{array}{|c|c|ccc|} \hline
p & \iff & \neg & \neg & p \\
\hline
\F & \T & \F & \T & \F \\
\T & \T & \T & \F & \T \\
\hline
\end{array}$
{{qed}}
Theorem: Rule of Transposition/Formulation 1

A statement and its contrapositive have the same truth value:
:$p \implies q \dashv \vdash \neg q \implies \neg p$
Its abbreviation in a tableau proof is $\textrm {TP}$.

Proof:
{{BeginTableau|p \implies q \vdash \neg q \implies \neg p}}
{{Premise|1|p \implies q}}
{{Assumption|2|\neg q}}
{{ModusTollens|3|1, 2|\neg p|1|2}}
{{Implication|4|1|\neg q \implies \neg p|2|3}}
{{EndTableau}}
{{Qed}}
Theorem: Rule of Transposition/Formulation 1

A statement and its contrapositive have the same truth value:
:$p \implies q \dashv \vdash \neg q \implies \neg p$
Its abbreviation in a tableau proof is $\textrm {TP}$.

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, the truth value under the main connectives match for all boolean interpretations.
:<nowiki>$\begin {array} {|ccc|ccccc|} \hline
p & \implies & q & \neg & q & \implies & \neg & p \\
\hline
\F & \T & \F & \T & \F & \T & \T & \F \\
\F & \T & \T & \F & \T & \T & \T & \F \\
\T & \F & \F & \T & \F & \F & \F & \T \\
\T & \T & \T & \F & \T & \T & \F & \T \\
\hline
\end {array}$</nowiki>
{{qed}}
Theorem: Rule of Transposition/Formulation 1

A statement and its contrapositive have the same truth value:
:$p \implies q \dashv \vdash \neg q \implies \neg p$
Its abbreviation in a tableau proof is $\textrm {TP}$.

Proof:
=== Proof of Forward Implication ===
{{:Rule of Transposition/Formulation 1/Forward Implication/Proof 1}}
=== Proof of Reverse Implication ===
{{:Rule of Transposition/Formulation 1/Reverse Implication/Proof 1}}
Theorem: Rule of Transposition/Formulation 1

A statement and its contrapositive have the same truth value:
:$p \implies q \dashv \vdash \neg q \implies \neg p$
Its abbreviation in a tableau proof is $\textrm {TP}$.

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
:<nowiki>$\begin {array} {|ccc||ccccc|} \hline
p & \implies & q & \neg & q & \implies & \neg & p \\
\hline
\F & \T & \F & \T & \F & \T & \T & \F \\
\F & \T & \T & \F & \T & \T & \T & \F \\
\T & \F & \F & \T & \F & \F & \F & \T \\
\T & \T & \T & \F & \T & \T & \F & \T \\
\hline
\end {array}$</nowiki>
{{qed}}
Theorem: Rule of Transposition/Formulation 1

A statement and its contrapositive have the same truth value:
:$p \implies q \dashv \vdash \neg q \implies \neg p$
Its abbreviation in a tableau proof is $\textrm {TP}$.

Proof:
{{BeginTableau|\neg q \implies \neg p \vdash p \implies q}}
{{Premise|1|\neg q \implies \neg p}}
{{Assumption|2|p}}
{{DoubleNegIntro|3|2|\neg \neg p|2}}
{{ModusTollens|4|1, 2|\neg \neg q|1|3}}
{{DoubleNegElimination|5|1, 2|q|4}}
{{Implication|6|1|p \implies q|2|5}}
{{EndTableau|Qed}}
Theorem: Rule of Transposition/Formulation 1

A statement and its contrapositive have the same truth value:
:$p \implies q \dashv \vdash \neg q \implies \neg p$
Its abbreviation in a tableau proof is $\textrm {TP}$.

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, the truth value under the main connectives match for all boolean interpretations.
:<nowiki>$\begin {array} {|ccccc|ccc|} \hline
\neg & q & \implies & \neg & p & p & \implies & q \\
\hline
\T & \F & \T & \T & \F & \F & \T & \F \\
\F & \T & \T & \T & \F & \F & \T & \T \\
\T & \F & \F & \F & \T & \T & \F & \F \\
\T & \T & \T & \F & \T & \T & \T & \T \\
\hline
\end {array}$</nowiki>
{{qed}}
Theorem: Rule of Transposition/Formulation 1/Proof 1

:$p \implies q \dashv \vdash \neg q \implies \neg p$

Proof:
=== Proof of Forward Implication ===
{{:Rule of Transposition/Formulation 1/Forward Implication/Proof 1}}
=== Proof of Reverse Implication ===
{{:Rule of Transposition/Formulation 1/Reverse Implication/Proof 1}}
Theorem: Positive Infinity is Maximal

Let $\struct {\overline \R, \le}$ be the extended real numbers with the usual ordering.
Then $+\infty$ is a maximal element of $\overline \R$.

Proof:
By the definition of the usual ordering on the extended real numbers:
:${\le} = {\le_\R} \cup \set {\tuple {x, +\infty}: x \in \overline \R} \cup \set {\tuple {-\infty, x}: x \in \overline \R}$
Suppose $x \in \overline \R$ and $+\infty \le x$.
That is:
: $\tuple {+\infty, x} \in {\le}$
By the definition of union, $\tuple {+\infty, x}$ must lie in one of the three sets whose union forms $\le$.
Since ${\le_\R} \subseteq \R \times \R$ and $+\infty \notin \R$:
:$\tuple {+\infty, x} \notin {\le_\R}$
Since $+\infty \ne -\infty$ by the definition of the extended real numbers:
:$\tuple {+\infty, x} \notin \set {\tuple {-\infty, x}: x \in \overline \R}$
Therefore:
:$\tuple {+\infty, x} \in \set {\tuple {x, +\infty}: x \in \overline \R}$
and we conclude that $x = +\infty$.
That is, $+\infty$ is a maximal element of $\overline \R$.
{{qed}}
Theorem: Negative Infinity is Minimal

Let $\struct {\overline \R, \le}$ be the extended real numbers with the usual ordering.
Then $-\infty$ is a minimal element of $\overline \R$.

Proof:
By the definition of the usual ordering on the extended real numbers:
:${\le} = {\le_\R} \cup \set {\tuple {x, +\infty}: x \in \overline \R} \cup \set {\tuple {-\infty, x}: x \in \overline \R}$
Suppose $x \in \overline \R$ and $x \le -\infty$.
That is:
:$\tuple {x, -\infty} \in {\le}$
By the definition of union, $\tuple {x, -\infty}$ must lie in one of the three sets whose union forms $\le$.
Since ${\le_\R} \subseteq \R \times \R$ and $-\infty \notin \R$:
:$\tuple {x, -\infty} \notin {\le_\R}$
Since $+\infty \ne -\infty$ by the definition of the extended real numbers:
:$\tuple {x, -\infty} \notin \set {\tuple {x, +\infty}: x \in \overline \R}$
Therefore:
:$\tuple {x, -\infty} \in \set {\tuple {-\infty, x}: x \in \overline \R}$
and we conclude that $x = -\infty$.
That is, $-\infty$ is a minimal element of $\overline \R$.
{{qed}}
Theorem: Inversion Mapping Reverses Ordering in Ordered Group/Corollary

{{begin-eqn}}
{{eqn | q = \forall x \in G
      | l = x \preccurlyeq e
      | o = \iff
      | r = e \preccurlyeq x^{-1}
}}
{{eqn | l = e \preccurlyeq x
      | o = \iff
      | r = x^{-1} \preccurlyeq e
}}
{{eqn | l = x \prec e
      | o = \iff
      | r = e \prec x^{-1}
}}
{{eqn | l = e \prec x
      | o = \iff
      | r = x^{-1} \prec e
}}
{{end-eqn}}

Proof:
By Inversion Mapping Reverses Ordering in Ordered Group:
{{begin-eqn}}
{{eqn | q = \forall x \in G
      | l = x \preccurlyeq e
      | o = \iff
      | r = e^{-1} \preccurlyeq x^{-1}
}}
{{eqn | l = e \preccurlyeq x
      | o = \iff
      | r = x^{-1} \preccurlyeq e^{-1}
}}
{{eqn | l = x \prec e
      | o = \iff
      | r = e^{-1} \prec x^{-1}
}}
{{eqn | l = e \prec x
      | o = \iff
      | r = x^{-1} \prec e^{-1}
}}
{{end-eqn}}
Since $e^{-1} = e$, the theorem holds.
{{qed}}
Theorem: Inversion Mapping Reverses Ordering in Ordered Group/Corollary

{{begin-eqn}}
{{eqn | q = \forall x \in G
      | l = x \preccurlyeq e
      | o = \iff
      | r = e \preccurlyeq x^{-1}
}}
{{eqn | l = e \preccurlyeq x
      | o = \iff
      | r = x^{-1} \preccurlyeq e
}}
{{eqn | l = x \prec e
      | o = \iff
      | r = e \prec x^{-1}
}}
{{eqn | l = e \prec x
      | o = \iff
      | r = x^{-1} \prec e
}}
{{end-eqn}}

Proof:
By the definition of an ordered group, $\preccurlyeq$ is a relation compatible with $\circ$.
Thus by Inverses of Elements Related by Compatible Relation: Corollary:
{{begin-eqn}}
{{eqn | q = \forall x \in G
      | l = x \preccurlyeq e
      | o = \iff
      | r = e \preccurlyeq x^{-1}
}}
{{eqn | l = e \preccurlyeq x
      | o = \iff
      | r = x^{-1} \preccurlyeq e
}}
{{end-eqn}}
By Reflexive Reduction of Relation Compatible with Group Operation is Compatible, $\prec$ is also compatible with $\circ$.
Thus again by Inverses of Elements Related by Compatible Relation: Corollary:
{{begin-eqn}}
{{eqn | q = \forall x \in G
      | l = x \prec e
      | o = \iff
      | r = e \prec x^{-1}
}}
{{eqn | l = e \prec x
      | o = \iff
      | r = x^{-1} \prec e
}}
{{end-eqn}}
{{qed}}
Theorem: Inversion Mapping Reverses Ordering in Ordered Group

{{begin-eqn}}
{{eqn | q = \forall x, y \in G
      | l = x \preccurlyeq y
      | o = \iff
      | r = e \prec y^{-1} \preccurlyeq x^{-1}
}}
{{eqn | q = \forall x, y \in S
      | l = x \prec y
      | o = \iff
      | r = y^{-1} \prec x^{-1}
}}
{{end-eqn}}

Proof:
By the definition of an ordered group, $\preceq$ is a relation compatible with $\circ$.
Thus by Inverses of Elements Related by Compatible Relation, we obtain the first result:
:$x \preccurlyeq y \iff y^{-1} \preccurlyeq x^{-1}$
By Reflexive Reduction of Relation Compatible with Group Operation is Compatible, $\prec$ is also compatible with $\circ$.
Thus by again Inverses of Elements Related by Compatible Relation, we obtain the second result:
:$x \prec y \iff y^{-1} \prec x^{-1}$
{{qed}}
Theorem: Inversion Mapping Reverses Ordering in Ordered Group

{{begin-eqn}}
{{eqn | q = \forall x, y \in G
      | l = x \preccurlyeq y
      | o = \iff
      | r = e \prec y^{-1} \preccurlyeq x^{-1}
}}
{{eqn | q = \forall x, y \in S
      | l = x \prec y
      | o = \iff
      | r = y^{-1} \prec x^{-1}
}}
{{end-eqn}}

Proof:
By Inversion Mapping Reverses Ordering in Ordered Group:
{{begin-eqn}}
{{eqn | q = \forall x \in G
      | l = x \preccurlyeq e
      | o = \iff
      | r = e^{-1} \preccurlyeq x^{-1}
}}
{{eqn | l = e \preccurlyeq x
      | o = \iff
      | r = x^{-1} \preccurlyeq e^{-1}
}}
{{eqn | l = x \prec e
      | o = \iff
      | r = e^{-1} \prec x^{-1}
}}
{{eqn | l = e \prec x
      | o = \iff
      | r = x^{-1} \prec e^{-1}
}}
{{end-eqn}}
Since $e^{-1} = e$, the theorem holds.
{{qed}}
Theorem: Inversion Mapping Reverses Ordering in Ordered Group

{{begin-eqn}}
{{eqn | q = \forall x, y \in G
      | l = x \preccurlyeq y
      | o = \iff
      | r = e \prec y^{-1} \preccurlyeq x^{-1}
}}
{{eqn | q = \forall x, y \in S
      | l = x \prec y
      | o = \iff
      | r = y^{-1} \prec x^{-1}
}}
{{end-eqn}}

Proof:
By the definition of an ordered group, $\preccurlyeq$ is a relation compatible with $\circ$.
Thus by Inverses of Elements Related by Compatible Relation: Corollary:
{{begin-eqn}}
{{eqn | q = \forall x \in G
      | l = x \preccurlyeq e
      | o = \iff
      | r = e \preccurlyeq x^{-1}
}}
{{eqn | l = e \preccurlyeq x
      | o = \iff
      | r = x^{-1} \preccurlyeq e
}}
{{end-eqn}}
By Reflexive Reduction of Relation Compatible with Group Operation is Compatible, $\prec$ is also compatible with $\circ$.
Thus again by Inverses of Elements Related by Compatible Relation: Corollary:
{{begin-eqn}}
{{eqn | q = \forall x \in G
      | l = x \prec e
      | o = \iff
      | r = e \prec x^{-1}
}}
{{eqn | l = e \prec x
      | o = \iff
      | r = x^{-1} \prec e
}}
{{end-eqn}}
{{qed}}
Theorem: Operating on Transitive Relationships Compatible with Operation

Let $\struct {S, \circ}$ be a magma.
Let $\RR$ be a transitive relation on $S$ which is compatible with $\circ$.
Let $\RR^=$ be the reflexive closure of $\RR$.
Let $x, y, z, w \in S$.
Then the following implications hold:
$(1): \quad$ If $x \mathrel \RR y$ and $z \mathrel \RR w$, then $x \circ z \mathrel \RR y \circ w$.
$(2): \quad$ If $x \mathrel \RR y$ and $z \mathrel {\RR^=} w$, then $x \circ z \mathrel \RR y \circ w$.
$(3): \quad$ If $x \mathrel {\RR^=} y$ and $z \mathrel \RR w$, then $x \circ z \mathrel \RR y \circ w$.
$(4): \quad$ If $x \mathrel {\RR^=} y$ and $z \mathrel {\RR^=} w$, then $x \circ z \mathrel {\RR^=} y \circ w$.

Proof:
We will prove $(1)$ and $(2)$. $(3)$ can be proven using precisely the same argument as $(2)$ and $(4)$ follows from $(1)$.
Suppose that $x \mathrel \RR y$ and $z \mathrel \RR w$.
By the definition of compatibility:
:$x \mathrel \RR y \implies x \circ z \mathrel \RR y \circ z$
:$z \mathrel \RR w \implies y \circ z \mathrel \RR y \circ w$
By transitivity:
:$(1): \quad \paren {x \mathrel \RR y} \land \paren {z \mathrel \RR w} \implies x \circ z \mathrel \RR y \circ w$
{{qed|lemma}}
Suppose $x \mathrel \RR y$ and $z \mathrel {\RR^=} w$.
By Reflexive Closure of Relation Compatible with Operation is Compatible, $\RR^=$ is compatible with $\circ$.
By the definition of compatibility:
:$x \mathrel \RR y \implies x \circ z \mathrel \RR y \circ z$
:$z \mathrel {\RR^=} w \implies y \circ z \mathrel {\RR^=} y \circ w$
By Extended Transitivity:
:$(2): \quad \paren {x \mathrel \RR y} \land \paren {z \mathrel {\RR^=} w} \implies x \circ z \mathrel \RR y \circ w$
{{qed|lemma}}
$(3)$ can be proven using precisely the same argument as $(2)$.
By Reflexive Closure of Relation Compatible with Operation is Compatible, $\RR^=$ is compatible with $\circ$.
By Reflexive Closure of Transitive Relation is Transitive, $\RR^=$ is transitive.
Thus $(4)$ follows from $(1)$.
{{qed}}
Category:Compatible Relations
Category:Transitive Relations
0awhkuotznyyro11lhuo9nqseuo5ede
Theorem: Operating on Ordered Group Inequalities

If $x \prec y$ and $z \prec w$, then $x \circ z \prec y \circ w$.
If $x \prec y$ and $z \preccurlyeq w$, then $x \circ z \prec y \circ w$.
If $x \preccurlyeq y$ and $z \prec w$, then $x \circ z \prec y \circ w$.
If $x \preccurlyeq y$ and $z \preccurlyeq w$, then $x \circ z \preccurlyeq y \circ w$.

Proof:
Because:
:$\struct {G, \circ, \preccurlyeq}$ is a group
:$\preccurlyeq$ is compatible with $\circ$
it follows from Reflexive Reduction of Relation Compatible with Group Operation is Compatible that $\prec$ is compatible with $\circ$ .
By the definition of an ordering, $\preccurlyeq$ is transitive and antisymmetric.
Therefore by Reflexive Reduction of Transitive Antisymmetric Relation is Strict Ordering, $\prec$ is transitive.
The result follows by Operating on Transitive Relationships Compatible with Operation.
{{qed}}
Theorem: Rule of Transposition/Formulation 2

:$\vdash \paren {p \implies q} \iff \paren {\neg q \implies \neg p}$

Proof:
{{BeginTableau |\vdash \paren {p \implies q} \implies \paren {\neg q \implies \neg p} }}
{{Assumption   |1|p \implies q}}
{{Assumption   |2|\neg q}}
{{ModusTollens |3|1, 2|\neg p|1|2}}
{{Implication  |4|1|\neg q \implies \neg p|2|3}}
{{Implication  |5||\paren {p \implies q} \implies \paren {\neg q \implies \neg p}|1|4}}
{{EndTableau|qed}}
Theorem: Rule of Transposition/Formulation 2

:$\vdash \paren {p \implies q} \iff \paren {\neg q \implies \neg p}$

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, the truth value under the main connective is true for all boolean interpretations.
:<nowiki>$\begin {array} {|ccc|c|ccccc|} \hline
(p & \implies & q) & \implies & (\neg & q & \implies & \neg & p) \\
\hline
\F & \T & \F & \T & \T & \F & \T & \T & \F \\
\F & \T & \T & \T & \F & \T & \T & \T & \F \\
\T & \F & \F & \T & \T & \F & \F & \F & \T \\
\T & \T & \T & \T & \F & \T & \T & \F & \T \\
\hline
\end {array}$</nowiki>
{{qed}}
Theorem: Rule of Transposition/Formulation 2

:$\vdash \paren {p \implies q} \iff \paren {\neg q \implies \neg p}$

Proof:
=== Proof of Forward Implication ===
{{:Rule of Transposition/Formulation 2/Forward Implication/Proof 1}}
=== Proof of Reverse Implication ===
{{:Rule of Transposition/Formulation 2/Reverse Implication/Proof 1}}
Theorem: Rule of Transposition/Formulation 2

:$\vdash \paren {p \implies q} \iff \paren {\neg q \implies \neg p}$

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
:<nowiki>$\begin{array}{|ccc|c|ccccc|} \hline
(p & \implies & q) & \iff & (\neg & q & \implies & \neg & p) \\
\hline
\F & \T & \F & \T & \T & \F & \T & \T & \F \\
\F & \T & \T & \T & \F & \T & \T & \T & \F \\
\T & \F & \F & \T & \T & \F & \F & \F & \T \\
\T & \T & \T & \T & \F & \T & \T & \F & \T \\
\hline
\end{array}$</nowiki>
{{qed}}
Theorem: Rule of Transposition/Formulation 2

:$\vdash \paren {p \implies q} \iff \paren {\neg q \implies \neg p}$

Proof:
{{BeginTableau|\vdash \paren {\neg q \implies \neg p} \implies \paren {p \implies q} }}
{{Assumption|1|\neg q \implies \neg p}}
{{Assumption|2|p}}
{{DoubleNegIntro|3|2|\neg \neg p|2}}
{{ModusTollens|4|1, 2|\neg \neg q|1|3}}
{{DoubleNegElimination|5|1, 2|q|4}}
{{Implication|6|1|p \implies q|2|5}}
{{Implication|7||\paren {\neg q \implies \neg p} \implies \paren {p \implies q}|1|6}}
{{EndTableau|qed}}
{{LEM|Double Negation Elimination|4}}
Theorem: Rule of Transposition/Formulation 2

:$\vdash \paren {p \implies q} \iff \paren {\neg q \implies \neg p}$

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, the truth value under the main connective is is true for all boolean interpretations.
:<nowiki>$\begin {array} {|ccccc|c|ccc|} \hline
(\neg & q & \implies & \neg & p) & \implies & (p & \implies & q) \\
\hline
\T & \F & \T & \T & \F & \T & \F & \T & \F \\
\F & \T & \T & \T & \F & \T & \F & \T & \T \\
\T & \F & \F & \F & \T & \T & \T & \F & \F \\
\T & \T & \T & \F & \T & \T & \T & \T & \T \\
\hline
\end {array}$</nowiki>
{{qed}}
Theorem: Complex Modulus is Norm

The complex modulus is a norm on the set of complex numbers $\C$.

Proof:
We prove the norm axioms.
Theorem: Set Difference of Relations Compatible with Group Operation is Compatible

Let $\struct {G, \circ}$ be a group.
Let $\RR, \QQ$ be relations on $G$ which are compatible with $\circ$.
Then the difference $\RR \setminus \QQ$ is compatible with $\circ$.

Proof:
By Complement of Relation Compatible with Group is Compatible, $\relcomp {G \times G} \QQ$ is compatible with $\circ$.
Thus by Intersection of Relations Compatible with Operation is Compatible, $\RR \cap \relcomp {G \times G} \QQ$ is compatible with $\circ$.
But:
:$\RR \cap \relcomp {G \times G} \QQ = \RR \setminus \QQ$
so the theorem holds.
{{qed}}
Category:Compatible Relations
jyg5vn2asa1vqciut2pcdlutk31nlto