# propositional logic - substitution

Prove: $\varphi_1 =\!\mathrel|\mathrel|\!= \varphi_2 \implies \varphi_1[\psi/p] =\!\mathrel|\mathrel|\!= \varphi_2[\psi/p]$.

We've proven that $\varphi_1 =\!\mathrel|\mathrel|\!= \varphi_2 \implies \psi[\varphi_1/p] =\!\mathrel|\mathrel|\!= \psi[\varphi_2/p]$.

Maybe you could give me a hint what way of proving I should use? I don't see over wich formula or rank I could use induction in a useful way..

($\phi =\!\mathrel|\mathrel|\!= \psi$ means $\phi \models \psi$ and $\psi \models \phi$)

Let $\varphi_1 =\!\mathrel|\mathrel|\!= \varphi_2$.

Let $v$ be so that $|p|_v$ = 1. If now $|\psi|_v = 1$ then clearly $\varphi_1[\psi/p] =\!\mathrel|\mathrel|\!= \varphi_2[\psi/p]$ (is this clear?).

Accordingly: Let $v$ be so that $|p|_v$ = 0. If now $|\psi|_v = 0$ then clearly $\varphi_1[\psi/p] =\!\mathrel|\mathrel|\!= \varphi_2[\psi/p]$ (is this clear?).

I don't know how to approach the cases when $|p|_v$ = 0 while $|\psi|_v = 1$ and $|p|_v$ = 1 while $|\psi|_v = 0$.

Other attempt:

Show the equivalent statement $\quad |\!\!\!= \varphi_1 \leftrightarrow \varphi_2 \implies |\!\!\!= \varphi_1[\psi/p] \leftrightarrow \varphi_2[\psi/p]$

Notice, that $\quad \varphi_1[\psi/p] \leftrightarrow \varphi_2[\psi/p] \quad \equiv \quad (\varphi_1 \leftrightarrow \varphi_2)[\psi/p]$

Let now $|\!\!\!= \varphi_1 \leftrightarrow \varphi_2$. Then $\varphi_1 \leftrightarrow \varphi_2$ is a tautology and hence is true for any valuation $v$. In particular $\varphi_1 \leftrightarrow \varphi_2$ is true independent of whether $|p|=0$ or $|p|=1$. It follows (is this right?) that $(\varphi_1 \leftrightarrow \varphi_2)[\psi/p]$ is also true for any valuation $v$ as well. The claim follows.

What on earth does $\models \models$ mean? – Chris Eagle May 9 '12 at 13:10
What on earth does $=| \models$ mean? – Chris Eagle May 9 '12 at 13:14
$=\!\mathrel|\mathrel|\!=$ yields $=\!\mathrel|\mathrel|\!=$ – joriki May 9 '12 at 13:19
I guess $a =\!\mathrel|\mathrel|\!= b$ means that both $a\vDash b$ and $b\vDash a$ ? – MJD May 9 '12 at 14:43