Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorPaul Blain Levy
    • CommentTimeMar 5th 2023
    • (edited Mar 5th 2023)

    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 XX, say that elements a,bXa, b \in X are trichotomously related when either aba \prec b or a=ba=b or bab \prec a. (Clearly no more than one of these can be true.) Say that \prec is trichotomous when any a,bXa,b \in X are trichotomously related.

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

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

    The claim is proved as follows. Decidability of the propositions aba \prec b and bab \prec a gives either aba \prec b or bab \prec a or both aba \nprec b and bab \nprec a. In the last case, xax \prec a implies xbx \prec b, since xx is trichotomously related with bb but xbx \neq b and bxb \nprec x, and likewise yby \prec b implies yay \prec a, so extensionality gives a=ba=b. Thus aa and bb are trichotomously related.

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

    • CommentRowNumber2.
    • CommentAuthormartinescardo
    • CommentTimeMar 6th 2023
    • (edited Mar 6th 2023)

    I formalized Paul’s proof in Agda back in November, here:

  1. 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.

    • CommentRowNumber4.
    • CommentAuthorDavidRoberts
    • CommentTimeAug 15th 2023
  2. That has the \Leftarrow direction, which is the nontrivial one.