Timeline for Does negative trichotomy hold for constructive ordinals?
Current License: CC BY-SA 4.0
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 10 at 5:03 | comment | added | Jim Kingdon | I won't try to add comments for all our fine tuning in metamath but a look at us.metamath.org/ileuni/onntri35.html will show what we have done (including a formalization of the proof from the HoTT Book mentioned above). | |
| Aug 5 at 15:00 | comment | added | Jim Kingdon | The metamath formalization is up at us.metamath.org/ileuni/onntri35.html . Oddly enough the one part which isn't formalized yet is "5 clearly implies 1 and 2". I assume the intended proof is based on excluded middle implying ordinal trichotomy? This can of course be done (the HoTT book has a proof) but we haven't yet formalized that - see github.com/metamath/set.mm/issues/739 | |
| Aug 3 at 6:39 | comment | added | Jim Kingdon | Nice. I have formalized most of this at github.com/metamath/set.mm/pull/4108 . Please speak up (on that pull request, I guess) if you have any questions or input about the formalization in metamath, or me listing you as a co-contributor there (for the informal proofs in the above answer). | |
| Jul 18 at 1:52 | history | edited | James E Hanson | CC BY-SA 4.0 |
added 221 characters in body
|
| Jul 18 at 1:42 | history | answered | James E Hanson | CC BY-SA 4.0 |