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