Timeline for What are these non-classical versions of ZFC defined by realizability?
Current License: CC BY-SA 4.0
14 events
when toggle format | what | by | license | comment | |
---|---|---|---|---|---|
S Aug 24 at 20:00 | history | bounty ended | CommunityBot | ||
S Aug 24 at 20:00 | history | notice removed | CommunityBot | ||
Aug 16 at 18:31 | history | edited | Christopher King | CC BY-SA 4.0 |
added 123 characters in body
|
S Aug 16 at 18:26 | history | bounty started | Christopher King | ||
S Aug 16 at 18:26 | history | notice added | Christopher King | Draw attention | |
Dec 28, 2023 at 2:32 | comment | added | Christopher King | @JamesHanson oh I wouldn't say it's obvious. It follows from theorem 10.1 in the first paper. The realizer is pretty straight forward though, you just extract the function from your existential proof. Actually, for $\Vdash$ you might not even need any choice in the meta-theory 🤔. | |
Dec 28, 2023 at 0:24 | comment | added | James E Hanson | Is it obvious that you actually get a realizer for countable choice? This isn't clear to me at all. | |
Dec 27, 2023 at 0:47 | comment | added | François G. Dorais | Well, coming up with a meaningful axiomatization always requires artistry. I don't think "open problem" is a good description of this process. | |
Dec 27, 2023 at 0:15 | comment | added | Christopher King | @FrançoisG.Dorais do you think it might be an open problem? Like Gro-Tsen brought to my attention this has been studied for a while. | |
Dec 26, 2023 at 23:22 | comment | added | François G. Dorais | These results are often known as "Characterization Theorems". There are several examples of these but, as far as I can tell, there are quite a few that are missing. At least in the sense of "never explicitly stated". | |
Dec 26, 2023 at 21:17 | comment | added | Gro-Tsen | Did you read McCarty's 1986 papers “Realizability and recursive set theory” and “Subcountability under realizability” and section 3.5 of van Oosten's book Realizability: An Introduction to its Categorical Side (2008)? I don't think they have an answer as precise as you ask, but they certainly provide some important background. | |
Dec 26, 2023 at 20:08 | history | edited | Christopher King | CC BY-SA 4.0 |
edited title
|
Dec 26, 2023 at 20:02 | history | edited | Christopher King | CC BY-SA 4.0 |
added 27 characters in body
|
Dec 26, 2023 at 19:49 | history | asked | Christopher King | CC BY-SA 4.0 |