See Kleene realizability in Peano arithmetic for a similar question, but about PA instead of ZFC. (In particular, an answer as specific as Emil Jeřábek's answer would be great!)
In the context of constructive set theory, consider two ways of defining realizability.
The first is $\Vdash$, which is just the set theoretic version of Kleene's realizability. The $\Vdash$ relation is defined at Realizability for Constructive Zermelo-Fraenkel Set Theory, "Definition: 4.1".
The second is $\Vdash_{rt}$ "realizability with truth". It is defined at The Disjunction and Related Properties for Constructive Zermelo-Fraenkel Set Theory, "Definition 5.2".
The main difference is that, in every subcase, $e \Vdash_{rt} \phi$ also asserts that $\phi$ is true. For example, $e \Vdash \phi \implies \psi$ means $$\forall f. (f \Vdash \phi \implies ef \Vdash \psi)$$ whereas $e \Vdash_{rt} \phi \implies \psi$ means $$(\phi^\circ \implies \psi^\circ) \land \forall f. (f \Vdash_{rt} \phi \implies ef \Vdash_{rt} \psi)$$
For example, if our meta-theory is ZFC, the statement "all real numbers are computable" is realized according to $\Vdash$ whereas the statement "not all real numbers are computable" is realized according to $\Vdash_{rt}$, but "there exists a real number that is not computable" is realized according to neither.
Now consider the following four theories:
| Known witness | Witness exists | |
|---|---|---|
| Anti-classical | $\text{ZFC}_1 = \{\phi : \exists e. \text{ZFC} \vdash (\overline e \Vdash \phi) \}$ | $\text{ZFC}_2 = \{\phi : \text{ZFC} \vdash (\exists e. e \Vdash \phi) \}$ |
| Realizable with truth | $\text{ZFC}_3 = \{\phi : \exists e. \text{ZFC} \vdash (\overline e \Vdash_{rt} \phi) \}$ | $\text{ZFC}_4 = \{\phi : \text{ZFC} \vdash (\exists e. e \Vdash_{rt} \phi) \}$ |
Usually realizability is considered with an intuitionistic meta-theory, but it works just as well with ZFC.
My question is how do you nicely axiomatize them, as was done in this answer for Peano arithmetic?
Some observations:
- $\text{ZFC}_1$ and $\text{ZFC}_3$ have the disjunction property and the other nice properties from the second paper. $\text{ZFC}_2$ and $\text{ZFC}_4$ do not because they prove LEM for $\Sigma^0_1$ sentences.
- They are definitely recursively enumerable, since we're just searching for proofs in ZFC.
- $$IZF \subset \text{ZFC}_1 \subset \text{ZFC}_2$$ $$IZF \subset \text{ZFC}_3 \subset \text{ZFC}_4 \subset \text{ZFC}$$
- Since ZFC has the axiom of choice, the four theories all prove the axiom of countable choice (and thus are not just $\text{IZF}$).
- $\text{ZFC}_1$ (and thus also $\text{ZFC}_2$) proves CT, which is incompatible with LEM.
- $\text{ZFC}_3$ (and thus also $\text{ZFC}_4$) proves $\lnot \phi$ for statements $\phi$ such that $\lnot \phi$ is a theorem of $\text{ZFC}$.
