# 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
{"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 1, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0, "url": "http://math.stackexchange.com/questions/126600/structural-induction-logic", "fetch_time": 1469448564000000000, "content_mime_type": "text/html", "warc_filename": "crawl-data/CC-MAIN-2016-30/segments/1469257824226.79/warc/CC-MAIN-20160723071024-00112-ip-10-185-27-174.ec2.internal.warc.gz", "warc_record_offset": 170321293, "warc_record_length": 18149, "token_count": 1236, "char_count": 4200, "score": 3.59375, "int_score": 4, "crawl": "CC-MAIN-2016-30", "snapshot_type": "latest", "language": "en", "language_score": 0.7796489000320435, "file_path": "/sailhome/yjruan/project/latent-lm/data/processed/finemath-4plus/finemath-4plus/train-00012-of-00064.parquet"}