2.5: Soundness

Mathematicians are by nature a conservative bunch. We speak not of political or social leanings, but of their professional outlook. In particular, a mathematician likes to know that when something has been proved, it is true. In this section we will prove a theorem that shows that the logical system that we have developed has this highly desirable property. This result is called the Soundness Theorem.

Let us restate the list of requirements that we set for our axioms and rules of inference:

1. There will be an algorithm that will decide, given a formula \(\theta\), whether or not \(\theta\) is a logical axiom.
2. There will be an algorithm that will decide, given a finite set of formulas \(\Gamma\) and a formula \(\theta\), whether or not \(\left( \Gamma, \theta \right)\) is a rule of inference.
3. For each rule of inference \(\left( \Gamma, \theta \right)\), \(\Gamma\) will be a finite set of formulas.
4. Each logical axiom will be valid.
5. Our rules of inference will preserve truth. In other words, for each rule of inference \(\left( \Gamma, \theta \right)\), \(\Gamma \models \theta\).

These requirements serve two purposes: They allow us to verify mechanically that an alleged deduction is in fact a deduction, and they provide the basis of the Soundness Theorem. Of course, we must first verify that the system of axioms and rules that we have set out in the preceding two sections satisfies these requirements.

That the first three requirements above are satisfied by our deduction system was noted as the axioms and rules were presented. These are the rules that are needed for deduction verification. We will discuss the last two requirements in more detail and then use those requirements to prove the Soundness Theorem.

Theorem 2.5.1. The logical axioms are valid.

Proof. We must check both the equality axioms and the quantifier axioms. First, consider equality axioms of type (E2). [(E1) and (E3) will be proved in the Exercises.]

Chaff: Let us mention that we will use Theorem 2.6.2 in this proof. Although the presentation of that result has been delayed in order to aid the flow of the exposition, you may want to look at the statement of that theorem now so you won't be surprised when it appears.

So fix a structure \(\mathfrak{A}\) and an assignment function \(s \: : \: Vars \rightarrow A\). We must show that

\[\mathfrak{A} \models \left( \left[ \left( x_1 = y_1 \right) \land \left( x_2 = y_2 \right) \land \cdots \land \left( x_n = y_n \right) \right] \rightarrow \left( f \left( x_1, x_2, \ldots, x_n \right) = f \left( y_1, y_2, \ldots, y_n \right) \right) \right) \left[ s \right].\]

As the formula in question is an implication, we may assume that the antecedent is satisfied by the pair \(\left( \mathfrak{A}, s \right)\), and thus \(s \left( x_1 \right) = s \left( y_1 \right)\), \(s \left( x_2 \right) = s \left( y_2 \right), \ldots,\) and \(s \left( x_n \right) = s \left( y_n \right)\). We must prove that \(\mathfrak{A} \models \left( f \left( x_1, x_2, \ldots, x_n \right) = f \left( y_1, y_2, \ldots, y_n \right) \right) \left[ s \right]\). From the definition of satisfaction (Definition 1.7.4), we know this means that we have to show

\[\bar{s} \left( f \left( x_1, x_2, \ldots, x_n \right) \right) = \bar{s} \left( f \left( y_1, y_2, \ldots, y_n \right) \right).\]

Now we look at the definition of term assignment function (Definition 1.7.3) and see that we must prove

\[f^\mathfrak{A} \left( \bar{s} \left( x_1 \right), \bar{s} \left( x_2 \right), \ldots, \bar{s} \left( x_n \right) \right) = f^\mathfrak{A} \left( \bar{s} \left( y_1 \right), \bar{s} \left( y_2 \right), \ldots, \bar{s} \left( y_n \right) \right).\]

But since \(\bar{s} \left( x_i \right) = s \left( x_i \right) = s \left( y_i \right) = \bar{s} \left( y_i \right)\), and since \(f^\mathfrak{A}\) is a function, this is true. Thus our equality axiom (E2) is valid.

Now we examine the quantifier axiom of type (Q1), reserving (Q2) for the Exercises. Once again, fix \(\mathfrak{A}\) and \(s\), and assume that the term \(t\) is substitutable for the variable \(x\) in the formula \(\phi\). We must show that

\[\mathfrak{A} \models \left[ \left( \forall x \phi \right) \rightarrow \phi_t^x \right] \left[ s \right].\]

So once again, we assume that \(\mathfrak{A} \models \left( \forall x \phi \right) \left[ s \right]\), and we show that \(\mathfrak{A} \models \phi_t^x \left[ s \right]\). By assumption, \(\mathfrak{A} \models \phi \left[ s \left[ x | a \right] \right]\) for any element \(a \in A\), so in particular, \(\mathfrak{A} \models \phi \left[ s \left[ x | \bar{s} \left( t \right) \right] \right]\).

Informally, this says that \(\phi\) is true in \(\mathfrak{A}\) with assignment function \(s\), where you interpret \(x\) as \(\bar{s} \left( t \right)\). It is plausible, given our assumption that \(t\) is substitutable for \(x\) in \(\phi\), that if we altered the formula \(\phi\) by replacing \(x\) by \(t\), then \(\phi_t^x\) would be true in \(\mathfrak{A}\) with assignment function \(s\). This is the content of Theorem 2.6.2. Since we know that \(\mathfrak{A} \models \phi \left[ s \left[ x | \bar{s} \left( t \right) \right] \right]\) and Theorem 2.6.2 states that this is equivalent to \(\mathfrak{A} \models \phi_t^x \left[ s \right]\), we have established \(\mathfrak{A} \models \phi_t^x \left[ s \right]\), so we have proved that axioms of type (Q1) are valid.

Thus, modulo your proofs of (E1), (E3), and (Q2), and the delayed proof of Theorem 2.6.2, all of our logical axioms are valid, and our proof is complete.

This leaves one more item on our list of requirements to check. We must show that our rules of inference preserve truth.

Theorem 2.5.2. Suppose that \(\left( \Gamma, \theta \right)\) is a rule of inference. Then \(\Gamma \models \theta\).

Proof. First, assume that \(\left( \Gamma, \theta \right)\) is a rule of type (PC). Then \(\Gamma\) is finite, and by Lemma 2.4.2, we know that

\[\left[ \gamma_{1 \: P} \land \gamma_{2 \: P} \land \cdots \land \gamma_{n \: P} \right] \rightarrow \theta_P\]

is a tautology, where \(\Gamma_P = \{ \gamma_{1 \: P}, \gamma_{2 \: P}, \ldots, \gamma_{n \: P} \}\) is the set of propositional formulas corresponding to \(\Gamma\) and \(\theta_P\) is the propositional formula corresponding to \(\theta\). But then, by Exercise 6 of Section 2.4, we know that

\[\left[ \gamma_1 \land \gamma_2 \land \cdots \land \gamma_n \right] \rightarrow \theta\]

is valid, and thus \(\Gamma \models \theta\).

The other possibility is that our rule of inference is a quantifier rule. So, suppose that \(x\) is not free in \(\psi\). We show that \(\left( \psi \rightarrow \phi \right) \models \left[ \psi \rightarrow \left( \forall x \phi \right) \right]\), leaving the other (Q2) rule for the Exercises.

So fix a structure \(\mathfrak{A}\) and assume \(\mathfrak{A} \models \left( \psi \rightarrow \phi \right)\). Thus our assumption is that for any assignment \(s\), \(\mathfrak{A} \models \left( \psi \rightarrow \phi \right) \left[ s \right]\). We must show that \(\mathfrak{A} \models \left( \psi \rightarrow \forall x \phi \right)\), which means that we must show that \(\left( \psi \rightarrow \forall x \phi \right)\) is satisfied in \(\mathfrak{A}\) under every assignment function. So let an assignment function \(t \: : \: Vars \rightarrow A\) be given. We must show that \(\mathfrak{A} \models \left( \psi \rightarrow \forall x \phi \right) \left[ t \right]\). If \(\mathfrak{A} \not\models \psi \left[ t \right]\), we are done, so assume that \(\mathfrak{A} \models \psi \left[ t \right]\). We want to prove that \(\mathfrak{A} \models \forall x \phi \left[ t \right]\), which means that if \(a\) is any element of \(A\), we must show that \(\mathfrak{A} \models \phi \left[ t \left[ x | a \right] \right]\).

We know, by assumption, that \(\mathfrak{A} \models \left( \psi \rightarrow \phi \right) \left[ t \left[ x | a \right] \right]\). Furthermore, Proposition 1.7.7 tells us that \(\mathfrak{A} \models \psi \left[ \left[ x | a \right] \right]\), as \(\mathfrak{A} \models \psi \left[ t \right]\), and \(t\) and \(t \left[ x | a \right]\) agree on all of the free variables of \(\psi\) (\(x\) is not free in \(\psi\) by assumption). But then, by the definition of satisfaction, \(\mathfrak{A} \models \phi \left[ t \left[ x | a \right] \right]\), and we are finished.

We are now at a point where we can prove the Soundness Theorem. The idea behind this theorem is very simple. Suppose that \(\Sigma\) is a set of \(\mathcal{L}\)-formulas and suppose that there is a deduction of \(\phi\) from \(\Sigma\). What the Soundness Theorem tells us is that in any structure \(\mathfrak{A}\) that makes all of the formulas of \(\Sigma\) true, \(\phi\) is true as well.

Theorem 2.5.3 (Soundness). If \(\Sigma + \phi\), then \(\Sigma \models \phi\).

Proof. Let Thm\(_\Sigma\) \(= \{ \phi | \Sigma \vdash \phi \}\), and let \(C = \{ \phi | \Sigma \models \phi \}\). We show that Thm\(_\Sigma\) \(\subseteq C\), which proves the theorem.

Notice that \(C\) has the following characteristics:

1. \(\Sigma \subseteq C\). If \(\sigma \in \Sigma\), then certainly \(\Sigma \models \sigma\).
2. \(\Lambda \subseteq C\). As the logical axioms are valid, they are true in any structure. Thus \(\Sigma \models \lambda\) for any logical axiom \(\lambda\), which means that if \(\lambda \in \Lambda\), then \(\lambda \in C\), as needed.
3. If \(\left( \Gamma, \theta \right)\) is a rule of inference and \(\Gamma \subseteq C\), then \(\theta \in C\). So assume that \(\Gamma \subseteq C\). To prove \(\theta \in C\) we must show that \(\Sigma \models \theta\). Fix a structure \(\mathfrak{A}\) such that \(\mathfrak{A} \models \Sigma\). We must prove that \(\mathfrak{A} \models \theta\).
   If \(\gamma\) is any element of \(\Gamma\), then since \(\gamma \in C\), we know that \(\Sigma \models \gamma\). Since \(\mathfrak{A} \models \Sigma\) and \(\Sigma \models \gamma\), we know that \(\mathfrak{A} \models \gamma\). But this says that \(\mathfrak{A} \models \gamma\) for each \(\gamma \in \Gamma\), so \(\mathfrak{A} \models \Gamma\). But Theorem 2.5.2 tells us that \(\Gamma \models \theta\), since \(\left( \Gamma, \theta \right)\) is a rule of inference. Therefore, since \(\mathfrak{A} \models \Gamma\) and \(\Gamma \models \theta\), \(\mathfrak{A} \models \theta\), as needed.

So \(C\) is a set of the type outlined in Proposition 2.2.4, and by that proposition, Thm\(_\Sigma\) \(\subseteq C\), as needed.

Notice that the Soundness Theorem begins to tie together the notions of deducibility and logical implication. It says, "If there is a deduction from \(\Sigma\) of \(\phi\), then \(\Sigma\) logically implies \(\phi\)." Thus the purely syntactic notion of deduction, a notion that relies only upon typographical considerations, is linked to the notions of truth and logical implication, ideas that are inextricably tied to mathematical structures and their properties. This linkage will be tightened in Chapter 3.

Chaff: The proof of the Soundness Theorem that we have presented above has the desirable qualities of being net and quick. It emphasizes a core fact about the consequences of \(\Sigma\), namely that Thm\(_\Sigma\) is the smallest set of formulas satisfying the given three conditions. Unfortunately, the proof has the less desirable attribute of being pretty abstract. Exercise 5 outlines a more direct, less abstract proof of the Soundness Theorem.

Exercises

1. Ingrid walks into your office one day and announces that she is puzzled. She has a set of axioms \(\Sigma\) in the language of number theory, and she has a formula \(\phi\) that she has proved using the assumptions in \(\Sigma\). Unfortunately, \(\phi\) is a statement that is not true in the standard model \(\mathfrak{N}\). Is this a problem? If it is a problem, what possible explanations can you think of that would explain what went wrong? If it is not a problem, why is it not a problem?
2. Prove that the equality axioms of type (E1) and (E3) are valid.
3. Show that the quantifier axioms of type (Q2) is valid.
4. Show that, if \(x\) is not free in \(\psi\), \(\left( \phi \rightarrow \psi \right) \models \left[ \left( \exists x \phi \right) \rightarrow \psi \right]\).
5. Prove the Soundness Theorem by induction on the complexity of the proof of \(\phi\). For the base cases, \(\phi\) is either a logical axiom or a member of \(\Sigma\). Then assume that \(\phi\) is proved by reference to a rule of inference. Show that in this case as well, \(\Sigma \models \phi\).