Substitution Theorems for Propositional Logic

Relate syntax and semantics.

Called metatheorems, because they are not formulas within the logic, but formulas about the logic.

From semantics we can prove the following lemma by induction.

Lemma: if $I_1(p) = I_2(p)$ for every $p \in FV(F)$ , then $e(F)(I_1)=e(F)(I_2)$ .

Substitutions

Substitution is a maping formulas to formulas,

$\begin{equation*} \sigma : D \to {\cal F} \end{equation*}$

where $D \subseteq {\cal F}$ is the domain of substitution, usually finite. We write it

$\begin{equation*} \sigma = \{F_1 \mapsto G_1,\ldots, F_n \mapsto G_n\} \end{equation*}$

Let ${\cal S}$ be set of all substitutions.

Substitution operator subst takes such a map and a formula and returns a new formula.

Recursive definition of subst:

For $F \in {\cal F}$ we write $F \sigma$ instead of $subst(\sigma)(F)$ , so

$\begin{equation*} subst : {\cal S} \to ({\cal F} \to {\cal F}) \end{equation*}$

Variable substitution is substitution where the domain is a subset of $V$ - it only replaces variables, not complex formulas.

Theorem: For formula $F$ , interpretation $I$ and variable substitution $\sigma = \{p_1 \mapsto F_1,\ldots,p_n \mapsto F_n\}$ ,

$\begin{equation*} e(subst(\{p_1 \mapsto F_1,\ldots,p_n \mapsto F_n\})(F))(I) = \end{equation*}$

Corollary (tautology instances): if $\models F$ , then $\models (subst(\sigma)(F))$ for every variable substitution $\sigma$ .

We say that two formulas are equivalent if $\models (F \leftrightarrow G)$ .

Lemma: If $\models (F \leftrightarrow G)$ then for every interpretation $I$ we have $e(F)(I) = e(G)(I)$ .

From the tautology instances Corrolary we obtain.

Corollary: if $\models (F \leftrightarrow G)$ and $\sigma$ is a variable substitution, then $\models (subst(\sigma)(F) \leftrightarrow subst(\sigma)(G))$ .

Does the theorem hold if $\sigma$ is not a variable substitution? No, because a general substitution could produce an arbitrary formula.

This theorem was about transforming formulas from the outside, ignoring the structure of certain subformulas.

We next justify transforming formulas from inside.

We say that $\sigma = \{F_1 \mapsto G_1,\ldots,F_n \mapsto G_n\}$ is equivalence-preserving iff for all $i$ where $1 \le i \le n$ we have $\models (F_i \leftrightarrow G_i)$ .

Theorem on Substituting Equivalent Subformulas: if $\sigma$ is equivalence-preserving, then for every formula $F$ we have $\models (F \leftrightarrow (subst(\sigma)(F))$ .