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!
Best Answer
Your induction hypothesis should be that $n>0$ and the result is true whenever $g(\psi,\phi_1)<n$. Now suppose that $g(\psi,\phi_1)=n$. They $\psi$ is either $\lnot\psi_1$ for some $\psi_1$, or $\psi_1\oplus\psi_2$ for some $\psi_1$ and $\psi_2$ and some $\oplus\in\{\land,\lor,\to,\leftrightarrow\}$.
If $\psi=\lnot\psi_1$, it’s not hard to see that $g(\psi_1,\phi_1)<n$, so if some $\mathcal{I} \models \varphi_1 \leftrightarrow \varphi_2$, then $\mathcal{I} \models \psi_1[\varphi_1] \leftrightarrow \psi_1[\varphi_2]$ by the induction hypothesis, and the desired result now presumably follows from your definition of $\models$.
The argument in case $\psi=\psi_1\oplus\psi_2$ is similar, since you will have $g(\psi_1,\phi_1),g(\psi_2,\phi_1)<n$.