I'm reading the Foundations of mathematical logic by Peter Hinman, and something is unclear to me in his applications of theorem 1.2.14.
Here's the theorem:
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 $\left\langle G_H : H \in \mathcal{H} \right\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:\overline{X} \to Z$ such that F extends $F_0$ and for each $H \in \mathcal{H}$ and $ x_0,..., x_{k_{H}-1} \in \overline{X}$, $ F(H(x_0,..., x_{k_{H}-1})) = G_{H}(F(x_0),..., F(x_{k_{H}-1}),x_0,...,x_{k_{H}-1}) $
when $k_{H}$ is the arity of function $H$ and $\overline{X}$ is the inductive closure of $\mathcal{X}$
After it's proof, there's a couple of examples, for instance:
(1) $\text{The set of sentence symbols which occur in a sentence } \phi \text{ is given by the unique function }$ $ At : Sent_L \to \mathcal{P}( \lbrace p_n : n \in \omega \rbrace) $ which satisfies the conditions $$(a) At(p_n) = \lbrace p_n \rbrace $$ $$(b) At(\neg p_n) = At(p_{n}) $$ $$(c) At(\bullet \phi \theta) = At(\phi)\, \cup \, At(\theta)$$ where • represents any one of the binary connectives.
$\omega$ denotes the set of natural numbers, and $Sent_L$ is the propositional language which is an example to an induction system. The author states that the way of defining this function corresponds to the principle that appears in the theorem, but I'm not sure how it works. In the theorem, $G_H$ are functions from the set $Z^{k_{H}}$ to $Z$ when $k_H$ is the arity of $H$, and in the example, the value of $At(H(p_n))$ for $H=\neg, \, \wedge, \, \vee, \, \to, \, \leftrightarrow $ may depend on the value of $At(p_n)$. Although it fits well with the intuition behind recursion, I can't figure out if it's possible to find the functions $G_H:(\mathcal{P}(\lbrace p_n : n \in \omega \rbrace))^{k_{H}} \to \mathcal{P}(\lbrace p_n : n \in \omega \rbrace)$ that will satisfy $At(H(p_n)) = G(At(p_n))$ for each sentence symbol $p_n$. Maybe the author meant that this definition corresponds with the proof of the theorem which uses generalized induction to define the extended function F, and we should justify the definition (1) by induction?
Let $X_0=\lbrace p_n : n \in \omega \rbrace$, $X = Sent_L$, $\mathcal{H}=\{\neg, \, \wedge, \, \vee, \, \to, \, \leftrightarrow\}$ and $Z=\mathcal{P}(X_0 )$.
Define functions $F_0:X_0 \rightarrow Z , G_{\neg}:Z\times X \rightarrow Z $ and $G_{\bullet}:Z^2\times X^2 \rightarrow Z $ as
$$F_0(p_n)=\{p_n\},$$ $$G_{\neg}(z,x)=z$$ $$G_{\bullet}\big{[}(p_1,p_2),\, (x_1,x_2)\big{]} = p_1 \cup p_2$$
The conditions satisfied by the function $F$ given by the theorem are precisely the conditions that define $At$.