Skip to main content
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