16. Completeness Theorem

The Completeness Theorem holds for first-order logic as well: whenever $\Gamma \vDash \phi$, then there exists a proof showing that $\Gamma \vdash \phi$ as well. The Completeness Theorem for first-order logic was first established by Kurt Gödel in his doctoral dissertation. It is not to be confused with his two incompleteness theorems, which we will cover later in the course.

Theorem. (Completeness Theorem for first-order logic) For every set $\Gamma$ of sentences and every sentence $\phi$, if $\Gamma \vDash \phi$ then $\Gamma \vdash \phi.$

The high-level approach to proving the Completeness Theorem is the same as in propositional logic. Namely, we want to show that every consistent set of sentences is satisfiable or, in other words, that it has a model. And instead of trying to establish this statement directly, we instead want to first consider a “special class” of consistent sets of sentences and show that all these sets have a model.

In propositional logic, the special class of consistent sets that we considered were the maximally consistent sets of formulas. In first-order logic, we have to consider an extension of this context which takes into account the added complications that we face in defining an entire structure (with domain, constants, functions, and predicates) that satisfies the sentences in the set $\Gamma$. We start by introducing the class of sets of sentences that will help us do that.

Maximal Consistency and Saturation

The notions of consistency and maximum consistency introduced in propositional logic also apply to sets of first-order logic formulas.

Definition. The set $\Gamma$ of first-order formulas is

consistent if $\Gamma \not\vdash \bot,$

inconsistent if $\Gamma \vdash \bot,$ and

maximally consistent if $\Gamma$ is consistent and for every sentence $\phi \notin \Gamma$, the set $\Gamma \cup \{\phi\}$ is inconsistent.

Maximally consistent sets of sentences satisfy many useful properties.

Proposition 1. For every maximally consistent set $\Gamma$ of formulas and any sentences $\phi$ and $\psi,$

$\Gamma \vdash \phi$ if and only if $\phi \in \Gamma.$

$\neg \phi \in \Gamma$ if and only if $\phi \notin \Gamma.$

$(\phi \wedge \psi) \in \Gamma$ if and only if $\phi \in \Gamma$ and $\psi \in \Gamma.$

$(\phi \vee \psi) \in \Gamma$ if and only if $\phi \in \Gamma$ or $\psi\in \Gamma.$

$(\phi \to \psi) \in \Gamma$ if and only if $\phi \notin \Gamma$ or $\psi \in \Gamma$.

$(\phi \leftrightarrow \psi) \in \Gamma$ if and only if either both or neither of $\phi$ and $\psi$ are in $\Gamma.$

We also want the set of sentences that we consider to satisfy some additional properties that will let us deal with the quantifiers. We do so by introducing one more definition.

Definition. A set $\Gamma$ of formulas over a first-order language is saturated if and only if for every formula $\phi$ over the language that contains a single free variable $x$, there is a constant $c$ in the language for which $(\exists x \, \phi \to \phi[x/c]) \in \Gamma.$

Sets of formulas that are both maximally consistent and saturated satisfy the following useful properties related to quantifiers.

Proposition 2. For every maximally consistent and saturated set $\Gamma$ of formulas and every formula $\phi$ that contains only $x$ as a free variable,

$\exists x \phi \in \Gamma$ if and only if there exists a closed term $t$ for which $\phi[x/t] \in \Gamma$ and

$\forall x \phi \in \Gamma$ if and only if for every closed term $t$, $\phi[x/t] \in \Gamma.$

Proof. By Proposition 1 and the assumption that $\Gamma$ is maximally consistent, to show that some sentence $\psi$ is in $\Gamma$, all we need to do is to show that $\Gamma \vdash \psi.$ This is what we do to prove both directions of each iff statement:

Consider first the case where $\exists x \phi \in \Gamma$. By the saturation property, there is a constant $c$ (which is also a closed term) for which $(\exists x \phi \to \phi[x/c]) \in \Gamma.$ With the →E rule, we then obtain $\Gamma \vdash \phi[x/c].$

In the other direction, if $\phi[x/t] \in \Gamma$ then by the ∃I rule, $\Gamma \vdash \exists x \phi.$

If $\forall x \phi \in \Gamma$ then with the ∀E rule we obtain $\Gamma \vdash \phi[x/t]$ for any closed term $t$.

Consider now the case where for every closed term $t$ we have $\phi[x/t] \in \Gamma.$ By the saturation property applied to the formula $\neg \phi,$ there exists a constant $c$ for which $(\exists x \neg \phi \to \neg \phi[x/c]) \in \Gamma.$ Since $c$ is also a term, we also have that $\phi[x/c] \in \Gamma.$ By applying the modus tollens derived rule, we then get $\Gamma \vdash \neg \exists \neg \phi.$ This last sentence is logically equivalent to $\forall x \phi,$ so by the maximal consistency of $\Gamma$ we must also have $\forall x \phi \in \Gamma.$

A Warm-Up Completeness Theorem

To establish the first special case of the Completeness Theorem, let us focus on maximally consistent and saturated sets of formulas. And let us make one other simplification: let us only examine sentences that do not use the identity predicate for now.

So let $\Gamma$ be maximally consistent and saturated. And let $\phi$ be an arbitrary sentence that does not include the = predicate. We want to construct a model $M_\Gamma$ for $\Gamma$, and we want it to satisfy ${\rm val}_{M_\Gamma}(\phi) = T$ if and only if $\phi \in \Gamma.$

How can we do this? The key insight that lets us do this easily is to notice that while the domain of structures is usually a natural set (like the set of natural numbers, integers, graphs, etc.), it does not have to be! In fact, we can define a domain set that is custom-built to make it easy to reason about $M_{\Gamma}$.

One way to apply this insight is to introduce the term model defined in the following way.

Definition. The term model $M^*_\Gamma$ for a maximally consistent and saturated set $\Gamma$ of formulas over the language $\mathcal{L}$ is the structure defined by

the domain $D_\Gamma$ is the set of terms in $\mathcal{L}$. We use bold font to distinguish between a term $t$ in a formula and its corresponding element ${\bf t}$ in $D_\Gamma.$

The constant $c$ in the signature is assigned the element $c^{M^*_\Gamma} = {\bf c}$.

Each function $f$ is defined by setting $f^{M^*_\Gamma}({\bf t_1},\ldots,{\bf t_n}) = {\bf f(t_1,\ldots,t_n)}.$

The $n$-ary predicate $P$ is defined to be the subset
\[P^{M^*_\Gamma} = \{ ({\bf t_1}, \ldots, {\bf t_n}) : P(t_1,\ldots,t_n) \in \Gamma \}.\]

Example. Consider a set of axioms $\Gamma$ over the natural language signature with the constant $0$, the unary successor function $S$, and the binary addition function.

The set of elements in the domain of the term model $M^*_\Gamma$ includes
\[{\bf 0}, \quad {\bf S(0)}, \quad {\bf (0 + 0)}, \quad {\bf S(S(0))}, \quad {\bf (0 + S(0))}\]
and infinitely many other elements. All of these elements are distinct: even though $0 = 0 + 0$ in the standard model of arithmetic that we usually consider, this is not the case here: ${\bf 0}$ and ${\bf 0 + 0}$ are two distinct (and thus non-equal) elements of the domain of the term model.

The constant $0$ is assigned the element $0^{M^*_\Gamma} = {\bf 0}$ in $M_\Gamma.$

The function $+$ is defined to be $(t_1 + t_2)^{M^*_\Gamma} = {\bf t_1 + t_2}$. For instance, $S(0 + S(0))^{M^*_\Gamma} = {\bf S(0 + S(0))}.$

A basic property of the term model is that every closed term evaluates to its corresponding symbol in this model.

Proposition 3. For every closed term $t$, ${\rm val}_{M^*_\Gamma}(t) = {\bf t}.$

Proof. By induction on the length of $t$.

In the base case, when $| t | = 1$, then the term $t$ consists of a single constant symbol $c$ and by definition it evaluates to the corresponding element ${\bf c}$.

For the induction step, when $|t| > 1$ then $t = f(t_1,\ldots,t_n)$ for some $n$-ary function $f$ and some $n$ closed terms $t_1,\ldots,t_n$. By the definition of $M^*_\Gamma$ and the induction hypothesis,
\[\begin{align*} {\rm val}_{M^*_\Gamma}\big( f(t_1,\ldots,t_n) \big) &= f^{M^*_\Gamma}\big( {\rm val}_{M^*_\Gamma}(t_1),\ldots,{\rm val}_{M^*_\Gamma}(t_n) \big) \\ &= f^{M^*_\Gamma}\big( {\bf t_1},\ldots,{\bf t_n} \big) \\ &= {\bf f(t_1,\ldots,t_n)}. \end{align*}\]

We can now prove the following special case of the Completeness Theorem.

Lemma 4. For any maximally consistent and saturated set $\Gamma$ of formulas and any formula $\phi$ that does not contain the = symbol, $M^*_\Gamma \vDash \phi$ if and only if $\phi \in \Gamma.$

Proof. We proceed by induction on the total number of connectives and quantifiers in $\phi$.

In the base case, when $\phi$ does not contain any quantifiers or connectives, then $\phi = P(t_1,\ldots,t_n)$ for some $n$-ary predicate $P$ and $n$ closed terms $t_1,\ldots,t_n$. By Proposition 3,
\[{\rm val}_{M^*_\Gamma}( P(t_1,\ldots,t_n) ) = P^{M^*_\Gamma}( {\bf t_1},\ldots,{\bf t_n})\]
and by construction this is True if and only if $P(t_1,\ldots,t_n) \in \Gamma.$

In the induction step, we consider the different possibilities on how $\phi$ is constructed.

If $\phi = (\psi \wedge \theta)$ then
\[{\rm val}_{M^*_\Gamma}( \psi \wedge \theta) = {\rm val}_{M^*_\Gamma}(\psi) \wedge {\rm val}_{M^*_\Gamma}(\theta).\]
By the induction hypothesis, the right-hand side of this equation evaluates to True if and only if $\psi \in \Gamma$ and $\theta \in \Gamma.$ Since $\Gamma$ is maximally consistent, this event holds if and only if $\phi = (\psi \wedge \theta) \in \Gamma$.

The cases where $\phi$ is obtained from applying one of the other connectives $\neg, \vee, \to, \leftrightarrow$ to shorter sentences are all as in the case above.

If $\phi = \exists x \psi$, then ${\rm val}_{M^*_\Gamma}(\exists x \psi)$ evaluates to True if and only if there is a domain element ${\bf t}$ which, when substituted for $x$ in $\psi$, causes the resulting sentence $\psi_{[x/{\bf t}]}$ to evaluate to True. By Proposition 3, this occurs if and only if there is a term $t$ for which ${\rm val}_{M^*_\Gamma}(\psi[x/t]) = T.$ By the induction hypothesis, this last event holds if and only if $\psi[x/t] \in \Gamma.$ And since $\Gamma$ is saturated, by Proposition 2 this occurs if and only if $\phi = \exists x \psi \in \Gamma.$

If $\phi = \forall x \psi$, then ${\rm val}_{M^*_\Gamma}(\forall x \psi)$ evaluates to True if and only if for every domain element ${\bf t}$, when ${\bf t}$ is substituted for $x$ in $\psi$, causes the resulting sentence $\psi_{[x/{\bf t}]}$ to evaluate to True. By Proposition 3, this occurs if and only if every term $t$ satisfies ${\rm val}_{M^*_\Gamma}(\psi[x/t]) = T.$ By the induction hypothesis, this last event holds if and only if $\psi[x/t] \in \Gamma.$ And since $\Gamma$ is saturated, by Proposition 2 this occurs if and only if $\phi = \forall x \psi \in \Gamma.$

Factoring the Term Model

The term model we constructed in the last section does not satisfy formulas that include the = symbol. For example, the formula $0 + 0 = 0$ that we could include in the set $\Gamma$ of axioms does not evaluate to True in the term model $M^*_\Gamma$ because ${\bf 0 + 0}$ and ${\bf 0}$ are distinct elements of its domain. But we do want to construct a model that does satisfy formulas in $\Gamma$ that include the = symbol, so we construct a different model for $\Gamma$ that we call the factored term model.

Definition. Fix any set $\Gamma$ of formulas. Define the equivalence relation for $\Gamma$ to be the binary relation $\approx_\Gamma$ such that for any two closed terms $t$ and $t'$,
\[t \approx_\Gamma t' \qquad \mbox{iff} \qquad t=t' \in \Gamma.\]

The relation $\approx_\Gamma$ is indeed an equivalence relation and it also satisfies other useful properties when $\Gamma$ is maximally consistent:

Proposition 5. For any maximally consistent set $\Gamma$ of sentences, the relation $\approx_\Gamma$ is relexive, symmetric, and transitive. Furthermore, if $t_1,\ldots,t_n$ are any $n$ closed terms, $i \in \{1,2,\ldots,n\}$, and $t'_i$ satisfies $t'_i \approx_\Gamma t_i$ then for any $n$-ary function $f$,
\[f(t_1,\ldots,t_n) \approx_\Gamma f(t_1,\ldots,t_{i-1},t'_i,t_{i+1},\ldots,t_n)\]
and for any $n$-ary predicate $P$,
\[P(t_1,\ldots,t_n) \in \Gamma \mbox{ iff } P(t_1,\ldots,t_{i-1},t'_i,t_{i+1},\ldots,t_n) \in \Gamma.\]

Proof.

(Reflexivity) Every closed term $t$ satisfies $\Gamma \vdash t = t$ by the =I rule, so when $\Gamma$ is maximally consistent $t = t \in \Gamma$ and by definition $t \approx_\Gamma t.$

(Symmetry) For all closed terms $t,t'$ that satisfy $t=t' \in \Gamma$, we have $\Gamma \vdash t' = t$ by the =E rule and so $t' = t \in \Gamma$. Therefore, whenever $t \approx_\Gamma t'$, then $t' \approx_\Gamma t$ as well.

(Transitivity) When $t_1,t_2,t_3$ satisfy $t_1 = t_2 \in \Gamma$ and $t_2 = t_3 \in \Gamma$, then by the =E rule $\Gamma \vdash t_1 = t_3$ and so $t_1 = t_3 \in \Gamma.$ Thus, whenever $t_1 \approx_\Gamma t_2$ and $t_2 \approx_\Gamma t_3$, then $t_1 \approx_\Gamma t_3$ as well.

(Functions) When $t_i = t'_i \in \Gamma$, then any model of $\Gamma$ evaluates $t_i$ and $t'_i$ to the same domain element, and so $f(t_1,\ldots,t_n) \approx_\Gamma f(t_1,\ldots,t_{i-1},t'_i,t_{i+1},\ldots,t_n).$

(Predicates) When and $t_i = t'_i \in \Gamma$, then by the =E rule and the maximal consistency of $\Gamma$, $P(t_1,\ldots,t_n) \in \Gamma$ if and only if $P(t_1,\ldots,t_{i-1},t'_i,t_{i+1},\ldots,t_n) \in \Gamma.$

We can use the relation $\approx_\Gamma$ to partition the set of all closed terms into equivalence classes.

Definition. For any maximally consistent set $\Gamma$ of formulas, define the equivalence class for the closed term $t$ to be
\[[t]_{\approx_\Gamma} = \{t' : t' \approx_\Gamma t\}.\]

We are now ready to introduce the factored term model:

Definition. The factored term model for the maximally consistent set $\Gamma$ of formulas is the structure $M^\approx_\Gamma$ with domain $D^\approx_\Gamma = \{ {\bf [t]_{\approx_\Gamma}} : t \mbox{ is a closed term}\}$ where we assign constant $c$ the element
\[c^{M^\approx_\Gamma} = {\bf [c]_{\approx_\Gamma}},\]
we define the $n$-ary function $f$ to take the values
\[f^{M^\approx_\Gamma}({\bf [t_1]_{\approx_\Gamma}},\ldots,{\bf [t_n]_{\approx_\Gamma}}) = {\bf [ f(t_1,\ldots,t_n) ]_{\approx_\Gamma}},\]
and we define the $n$-ary predicate $P$ to be the set
\[P^{M^\approx_\Gamma} = \{ ({\bf [t_1]_{\approx_\Gamma}},\ldots,{\bf [t_n]_{\approx_\Gamma}}) : P(t_1,\ldots,t_n) \in \Gamma\}.\]

When $\Gamma$ is any maximally consistent set of sentences, the factored term model $M_\Gamma^\approx$ is well-defined and satisfies ${\rm val}_{M^\approx_\Gamma}(t) = {\bf [t]_{\approx_\Gamma}}$ for every closed term $t$. We use $M_\Gamma^\approx$ to obtain the completeness theorem for maximally consistent and saturated sets of formulas.

Lemma 6. Every maximally consistent and saturated set $\Gamma$ of sentences is satisfiable.

Proof. We prove the stronger statement that for every sentence $\phi$, the factored term model satisfies $M^\approx_\Gamma \vDash \phi$ if and only if $\phi \in \Gamma$ by induction on the total number of logical connectives and quantifiers in $\phi.$

In the base case, when $\phi$ does not contain any quantifiers or connectives, there are two possibilities.

If $\phi = P(t_1,\ldots,t_n)$ then as in the proof of Lemma 4, we have
\[\begin{align*}{\rm val}_{M^\approx_\Gamma}(P(t_1,\ldots,t_n)) &= P^{M_\Gamma^\approx}( {\rm val}_{M^\approx_\Gamma}(t_1),\ldots,{\rm val}_{M^\approx_\Gamma}) \\ &= P^{M_\Gamma^\approx}( {\bf [t_1]_{\approx_\Gamma}},\ldots, {\bf [t_n]_{\approx_\Gamma}})\end{align*}\]
and this evalutes to True if and only if $\phi \in \Gamma.$

If $\phi$ is of the form $t_1 = t_2$ then ${\rm val}_{M^\approx_\Gamma}(\phi)$ is True if and only if ${\bf [t_1]_{\approx_\Gamma}} = {\bf [t_2]_{\approx_\Gamma}}$ or, equivalently, if $t_1 \approx_\Gamma t_2$. By definition, this equivalence holds if and only if $t_1 = t_2 \in \Gamma.$

The induction step of the argument proceeds exactly as in the proof of Lemma 4, again with a case analysis for the different ways that $\phi$ can be constructed from simpler sentences with a logical connective or a quantifier.

Wrapping Up the Proof

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

Theorem. (Completeness Theorem, restated) For every set $\Gamma$ of sentences and every sentence $\phi$, if $\Gamma \vDash \phi$ then $\Gamma \vdash \phi.$

Proof. As in the proof of the Completeness Theorem for propositional logic in Lecture 8, it suffices to show that whenever $\Gamma$ is consistent then it is also satisfiable.

Consider any consistent set $\Gamma$ of sentences over a signature $\sigma.$ Let $\sigma^+$ denote the extension of $\sigma$ obtained by adding a constant symbol $c_{\phi,x_i}$ for each pair $(\phi,x_i)$ where the variable $x_i$ is the only free variable in the formula $\phi$. Define $\Gamma^+ = \Gamma \cup \{ \phi[x_i/c_{\phi,x_i}] : x_i \mbox{ is the only free variable in } \phi \}$ to be the extension of $\Gamma$ over $\sigma^+$. The set $\Gamma^+$ is saturated by construction. And we can obtain a maximally consistent and saturated set $\Gamma' \supseteq \Gamma^+$ by using the same construction and argument as in the proof of Lemma 4 in Lecture 8.

By Lemma 6, the set $\Gamma'$ is satisfiable. Let $M$ be any model of $\Gamma'$. Since $\Gamma^+$ is a subset of $\Gamma'$, then $M$ is also a model of $\Gamma^+$. Define the structure $M^-$ over $\sigma$ to be the restriction of $M$ over this signature. (In other words, we simply ignore the assignments that $M$ assigns to the $c_{\phi,x_i}$ constant symbols added to $\sigma^+$.) This structure satisfies all the sentences in $\Gamma$, so it is also a model of it. Therefore, $\Gamma$ is satisfiable.