Definition by Recursion 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. 
 A: 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$.
