I have to prove the replacement lemma by structural induction. We define the logical complexity of a formula as follows:
Let $\varphi$ be a formula.
If $\varphi \in \left\{t, f\right\} \cup IV$ (where $IV$ is the set of propositional atoms), then $complexity(\varphi) = 0$.
If $\varphi = \neg \varphi_1$, then $complexity(\varphi) = complexity(\varphi_1) + 1$
If $\varphi = \varphi_1 \star \varphi_2$ $(\star \in \left\{\wedge, \rightarrow, \vee, \leftrightarrow \right\})$, then $complexity(\varphi) = complexity(\varphi_1) + complexity(\varphi_2) + 1$.
Now i shall prove the classical replacement lemma (semantic version). I.e
If $\mathcal{I} \models \varphi_1 \leftrightarrow \varphi_2$ for some interpretation $\mathcal{I}$ then $\mathcal{I} \models \psi\left[\varphi_1\right] \leftrightarrow \psi\left[\varphi_2\right]$
There's a hint that I shall prove the theorem by induction on
$g(\psi, \varphi_1) = complexity(\psi) - complexity(\varphi_1)$.
My idea is the following:
Let $n = g(\psi, \varphi_1)$.
Induction Base (n = 0): in this case it holds that (assuming $\psi$ contains at least on occurrence of $\varphi_1$) $\psi = \varphi_1$.
Induction Base (n = 1): Same here with $\psi = \neg \varphi_1$
Induction Base (n = 2): Same here with $\psi = \varphi_1 \star p$ for some prop. atom $p$ and $\star \in \left\{\wedge, \rightarrow, \vee, \leftrightarrow \right\}$
The problem now is the hypothesis. Assume the theorem holds for som $n$. Now show that it holds for $n + 1$...
Is this the right approach? How can I infer from $n$ to $n + 1$. Or am I completely wrong with my approach.
Thank you!