15. Soundness Theorem

As was the case with Propositional Logic, we have now reached the stage where we have two different notions of “derivations” from premises to a conclusion in first-order logic:

• \(\Gamma \vDash \phi\) represents that \(\phi\) is a logical consequence of \(\Gamma\) in that every structure that causes all sentences in \(\Gamma\) to evaluate to True also causes \(\phi\) to evaluate to True.

• \(\Gamma \vdash \phi\) means that \(\phi\) is implied by \(\Gamma\) in that there is a formal proof in our natural deduction system with premises in \(\Gamma\) and conclusion \(\phi\).

Is it still the case that \(\Gamma \vDash \phi\) if and only if \(\Gamma \vdash \phi\)? As we will see in this lecture and the next one, this is indeed the case in first-order logic. But showing this equivalence requires establishing new Soundness and Completness Theorems.

In this lecture, we start with the Soundness Theorem.

Theorem. (Soundness Theorem for First-Order Logic) For every set \(\Gamma\) of sentences and every sentence \(\phi\) in first-order logic, if \(\Gamma \vdash \phi\) then \(\Gamma \vDash \phi.\)

Proof Overview

The high-level strategy of the proof of the Soundness Theorem is the same as the strategy that we used to prove the analogous theorem in propositional logic. Namely, we want to proceed by induction on the line number \(k = 1,2,\ldots,n\) of the proof and show that the formula \(\phi_k\) on the \(k\)th line is a logical consequence of \(\Gamma\) and the set \(A_k\) of undischarged assumptions at line \(k\).

But this strategy immediately runs into a problem. As we have seen, only sentences in first-order logic can be evaluated under a given structure, so it doesn’t even make sense to ask whether \(\Gamma \cup A_k \vDash \phi_k\) or not when \(\phi_k\) has any free variables. And this is a problem we must overcome, since some of the basic rules that we introduced to deal with quantifiers do introduce such formulas in our formal proofs.

We get around this problem by introducing the notion of the closure of formulas in first-order logic.

Definition. The closure of the signature \(\sigma\) is the signature \(\overline\sigma\) obtained by adding a constant symbol \(c_{x_1}, c_{x_2}, c_{x_3},\ldots\) for each variable symbol \(x_1,x_2,x_3,\ldots\). (All these symbols must be distinct from the symbols already defined in \(\sigma\).

The closure of the first-order logic formula \(\phi\) over the signature \(\sigma\) is the sentence \(\overline{\phi}\) obtained by replacing each free instance of a variable \(x_n\) with the constant \(c_{x_n}\) for all \(n = 1,2,3,\ldots\).

Soundness of the Rules

Proposition 1. For any set \(\Gamma\) of sentences, any terms \(t\) and \(u\), any formulas \(\phi\), \(\psi\), and \(\theta\), and any contradiction \(\bot\):

• (⋀I) If \(\Gamma \vDash \overline\phi\) and \(\Gamma \vDash \overline\psi\), then \(\Gamma \vDash \overline{(\phi \wedge \psi)}.\)
• (⋀E) If \(\Gamma \vDash \overline{(\phi \wedge \psi)}\), then \(\Gamma \vDash \overline\phi\) and \(\Gamma \vDash \overline\psi.\)
• (⋁I) If \(\Gamma \vDash \overline\phi\) or \(\Gamma \vDash \overline\psi\), then \(\Gamma \vDash \overline{(\phi \vee \psi)}.\)
• (⋁E) If \(\Gamma \vDash \overline{(\phi \vee \psi)}\), \(\Gamma \cup \{\overline\phi\} \vDash \overline\theta\) and \(\Gamma \cup \{\overline\psi\} \vDash \overline\theta\), then \(\Gamma \vDash \overline\theta\).
• (→I) If \(\Gamma \cup \{\overline\phi\} \vDash \overline\psi\) then \(\Gamma \vDash \overline{(\phi \to \psi)}.\)
• (→E) If \(\Gamma \vDash \overline{(\phi \to \psi)}\) and \(\Gamma \vDash \overline\phi\) then \(\Gamma \vDash \overline\psi.\)
• (↔︎I) If \(\Gamma \vDash \overline{(\phi \to \psi)}\) and \(\Gamma \vDash \overline{(\psi \to \phi)}\), then \(\Gamma \vDash \overline{(\phi \leftrightarrow \psi)}.\)
• (↔︎E) If \(\Gamma \vDash \overline{(\phi \leftrightarrow \psi)}\), then \(\Gamma \vDash \overline{(\phi \to \psi)}\) and \(\Gamma \vDash \overline{(\psi \to \phi)}.\)
• (¬I) If \(\Gamma \cup \{\overline\phi\} \vDash \bot\) then \(\Gamma \vDash \overline{\neg \phi}.\)
• (¬E) If \(\Gamma \vDash \overline\phi\) and \(\Gamma \vDash \overline{\neg \phi}\), then \(\Gamma \vDash \bot.\)
• (⊥E) If \(\Gamma \vDash \bot\), then \(\Gamma \vDash \overline\phi\)
• (RAA) If \(\Gamma \cup \{\overline{\neg \phi}\} \vDash \bot\) then \(\Gamma \vDash \overline\phi.\)
• (=I) \(\Gamma \vDash \overline{t = t}.\)
• (=E) If \(\Gamma \vDash \overline{t=u}\) and \(\Gamma \vDash \overline\phi\), then \(\Gamma \vDash \overline{\phi[t/^*u]}.\)
• (∀I) If \(\Gamma \vDash \overline\phi\) and \(v\) is a variable that does not appear in any sentence of \(\Gamma\), then \(\Gamma \vDash \overline{\forall x \phi[v/x]}.\)
• (∀E) If \(\Gamma \vDash \overline{\forall x \phi}\) and \(t\) does not contain any variables that become bound when \(t\) is substituted for \(x\) in \(\phi\), then \(\Gamma \vDash \overline{\phi[x/t]}.\)
• (∃I) If \(\Gamma \vDash \overline{\phi}\) and \(x\) does not appear in \(\phi\), then \(\Gamma \vDash \overline{\exists x \phi[v/^*x]}.\)
• (∃E) If \(\Gamma \vDash \overline{\exists x \phi}\), \(\Gamma \cup \{\overline{\phi[x/v]}\} \vDash \overline{\psi}\), and \(v\) does not appear in \(\phi\), \(\psi\), or any sentence in \(\Gamma\), then \(\Gamma \vDash \overline{\psi}.\)

Proof.

• (⋀I) If \(\Gamma \vDash \overline\phi\) and \(\Gamma \vDash \overline\phi\) then every model \(M\) of \(\Gamma\) satisfies \({\rm val}_M(\overline\phi) = T\) and \({\rm val}_M(\overline\psi) = T\) so it also satisfies

  \[{\rm val}_M(\overline{\phi \wedge \psi}) = {\rm val}_M(\overline\phi) \wedge {\rm val}_M(\overline\psi) = T.\]

• (⋀E) If \(\Gamma \vDash \overline{(\phi \wedge \psi)}\), then every model \(M\) of \(\Gamma\) satisfies

  \[{\rm val}_M(\overline\phi) \wedge {\rm val}_M(\overline\psi) = {\rm val}_M(\overline{\phi \wedge \psi}) = T\]

  so it also satisfies \({\rm val}_M(\overline\phi) = T\) and \({\rm val}_M(\overline\psi) = T.\)

• (⋁I) If \(\Gamma \vDash \overline\phi\) or \(\Gamma \vDash \overline\psi\), then every model \(M\) of \(\Gamma\) satisfies \({\rm val}_M(\overline\phi) = T\) or \({\rm val}_M(\overline\psi) = T\) so it also satisfies

  \[{\rm val}_M(\overline{\phi \vee \psi}) = {\rm val}_M(\overline\phi) \vee {\rm val}_M(\overline\psi) = T.\]

• (⋁E) If \(\Gamma \vDash \overline{(\phi \vee \psi)}\) then every model \(M\) of \(\Gamma\) satisfies

  \[{\rm val}_M(\overline{\phi}) \vee {\rm val}_M(\overline\psi) = {\rm val}_M(\overline{\phi \vee \psi}) = T\]

  so it also satisfies \({\rm val}_M(\overline\phi) = T\) or \({\rm val}_M(\overline\psi) = T.\) Therefore, \(M\) is also a model of \(\Gamma \cup \{\overline\phi\}\) or \(\Gamma \cup \{\overline\psi\}.\) If in addition \(\Gamma \cup \{\overline\phi\} \vDash \overline\theta\) and \(\Gamma \cup \{\overline\psi\} \vDash \overline\theta\), then \({\rm val}_M(\overline\theta) = T.\)

• (→I) If \(\Gamma \cup \{\overline\phi\} \vDash \overline\psi\) then every model \(M\) of \(\Gamma\) satisfies one of the following two conditions:

  • If \({\rm val}_M(\overline\phi) = T\), then \(M\) is also a model of \(\Gamma \cup \{\overline\phi\}\) so \({\rm val}_M(\overline\psi) = T\) as well. In this case,

    \[{\rm val}_M(\overline{\phi \to \psi}) = {\rm val}_M(\overline\phi) \to {\rm val}_M(\overline\psi) = T \to T = T.\]

  • If \({\rm val}_M(\overline\phi) = F,\) then

    \[{\rm val}_M(\overline{\phi \to \psi}) = {\rm val}_M(\overline\phi) \to {\rm val}_M(\overline\psi) = F \to {\rm val}_M(\overline\psi) = T.\]

  In both cases, \({\rm val}_M(\overline{\phi \to \psi}) = T.\)

• (→E) If \(\Gamma \vDash \overline{(\phi \to \psi)}\) and \(\Gamma \vDash \overline\phi\), then every model \(M\) of \(\Gamma\) satisfies \({\rm val}_M(\overline{\phi \to \psi}) = T\) and \({\rm val}_M(\overline\phi) = T\) so it also satisfies

  \[T = {\rm val}_M(\overline{\phi \to \psi}) = {\rm val}_M(\overline\phi) \to {\rm val}_M(\overline\psi) = T \to {\rm val}_M(\overline\psi),\]

  and this identity can only be satisfied when \({\rm val}_M(\overline\psi) = T.\)

• (↔︎I) If \(\Gamma \vDash \overline{(\phi \to \psi)}\) and \(\Gamma \vDash \overline{(\psi \to \phi)}\), then every model \(M\) of \(\Gamma\) satisfies \({\rm val}_M(\overline{\phi \to \psi}) = T\) and \({\rm val}_M(\overline{\psi \to \phi}) = T\) so it also satisfies

  \[\begin{align*} {\rm val}_M(\overline{\phi \leftrightarrow \psi}) &= {\rm val}_M(\overline\phi) \leftrightarrow {\rm val}_M(\overline\psi) \\ &= ({\rm val}_M(\overline\phi) \to {\rm val}_M(\overline\psi)) \wedge ({\rm val}_M(\overline\psi) \to {\rm val}_M(\overline\phi)) \\ &= {\rm val}_M(\overline{\phi \to \psi}) \wedge {\rm val}_M(\overline{\psi \to \phi}) = T.\end{align*}\]

• (↔︎E) If \(\Gamma \vDash \overline{(\phi \leftrightarrow \psi)}\), then every model \(M\) of \(\Gamma\) satisfies

  \[\begin{align*} {\rm val}_M(\overline{\phi \to \psi}) \wedge {\rm val}_M(\overline{\psi \to \phi}) &= ({\rm val}_M(\overline\phi) \to {\rm val}_M(\overline\psi)) \wedge ({\rm val}_M(\overline\psi) \to {\rm val}_M(\overline\phi)) \\ &= {\rm val}_M(\overline\phi) \leftrightarrow {\rm val}_M(\overline\psi) \\ &= {\rm val}_M( \overline{\phi \leftrightarrow \psi}) = T \end{align*}\]

  so it also satisfies \({\rm val}_M(\overline{\phi \to \psi}) = T\) and \({\rm val}_M(\overline{\psi \to \phi}) = T.\)

• (¬I) If \(\Gamma \cup \{\overline\phi\} \vDash \bot\) then every model \(M\) of \(\Gamma\) satisfies \({\rm val}_M(\overline\phi) = F\). That’s because otherwise \(M\) is a model of \(\Gamma \cup \{\overline\phi\}\) and in that case \({\rm val}_M(\bot) = T\), contradicting the fact that any evaluation of \(\bot\) is False. So

  \[{\rm val}_M(\overline{\neg \phi}) = \neg {\rm val}_M(\overline\phi) = \neg F = T.\]

• (¬E) If \(\Gamma \vDash \overline\phi\) and \(\Gamma \vDash \overline{\neg \phi}\), then any model \(M\) of \(\Gamma\) satisfies

  \[T = {\rm val}_M(\overline{\neg \phi}) = \neg {\rm val}_M(\overline\phi)= \neg T = F.\]

  This contradiction means that there is no model of \(\Gamma\). Therefore, every formula, including the contradiction \(\bot\) is a logical consequence of \(\Gamma\).

• (⊥E) If \(\Gamma \vDash \bot\), then there is no model of \(\Gamma\) and, therefore, \(\Gamma \vDash \overline\phi\) for any formula \(\phi\).

• (RAA) If \(\Gamma \cup \{\overline{\neg \phi}\} \vDash \bot\) then every model \(M\) of \(\Gamma\) satisfies \({\rm val}_M(\overline{\neg \phi}) = F\) otherwise \(M\) would be a model of \(\Gamma \cup \{\overline{\neg \phi}\}\) and hence satisfy \({\rm val}_M(\bot) = T\), a contradiction. So

  \[F = {\rm val}_M(\overline{\neg \phi}) = \neg {\rm val}_M(\overline\phi),\]

  and \({\rm val}_M(\overline\phi) = T.\)

• (=I) By definition of the identity relation, every structure \(M\) satisfies

  \[{\rm val}_M(\overline{t = t}) = T\]

  so, in particular, every model of \(\Gamma\) satisfies this identity.

• (=E) If \(\Gamma \vDash \overline{t=u}\), then every model \(M\) of \(\Gamma\) satisfies

  \[{\rm val}_M(\overline{t}) = {\rm val}_M(\overline{u})\]

  (i.e., both \(\overline{t}\) and \(\overline{u}\) evaluate to the same element of the domain in \(M\)) so by the recursive definition evaluations, it also satisfies \({\rm val}_M(\overline\phi) = {\rm val}_M(\overline{\phi[t/^*u]})\) for every formula \(\phi\). When \(\Gamma \vDash \overline\phi\) as well, then the value of this formula is True.

• (∀I) If \(\Gamma \vDash \overline\phi\) then every model \(M\) of \(\Gamma\) satisfies \({\rm val}_M(\overline\phi) = T.\) When \(v\) is a variable that does not appear in any sentence of \(\Gamma\), then we also have that every structure \(M'\) that is identical to \(M\) except for the element that it assigns to the constant \(c_v\) is also a model of \(\Gamma\) and therefore satisfies \({\rm val}_{M'}(\overline\phi) = T.\) Therefore, by definition, \({\rm val}_M(\overline{\forall x \phi[v/x]}) = T.\)

• (∀E) If \(\Gamma \vDash \overline{\forall x \phi}\) then every model \(M\) of \(\Gamma\) satisfies \({\rm val}_M(\overline{\forall x \phi}) = T.\) By definition, this means that replacing \(x\) with any element of the domain of \(M\) gives a formula that also evaluates to True in \(M\). In other words, as long as \(t\) does not contain any variables that become bound when it is substituted for \(x\) in \(\phi\), we have \({\rm val}_M(\overline{\phi[x/t]}) = T.\)

• (∃I) If \(\Gamma \vDash \overline{\phi}\) then every model \(M\) of \(\Gamma\) satisfies \({\rm val}_M(\overline\phi) = T.\) And in this evaluation of \(\overline\phi\), every free instance of \(v\) in \(\phi\) evaluates to \(c_v^M.\) So there is a value of \(x\) (namely, \(c_v^M\)) that causes the closure of the formula \(\psi = \phi[v/^*x]\) obtained by performing a partial substitution of \(v\) with \(x\) in \(\phi\) to evaluate to True in \(M\). Hence, by definition \({\rm val}_M(\overline{\exists x \phi[v/^*x]}) = T.\)

• (∃E) If \(\Gamma \vDash \overline{\exists x \phi}\) then for every model \(M\) of \(\Gamma\) there is an element \(d\) of the domain for which \({\rm val}_M(\phi_{[x/d]}) = T.\) When \(v\) does not appear in \(\Gamma\), then the structure \(M'\) that is identical to \(M\) except that it sets \(c_v^{M'} = d\) is also a model of \(\Gamma\) and satisfies \({\rm val}_M(\overline{\phi[x/v]}) = T.\) So \(M'\) is a model of \(\Gamma \cup \{\overline{\phi[x/v]}\}\) and if \(\Gamma \cup \{\overline{\phi[x/v]}\} \vDash \overline{\psi}\) then \({\rm val}_{M'}(\overline\psi) = T.\) And when \(v\) does not appear in \(\psi\), then \({\rm val}_M(\overline\psi) = {\rm val}_{M'}(\overline\psi) = T.\)

Proof of the Soundness Theorem

We are now ready to complete the proof of the Soundness Theorem for first-order logic.

Theorem. (Soundness Theorem, restated) For every set \(\Gamma\) of sentences and every sentence \(\phi\) in first-order logic, if \(\Gamma \vdash \phi\) then \(\Gamma \vDash \phi.\)

Proof. Fix any \(\Gamma\) and \(\phi\) for which \(\Gamma \vdash \phi\) and let \(\phi_1,\ldots,\phi_n\) denote the formulas on each line of a formal proof of this implication. We prove by induction on the line number \(k\) in \(1 \le k \le n\) that

\[\Gamma \cup A_k \vDash \overline{\phi_k}.\]

Doing so completes the proof of the theorem since we must have \(\phi_n = \phi\) and \(A_n = \emptyset\) in the final line of the proof.

In the base case when \(k=1\), there are three possibilities for the justification of the first line of the proof:

• PR: Then \(\phi_1\) is a sentence in \(\Gamma\) and so \(\Gamma \vDash \overline\phi_1\).
• AS: Then \(A_1 = \{\overline{\phi_1}\}\) and so \(\Gamma \cup A_1 \vDash \overline{\phi_1}.\)
• =I: Then \(\phi_1\) is of the form \(t=t\) and from the =I case of Proposition 1, \(\Gamma \vDash \phi_1.\)

For the induction step, fix \(k > 1.\) By the induction hypothesis, we can assume that for every \(i < k\), we have \(\Gamma \cup A_i \vDash \phi_i.\) Consider the different possible justifications for the \(k\)th line of the proof:

• PR, AS, or =I: Then with the same argument used in the base case guarantees that \(\Gamma \cup A_k \vDash \overline{\phi_k}.\)
• R: In this case \(\phi_k = \phi_i\) for some \(i < k\) where \(A_i \subseteq A_k\). Then \(\Gamma \cup A_k \vDash \phi_k.\)
• ⋀I: Then \(\phi_k = (\phi_i \wedge \phi_j)\) for some \(i,j < k\) where \(A_i, A_j \subseteq A_k.\) By the induction hypothesis, \(\Gamma \cup A_i \vDash \overline{\phi_i}\) and \(\Gamma \cup A_j \vDash \overline{\phi_j}.\) So by the ⋀I case of Proposition 1, \(\Gamma \cup A_k \vDash \overline{(\phi_i \wedge \phi_j)}.\)
• ⋀E, ⋁I, ⋁E, →I, →E, ↔︎I, ↔︎E, ¬I, ¬E, =E, ∀I, ∀E, ∃I, and ∃E: All these cases follow similarly by using the appropriate case of Proposition 1.