Lesson 15

We next prove a reassuring result, stating that our proof system is sound, in that it only proves valid consequences.

Theorem (The Soundness Theorem). If \(\Delta \vdash \phi\), then \(\Delta \models \phi\).

Proof. Consider any proof \(S = (\phi_{1}, …, \phi_{n})\) from \(\Delta\). We shall show by induction that \(\Delta \models \phi_{i}\). If \(\phi_{i}\) is a logical or non-logical axiom, then clearly \(\Delta \models \phi_{i}\). So, suppose that \(\phi_{i}\) is obtained from \(\phi_{j}\), \(j < i\), and \(\phi_{j} \Rightarrow \phi_{i}\) by modus ponens. Then, by induction, \(\Delta \models \phi_{j}\) and \(\Delta \models \phi_{j} \Rightarrow \phi_{i}\). Thus any model that satisfies \(\Delta\) also satisfies \(\phi_{j}\) and \(\phi_{j} \Rightarrow \phi_{i}\); therefore it satisfies \(\phi_{i}\). It follows that \(\Delta \models \phi_{i}\).◼

The converse of the soundness theorem, the completeness theorem for first-order logic due to Kurt Gödel, states that the proof system introduced in the previous section is able to prove all valid consequences:

Theorem. If \(\Delta \models \phi\), then \(\Delta \vdash \phi\).

We will prove a variant of this result, namely the following:

Theorem. If \(\Delta\) is consistent, then it has a model.

To show that the original form follows from the second, suppose that \(\Delta \models \phi\). This means that any model that satisfies all expressions in \(\Delta\) also satisfies \(\phi\) (and, naturally, falsifies \(\neg\phi\)). Hence, no model satisfies all expressions in \(\Delta \cup \{\neg\phi\}\), and hence (here we are using the second form of the theorem) this set is inconsistent. Arguing by contradiction, \(\Delta \vdash \phi\). Also, the second form can be easily seen to be a consequence of the first.

But before we prove it, let's talk about its consequences. Since the completeness and soundness theorems identify valid sentences with first-order theorems, the computational problem Validity (given an expression, is it valid?) is the same as Theoremhood. Hence,

Corollary. Validity is recursively enumerable.

Another immediate consequence of the completeness theorem is the following important property of first-order logic (the same result for Boolean logic, much easier to prove), called the Compactness Theorem:

Corollary. If all finite subsets of a set of sentences \(\Delta\) are satisfiable, then \(\Delta\) is satisfiable.

Proof. Suppose that \(\Delta\) is not satisfiable, but all of its finite subsets are. Then, by the completeness theorem, there is a proof of a contradiction from \(\Delta\): \(\Delta \vdash \phi \wedge \neg \phi\). This proof employs finitely many sentences from \(\Delta\). Therefore, there is a finite subset of \(\Delta\) (the one involved in the proof of the contradiction) that is unsatisfiable, contrary to our assumption.◼

A first application of the compactness theorem shows that the nonstandard model \(\mathbb{N}'\) of number theory (the natural numbers plus a disjoint copy of the integers, introduced before) cannot be differentiated from \(\mathbb{N}\) by first-order sentences.

Corollary. If \(\Delta\) is a set of first-order sentences such that \(\mathbb{N}\models \Delta\), then there is a model \(\mathbb{N}'\) such that \(\mathbb{N}' \models \Delta\), and the universe of \(\mathbb{N}'\) is a proper superset of the universe of \(\mathbb{N}\).

Proof. Left as an exercise.◼

The proof of the completeness theorem establishes the following basic fact about models:

Corollary. If a sentence has a model, it has a countable model.

Proof. The model \(M\) constructed in the proof of the completeness theorem is countable, since the vocabulary \(\Sigma'\) is countable. \(\square\)◼ But, of course, a countable model can be either finite or infinite. The model \(M\) in the proof of the completeness theorem is in general infinite. Is it true that all sentences have a countably infinite model? The answer is “no”. Some sentences, such as \(\forall x \forall y (x = y)\) and \(\exists x \exists y \forall z (z = x \vee z = y)\), have no infinite models. However, this is achieved by specifying an upper bound on the cardinality of any model (one for the former, two for the latter). Our next result states in essence that this is the only way for a sentence to avoid satisfaction by infinite models, called the Löwenheim–Skolem Theorem.

Corollary. If a sentence \(\phi\) has finite models of arbitrarily large cardinality, then it has an infinite model.

Proof. Consider the sentence \(\psi_{k} = \exists x_{1} … \exists x_{k} \bigwedge_{1 \leq i < j \leq k}\neg(x_{i} = x_{j})\), where \(k > 1\) is an integer. Obviously, \(\psi_{k}\) states that there are at least \(k\) distinct elements in the universe; it cannot be satisfied by a model with a universe containing \(k - 1\) or fewer elements, and any model with \(k\) or more elements satisfies it.

Let us assume, for the sake of contradiction, that \(\phi\) has arbitrarily large models, but no infinite model. Consider thus the set of sentences \(\Delta = \{\phi\} \cup \{\psi_{k} : k = 2, 3, …\}\). If \(\Delta\) has a model \(M\), then \(M\) cannot be finite (because, if it were, and had \(k\) elements, it would not satisfy \(\psi_{k+1}\)), and cannot be infinite (it would satisfy \(\phi\)). So, \(\Delta\) has no model.

By the compactness theorem, there is a finite set \(D \subset \Delta\) that has no model. This subset must contain \(\phi\) (otherwise, any sufficiently large model would satisfy all \(\psi_{k}\)’s in \(D\)). Suppose then that \(k\) is the largest integer such that \(\psi_{k} \in D\). By our hypothesis, \(\phi\) has a finite model of cardinality larger than \(k\). It follows that this model satisfies all sentences in \(D\), a contradiction.◼

In the practice, we will demonstrate that the REACHABILITY problem cannot be expressed by first-order logic. The underlying intuition is quite straightforward: expressing the existence of a path between two vertices in a graph requires arbitrarily many quantifiers.

Nevertheless, this result is of significant interest, for several reasons. First, it constitutes a nontrivial impossibility theorem, and impossibility theorems are precisely the kinds of results we would hope to establish in complexity theory (and are, indeed, still far from proving…). Moreover, this impossibility result has stimulated the investigation of suitable extensions of first-order logic, and has ultimately contributed to an important aspect of the deep relationship between complexity theory and logic. However, a detailed exploration of this topic lies beyond the scope of this course.