I'm working through Hinman's Fundamentals of Mathematical Logic in order to review some things, and got stuck in an exercise from section 1.2. Specifically, he asks us to prove (what he calls) the Generalized Recursion Theorem using the inductive closure of an induction system and without using ordinary recursion. I'll first state some definitions, then the theorem, and finally I'll explain my difficulties with the proof.
An induction system is simply a triple $\mathcal{X} = (X, X_0, \mathcal{H})$, such that $X$ is a non-empty set, $X_0 \subseteq X$ and $\mathcal{H}$ is a set of finitary functions on $X$. Now, for any induction system $\mathcal{X}$ and any $Y \subseteq X$, we say that $Y$ is $\mathcal{X}$-closed iff $X_0 \subseteq Y$ and, for all $H \in \mathcal{H}$ and all $x_0, \dots, x_{k_H-1}$ (where $k_H$ is the arity of $H$), $H(x_0, \dots, x_{k_H-1}) \in Y$. Given this, we define the inductive closure of $X_0$ under $\mathcal{H}$, in symbols $\bar{X}$, as the smallest $\mathcal{X}$-closed subset of $X$. Finally, if the images of $H \in \mathcal{H}$ are pairwise disjoint and disjoint from $X_0$, and if every $H \in \mathcal{H}$ is injective on $X$, we say that $\mathcal{X}$ has unique readability.
Hinman than states the following theorem (definition by generalized recursion):
Let $\mathcal{X} = (X, X_0, \mathcal{H})$ be an induction system which has unique readability. For any set $Z$, any function $F_0: X_0 \to Z$ and any family $\langle G_H : H \in \mathcal{H}\rangle$ of functions such that for all $H \in \mathcal{H}$, $G_H: Z^{K_H} \times X^{k_H} \to Z$, there exists a unique function $F: \bar{X} \to Z$ such that $F$ extends $F_0$ and for each $H \in \mathcal{H}$ and $x_0, \dots, x_{k_H-1} \in \bar{X}$,
$F(H(x_0, \dots, x_{k_H-1})) = G_H(F(x_0), \dots, F(x_{k_H-1}), x_0, \dots, x_{k_H-1})$.
In exercise 1.2.20, Hinman asks us to prove this result without appealing to the special case of ordinary recursion over $\omega$. He suggest the following method: identify $F_0$ with its graph and consider an inductive system $\mathcal{Y} = (\bar{X} \times Z, F_0, \mathcal{I})$ whose inductive closure is the desired $F$. It seems clear that most of the work of the exercise goes into finding an appropriate family of functions which yield the desired $F$; once you find this family, proving that $F$ is a function with the desired properties should be easy. My problem is precisely in identifying this $\mathcal{I}$. My first impulse was to define this $\mathcal{I}$ by defining it as a family of approximation functions $F_n$ such that, for each $n$, $F_n(x) = G_H(F_{n-1}(x_0), \dots, F_{n-1}(x_{k_H-1}), x_0, \dots, x_{k_H-1})$. But this will obviously use recursion in order to define each $F_n$, so it's not what Hinman wants. Another idea was to use directly the functions $G_H$, but these have domains disjoint from $F$, so it doesn't seem to work either. After that, I didn't have any other idea. Any suggestions?
EDIT: One thing that I realized is that for $I \in \mathcal{I}$, the domain of $I$ will be $(\bar{X} \times Z)^{k_I}$ ($k_I$ being the arity of $I$) and the range will be $\bar{X} \times Z$. So what I need is a family of functions whose domain will be (the graph of) functions from $\bar{X}$ to $Z$ and whose range will be (I think) the (graphs of the) surrogate functions I want. But I'm still in doubt about how to describe this family...
Well, since nobody has tackled this question, I ended up sending an email to prof. Hinman himself, who was kind enough to give me the correct equation for the family of functions $\mathcal{Y}$. Here's the full answer that I worked out for this question (it's a bit sketchy at the end, but the idea is clear enough, I think).
First, identify $F_0$ with its graph, so that $F_0 \subseteq \bar{X} \times Z$. Set now an induction system $\mathcal{Y} = (\bar{X} \times Z, F_0, \mathcal{I})$ such that, for each $H \in \mathcal{H}$, $\mathcal{I} = \{ I_H \; | \; H \in \mathcal{H}\}$. Define
I claim that $\bar{Y}$ is the desired $F$.
First, we need to show that $\bar{Y}$ is a function, that is, that for each $x \in \bar{X}$, there is one, and only one $z \in Z$, such that $(x, z) \in \bar{Y}$; in other words, if $(x, y) \in \bar{Y}$ and $(x, y') \in \bar{Y}$, then $y = y'$. The proof is by $\mathcal{Y}$-induction. Since $F_0$ is by hypothesis a function, it's clear that every pair in $F_0$ satisfies the theorem. Assume the induction hypothesis, that is, that the theorem holds for $(x_0, z_0), \dots, (x_{k_H -1}, z_{k_H-1})$ and consider $I_H((x_0, z_0), \dots, (x_{k_H -1}, z_{k_H-1})) = (x, z)$. Suppose there are $x'_0, \dots, x'_{k_H-1}, z'_0, \dots, z'_{k_H-1}$ such that $I_H((x'_0, z'_0), \dots, (x'_{k_H-1}, z'_{k_H-1})) = (x, z')$. By definition, $I_H = ((x_0, z_0), \dots, (x_{k_H -1}, z_{k_H-1})) = (H(x_0,\dots, x_{k_H-1}), G_H(z_0, \dots, z_{k_H-1}, x_0, \dots, x_{k_H-1}))$.
Thus, $x = H(x_0, \dots, x_{k_H-1}) = H(x'_0, \dots, x'_{k_H-1})$. Since, by hypothesis, $H$ is injective, it follows that $x_0 = x'_0, \dots, x_{k_H-1} = x'_{k_H-1}$. But then, by the induction hypothesis, $z_0 = z'_0, \dots, z_{k_H-1} = z'_{k_H-1}$, whence $(x, z) = I_H((x_0, z_0), \dots, (x_{k_H -1}, z_{k_H-1})) = I_H((x'_0, z'_0), \dots, (x'_{k_H-1}, z'_{k_H-1})) = (x, z')$, that is, $z = z'$.
Second, I'll show that $\bar{Y}$ satisfies the conditions of the theorem. In order to facilitate reading, let's set $\bar{Y} = F$. In the first place, since $F_0 \subseteq \bar{Y}$ by definition, it's obvious that $F$ extends $F_0$. So it remains to be seen that, for each $H \in \mathcal{H}$ and $x_0, \dots, x_{k_H-1}$,
Again, the proof is by $\mathcal{Y}$-induction. So identify $F$ with its graph. For the basis case, there's nothing to prove. Assume, as the induction hypothesis, that the above equation holds for $(x_0, z_0), \dots, (x_{k_H-1}, z_{k_H-1})$. Consider now $I_H((x_0, z_0), \dots, (x_{k_H-1}, z_{k_H-1}))$, i.e. the pair $(H(x_0, \dots, x_{k_H-1}), G_H(z_0, \dots, z_{k_H-1}, \dots, x_0, \dots, x_{k_H-1})$. But, for each $z_i (i \leq k_H-1)$, it's obvious that $z_i = F(x_i)$, thus concluding the proof.