Substitutions

In the previous tutorial, we saw that

\[ (\neg( p_1\vee p_2))\mathrel{\mathsf{eq}} ((\neg p_1)\wedge (\neg p_2)). \]

Suppose that you are interested whether the following is true:

1. Is it true that \((\neg( p_2\vee p_3))\mathrel{\mathsf{eq}} ((\neg p_2)\wedge (\neg p_3))\)?
2. Is it true that \((\neg( p_3\vee (p_1\wedge p_2)))\mathrel{\mathsf{eq}} ((\neg p_3)\wedge (\neg (p_1\wedge p_2)))\)?
3. Is it true that \((\neg((p_3\vee p_4)\vee (p_1\wedge p_2)))\mathrel{\mathsf{eq}} ((\neg (p_3\vee p_4))\wedge (\neg (p_1\wedge p_2)))\)?

Of course, you could verify that each of the above equivalences are true by finding the appropriate truth tables. If you do this, then you will quickly note that you will repeat a lot of the work you did to show that \((\neg( p_1\vee p_2))\mathrel{\mathsf{eq}} ((\neg p_1)\wedge (\neg p_2)).\) The key observation is that no matter what formulas \(\varphi\) and \(\psi\) are, \((\neg( \varphi\vee \psi))\) is logically equivalent to \(((\neg \varphi)\wedge (\neg \psi))\). A substitution is a way to make this observation precise.

Substitution

Suppose that \(\sigma\) is a signature. A substitution \(S\) (for \(LP(\sigma)\)) is a function \(S:\{q_1,\ldots, q_k\}\rightarrow LP(\sigma)\). So, for each \(1\le i\le k\), the atomic proposition \(q_i\) is assigned a formula \(\psi_i\) of \(LP(\sigma)\). Typically, substitutions are written as follows:

\[ \psi_1/q_1, \psi_2/q_2,\ldots, \psi_k/q_k \]

We apply a substitution \([\psi_1/q_1, \psi_2/q_2,\ldots, \psi_k/q_k]\) to a formula \(\varphi\) by simultaneously replacing every occurence of \(q_i\) in \(\varphi\) with \(\psi_i\). We denote the application of a substitution as follows:

\[ \varphi[\psi_1/q_1, \psi_2/q_2,\ldots, \psi_k/q_k] \]

The application of a substitution is defined by the following compositional definition:

Applying a Substitution

Suppose that \(\varphi\) is a formula of \(LP(\sigma)\), \(q_1,\ldots,q_k\) are atomic propositions and \(\psi_1,\ldots\psi_k\) are formulas of \(LP(\sigma)\).

1. if \(\varphi\) is an atomic proposition, then

   \[ \varphi[\psi_1/q_1,\ldots,\psi_k/q_k]=\begin{cases} \psi_j & \mbox{if }\varphi\mbox{ is }q_i (1\le i\le k)\\ \varphi & \mbox{otherwise} \end{cases} \]

2. if \(\varphi=(\neg\chi)\) where \(\chi\) is a formula, then

   \[ \varphi[\psi_1/q_1,\ldots,\psi_k/q_k] = (\neg \chi[\psi_1/q_1,\ldots,\psi_k/q_k]) \]

3. if \(\varphi=(\chi_1\Box \chi_2)\) where \(\chi_1\) and \(\chi_2\) are formulas and \(\Box\in\{\wedge, \vee, \rightarrow,\leftrightarrow\}\), then

   \[ \varphi[\psi_1/q_1,\ldots,\psi_k/q_k] = (\chi_1[\psi_1/q_1,\ldots,\psi_k/q_k]\Box \chi_2[\psi_1/q_1,\ldots,\psi_k/q_k]) \]

For example, we use the above definition to show that

\[ (\neg(p_1\vee p_2))[(\neg p_3)/p_1, p_4/p_2] = (\neg((\neg p_3)\vee p_4)) \]

as follows:

\[ \begin{eqnarray} (\neg(p_1\vee p_2))[(\neg p_3)/p_1, p_4/p_2] & = & (\neg(p_1\vee p_2)[(\neg p_3)/p_1, p_4/p_2])\\ & = & (\neg(p_1[(\neg p_3)/p_1, p_4/p_2]\vee p_2[(\neg p_3)/p_1, p_4/p_2]))\\ & = & (\neg((\neg p_3)\vee p_4))\\ \end{eqnarray} \]

Examples of substitutions

1. \((\neg( p_1\vee p_2))[p_2/p_1,p_3/p_2] = (\neg( p_2\vee p_3))\)
2. \(((\neg p_1)\wedge (\neg p_2))[p_2/p_1, p_3/p_2] = ((\neg p_2)\wedge (\neg p_3))\)
3. \((\neg( p_1\vee p_2))[p_3/p_1,(p_1\wedge p_2)/p_2] = (\neg( p_3\vee (p_1\wedge p_2)))\)
4. \(((\neg p_1)\wedge (\neg p_2))[p_3/p_1,(p_1\wedge p_2)/p_2] = ((\neg p_3)\wedge (\neg (p_1\wedge p_2)))\)
5. \((\neg( p_1\vee p_2))[(p_3\vee p_4)/p_1,(p_1\wedge p_2)/p_2] = (\neg((p_3\vee p_4)\vee (p_1\wedge p_2)))\)
6. \(((\neg p_1)\wedge (\neg p_2))[(p_3\vee p_4)/p_1,(p_1\wedge p_2)/p_2] = ((\neg (p_3\vee p_4))\wedge (\neg (p_1\wedge p_2)))\)

The first observation is that \(\mathop{\mathsf{eq}}\) is an equivalenc relation:

Lemma: Logical equivalence is an equivalence relation

1. Reflexivity: For all formulas \(\varphi\) of \(LP(\sigma)\), \(\varphi\ \mathop{\mathsf{eq}}\ \varphi\).
2. Symmetry: For all formulas \(\varphi_1, \varphi_2\) of \(LP(\sigma)\), if \(\varphi_1\ \mathop{\mathsf{eq}}\ \varphi_2\), then \(\varphi_2\ \mathop{\mathsf{eq}}\ \varphi_1\).
3. Transitivity: For all formulas \(\varphi_1, \varphi_2, \varphi_3\) of \(LP(\sigma)\), if \(\varphi_1\ \mathop{\mathsf{eq}}\ \varphi_2\) and \(\varphi_2\ \mathop{\mathsf{eq}}\ \varphi_3\), then \(\varphi_1\ \mathop{\mathsf{eq}}\ \varphi_3\).

The following two fundamental theorems show how to use subtitutions to derive logical equivalences.

Substitution Theorem

Let \(S\) be a substitution and \(\varphi_1\) and \(\varphi_2\) formulas of \(LP(\sigma)\). If \(\varphi_1\mathop{\mathsf{eq}}\varphi_2\), then \(\varphi_1[S]\mathop{\mathsf{eq}}\varphi_2[S]\).

The substituion theorem can be used to verify the above three logical equivalences. For instance, to prove that \((\neg( p_2\vee p_3))\mathrel{\mathsf{eq}} ((\neg p_2)\wedge (\neg p_3))\), first note that we have shown that \((\neg( p_1\vee p_2))\mathrel{\mathsf{eq}} ((\neg p_1)\wedge (\neg p_2))\). Then, by the substitution theorem:

\[ (\neg( p_1\vee p_2))[p_2/p_1, p_3/p_2]\mathrel{\mathsf{eq}} ((\neg p_1)\wedge (\neg p_2))[p_2/p_1, p_3/p_2] \]

That is, we have that:

\[ (\neg( p_2\vee p_3))\mathrel{\mathsf{eq}} ((\neg p_2)\wedge (\neg p_3)) \]

The next theorem allows for the replacement of logically equivalent formulas.

Replacement Theorem

Let \(S_1\) and \(S_2\) be the substitutions

\[ [\psi_1,q_1,\ldots,\psi_k,q_k]\qquad\qquad[\psi'_1,q_1,\ldots,\psi'_k,q_k] \]

where for each \(1\le j\le k\), \(\psi_j\mathop{\mathsf{eq}}\psi'_j\). Then for all formulas \(\varphi\), \(\varphi[S_1]\mathop{\mathsf{eq}}\varphi[S_2]\).

Applying the Substitution and Replacement Theorems

We can use the Substitution and Replacement theorem to show that

\[ ((\neg p_3)\rightarrow p_4)\ \mathop{\mathsf{eq}}\ (p_3\vee p_4) \]

We have already seen that \((p_1\rightarrow p_2)\ \mathop{\mathsf{eq}}\ ((\neg p_1)\vee p_2)\). Then, by the substituion theorem:

\[ (p_1\rightarrow p_2)[(\neg p_3)/p_1, p_4/p_2]\ \mathop{\mathsf{eq}}\ ((\neg p_1)\vee p_2)[(\neg p_3)/p_1, p_4/p_2] \]

That is, we have that:

\[ ((\neg p_3)\rightarrow p_4)\ \mathop{\mathsf{eq}}\ ((\neg (\neg p_3))\vee p_4) \]

In the previous tutorial, we have that

\[ (\neg(\neg p_1))\ \mathrel{\mathsf{eq}}\ p_1 \]

By the subsitution theorem,

\[ (\neg(\neg p_3)) = (\neg(\neg p_1))[p_3/p_1]\ \mathrel{\mathsf{eq}}\ p_1[p_3/p_1]=p_3 \]

Then by the Replacement Theorem, we have that

\[ (p_3\vee p_4)[(\neg(\neg p_3))/p_3]\ \mathop{\mathsf{eq}}\ (p_3\vee p_4)[p_3/p_3] \]

So, we have shown:

1. \(((\neg p_3)\rightarrow p_4)\ \mathop{\mathsf{eq}}\ ((\neg (\neg p_3))\vee p_4)\)
2. \(((\neg(\neg p_3))\vee p_4)\ \mathop{\mathsf{eq}}\ (p_3\vee p_4)\)

By transitivity of logical equivalence, we have that:

\[ ((\neg p_3)\rightarrow p_4)\ \mathop{\mathsf{eq}}\ (p_3\vee p_4). \]

Aditional Reading

• Section 3.7 of Mathematical Logic by Chiswell and Hodges.

Exercises

1. Use the Substitution Theorem to show that \((\neg( p_3\vee (p_1\wedge p_2)))\mathrel{\mathsf{eq}} ((\neg p_3)\wedge (\neg (p_1\wedge p_2)))\).

   Show Answer

   We have seen in the previous tutorial that:

   \[ (\neg(p_1\vee p_2)) \mathrel{\mathsf{eq}} ((\neg p_1)\wedge \neg(p_2)) \]

   Then, by the substitution theorem, we have that:

   \[ (\neg(p_1\vee p_2))[p_3/p_1, (p_1\wedge p_2)/p_2] \mathrel{\mathsf{eq}} ((\neg p_1)\wedge \neg(p_2))[p_3/p_1, (p_1\wedge p_2)/p_2] \]

   Applying the substitutions, we have:

   \[ (\neg( p_3\vee (p_1\wedge p_2)))\mathrel{\mathsf{eq}} ((\neg p_3)\wedge (\neg (p_1\wedge p_2))). \]

2. Use the Substitution Theorem to show that

   \[ (\neg((p_3\vee p_4)\vee (p_1\wedge p_2)))\mathrel{\mathsf{eq}} ((\neg (p_3\vee p_4))\wedge (\neg (p_1\wedge p_2))). \]
   Show Answer

   We have seen in the previous tutorial that:

   \[ (\neg(p_1\vee p_2)) \mathrel{\mathsf{eq}} ((\neg p_1)\wedge \neg(p_2)) \]

   Then, by the substitution theorem, we have that:

   \[ (\neg(p_1\vee p_2))[(p_3\vee p_4)/p_1, (p_1\wedge p_2)/p_2] \mathrel{\mathsf{eq}} ((\neg p_1)\wedge \neg(p_2))[(p_3\vee p_4)/p_1, (p_1\wedge p_2)/p_2] \]

   Applying the substitutions, we have:

   \[ (\neg((p_3\vee p_4)\vee (p_1\wedge p_2)))\mathrel{\mathsf{eq}} ((\neg (p_3\vee p_4))\wedge (\neg (p_1\wedge p_2))). \]

3. Use the Substitution Theorem to show that:

   \[ p_2\ \mathop{\mathsf{eq}}\ (p_2\wedge p_3)\vee (p_2\wedge (\neg p_3)). \]
   Show Answer

   We first note that \(p_2\mathop{\mathsf{eq}}(p_2\wedge (p_3\vee (\neg p_3))\)

   \(p_2\)	\(p_3\)	\((p_3\vee (\neg p_3))\)	\((p_2\wedge (p_3\vee (\neg p_3))\)
   \(\mathsf{T}\)	\(\mathsf{T}\)	\(\mathsf{T}\)	\(\mathsf{T}\)
   \(\mathsf{T}\)	\(\mathsf{F}\)	\(\mathsf{T}\)	\(\mathsf{T}\)
   \(\mathsf{F}\)	\(\mathsf{T}\)	\(\mathsf{T}\)	\(\mathsf{F}\)
   \(\mathsf{F}\)	\(\mathsf{F}\)	\(\mathsf{T}\)	\(\mathsf{F}\)

   Now, from the previous tutorial we have that:

   \[ ( p_1\wedge(p_2\vee p_3))\mathrel{\mathsf{eq}} (( p_1 \wedge p_2)\vee ( p_1\wedge p_3)) \]

   By the substitution theorem we have that, where \(S\) is the substituion \(p_2/p_1, p_3/p_2, (\neg p_3)/p_3\)

   \[ ( p_1\wedge(p_2\vee p_3))[S]\mathrel{\mathsf{eq}} (( p_1 \wedge p_2)\vee ( p_1\wedge p_3))[S] \]

   Applying the substitution gives:

   \[ (p_2\wedge (p_3\vee (\neg p_3)))\ \mathop{\mathsf{eq}}\ ((p_2\wedge p_3)\vee (p_2\wedge (\neg p_3))). \]

   By transitivity of \(\mathsf{eq}\), we have that:

   \[ p_2\ \mathop{\mathsf{eq}}\ (p_2\wedge p_3)\vee (p_2\wedge (\neg p_3)). \]

4. Use the substitution and replacement theorem to show that:

   \[ (\neg (p_1\rightarrow p_2)) \mathop{\mathsf{eq}} (p_1\wedge \neg p_2). \]
   Show Answer

   We first recall that:

   \[ p_1\rightarrow p_2 \mathop{\mathsf{eq}} \neg p_1\vee p_2 \]

   By the Repalcement Theorem,

   \[ \neg (p_0)[(p_1\rightarrow p_2)/p_0] \mathop{\mathsf{eq}} \neg (p_0)[((\neg p_1)\vee p_2)/p_0] \]

   Applying the substitution, we have that:

   \[ \neg (p_1\rightarrow p_2)\mathop{\mathsf{eq}} \neg(\neg p_1\vee p_2) \]

   We note that:

   \[ \neg (p_1\vee p_2) \mathop{\mathsf{eq}} ((\neg p_1)\wedge (\neg p_2)) \]

   By the Substitution Theorem, we have that:

   \[ \neg (p_1\vee p_2)[\neg p_1/p_1] \mathop{\mathsf{eq}} ((\neg p_1)\wedge (\neg p_2))[\neg p_1/p_1] \]

   Applying the substitution we have that:

   \[ \neg ((\neg p_1)\vee p_2) \mathop{\mathsf{eq}} ((\neg(\neg p_1))\wedge (\neg p_2)) \]

   We have that:

   \[ (\neg (\neg p_1))\mathop{\mathsf{eq}} p_1 \]

   By the Replacement Theorem,

   \[ (p_1\wedge (\neg p_2))[(\neg(\neg p_1))/p_1]\mathop{\mathsf{eq}} (p_1\wedge (\neg p_2))[p_1/p_1] \]

   Applying the substitutions, we have that:

   \[ ((\neg(\neg p_1))\wedge (\neg p_2)) \mathop{\mathsf{eq}} (p_1\wedge (\neg p_2)) \]

   Applying transitivity twice, we have the following:

   \[ (\neg (p_1\rightarrow p_2)) \mathop{\mathsf{eq}} (p_1\wedge \neg p_2). \]