Realizability for constructive Zermelo-Fraenkel set theory

Question

$ \def \CZF {\mathbf {CZF}} \def \IZF {\mathbf {IZF}} \def \A {\mathcal A} \def \then {\mathrel \rightarrow} \def \r {\mathrel \Vdash} \DeclareMathOperator \V V $ In "Realizability for Constructive Zermelo-Fraenkel Set Theory", Michael Rathjen shows that a notion of realizability due to Charles McCarty works well for $ \CZF $ (Constructive Zermelo-Fraenkel set theory), a more restricted theory than $ \IZF $ (Intuitionistic Zermelo-Fraenkel set theory), which is the theory of concern in McCarty's work.

The notion is defined in terms of the realizability (class) structure $ \V ( \A ) $ over an applicative structure $ \A $. For $ e \in | \A | $ and a sentence $ \phi $ in the language of set theory extended by adding constants denoting members of $ \V ( \A ) $, realizability of $ \phi $ by $ e $ is defined recursively on the subformula tree of $ \phi $, and the notation "$ e \r \phi $" is used, read as "$ e $ realizes $ \phi $". The definition for the cases where $ \phi $ is not atomic is similar to the definitions for corresponding cases in the other well-known notions of realizability, e.g. that of Kleene defined for the theories of arithmetic. It is the definition of realizability for atomic sentences which I can't quite understand:

\begin{align*} e \r a \in b \iff& \exists c \big( \langle ( e ) _ 0 , c \rangle \in b \land ( e ) _ 1 \r a = c \big) \\ e \r a = b \iff& \forall f , d \Big( \big( \langle f , d \rangle \in a \then ( e ) _ 0 f \r d \in b \big) \land {} \\ &\qquad\qquad \big( \langle f , d \rangle \in b \then ( e ) _ 1 f \r d \in a \big) \Big) \end{align*}

Here $ a , b \in \V ( \A ) $, juxtaposition is used to denote application in the structure $ \A $, $ \langle . , . \rangle $ is a fixed pairing function, and $ ( . ) _ 0 $ and $ ( . ) _ 1 $ are the corresponding projections.

Struggling to understand how this definition works, I ended up asking myself the following questions, which I couldn't figure out, and thus I decided to ask here.

1. Isn't this definition circular? Something of the form $ e \r a = b $ appears in the definition of $ e \r a \in b $, and vice versa.
2. Is this definition sensitive to the minimal language of set theory? More specifically, if one extends the language by adding function symbols to the language, say a unary symbol denoting the union of members of a set, would the notion cease to work? Would one need to break the case of atomic sentences into cases where the form of the terms appearing in the sentence is taken into account? Or would it be similar to Kleene's realizability where the atomic sentences are treated regardless of the addition and multiplication symbols appearing in the terms?
3. In case where adding function symbols does not affect the way the definition works, does constructivity of the intended function really matter? This question comes for example from the fact that $ \IZF $ contains power sets, which may not be considered constructive (as they are rejected in $ \CZF $). To make this more specific and go even beyond $ \IZF $, would the notion of realizability work if we add a binary function symbol $ \chi $ to the language, with the intended meaning of the characteristic (class) function of membership, and add the following axioms to the language (one can either add $ \varnothing $ and $ \{ . \} $ to the language, or modify the following sentences in the obvious way so that they don't contain these symbols)?
   • $ \forall x , y ( x \in y \then \chi ( x , y ) = \{ \varnothing \} ) $
   • $ \forall x , y ( \neg x \in y \then \chi ( x , y ) = \varnothing ) $

---

Rathjen, Michael, Realizability for constructive Zermelo-Fraenkel set theory, doi:10.1017/9781316755785.015 Stoltenberg-Hansen, Viggo (ed.) et al., Logic colloquium ’03. Proceedings of the annual European summer meeting of the Association for Symbolic Logic (ASL), Helsinki, Finland, August 14–20, 2003. Wellesley, MA: A K Peters; Urbana, IL: Association for Symbolic Logic (ASL) (ISBN 1-56881-293-0/hbk; 1-56881-294-9/pbk). Lecture Notes in Logic 24, 282-314 (2006). ZBL1102.03053.

McCarty, Charles, Realizability and recursive set theory, doi:10.1016/0168-0072(86)90050-3 Ann. Pure Appl. Logic 32, 153-183 (1986). ZBL0631.03035.

Answer 1

For your first question, the definition of $e\Vdash x\in y$ and $e\Vdash x=y$ seems circular, but $\mathsf{CZF}$ provides a way to avoid the circularity, called inductive definition.

Definition. An inductive definition is a class $\Phi\subseteq \mathcal{P}(V)\times V$. For each inductive definition $\Phi$, define $\Gamma_\Phi(X)=\{a \mid \exists Y\subset X : (Y,a)\in \Phi\}$.

(Note that $X$ may be a class, but $Y$ must be a set.)

Sometimes we write $X/_\Phi a$ or $X\vdash_\Phi a$ instead of $(X, a)\in \Phi$, to emphasize the analog between deduction and inductive definition. In that view, we may think $\Gamma_\Phi(X)$ the least class containing $X$ that is closed under $\Phi$-deduction.

It is known that $\mathsf{CZF}$ admits arbitrary inductive definition (unlike $\mathsf{KP}$ only admit $\Sigma$-ones):

Theorem. (Class Inductive Definition Theorem) Let $\Phi$ be an inductive definition. Then there is a unique $\Gamma_\Phi$-least fixed point $I(\Phi)$, i.e., $I(\Phi)$ is least among classes such that $\Gamma_\Phi(I(\Phi))\subseteq I(\Phi)$.

But justifying the circular definition with an inductive definition is sometimes a bit tricky. In our case, it seems that we need a 'mutual' inductive definition to justify it.

Fortunately, it turns out that this is not the case: we may remove every formula of the form $f\Vdash x\in y$ in the definition of $e\Vdash a=b$ by replacing $f\Vdash x\in y$ to its definition, so we have a recursive definition of $e\Vdash a=b$. Then we can define $e\Vdash a\in b$ from $f\Vdash x=y$.

---

For your second question, I do not get the point of your question clearly, but if my understanding ― whether adding a new predicate or function into the language affects the definability of $\Vdash$ ― is correct, then I think the answer is yes in general. The reason is that Class Inductive Definition Theorem works for arbitrary $\Phi$, although adding functional symbols would require more justifications. For example, consider the case of adding the binary unpaired order function $\{,\}$. For each $a,b\in V^{\mathcal{A}}$ for a pca $\mathcal{A}$, define $$\mathsf{up}(a,b) = \{\langle\underline{0}, a\rangle,\langle\underline{1}, b\rangle\}.$$ Now interpret $\{,\}$ by making use of $\mathsf{up}$, that is, for each $a,b\in V^\mathcal{A}$, take $\{a,b\}^{V(\mathcal{A})} := \mathsf{up}(a,b)$. This means we will replace every occurrence of $\{a,b\}$ in the realizability relation to $\mathsf{up}(a,b)$.

A more dramatic example would be given by Chen and Rathjen: they defined $\Vdash$ over the extension of $\mathsf{CZF}$, which contains natural numbers and relevant operations as primitive notions. (Also it looks like a mere combination of the realizability à la McCarty and that of Kleene.)

---

For the last question, I think the answer is yes if the ambient theory ($\mathsf{CZF}$ in our case) proves the functionality of our desired function. The following theorem seems relevant (Proposition 9.6.2 of Aczel and Rathjen.)

Theorem. Let $T$ be a theory which comprises $\mathsf{BCST}$ (e.g. $\mathsf{CZF}$). Suppose $T \vdash ∀x ∃!yΦ(x, y)$. Let $T_Φ$ be obtained by adjoining a function symbol $F_Φ$ to the language, extending the schemata to the enriched language, and adding the axiom $∀x Φ(x, F_Φ(x ))$. Then $T_Φ$ is conservative over $T$.

Focusing on your example, in fact, we can define $\chi$ over $\mathsf{CZF}$: take $\chi(x,y)=\{0\mid x\in y\}$. By using this definition, we have a conservative extension of $\mathsf{CZF}$, and we may simply reduce $\chi$ in the extended language to a corresponding definition over $\mathsf{CZF}$.