Replacing variables by propositional formulas in a propositional formula yields a new propositional formula. This process is called substitution.

Example Suppose $\varphi$ is given by $\varphi = (X_0 \vee \neg (X_1 \leftrightarrow X_2))$. When we now replace $X_0$ by $\neg X_3$ and $X_1$ by $X_2 \wedge X_0$, we obtain $\neg X_3 \vee \neg ((X_2 \wedge X_0) \leftrightarrow X_2))$.

Formal definition

A substitution is a partial function $\text{PVars} \not\to F_\text{PL}$. The value of such a function for a variable $X_i$ is called the substituent for $X_i$.

Example In the above example, we use the substitution $\{X_0 \mapsto \neg X_3, X_1 \mapsto X_2 \wedge X_0\}$.

Given a substitution $\sigma$ as above, we define $\varphi\sigma$ for every propositional formula $\varphi$ by induction.

Base mapping

$\top\sigma = \top$.
$\bot\sigma = \bot$.
For every $i \in \mathbf N$, $$X_i\sigma = \begin{cases} \sigma(X_i) & \text{if $X_i \in \text{dom}(\sigma)$,}\\ X_i & \text{else.} \end{cases}$$

Inductive rule

If $C$ is an $n$-ary connective and $\varphi_0, \dots, \varphi_{n-1}$ are propositional formulas, then $$(C(\varphi_0, \dots, \varphi_{n-1}))\sigma = C(\varphi_0\sigma, \dots, \varphi_{n-1}\sigma)\enspace.$$

Example Let $\sigma = \{X_0 \mapsto \neg X_3, X_1 \mapsto X_2 \wedge X_0\}$. Then \begin{aligned} (X_0 \vee \neg (X_1 \leftrightarrow X_2))\sigma & = X_0 \sigma \vee (\neg (X_1 \leftrightarrow X_2))\sigma&& \text{inductive rule for $\vee$} \\ & = \sigma(X_0) \vee \neg ((X_1 \leftrightarrow X_2)\sigma) && \text{base mapping and inductive rule for $\neg$}\\ & = \neg X_3 \vee \neg (X_1\sigma \leftrightarrow X_2\sigma)) && \text{definition of $\sigma$ and inductive rule for $\leftrightarrow$}\\ & = \neg X_3 \vee \neg (\sigma(X_1) \leftrightarrow X_2) && \text{base mapping, twice} \\ & = \neg X_3 \vee \neg ((X_2 \wedge X_0) \leftrightarrow X_2)) && \text{definition of $\sigma$} \end{aligned}

Substitution lemma

Consider the arithmetic expression $x + 3$ and the substitution $\{x \mapsto y^2\}$. Suppose you wanted to evalute $(x+3)\{x \mapsto y^2\}$ under an assignment $\{y \mapsto 5\}$. Then you would have two options:

You apply the substitution. Result: $y^2 + 3$. You evaluate this expression under the assignment. Result: $5^2 + 3$, which equals 28.
You evaluate the substituent for $x$, namely $y^2$, under the assignment. Result: $25$. You evaluate $x+3$ under the adapted assignment $\{x \mapsto 25\}$. Result: $25 + 3$, which equals $28$.

This is a general principle: to evaluate a formula after a substitution, one can evaluate it under an adapted assignment, where the values for the variables are obtained by evaluating its substitutents.

To phrase this statement we define what it means for a substitution to act on a variable assignment. Let $\sigma$ be a substitution and $\beta$ a variable assignment. Then $\beta^\sigma$ is the variable assignment defined as follows, where $i \in \mathbf N$. $$(\beta^\sigma)(X_i) = \begin{cases} \llbracket \sigma(X_i) \rrbracket_\beta \enspace, & \text{if $X_i \in \text{dom}(\sigma)$,}\\ \llbracket(X_i)\rrbracket_\beta \enspace, & \text{otherwise.} \end{cases}$$ In other words, $\beta^\sigma(X_i) = \llbracket X_i\sigma\rrbracket_\beta$.

Formal statement

Substitution lemma For all $\varphi \in F_\text{AL}$, substitutions $\sigma \colon V_\text{AL} \not\to F_\text{PL}$, and assignments $\beta$: $$\llbracket\varphi\sigma\rrbracket_\beta = \llbracket\varphi\rrbracket_{\beta^\sigma} \enspace.$$

Proof The proof is by induction.

Base step. We have \begin{aligned} \llbracket\top\sigma\rrbracket_\beta & = \llbracket \top\rrbracket_\beta && \text{application of $\sigma$, base mapping}\\ & = 1 && \text{semantics of propositional logic, base mapping}\\ & = \llbracket \top\rrbracket_{\beta^\sigma} && \text{semantics of propositional logic, base mapping} \end{aligned}

A similar argument can be used for $\bot$.

For $\varphi = X_i$, we distinguish two cases.

First case, $X_i \in \text{dom}(\sigma)$. Then \begin{aligned} \llbracket X_i \rrbracket_{\beta^\sigma} & = (\beta^\sigma)(X_i) && \text{semantics of propositional logic, base mapping}\\ & = \llbracket\sigma(X_i)\rrbracket_\beta && \text{definition of $\beta^\sigma$}\\ & = \llbracket\varphi\sigma\rrbracket_\beta && \text{application of $\sigma$, base mapping} \end{aligned}

Second case, $X_i \notin \text{dom}(\sigma)$. Then \begin{aligned} \llbracket X_i \rrbracket_{\beta^\sigma} & = (\beta^\sigma)(X_i) && \text{semantics of propositional logic, base mapping}\\ & = \llbracket X_i \rrbracket_\beta && \text{definition of $\beta^\sigma$}\\ & = \llbracket\varphi\sigma\rrbracket_\beta && \text{application of $\sigma$, base mapping} \end{aligned}

Inductive step. Let $C$ be an $n$-ary connective and let $\varphi_0, \dots, \varphi_{n-1} \in F_\text{PL}$. Then \begin{aligned} {}\llbracket C(\varphi_0, \dots, \varphi_{n-1})\sigma\rrbracket_\beta & = \llbracket C(\varphi_0\sigma, \dots, \varphi_{n-1}\sigma)\rrbracket_\beta && \text{application of $\sigma$, inductive step}\\ & = f_C(\llbracket\varphi_0\sigma\rrbracket_\beta, \dots, \llbracket\varphi_{n-1}\sigma\rrbracket_\beta && \text{semantics of propositional logic, inductive step}\\ & = f_C(\llbracket\varphi_0\rrbracket_{\beta^\sigma}, \dots, \llbracket\varphi_{n-1}\rrbracket_{\beta^\sigma}) && \text{inductive assumption}\\ & = \llbracket C(\varphi_0, \dots, \varphi_{n-1})\rrbracket_{\beta^\sigma} && \text{semantics of propositional logic, inductive step} \end{aligned}

This concludes the proof.

Applications

There are many applications of the substitution lemma. Two important ones follow.

Moving an assignment into a formula

First, we can now argue that instead of evaluating a formula under an assignment we can first replace every variable by the corresponding truth value and then evaluate the resulting formula which has no variables anymore.

For every variable assignment $\beta$, let $\sigma_\beta$ be the substitution defined by $$\sigma_\beta(X_i) = \begin{cases} \bot \enspace, & \text{if $\beta(X_i) = 0$,}\\ \top \enspace, & \text{otherwise.} \end{cases} $$

Note that ${\gamma}^{\sigma_\beta} = \beta$ holds for every variable assignment $\gamma$ simply because in $\sigma_\beta(X_i)$ there does not occur any variable for any $i \in \mathbf N$.

Lemma For every propositional formula $\varphi$ and every propositional variable assignment $\beta$, $$\llbracket \varphi\rrbracket_\beta = \llbracket \varphi\sigma_\beta \rrbracket_\emptyset \enspace.$$ Note that the formula on the right-hand side has no variables. This justifies that it is evaluated under an empty assignment.

Proof The proof is very simple: \begin{align} \llbracket \varphi\rrbracket_\beta & = \llbracket \varphi\rrbracket_{\beta^{\sigma_\beta} } && \text{see above}\\ & = \llbracket \varphi\sigma_\beta \rrbracket_\beta && \text{substitution lemma}\\ & = \llbracket \varphi\sigma_\beta \rrbracket_\emptyset && \text{coincidence lemma and } \operatorname{vars}(\varphi \sigma_\beta) = \emptyset \text{.}\\ \end{align}

Equivalence is kept under substitution

Second, we can now argue that in an equivalence between propositional formulas we can replace variables by arbitrary formulas and keep the equivalence.

Equivalence lemma Let $\varphi$ and $\psi$ be propositional formulas and let $\sigma$ be any substitution. If $\varphi \SemEquiv \psi$, then $\varphi \sigma \SemEquiv \psi\sigma$.

Proof The proof is straightforward. Let $\varphi$ and $\psi$ be propositional formulas and $\sigma$ any substitution. Further, assume $\varphi \SemEquiv \psi$ and let $\beta$ be any propositional assignment. Then \begin{align} \llbracket \varphi\sigma \rrbracket_{\beta} & = \llbracket \varphi \rrbracket_{\beta^\sigma} && \text{substitution lemma}\\ & = \llbracket \psi \rrbracket_{\beta^\sigma} && \text{assumption $\varphi \SemEquiv \psi$}\\ & = \llbracket \psi\sigma \rrbracket_{\beta} && \text{substitution lemma} \end{align} This completes the proof.

Exercises

Exercise Gegeben sei Substitution $\sigma=\{X_0\mapsto \neg X_1, X_1\mapsto X_2\wedge X_0, X_2\mapsto \bot\}$, die aussagenlogische Formel $\varphi=(X_0 \wedge (X_2\mathrel{\dot{\vee}}X_0))\vee X_1\vee X_3$, sowie die partielle Belegung $\beta=\{X_0\mapsto 0, X_1\mapsto 0, X_2\mapsto 1,X_3\mapsto 0\}$.

Lösen Sie die Substitution in $\varphi\sigma$ schrittweise auf und geben Sie dabei jeden Schritt an.
Geben Sie $\beta^{\sigma}$ an.
Werten Sie $\varphi\sigma$ unter $\beta$ und $\varphi$ unter $\beta^{\sigma}$ aus und geben $\llbracket\varphi\sigma\rrbracket_\beta$ und $\llbracket\varphi\rrbracket_{\beta^{\sigma}}$ an.

Lösung

Gegeben sei die Substitution $\sigma=\{X_0\mapsto \neg X_1, X_1\mapsto X_2\wedge X_0, X_2\mapsto \bot\}$, die aussagenlogische Formel $\varphi=(X_0 \wedge (X_2\mathrel{\dot{\vee}}X_0))\vee X_1\vee X_3$, sowie die partielle Belegung $\beta=\{X_0\mapsto 0, X_1\mapsto 0, X_2\mapsto 1,X_3\mapsto 0\}$.

\begin{align} \varphi\sigma &= ((X_0 \wedge (X_2\mathrel{\dot{\vee}}X_0))\vee X_1\vee X_3)\sigma && \text{Def. $\varphi$}\\ &= ((X_0 \wedge (X_2\mathrel{\dot{\vee}}X_0))\sigma\vee X_1\sigma\vee X_3\sigma) && \text{Def. $\sigma$ und induktive Regel für $\bigvee$}\\ &= ((X_0\sigma \wedge (X_2\mathrel{\dot{\vee}}X_0)\sigma)\vee X_1\sigma\vee X_3\sigma) && \text{Def. $\sigma$ und induktive Regel für $\wedge$}\\ &= ((X_0\sigma \wedge (X_2\sigma\mathrel{\dot{\vee}}X_0\sigma))\vee X_1\sigma\vee X_3\sigma) && \text{Def. $\sigma$ und induktive Regel für $\mathrel{\dot{\vee}}$}\\ &= ((\sigma(X_0) \wedge (\sigma(X_2)\mathrel{\dot{\vee}}\sigma(X_0)))\vee \sigma(X_1)\vee X_3) && \text{$5\times$ Def. $X_i\sigma$ }\\ &= ((\neg X_1 \wedge (\bot\mathrel{\dot{\vee}}\neg X_1))\vee (X_2\wedge X_0)\vee X_3) && \text{$5\times$ Def. $\sigma$}\\ \end{align}
\begin{align} \beta^{\sigma} &= \{X_0\mapsto \llbracket \sigma(X_0) \rrbracket_\beta, X_1\mapsto \llbracket \sigma(X_1) \rrbracket_\beta,X_2\mapsto \llbracket \sigma(X_2) \rrbracket_\beta, X_3\mapsto \llbracket X_3 \rrbracket_\beta\} && \text{Def. $\beta^\sigma$}\\ &= \{X_0\mapsto \llbracket \neg X_1 \rrbracket_\beta, X_1\mapsto \llbracket X_2\wedge X_0 \rrbracket_\beta,X_2\mapsto \llbracket \bot \rrbracket_\beta, X_3\mapsto \beta(X_3)\} && \text{Def. $\sigma$, Def. $\llbracket\cdot\rrbracket_\beta$}\\ &= \{X_0\mapsto 1, X_1\mapsto 0,X_2\mapsto 0, X_3\mapsto 0\} && \text{Mehrfach Def. $\llbracket\cdot\rrbracket_\beta$, Def. $\beta$}\\ \end{align}
$\llbracket\varphi\sigma\rrbracket_\beta = 1$ und $\llbracket\varphi\rrbracket_{\beta^{\sigma}}=1$.

Substitution in propositional logic

From Learning Logic for Computer Science

Contents