nyuuzyou/wikis huggingface dataset:
Extended Soundness Theorem for Propositional Tableaux and Boolean Interpretations

== Theorem ==
Tableau proofs (in terms of propositional tableaux) are a strongly sound proof system for boolean interpretations.
That is, for every collection $\mathbf H$ of WFFs of propositional logic and every WFF $\mathbf A$:
:$\mathbf H \vdash_{\mathrm{PT}} \mathbf A$ implies $\mathbf H \models_{\mathrm{BI}} \mathbf A$
== Proof ==
By definition of tableau proof, $\mathbf H \vdash_{\mathrm{PT}} \mathbf A$ means:
:There exists a tableau confutation of $\mathbf H \cup \set {\neg\mathbf A}$.
By Tableau Confutation implies Unsatisfiable, it follows that $\mathbf H \cup \set {\neg\mathbf A}$ is unsatisfiable for boolean interpretations.
Therefore, if some boolean interpretation $v$ models $\mathbf H$:
:$v \models_{\mathrm{BI}} \mathbf H$
then since $\mathbf H \cup \set {\neg\mathbf A}$ is unsatisfiable:
:$v \not\models_{\mathrm{BI}} \neg\mathbf H$
Now by definition of the relation $\models_{\mathrm{BI}}$, it must be that:
:$\map v {\neg \mathbf A} = F$
By the truth table for $\neg$, this implies:
:$\map v {\mathbf A} = T$
which is to say $v \models_{\mathrm{BI}} \mathbf A$.
Hence:
:$v \models_{\mathrm{BI}} \mathbf H$ implies $v \models_{\mathrm{BI}} \mathbf A$
that is, $\mathbf A$ is a $\mathrm{BI}$-semantic consequence of $\mathbf H$:
:$\mathbf H \models_{\mathrm{BI}} \mathbf A$
which was to be shown.
== Also see ==
* Extended Completeness Theorem for Propositional Tableaux and Boolean Interpretations, which proves:
*:If $\mathbf H \models \mathbf A$, then $\mathbf H \vdash \mathbf A$.
== Sources ==
* : $\S 1.8$: Soundness: Theorem $1.8.3$
Category:Propositional Tableaux
Category:Named Theorems
Extended Transitivity

== Theorem ==
Let $S$ be a set.
Let $\RR$ be a transitive relation on $S$.
Let $\RR^=$ be the reflexive closure of $\RR$.
Let $a, b, c \in S$.
Then:
== Proof ==
$(1)$ follows from the definition of a transitive relation.
$(4)$ follows from Reflexive Closure of Transitive Relation is Transitive.
Suppose that:
:$\paren {a \mathrel \RR b} \land \paren {b \mathrel {\RR^=} c}$
By the definition of reflexive closure:
:$b \mathrel \RR c$ or $b = c$
If $b = c$, then since $a \mathrel \RR b$:
:$a \mathrel \RR c$
If $b \mathrel \RR c$ then by transitivity of $\RR$:
:$a \mathrel \RR c$
Thus $(2)$ holds.
A similar argument proves that $(3)$ holds as well:
Suppose that:
:$\paren {a \mathrel {\RR^=} b} \land \paren {b \mathrel \RR c}$
By the definition of reflexive closure:
:$a \mathrel \RR b$ or $a = b$
If $a = b$, then since $b \mathrel \RR c$:
:$a \mathrel \RR c$
If $a \mathrel \RR b$ then by transitivity of $\RR$:
:$a \mathrel \RR c$
Thus $(3)$ holds.
Category:Transitive Relations
Category:Reflexive Closures
Extending Operation is a Slowly Progressing Mapping

== Theorem ==
Let $S$ denote the class of all ordinal sequences.
Let $E: S \to S$ be an extending operation on $S$.
Then $E$ is a slowly progressing mapping.
== Proof ==
Let $\theta \in S$ be an $\alpha$-sequence.
By definition of extending operation:
:$\map E \theta = \theta \cup \tuple {\alpha, x}$
where $x$ is arbitrary.
Thus:
:$\theta \subseteq \map E \theta$
and it is seen that $E$ is by definition a progressing mapping.
It is also seen that:
:$\card \theta = \card \alpha$
while:
:$\card {\map E \theta} = \card \alpha + 1$
demonstrating that $E$ is a slowly progressing mapping.
== Sources ==
* : Chapter $6$: Order Isomorphism and Transfinite Recursion: $\S 5$ Transfinite recursion theorems
Category:Extending Operations
Category:Slowly Progressing Mappings
Extending Operation is a Strictly Progressing Mapping

== Theorem ==
Let $S$ denote the class of all ordinal sequences.
Let $E: S \to S$ be an extending operation on $S$.
Then $E$ is a strictly progressing mapping.
== Proof ==
Let $\theta \in S$ be an $\alpha$-sequence.
By definition of extending operation:
:$\map E \theta = \theta \cup \tuple {\alpha, x}$
where $x$ is arbitrary.
From Extending Operation is a Slowly Progressing Mapping we have that $E$ is a progressing mapping.
By definition of $\alpha$-sequence:
:$\alpha \notin \Dom \theta$
and so:
:$\tuple {\alpha, x} \notin \theta$
Hence:
:$\theta \subsetneqq \map E \theta$
demonstrating that $E$ is a strictly progressing mapping.
== Sources ==
* : Chapter $6$: Order Isomorphism and Transfinite Recursion: $\S 5$ Transfinite recursion theorems
Category:Extending Operations
Category:Strictly Progressing Mappings
Extension Realizing All Types

== Theorem ==
Let $\MM$ be an $\LL$-structure.
Let $M$ be its universe.
There is an elementary extension $\NN$ of $\MM$ such that every type over $M$ (relative to $\MM$) is realized in $\NN$.
== Proof ==
Let $\map S \MM$ denote the set containing all complete types over $M$ of every number of free variables.
Let $\kappa = \size{\map S \MM}$.
Use a bijection between $\kappa$ and $\map S \MM$ to write the elements of $\map S \MM$ as $p_\alpha$ for $\alpha < \kappa$.
For each $\alpha < \kappa$, let $N_\alpha$ be an elementary extension of $\MM$ which has an ordered tuple $\bar a_\alpha$ realizing $p_\alpha$.
Such extensions and tuples exist by Type is Realized in some Elementary Extension.
We will construct the extension claimed by the theorem as the union over a chain of elementary extensions defined using Transfinite Induction.
At each step, we use the Elementary Amalgamation Theorem to add on $N_\alpha$.
Base case $\alpha = 0$:
Let $\BB_0 = \MM$.
Note that $\BB_0$ is an elementary extension of $\MM$ by choice of $\NN_0$.
Limit ordinals $\alpha \le \kappa$:
Let $\ds \BB_\alpha = \bigcup_{\beta \mathop < \alpha} \BB_\beta$
$\BB_\alpha$ is an elementary extension of $\MM$ by Union of Elementary Chain is Elementary Extension.
Successor ordinals $\alpha + 1$ for $\alpha < \kappa$:
We have that $\BB_\alpha$ and $\NN_\alpha$ are both elementary extensions of $\MM$.
By the Elementary Amalgamation Theorem, there is:
:an elementary extension $\BB_{\alpha + 1}$ of $\BB_\alpha$
and:
:an elementary embedding $g_\alpha: \NN_\alpha \to \BB_{\alpha + 1}$ which is the identity on $M$ viewed as a subset of $\NN_\alpha$.
Note that $\map {g_\alpha} {\bar a_\alpha}$ realizes $p_\alpha$ in $\BB_{\alpha + 1}$ since $g_\alpha$ is elementary.
Thus $\BB_{\alpha + 1}$ is an elementary extension of $\MM$ which contains $\map {g_\alpha} {\bar a_\alpha}$ realizing $p_\alpha$.
Now, let $\ds \BB = \bigcup_{\alpha < \kappa} \BB_\alpha$.
$\BB$ is an elementary extension of each $\BB_\alpha$ by Union of Elementary Chain is an Elementary Extension.
In particular, $\BB$ is an elementary extension of $\BB_0 = \MM$
We have that:
:each $p_\alpha$ is realized in $\BB_{\alpha + 1}$ by the corresponding $\map {g_\alpha} {\bar a_\alpha}$
and:
:$\BB$ is an elementary extension of each $\BB_{\alpha + 1}$
Thus we have that $\map {g_\alpha} {\bar a_\alpha}$ realizes $p_\alpha$ in $\BB$.
Category:Model Theory for Predicate Logic
Extension Theorem for Distributive Operations

== Theorem ==
Let $\struct {R, *}$ be a commutative semigroup, all of whose elements are cancellable.
Let $\struct {T, *}$ be an inverse completion of $\struct {R, *}$.
Let $\circ$ be an operation on $R$ which distributes over $*$.
Then the following hold:
=== Existence and Uniqueness ===
=== Associativity ===
=== Commutativity ===
=== Identity ===
=== Cancellability ===
== Sources ==
* : Chapter $\text {IV}$: Rings and Fields: $20$. The Integers: Theorem $20.8$
Category:Inverse Completions
Category:Semigroups
Category:Distributive Operations
Category:Extension Theorem for Distributive Operations
Extension Theorem for Distributive Operations/Associativity

== Theorem ==
Let $\circ'$ be the unique operation on $T$ which distributes over $*$ in $T$ and induces on $R$ the operation $\circ$.
Then:
:If $\circ$ is associative, then so is $\circ'$.
== Proof ==
We have that $\circ'$ exists and is unique by Extension Theorem for Distributive Operations: Existence and Uniqueness.
Suppose $\circ$ is associative.
As $\circ'$ distributes over $*$, for all $n, p \in R$, the mappings:
are endomorphisms of $\struct {T, *}$ that coincide on $R$ by the associativity of $\circ$ and hence are the same mapping.
Therefore:
:$\forall x \in T, n, p \in R: \paren {x \circ' n} \circ' p = x \circ' \paren {n \circ' p}$
Similarly, for all $x \in T, p \in R$, the mappings:
are endomorphisms of $\struct {T, *}$ that coincide on $R$ by what we have proved and hence are the same mapping.
Therefore:
:$\forall x, y \in T, p \in R: \paren {x \circ' y} \circ' p = x \circ' \paren {y \circ' p}$
Finally, for all $x, y \in T$, the mappings:
are endomorphisms of $\struct {T, *}$ that coincide on $R$ by what we have proved and hence are the same mapping.
Therefore $\circ'$ is associative.
== Sources ==
* : Chapter $\text {IV}$: Rings and Fields: $20$. The Integers: Theorem $20.8: 1^\circ$
Category:Extension Theorem for Distributive Operations
Extension Theorem for Distributive Operations/Cancellability

== Theorem ==
Then:
:Every element of $R$ cancellable for $\circ$ is also cancellable for $\circ'$.
== Proof ==
Let $a$ be an element of $R$ cancellable for $\circ$.
Then the restrictions to $R$ of the endomorphisms:
:$\lambda_a: x \mapsto a \circ' x$
:$\rho_a: x \mapsto x \circ' a$
of $\struct {T, *}$ are monomorphisms.
But then $\lambda_a$ and $\rho_a$ are monomorphisms by the Extension Theorem for Homomorphisms.
Hence $a$ is cancellable for $\circ'$.
== Sources ==
* : Chapter $\text {IV}$: Rings and Fields: $20$. The Integers: Theorem $20.8: 4^\circ$
Category:Extension Theorem for Distributive Operations
Extension Theorem for Distributive Operations/Commutativity

== Theorem ==
Let $\circ'$ be the unique operation on $T$ which distributes over $*$ in $T$ and induces on $R$ the operation $\circ$.
Then:
:If $\circ$ is commutative, then so is $\circ'$
== Proof ==
We have that $\circ'$ exists and is unique by Extension Theorem for Distributive Operations: Existence and Uniqueness.
Suppose $\circ$ is commutative.
As $\circ'$ distributes over $*$, for all $n \in R$, the mappings:
are endomorphisms of $\struct {T, *}$ that coincide on $R$ by the commutativity of $\circ$ and hence are the same mapping.
Therefore $\forall x \in T, n \in R: x \circ' n = n \circ' x$.
Finally, for all $y \in T$, the mappings:
are endomorphisms of $\struct {T, *}$ that coincide on $R$ by what we have proved and hence are the same mapping.
Therefore $\circ'$ is commutative.
== Sources ==
* : Chapter $\text {IV}$: Rings and Fields: $20$. The Integers: Theorem $20.8: 2^\circ$
Category:Extension Theorem for Distributive Operations
Extension Theorem for Distributive Operations/Existence and Uniqueness

== Theorem ==
Then:
:There exists a unique operation $\circ'$ on $T$ which distributes over $*$ in $T$ and induces on $R$ the operation $\circ$.
== Proof ==
We have that all the elements of $\struct {R, *}$ are cancellable.
Thus Inverse Completion of Commutative Semigroup is Abelian Group can be applied.
So $\struct {T, *}$ is an abelian group.
=== Existence ===
For each $m \in R$, we define $\lambda_m: R \to T$ as:
:$\forall x \in R: \map {\lambda_m} x = m \circ x$
Then:
So $\lambda_m$ is a homomorphism from $\struct {R, *}$ into $\struct {T, *}$.
Now, by the Extension Theorem for Homomorphisms, every homomorphism from $\struct {R, *}$ into $\struct {T, *}$ is the restriction to $R$ of a unique endomorphism of $\struct {T, *}$.
This can be applied because $\struct {T, *}$ is abelian.
We have just shown that $\lambda_m$ is such a homomorphism.
Therefore there exists a unique endomorphism $\lambda'_m: T \to T$ which extends $\lambda_m$.
Now:
By Homomorphism on Induced Structure to Commutative Semigroup:
:$\lambda'_m * \lambda'_n$ is an endomorphism of $\struct {T, *}$ that, as we have just seen, coincides on $R$ with $\lambda'_{m * n}$.
Hence $\lambda'_{m * n} = \lambda'_m * \lambda'_n$.
Similarly, for each $z \in T$, we define $\rho_z: R \to T$ as:
:$\forall m \in R: \map {\rho_z} m = \map {\lambda'_m} z$
Then:
Therefore $\rho_z$ is a homomorphism from $\struct {R, *}$ into $\struct {T, *}$.
Consequently there exists a unique endomorphism $\rho'_z: T \to T$ extending $\rho_z$.
By Homomorphism on Induced Structure to Commutative Semigroup:
:$\rho'_y * \rho'_z$ is an endomorphism on $\struct {T, *}$ that coincides (as we have just seen) with $\rho'_{y * z}$ on $R$.
Hence $\rho'_{y * z} = \rho'_y * \rho'_z$.
Now we define an operation $\circ'$ on $T$ by:
:$\forall x, y \in T: x \circ' y = \map {\rho'_y} x$
Now suppose $x, y \in R$. Then:
so $\circ'$ is an extension of $\circ$.
Next, let $x, y, z \in T$. Then:
So $\circ'$ is distributive over $*$.
=== Uniqueness ===
To show that $\circ'$ is unique, let $\circ_1$ be any operation on $T$ distributive over $*$ that induces $\circ$ on $R$.
Since $\circ'$ and $\circ_1$ both distribute over $*$, for every $m \in R$, the mappings:
are endomorphisms of $\struct {T, *}$ that coincide on $R$, so must be the same mapping.
Therefore:
:$\forall m \in R, y \in T: m \circ_1 y = m \circ' y$
Similarly, for every $y \in T$, the mappings:
are endomorphisms of $\struct {T, *}$ that coincide on $R$ by what we have just proved.
So these two mappings must be the same mapping.
Hence:
:$\forall x, y \in T: x \circ_1 y = x \circ' y$
Thus $\circ'$ is the only operation on $T$ which extends $\circ$ and distributes over $*$.
== Sources ==
* : Chapter $\text {IV}$: Rings and Fields: $20$. The Integers: Theorem $20.8$
Category:Extension Theorem for Distributive Operations
Extension Theorem for Distributive Operations/Identity

== Theorem ==
Let $\circ'$ be the unique operation on $T$ which distributes over $*$ in $T$ and induces on $R$ the operation $\circ$.
Then:
:If $e$ is an identity for $\circ$, then $e$ is also an identity for $\circ'$.
== Proof ==
We have that $\circ'$ exists and is unique by Extension Theorem for Distributive Operations: Existence and Uniqueness.
Let $e$ be the identity element of $\struct {R, \circ}$.
Then the restrictions to $R$ of the endomorphisms $\lambda_e: x \mapsto e \circ' x$ and $\rho_e: x \mapsto x \circ' e$ of $\struct {T, *}$ are monomorphisms.
But then $\lambda_e$ and $\rho_e$ are monomorphisms by the Extension Theorem for Homomorphisms.
Hence it follows that $e$ is the identity element of $T$.
== Sources ==
* : Chapter $\text {IV}$: Rings and Fields: $20$. The Integers: Theorem $20.8: 3^\circ$
Category:Extension Theorem for Distributive Operations
Extension Theorem for Isomorphisms

== Theorem ==
Let the following conditions be fulfilled:
:Let $\struct {S, \circ}$ be a commutative semigroup with cancellable elements
:Let $\phi$ be an isomorphism from $\struct {S, \circ}$ into a semigroup $\struct {T, *}$
:Let $\struct {S', \circ'}$ be an inverse completion of $\struct {S, \circ}$
:Let $\struct {T', \circ'}$ be an inverse completion of $\struct {T, \circ}$.
Then there is a unique isomorphism $\phi': S' \to T'$ extending $\phi$.
== Proof ==
Let $C$ be the subsemigroup of cancellable elements of $S$.
It is proved that this is a semigroup by Cancellable Elements of Semigroup form Subsemigroup.
The set of cancellable elements of $T$ is $\phi \sqbrk C$.
By the Extension Theorem for Homomorphisms, there is:
:A unique homomorphism $\phi'$ from $S'$ into $T'$ extending $\phi$
and:
:A unique homomorphism $\psi$ from $T'$ into $S'$ extending $\phi^{-1}$.
Therefore, $\psi \circ \phi'$ is an endomorphism of $S'$ whose restriction to $S$ is the inclusion mapping $\iota_S: S \to S'$:
:$\forall x \in S: \map \iota x = x$
From Inclusion Mapping is Monomorphism, $\iota_S$ is a monomorphism from $S$ into $S'$.
But by the Extension Theorem for Homomorphisms, the identity automorphism of $S'$ is the only endomorphism of $S'$ extending $\iota_S$ from $S$ into $S'$, so:
:$\psi \circ \phi' = I_{S'}$
Similarly:
:$\phi' \circ \psi = I_{T'}$
So by Bijection iff Left and Right Inverse, $\phi'$ is a bijection and therefore an isomorphism.
== Sources ==
* : Chapter $\text {IV}$: Rings and Fields: $\S 20$: The Integers: Theorem $20.5$
Category:Semigroup Isomorphisms
Category:Inverse Completions
Category:Semigroups
Category:Named Theorems
Extension Theorem for Positive Linear Functional defined on Cofinal Linear Subspace/Lemma 1

== Lemma ==
Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \succeq}$ be a preordered vector space over $\R$.
Let $Y$ be a linear subspace of $X$ that is cofinal in $\struct {X, \succeq}$.
Let:
:$P = \set {x \in X : x \succeq {\mathbf 0}_X}$
Let:
:$Z = Y + P - P = \set {y + z - w : y \in Y, \, z, w \in P}$
be the Minkowski sum of $Y$, $P$ and $-P$.
Then:
:$Z$ is a linear subspace of $X$. 
== Proof ==
We use the One-Step Vector Subspace Test.
Since $Y \ne \O$ and $P \ne \O$ we clearly have $Z \ne \O$.
Let $x_1, x_2 \in Z$ and $\lambda \in \R$.
Then there exists $y_1, y_2 \in Y$ and $z_1, w_1, z_2, w_2 \in P$ such that:
:$x_1 = y_1 + z_1 - w_1$
and:
:$x_2 = y_2 + z_2 - w_2$
First suppose that $\lambda \ge 0$. 
We can write:
:$x_1 + \lambda x_2 = \paren {y_1 + \lambda y_2} + \paren {z_1 + \lambda z_2} - \paren {w_1 + \lambda w_2}$
Since $z_2, w_2 \succeq {\mathbf 0}_X$, we have $\lambda z_2, \lambda w_2 \succeq {\mathbf 0}_X$ by the definition of a preordered vector space.
Again from the definition of a preordered vector space we have $z_1 + \lambda z_2 \succeq {\mathbf 0}_X$ and $w_1 + \lambda w_2 \succeq {\mathbf 0}_X$.
So $z_1 + \lambda z_2 \in P$ and $w_1 + \lambda w_2 \in P$.
Since $Y$ is a linear subspace, we have $y_1 + \lambda y_2 \in Y$.
Hence we have $x_1 + \lambda x_2 \in Y + P - P$ in the case $\lambda \ge 0$. 
In the case $\lambda < 0$ we can write:
:$x_1 + \lambda x_2 = \paren {y_1 + \lambda y_2} + \paren {z_1 - \lambda w_2} - \paren {w_1 - \lambda z_2}$
Noting that $-\lambda \ge 0$, we have $z_1 - \lambda w_2 \in P$ and $w_1 - \lambda z_2 \in P$. 
Hence $x_1 + \lambda x_2 \in Y + P - P$ in the case $\lambda < 0$ as well.
So $Z$ is a linear subspace of $X$ by the One-Step Vector Subspace Test.
Extension Theorem for Positive Linear Functional defined on Cofinal Linear Subspace/Lemma 2

== Theorem ==
Let $\GF \in \set {\R, \C}$.
Let $\struct {X, \succeq}$ be a preordered vector space over $\R$.
Let $Y$ be a linear subspace of $X$ that is cofinal in $\struct {X, \succeq}$.
Let:
:$P = \set {x \in X : x \succeq {\mathbf 0}_X}$
Let:
:$Z = Y + P - P = \set {y + z - w : y \in Y, \, z, w \in P}$
be the Minkowski sum of $Y$, $P$ and $-P$.
Define $q : Z \to \R$ by:
:$\map q x = \inf \set {\map {f_0} y : y \in Y \text { and } y \succeq x}$
for each $x \in Z$.
That $q$ is well-defined was established in Extension Theorem for Positive Linear Functional defined on Cofinal Linear Subspace.
Then:
:$q$ is a sublinear functional.
== Proof ==
Let $x, z \in Z$. 
Note that if $y, w \in Y$ have $y \succeq x$ and $w \succeq z$, we have $y + w \succeq x + z$.
We are then able to deduce that:
:$\set {\map {f_0} {y + w} : y, w \in Y \text { and } y \succeq x, \, w \succeq z} \subseteq \set {\map {f_0} y : y \in Y \text { and } y \succeq x + z}$
From Infimum of Subset, we have:
:$\map q {x + z} \le \inf \set {\map {f_0} {y + w} : y, w \in Y \text { and } y \succeq x, \, w \succeq z}$
We further have from linearity:
:$\inf \set {\map {f_0} {y + w} : y, w \in Y \text { and } y \succeq x, \, w \succeq z} = \inf \set {\map {f_0} y : y \in Y \text { and } y \succeq x} + \inf \set {\map {f_0} w : w \in Y \text { and } w \succeq z}$
That is:
:$\map q {x + z} \le \map q x + \map q z$
So we have subadditivity. 
We just need to establish positive homogeneity. 
Let $x \in X$ and $\lambda > 0$. 
The key to this is the fact that for $\lambda > 0$ we have:
:$\set {y \in Y : y \succeq \lambda x} = \lambda \set {y \in Y : y \succeq x}$
From the definition of a preordered vector space, we have:
:$y \succeq \lambda x$ $\lambda^{-1} y \succeq x$ 
giving the equality.
Taking infimums and using Multiple of Infimum, we have:
:$\map q {\lambda x} = \lambda \map q x$ for each $x \in X$ and $\lambda > 0$.
We conclude that $q$ is a sublinear functional.
Extension Theorem for Total Orderings

== Theorem ==
Let the following conditions be fulfilled:
:$(1):\quad$ Let $\struct {S, \circ, \preceq}$ be a totally ordered commutative semigroup
:$(2):\quad$ Let all the elements of $\struct {S, \circ, \preceq}$ be cancellable
:$(3):\quad$ Let $\struct {T, \circ}$ be an inverse completion of $\struct {S, \circ}$.
Then:
:$(1):\quad$ The relation $\preceq'$ on $T$ satisfying $\forall x_1, x_2, y_1, y_2 \in S: x_1 \circ {y_1}^{-1} \preceq' x_2 \circ {y_2}^{-1} \iff x_1 \circ y_2 \preceq x_2 \circ y_1$ is a well-defined relation
:$(2):\quad$ $\preceq'$ is the only total ordering on $T$ compatible with $\circ$
:$(3):\quad$ $\preceq'$ is the only total ordering on $T$ that induces the given ordering $\preceq$ on $S$.
== Proof ==
By Inverse Completion is Commutative Semigroup:
:every element of $T$ is of the form $x \circ y^{-1}$ where $x, y \in S$.
=== Proof that Relation is Well-Defined ===
First we need to show that $\preceq'$ is well-defined.
So we need to show that if $x_1, x_2, y_1, y_2, z_1, z_2, w_1, w_2 \in S$ satisfy:
then:
:$x_2 \circ {w_2}^{-1} = y_2 \circ {z_2}^{-1}$
We have:
and:
So:
Thus $\preceq'$ is a well-defined relation on $T$.
=== Proof that Relation is Transitive ===
To show that $\preceq'$ is transitive:
Thus $\preceq'$ is transitive.
=== Proof that Relation is Total Ordering ===
To show that $\preceq'$ is a total ordering on $T$ compatible with $\circ$:
Let $z_1, z_2 \in T$.
Then:
:$\exists x_1, x_2, y_1, y_2 \in S: z_1 = x_1 \circ y_1^{-1}, z_2 = x_2 \circ y_2^{-1}$
Then:
:$z_1 \circ y_1 = x_1$
:$z_2 \circ y_2 = x_2$
As $\preceq$ is a total ordering on $S$, either:
:$z_1 \circ y_1 \circ y_2 \preceq z_2 \circ y_2 \circ y_1$
or:
:$z_2 \circ y_2 \circ y_1 \preceq z_1 \circ y_1 \circ y_2$
, suppose that:
:$z_1 \circ y_1 \circ y_2 \preceq z_2 \circ y_2 \circ y_1$
So:
and it is seen that $\preceq'$ is a total ordering on $T$.
=== Proof that Relation is Compatible with Operation ===
Let $x_1, x_2, y_1, y_2 \in T$ such that $x_1 \preceq' x_2, y_1 \preceq' y_2$.
We need to show that $x_1 \circ y_1 \preceq' x_2 \circ y_2$.
Let:
: $x_1 = r_1 \circ s_1^{-1}, x_2 = r_2 \circ s_2^{-1}$
: $y_1 = u_1 \circ v_1^{-1}, y_2 = u_2 \circ v_2^{-1}$
We have:
and
Because of the compatibility of $\preceq$ with $\circ$ on $S$:
Thus compatibility is proved.
=== Proof about Restriction of Relation ===
To show that the restriction of $\preceq'$ to $S$ is $\preceq$:
Conversely:
=== Proof that Relation is Unique ===
To show that $\preceq'$ is unique:
Let $\preceq^*$ be any ordering on $T$ compatible with $\circ$ that induces $\preceq$ on $S$.
Then:
Then:
So:
Hence as every element of $T$ is of the form $x \circ y^{-1}$ where $x, y \in S$, the orderings $\preceq^*$ and $\preceq'$ are identical.
== Sources ==
* : Chapter $\text {IV}$: Rings and Fields: $20$. The Integers: Theorem $20.6$
Category:Total Orderings
Category:Semigroups
Category:Named Theorems