Timeline for Is Bauer–Hanson’s result “there is a topos where the Dedekind reals are countable” novel?
Current License: CC BY-SA 4.0
7 events
when toggle format | what | by | license | comment | |
---|---|---|---|---|---|
Aug 23, 2023 at 23:55 | history | edited | LSpice | CC BY-SA 4.0 |
Name of paper; typo
|
Aug 23, 2023 at 18:09 | comment | added | James E Hanson | Well technically doesn't the tripos-to-topos construction (typically) use a whole model of ZFC? Isn't that a tad bit less constructive than one measly little application of weak Kőnig's lemma? | |
Aug 23, 2023 at 17:30 | comment | added | Andrej Bauer | I'd say we construct the topos allright, but we don't construct a Miller sequence (by which the topos is parameterized), because its existence is non-constructive. | |
Aug 23, 2023 at 17:20 | history | edited | James E Hanson | CC BY-SA 4.0 |
added 8 characters in body
|
Aug 23, 2023 at 17:13 | history | edited | James E Hanson | CC BY-SA 4.0 |
added 599 characters in body
|
Aug 23, 2023 at 17:07 | comment | added | James E Hanson | I guess I should be slightly careful with the word 'construct' when referring to the topos itself in that the proof relies on a strengthened form of Brouwer's fixed-point theorem, which is famously non-constructive. Although we were told by Blechschmidt that known conservativity results imply that the consistency result itself must go through in IZF. | |
Aug 23, 2023 at 16:52 | history | answered | James E Hanson | CC BY-SA 4.0 |