That has the $\Leftarrow$ direction, which is the nontrivial one.

]]>Is this also available at https://www.cs.bham.ac.uk/~mhe/TypeTopology/Ordinals.Notions.html#is-decidable-order?

]]>Following discussion with Sean Moss, here’s an improved version of this result: A well-founded relation is trichotomous iff it is transitive and extensional and decidable.

]]>I formalized Paul’s proof in Agda back in November, here: https://www.cs.bham.ac.uk/~mhe/TypeTopology/Ordinals.Notions.html#is-decidable-order.

]]>As explained in the well-order article, any well-order (i.e. extensional, transitive well-founded relation) is a linear order in classical mathematics. The proof given is rather complicated. Happily, within constructive mathematics, there’s a stronger result with a simple proof, as I’ll explain.

Given an irreflexive, transitive relation $\prec$ on a set $X$, say that elements $a, b \in X$ are *trichotomously related* when either $a \prec b$ or $a=b$ or $b \prec a$. (Clearly no more than one of these can be true.) Say that $\prec$ is *trichotomous* when any $a,b \in X$ are trichotomously related.

Theorem: a transitive well-founded relation $\prec$ on a set $X$ is trichotomous iff it is both extensional and decidable.

Proof: ($\Rightarrow$) is trivial. For ($\Leftarrow$), we claim that, for any $a,b \in X$, if $a$ is trichotomously related with every $y \prec b$, and every $x \prec a$ with $b$, then $a$ and $b$ are trichotomously related. Therefore any $a,b \in X$ are trichotomously related, by induction.

The claim is proved as follows. Decidability of the propositions $a \prec b$ and $b \prec a$ gives either $a \prec b$ or $b \prec a$ or both $a \nprec b$ and $b \nprec a$. In the last case, $x \prec a$ implies $x \prec b$, since $x$ is trichotomously related with $b$ but $x \neq b$ and $b \nprec x$, and likewise $y \prec b$ implies $y \prec a$, so extensionality gives $a=b$. Thus $a$ and $b$ are trichotomously related.

Martín Escardó has pointed out to me that this proof lies within intensional Martin-Löf dependent type theory.

]]>