Strict Positivity Property induces Total Ordering

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $\struct {D, +, \times}$ be an integral domain whose zero is $0_D$.

Let $D$ be endowed with a (strict) positivity property $P: D \to \set {\mathrm T, \mathrm F}$.


Then there exists a total ordering $\le$ on $\struct {D, +, \times}$ induced by $P$ which is compatible with the ring structure of $\struct {D, +, \times}$.


Proof

By definition of the strict positivity property:

\((P \, 1)\)   $:$   Closure under Ring Addition:      \(\displaystyle \forall a, b \in D:\) \(\displaystyle \map P a \land \map P b \implies \map P {a + b} \)             
\((P \, 2)\)   $:$   Closure under Ring Product:      \(\displaystyle \forall a, b \in D:\) \(\displaystyle \map P a \land \map P b \implies \map P {a \times b} \)             
\((P \, 3)\)   $:$   Trichotomy Law:      \(\displaystyle \forall a \in D:\) \(\displaystyle \map P a \lor \map P {-a} \lor a = 0_D \)             
For $P \, 3$, exactly one condition applies for all $a \in D$.             


Let us define a relation $<$ on $D$ as:

$\forall a, b \in D: a < b \iff \map P {-a + b}$


Setting $a = 0$:

$\forall b \in D: 0 < b \iff \map P b$

demonstrating that (strictly) positive elements of $D$ are those which are greater than zero.


From Relation Induced by Strict Positivity Property is Compatible with Addition we have that $<$ is compatible with $+$.


From Relation Induced by Strict Positivity Property is Transitive we have that $<$ is transitive.

From Relation Induced by Strict Positivity Property is Asymmetric and Antireflexive we have that $<$ is asymmetric and antireflexive.

Thus by definition, $<$ is a strict ordering.


Let the relation $\le$ be defined as the reflexive closure of $<$.

From Reflexive Closure of Strict Ordering is Ordering we have that $\le$ is an ordering on $D$.


From Relation Induced by Strict Positivity Property is Trichotomy, and from the Trichotomy Law (Ordering), we have that $\le$ is a total ordering.

Hence the result.

$\blacksquare$


Also see


Sources