# Structural Induction — Logic

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!

-
It seems to me that the natural induction is on max of the complexities. –  André Nicolas Mar 31 '12 at 16:26
Excuse me, what do you mean exactly? –  morris Mar 31 '12 at 16:38
You are really doing an induction on the formation tree. If you are going to replace the natural tree induction by one on a numerical measure of complexity, that numerical measure must take into account the "most complex" of the formulas involved. –  André Nicolas Mar 31 '12 at 16:58
Ok, so obviously $complexity(\psi) \geq complexity(\varphi_1)$. So I assign $n$ to the difference between the complexities. But how can I conclude that if the theorem holds for $n$, it must hold for $n+1$. Actually I don't really understand what the difference of the complexities is good for. But it's the way I shall do the proof. –  morris Mar 31 '12 at 17:04

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$.
Thank you very much, so actually I don't need any more base cases than the trivial one with $\varpsi$ being the subformula itself, right? From other sources in the web I just saw proofs constructing the formula according to the inductive definition step-by-step. Why does one actually need this definition of logical complexity? Or is it just this task which entertains such an "odd" concept? –  morris Mar 31 '12 at 19:41
@morris: That’s right: the trivial one is the only necessary base case. I wouldn’t have bothered with a numerical definition of complexity; I’d just have used structural induction directly on the construction of the formula $\psi$. I don’t understand why it’s done numerically in your setting. –  Brian M. Scott Mar 31 '12 at 19:48
I didn't too, that was the problem. It's an exercise at my logic course and the operations with complexity and especially that $f(\cdot, \cdot$) kinda confused me. However thanks for your help! –  morris Mar 31 '12 at 19:51