Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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.
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.
1 to 2 of 2