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!

  • $\begingroup$ It seems to me that the natural induction is on max of the complexities. $\endgroup$ – André Nicolas Mar 31 '12 at 16:26
  • $\begingroup$ Excuse me, what do you mean exactly? $\endgroup$ – morris Mar 31 '12 at 16:38
  • $\begingroup$ 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. $\endgroup$ – André Nicolas Mar 31 '12 at 16:58
  • $\begingroup$ 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. $\endgroup$ – 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$.

  • $\begingroup$ 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? $\endgroup$ – morris Mar 31 '12 at 19:41
  • $\begingroup$ @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. $\endgroup$ – Brian M. Scott Mar 31 '12 at 19:48
  • $\begingroup$ 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! $\endgroup$ – morris Mar 31 '12 at 19:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.