Definition:Strict Negativity Property

From ProofWiki
Jump to navigation Jump to search


Let $\struct {D, +, \times}$ be an ordered integral domain, whose (strict) positivity property is denoted $P$.

The strict negativity property $N$ is defined as:

$\forall a \in D: \map N a \iff \map P {-a}$

This is compatible with the trichotomy law:

$\forall a \in D: \map P a \lor \map P {-a} \lor a = 0_D$

which can therefore be rewritten:

$\forall a \in D: \map P a \lor \map N a \lor a = 0_D$

or even:

$\forall a \in D: \map N a \lor \map N {-a} \lor a = 0_D$