Timeline for Does negative trichotomy hold for constructive ordinals?
Current License: CC BY-SA 4.0
4 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 24, 2023 at 2:02 | vote | accept | Jim Kingdon | ||
| Sep 23, 2023 at 16:30 | comment | added | Peter LeFanu Lumsdaine | Very neat! OP’s link in comments to us.metamath.org/ileuni/ordtriexmid.html confirms he’s using the Powell definition of ordinal as “hereditarily transitive set”, which under a mild core of set theory matches what you take here. // A very slight rephrasing perhaps makes the countermodel simpler to follow: OP’s “not-not trichotomy” implies “for any down-closed subsets $X,Y \subseteq \omega$, not-not ($X \subseteq Y$ or $Y \subseteq X$)”; then your model is a counterexample to the latter, with $X, Y$ just as subsets of $\omega$ (so we never need to view them as ordinals in the topos). | |
| Sep 23, 2023 at 14:41 | history | edited | David Wärn | CC BY-SA 4.0 |
correct typo
|
| Sep 23, 2023 at 14:02 | history | answered | David Wärn | CC BY-SA 4.0 |