I just started studying logic, not as a course at a university, but as pastime. Since I do not study logic at an institution I use many different textbooks, including Enderton's $A$ $Mathematical$ $Introduction$ $to$ $Logic$ and Van Dalen's $Logic$ $and$ $Structure$. Now, my question is this: Is the following theorem (Van Dalen p. 11) a reformulation of the usual recursion theorem? If not, then how would one go about proving this theorem.
Let mappings $H_{\square}: A^{2} \to A$ and $H_{\neg}:A \to A$ be given and let $H_{at}$ be a mapping from the set of atoms into $A$, then there exists exactly one mapping $F:PROP \to A$ $$F(\phi) = H_{at}(\phi) \quad \text{for $\phi$ atomic,}$$ $$ F((\phi \square \psi)) = H_{\square}(F(\phi),F(\psi)),$$ $$F((\neg \phi)) =H_{\neg}(F(\phi))$$
Thank you for taking the time to read this question.
Depending on what you mean by "the" recursion theorem (there are too many results using the same name), this claim may or may not be seen as a particular case, or even as equivalent. I find it better to argue directly than to try to make it fit abstractly into some setting and then deduce it as a corollary.
One way to proceed is by strong induction on the length of the propositional formulas, first verifying that for each $n$ there is a unique $F_n$ defined on formulas of length at most $n$, and satisfying the three requirements.
This is clear if $n=1$, since the last two clauses doe not apply, and the first one tells us exactly what $F_1$ is: $$F_1=H_{at}\upharpoonright\{\mbox{Propositional formulas}\}.$$
If $n>1$ and the result is true for formulas of length strictly less $n$, it also holds for formulas of length $n$, that is: If for all $m<n$ there is a unique $F_m$ defined on formulas of length at most $m$ and satisfying the three requirements, then the same holds for $n$.
To see this, suppose first that $F_n$ and $F_n'$ are two functions satisfying the three requirement, and defined on the set of formulas of length at $n$. For any $m<n$, the restriction of $F_n$ to formulas of length at most $m$ must be $F_m$ (by the inductive assumption) and similarly for $F_n'$. It follows that if $F_n$ and $F_n'$ disagree, the disagreement occurs on a formula of length precisely $n$. But any such formula, not being atomic, is either $(\lnot\phi)$ or $(\phi\mathrel{\square}\psi)$ for some shorter formulas $\phi,\psi$, and some binary connective $\square$.
In the first case, we have $$ F_n((\lnot\phi))=H_{\lnot}(F_n(\phi))=H_{\lnot}(F_{n-3}(\phi))=H_{\lnot}(F_n'(\phi))=F_n'((\lnot\phi)), $$ since $F_n$ and $F_{n'}$ satisfy the third requirement, and the inductive assumption on the uniquenesss of $F_{n-3}$.
The second case is completely analogous. This shows that there is no disagreement between $F_n$ and $F_n'$, and uniqueness follows.
To prove existence is similar, if only slightly more cumbersome. We can define $F_n$ using the three given clauses, and the existence of the previous functions $F_m$. For example, $F_n(\phi)$ is defined as $F_1(\phi)$ if $\phi$ is atomic, and as $H_\square(F_m(\psi),F_j(\tau))$, if $\phi$ is $(\psi\mathrel{\square}\tau)$ where $\psi$ is a formula of length $m$ and $\tau$ is a formula of length $j$ (and similarly for the remaining case).
That this is well defined follows from the (previously established) result that there is unique readability of formulas, so: Given any $\phi$, it is either atomic, or it has the form $(\lnot\tau)$, and $\tau$ is a formula, or it has the form $(\psi\mathrel{\square}\tau)$, for some formulas $\psi,\tau$ and some binary connective $\square$. Moreover, these cases are mutually exclusive, and in the last case, there is a unique such decomposition of $\phi$.
Once we have that $F_n$ is well-defined, it follows trivially that it satisfies the three requirements: First, the inductive assumption gives us (again) that $F_n$ extends the unique $F_m$ whenever $m<n$. This ensures that the three requirements hold when evaluating $F_n(\phi)$ for formulas $\phi$ of length less than $n$. For $\phi$ of length precisely $n$, this follows from the definition of $F_n$, noticing that since $F_n$ extends the functions $F_m$ for $m<n$, then, for example, $$ F_n((\psi\mathrel{\square}\tau))=H_\square(F_m(\psi),F_j(\tau))=H_\square(F_n(\psi),F_n(\tau)). $$
Now that we have established existence and uniqueness of the $F_n$, we have that the functions are compatible, in the sense that their graphs extend each other: $$F_1\subseteq F_2\subseteq F_3\subseteq \dots$$ This means that $F=\bigcup_n F_n$ is a function, and it satisfies the three requirements since each $F_n$ does. But $F$ has domain the set $\mathsf{PROP}$ of all propositional formulas. Uniqueness of $F$ is as before, noticing that if $F$ is any function with domain $\mathsf{PROP}$ and satisfying the three requirements, its restriction to formulas of length at most $n$ is precisely $F_n$, so in fact $F=\bigcup_n F_n$.