$ \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.

- 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.
- 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?
- 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**, 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**, Ann. Pure Appl. Logic 32, 153-183 (1986). ZBL0631.03035.

Foundations of Constructive Mathematics, which is a clear exposition of most results up to that point, and probably includes McCarty’s work in the part on realizability for CZF. $\endgroup$