Timeline for Does negative trichotomy hold for constructive ordinals?
Current License: CC BY-SA 4.0
16 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 18 at 1:42 | answer | added | James E Hanson | timeline score: 2 | |
| Sep 24, 2023 at 9:14 | comment | added | Peter LeFanu Lumsdaine | [cont’d] In constructive settings, there really aren’t enough such orderings, and this motivates the zoo of other notions of ordinals, whose relationships are rather subtler. But the equivalence between “hereditarily transitive set” and “trans, w-f, ext’l relation” is straightforward and unproblematic. | |
| Sep 24, 2023 at 9:07 | comment | added | Peter LeFanu Lumsdaine | @ Jim Kingdon: Regarding the equivalence between definitions: The definition used in David Wärn’s answer is, essentially, the “structural”/“foundation-agnostic” way of phrasing the Powell definition that you link. It’s immediate (just from regularity + extensionality) that any hereditarily transitive set is a transitive, extensional, well-founded relation. Conversely, if you have enough set theory to do Mostowski collapse (so IZF certainly suffices), then every trans, ext, w-f relation is uniquely isomorphic to some hereditarily transitive set. [cont’d] | |
| Sep 24, 2023 at 2:02 | vote | accept | Jim Kingdon | ||
| Sep 24, 2023 at 1:59 | comment | added | Jim Kingdon | The definition of ordinal I have been working with is a class that is transitive and whose elements are transitive (and < is ∈). See us.metamath.org/ileuni/df-iord.html including a link to the Stanford Encyclopedia of Philosophy page that I was using as my reference. Obviously the rabbit hole of differing definitions of ordinal is a bit deeper than I realized but I'll accept the David Wärn answer because (assuming Peter LeFanu Lumsdaine's comment that it is indeed about this definition) that answers the question in the negative. | |
| Sep 23, 2023 at 14:02 | answer | added | David Wärn | timeline score: 7 | |
| Sep 23, 2023 at 10:02 | comment | added | Ingo Blechschmidt | The answer does NOT seem to be in this paper, but it still felt right to reference this jewel of Nicolai Kraus, Fredrik Nordvall Forsberg and Chuangjie Xu (and also Tom de Jong in a follow-up paper). They greatly clarify and explore the relations between several proposals for ordinals. They also study an intriguing form of trichotomy: trichotomy for ordinals which are known to be bounded by a common upper bound. | |
| Sep 23, 2023 at 6:56 | comment | added | Andrej Bauer | Strengthening @JamesHanson's question, which definition of ordinals are you using? There are several constructively inequivalent definitions. After thinking about this for 10 minutes, having an answer for any definition would be interesting. | |
| Sep 21, 2023 at 15:55 | comment | added | James E Hanson | What is the precise definition of $<$ that you're using? The answer might depend on that. Also, what does the double-negation translation of ZF into IZF get you in this context? Is it $\neg \neg \forall AB \neg\neg(A < B \vee A = B \vee B < A)$? | |
| Sep 21, 2023 at 15:20 | answer | added | Paul Taylor | timeline score: 1 | |
| Aug 25, 2023 at 16:45 | comment | added | Jim Kingdon | The elementary methods I and my collaborators used to find taboos at places like us.metamath.org/ileuni/ordtriexmid.html do not seem obviously applicable (at least, I didn't see how). | |
| Aug 25, 2023 at 16:42 | history | edited | Jim Kingdon | CC BY-SA 4.0 |
added 195 characters in body
|
| Aug 19, 2023 at 6:30 | comment | added | Dan Doel | Paul Taylor's Intuitionistic Sets and Ordinals suggests this is not possible. See page 18. There's no derivation of some 'taboo' though. Just a statement that the classical proof of trichotomy cannot be adapted even to a double negated version. | |
| Aug 13, 2023 at 23:03 | comment | added | Joel David Hamkins | Not sure if it is related, but the strength of the comparability principle for class well orders in second-order set theory (over GBC, for example, with classical logic) is an open question. The issues feel similar. | |
| Aug 13, 2023 at 22:52 | comment | added | mick | nice question ! | |
| Aug 13, 2023 at 22:20 | history | asked | Jim Kingdon | CC BY-SA 4.0 |