Suppose I'm working in the language of first order logic and I have wffs of the following form.
- If $\phi$ is atomic then $\phi$ is a wff.
- If $\phi$ is a wff then $(\lnot \phi)$ is a wff.
- If $\phi$ and $\psi$ are wffs then $(\phi \implies \psi)$ is a wff.
It is then possible to define the depth of a wff $D$ (thought of as a function from wffs to the natural numbers) as
- If $\phi$ is atomic then $D(\phi)=1$
- If $\phi\equiv (\lnot \psi)$ with $\psi$ a wff then $D(\phi) = D(\psi)+1$
- If $\phi \equiv (\pi \implies \psi)$ with $\pi, \psi$ wffs then $D(\phi) = \max(D(\pi), D(\psi))+1$
I'm realize we may working with informal notions when defining the language, but there should be a formal-like justification along the lines of the recursion theorem that justifies the definition of the function $D$.
I understand the recursion theorem to be
Let $X$ be a set, let $a\in X$ and let $g:X\to X$ be a function. Then there exists a unique function $f:\mathbb{N}\to X$ such that $f(1)=a$ and $f(n+1) = g(f(n))$ for all $n$.
I imagine that in my case $X$ is the set of wffs and the function $g$ is one of the formation rules for wffs. Like $g_{\lnot}(\phi) \equiv (\lnot \phi)$ or $g_{\implies}(\pi, \psi) \equiv (\pi \implies \psi)$. But this is my first point of confusion. In this case I seem to have two functions $g$ rather than just one. How to apply the recursion theorem?
Second, the recursion theorem seems to imply the existence of a function $f:\mathbb{N}\to X$, but I'm seeing a function $D: X\to \mathbb{N}$, so not sure what needs to be adjusted to help justify the definition of the function $D$.
Finally, the reason I am interested in this is that it seems to me the existence of such a function $D$ is non-trivial. In fact, it somehow relies on the unique readability of wffs. For example, if my formation rules had no parentheses we could consider the wff $$ \phi \equiv \lnot \pi \implies \lnot \psi $$ If we parse this as $((\lnot \pi)\implies (\lnot \psi))$ then $D(\phi) = 3$, but if we parse it as $(\lnot(\pi\implies (\lnot \pi)))$ then $D(\phi) = 4$. In this case $D$ is only a non-functional relation between wffs and $\mathbb{N}$. So my goal is to capture a formal/informal proof that $D$ is a well-defined function on wffs which illuminates the fact that unique readability of wffs is necessary for the definition.