0
$\begingroup$

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]$$

$\endgroup$
1
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Thanks and excuse me! I can not see any connection between your answer and my question. Do you mean that my question is an abuse of notation? $\endgroup$ – Dandelion Oct 26 '16 at 11:00

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.