Substituting a proposition instead of atoms

Question

Substitution theroem in propositional logic states that for atomic $p$ and propositions $\varphi,\psi_1,\psi_2$ we have:

$$ \psi_1\leftrightarrow \psi_2 \Longrightarrow \varphi[\psi_1|p] \leftrightarrow \varphi[\psi_2|p]$$

Can we instead of substituting atomics, substitute a proposition $\gamma$?

$$ \psi_1\leftrightarrow \psi_2 \Longrightarrow \varphi[\psi_1|\gamma] \leftrightarrow \varphi[\psi_2|\gamma]$$

Answer 1

You have to take care of the symbols...

$\varphi, \psi, \ldots$ are meta-variables, i.e. they stay for formulae of the calculus.

Formulae of the calculus are composed of atoms and conncetives.

Examples :

$p_1 \lor p_2$

is a formula of the calculus, while :

$\varphi \lor \psi$

is an "schema" in the meta-theory denoting the infinite collection of formulae with the same "form", like :

$p_1 \lor p_2, (p_1 \land p_2) \lor (p_1 \land p_2), \ldots$

The substitution theorem is a theorem (in the meta-theory) expressing a property of the calculus; in the calculus we have only atoms and thus we have to replace them.

---

In a certain sense, the replacement of formulae is "built-in" into the schematic symbolism used in the meta-theory.

If e.g. we have proved that :

$\vDash \varphi \lor \lnot \varphi$

this holds for a formula of the calculus whatever.

Every "instance" of it that we can produce replacing the meta-variable $\varphi$ with a formula of the calculus (e.g. $p_1 \land p_2$) will be a tautology.

This means that the "generalized" substitution theorem (from atoms to formulae) is not really necessary.

Consider the following case :

$\psi_1 := p_1 \to p_2$, and $\psi_2 := \lnot p_1 \lor p_2$.

We have that : $\vDash \psi_1 ↔ \psi_2$.

And consider the schema :

$\varphi := \theta \land \gamma$.

We want to use the "generalized" substitution theorem in order to prove that :

$\vDash [\theta \land (p_1 \to p_2)] ↔ [\theta \land (\lnot p_1 \lor p_2)]$.

We do not need it, because we can use the formula :

$\varphi := q_1 \land q_2$

and apply first the "restricted" subsitution theorem with $\theta$ in place of the atom $q_1$ to get from : if $\vDash \theta ↔ \theta$, then $\vDash \varphi[\theta/q_1] ↔ \varphi [\theta /q_1]$ the "intermediate" result :

$\vDash \theta \land q_2 ↔ \theta \land q_2$.

Now we can apply again the substitution theorem to $\varphi' := \theta \land q_2$ with $\psi_1$ and $\psi_2$ above to get the final result :

$\vDash [\theta \land (p_1 \to p_2)] ↔ [\theta \land (\lnot p_1 \lor p_2)]$.

---

Note For a formal treatment, you can see the post proving tautologically equivalent.