I'm using Van Dalen's Logic and Structure to get a better grip on logic, with particular interest in recursively defined structures. The first chapter deals with propositional logic. At a certain point, the following theorem is given:
Definition by recursive formulas : Let $A$ a set, $H_{At} : At \to A$ and $H_\circ : A^2 \to A$. There is a unique $F : PROP \to A$ such that $$ \begin{cases} F(\psi) &= H_{At}(\psi) \\ F(\psi \circ \varphi) &= H_\circ(F(\psi), F(\varphi)) \end{cases} $$
Here, $PROP$ is the set of all propositional formulas, $At$ is the subset of $PROP$ comprised of only atomic propositions ($p_1, p_2, \ldots)$, and $\circ$ is any logical connective ($\land, \lor, \ldots$).
The theorem is clear enough. It provides a formal understanding of recursive formulas and shows how functions from propositions to values can be recursively reduced to functions from atomic propositions to values.
Later on, I found this problem:
Define a recursive function that maps to every $\varphi \in PROP$ the number of left parenthesis in the formula.
I solved this problem in the following manner. First, let $f: PROP \to \mathbb{N}$ be the required function. We must consider four possible cases: $\varphi$ is atomic, $\varphi \circ \psi$ are both non-atomic, $\varphi \circ \psi$ has one atomic and one non-atomic, or $\varphi \circ \psi$ are both atomic. This is clear, because the amount of parenthesis depends only on this.
Further explanation: A connective between two atomic propositions has no parenthesis; a connective between an atomic and a non-atomic has parenthesis only on the non-atomic proposition; a connective between two non-atomic propositions has parenthesis surrounding both.
So, we come to the following formulation:
\begin{align*} &f(\varphi) = 0 ~ ~ ~ ~ ~ ~ ~ ~ ~ \varphi \in At \\ &f(\varphi \circ \psi) = \begin{cases} 1 + f(\varphi) + f(\psi) & \varphi \in At \lor^{\text{exclusive}} \psi \in At \\ f(\varphi) + f(\psi) & \{\varphi, \psi\} \subseteq At \\ 2 + f(\varphi) + f(\psi) & \text{otherwise} \end{cases} .\end{align*}
For example, consider $P = \left( (a \land b) \to q) \right) \to \left( (a \lor b) \land c \right)$. Then
\begin{align*} f(P) &= 2 + f\left( (a \land b) \to q \right) + f\left( (a \lor b) \land c \right) \\ &=2 + (1 + f(a \land b) + f(q)) + (1 + f(a \lor b) + f(c)) \\ &= 2 + 1 + 1 \\ &= 4 .\end{align*}
which is the correct result.
Although my function works, in the sense that it maps propositions to the desired value, I am not sure it follows the form defined in the theorem presented at the beginning of the question. Namely, the function does not map the case $\varphi \circ \psi$ to a single $H_\circ(F(\varphi), F(\phi))$. On the contrary, our $H_\circ$ function has different definitions according to whether its arguments are both atomic, both non-atomic, etc.
This may seem a minor detail, but I am highly concerned with rigor here (what's the point of studying logic rigorously if not). Is my $f$ function correct, in the sense that it is a recursive definition in the sense given by the theorem?