[[!redirects decidable pseudo-order]] [[!redirects decidable strict total order]] [[!redirects decidable strict linear order]] [[!redirects decidable strictly ordered set]] ## Definition ## Given a [[decidable set]] $(A, \equiv)$, a function $(-)\lt(-):A \times A \to \mathbb{2}$ is a __decidable strict order__ (also called __decidable strict total order__, __decidable strict linear order__, or __decidable pseudo-order__) if it comes with * an identity $$\iota: \prod_{a:A} P(a) = 1$$ representing the irreflexivity condition for the decidable binary relation, where the decidable predicate $P(a)$ is defined as $$P(a) \coloneqq \neg(a \lt a)$$ * an identity $$\kappa: \prod_{a:A} \prod_{b:A} \prod_{c:A} Q(a,b,c) = 1$$ representing the comparison condition for the binary relation, where the decidable predicate $Q(a,b,c)$ is defined as $$Q(a,b,c) \coloneqq (a \lt c) \implies ((a \lt b) \vee (b \lt c))$$ * an identity $$\gamma: \prod_{a:A} \prod_{b:A} R(a,b) = 1$$ representing the connectedness condition for the binary relation, where the decidable predicate $R(a,b)$ is defined as $$R(a,b) \coloneqq \neg((a \lt b) \wedge (b \lt a)) \implies (a \equiv b)$$ * an identity $$\alpha: \prod_{a:A} \prod_{b:A} S(a,b) = 1$$ representing the asymmetry condition for the binary relation, where the decidable predicate $S(a,b)$ is defined as $$S(a,b) \coloneqq (a \lt b) \implies \neg(b \lt a)$$ $A$ is called a __decidable strictly ordered set__. ## See also ## * [[decidable directed graph]] * [[decidable set]] * [[decidable open interval]] * [[decidable dense strict order]] category: not redirected to nlab yet