Just and Weese I: Proof of Generalized Recursive Definitions

36 Views Asked by At

In Section 4.2 of "Discovering Modern Set Theory I." by Just and Weese, The proof of Theorem 25 (Principle of Generalized Recursive Definitions) considers the set of all $z \in Z$ such that there exists a function $F_z : I(z) \to X$ such that $F(y) = G(F|I(y),y)$ for each $y \in I(z)$. I am confused by this, and not just for lack of subscripts on $F$.

1) Since a wellfounded relation need not be transitive, $F_z(y) = G(F_z|I(y),y)$ does not seem to work, because $F_z|I(y)$ may not be a total function from $I(y)$ to $X$ since $y \in I(z) \kern.6em\not\kern -.6em \implies I(y) \subseteq I(z)$.

2) $F_z(y) = G(F_y|I(y),y)$ seems more plausible, but other $F_y$ have not been introduced in the preceding prose (whereas $F_z$ is explicitly quantified).

Should $F_z$'s domain be expanded to include the "downward closure" of $z$ with respect to the well-founded relation $W$, or am I missing something?