# 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.

Denote with $\cong$ the equivalence of formulae with respect to valuations; indicate with $\phi(\vec q)$ that the propositional variables in $\phi$ are all among $\vec q$. I write $v(\phi)$ where you write $|\phi|_v$.

Suppose $\phi_1(\vec q,p) \cong \phi_2(\vec q,p)$, and let $\psi(\vec q, \vec r)$ be another formula.

We need to establish that $\phi_1[\psi/p] \cong \phi_2[\psi/p]$. Note that $\phi_1[\psi/p](\vec q,\vec r)$ and $\phi_2[\psi/p](\vec q,\vec r)$.

Let $v: \vec q,\vec r \to \{0,1\}$ be an arbitrary valuation. We have to prove that $v(\phi_1[\psi/p]) = v(\phi_2[\psi/p])$.

To this end, define a different valuation $v': \vec q, p \to \{0,1\}$ by:

$$v'(q) = \begin{cases} v(q) & \text{if q \ne p} \\ v(\psi) & \text{if q = p} \end{cases}$$

We can now prove by induction on the complexity of $\phi(\vec q,p)$ that $v'(\phi) = v(\phi[\psi/p])$; this is (almost) tautologous.

Since $\phi_1 \cong \phi_2$, we infer that $v'(\phi_1) = v'(\phi_2)$, and hence that $v(\phi_1[\psi/p]) = v(\phi_2[\psi/p])$.

In conclusion, since $v$ was arbitrary, we conclude that $\phi_1[\psi/p] \cong \phi_2[\psi/p]$.