Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorPaul Blain Levy
   • CommentTimeMar 5th 2023
   • (edited Mar 5th 2023)
   • PermaLink
   Author: Paul Blain Levy
   Format: MarkdownItexAs 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]].

   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 on a set , say that elements are trichotomously related when either or or . (Clearly no more than one of these can be true.) Say that is trichotomous when any are trichotomously related.

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

   Proof: () is trivial. For (), we claim that, for any , if is trichotomously related with every , and every with , then and are trichotomously related. Therefore any are trichotomously related, by induction.

   The claim is proved as follows. Decidability of the propositions and gives either or or both and . In the last case, implies , since is trichotomously related with but and , and likewise implies , so extensionality gives . Thus and are trichotomously related.

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

2. • CommentRowNumber2.
   • CommentAuthormartinescardo
   • CommentTimeMar 6th 2023
   • (edited Mar 6th 2023)
   • PermaLink
   Author: martinescardo
   Format: MarkdownItexI formalized Paul's proof in Agda back in November, here: https://www.cs.bham.ac.uk/~mhe/TypeTopology/Ordinals.Notions.html#is-decidable-order.

   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.

3. • CommentRowNumber3.
   • CommentAuthorPaul Blain Levy
   • CommentTimeAug 11th 2023
   • PermaLink
   Author: Paul Blain Levy
   Format: MarkdownItexFollowing 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.

   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.

4. • CommentRowNumber4.
   • CommentAuthorDavidRoberts
   • CommentTimeAug 15th 2023
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexIs this also available at <https://www.cs.bham.ac.uk/~mhe/TypeTopology/Ordinals.Notions.html#is-decidable-order>?

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

5. • CommentRowNumber5.
   • CommentAuthorPaul Blain Levy
   • CommentTimeAug 15th 2023
   • PermaLink
   Author: Paul Blain Levy
   Format: MarkdownItexThat has the $\Leftarrow$ direction, which is the nontrivial one.

   That has the direction, which is the nontrivial one.