This is an old revision of the document!

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, \[

 \sigma : D \to {\cal F}

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

 \sigma = \{F_1 \mapsto G_1,\ldots, F_n \mapsto G_n\}

\] 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 \[

 subst : {\cal S} \to ({\cal F} \to {\cal F})

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\}$ , \[

 e(subst(\{p_1 \mapsto F_1,\ldots,p_n \mapsto F_n\})(F))(I) =

 e(F)(I[p_1 \mapsto e(F_1)(I),\ldots,p_n \mapsto e(F_n)(I)])

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

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.

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

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)$ .

Lemma: If $\models (F \leftrightarrow G)$ then for every interpretation $I$ we have $e(F)(I) = e(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))$ .