Satisfiability and validity in first-order logic

Satisfiability and validity in first-order logic#

This section contains a proof of Church’s Theorem that satisfiability of first-order logic is undecidable. We assume that you know what a first-order logic sentence is, or that you are willing to read on and look things up elsewhere as needed. A first-order logic sentence $\phi$ is satsifiable if $\phi$ has a model.

Theorem 17

The set $SAT_{FO}$ of sentences of first-order logic which are satisfiable is undecidable. In fact $\overline{K}\leq_m SAT_{FO}$.

Before we start in on the proof we want to outline the overall strategy. We build on the undecidability of tiling. So you will want to recall the (finite pointed) tile sets and also what it means for a tile set to tile the quadrant. We want to construct a computable function taking tile sets to logic sentences with the property that $\mathcal{T}$ can tile the quadrant iff $\varphi(\mathcal{T})$ has a model. If $\mathcal{T}$ can tile the quadrant, then the model of $\varphi(\mathcal{T})$ which we have in mind is the quadrant with the tiling on it. But as with all reductions, we need to be sure that if there is any model of $\varphi(\mathcal{T})$, then there is a tiling of the quadrant with $\mathcal{T}$. This goes via considering the quadrant $N\times N$ as a structure which interprets a simple signature. This is what comes next. The discussion sets aside the tiling at first and just consider the quadrant. After we prove an important lemma about this model, we return to tile sets and tilings of the quadrant.

The quadrant as a model#

Until further notice, our signature $\Sigma$ contains a constant $0$, and two unary function symbols $n$ and $e$, standing for north and east. We have in mind a specific $\Sigma$-structure which we call $\mathcal{Q}$ for quadrant. The points of the quadrant are pairs of natural numbers, so $G = N\times N$. The symbols $n$ and $e$ are interpreted as follows:

\[\begin{split} \begin{array}{lcl} 0 & = & (0,0)\\ n(i,j) & = & (i, j+1)\\ e(i,j) & = & (i+1, j)\\ \end{array} \end{split}\]

This is our intended model.

Axioms for the quadrant#

This material is not needed in the theorem below and so should be deleted.

We next write down four sentences in our signature which are true in the quadrant. Here they are in English and as first-order sentences $\phi_1$, $\ldots$, $\phi_4$:

$n$ and $e$ are one-to-one: $(\forall x)(\forall y) (n(x) = n(y)\to x = y)$, and similarly for $e$.
$n$ and $e$ commute: $(\forall x)(n(e(x)) = e(n(x)))$.
$0$ is not in the image of $n$, and $0$ is not in the image of $e$: $(\forall x)\neg (n(x) = 0)$, and similarly for $e$.
For all $x$, if $x$ is not in the image of $n$, then $e(x)$ also is not in the image of $n$.

Let $\phi_{quad}$ be $\phi_1 \wedge \phi_2 \wedge \phi_3 \wedge \phi_4$.

Exercise 95

Write out $\phi_4$ in first-order logic.

Lemma 13

$\mathcal{G}\models \phi_{quad}$. If $\mathcal{M}$ is any model of $\phi_{quad}$, then the reachable submodel of $\mathcal{M}$ is isomorphic to the quadrant.

Proof. It is clear that $\mathcal{G}\models \phi_{quad}$. We turn to the second assertion.

Let $\mathcal{M}$ satisfy $\phi_{quad}$. Observe that the every point in $M$ of the form $n^i e^j(0)$ belongs to the reachable submodel $\mathcal{M}_{reach}$. Going the other way, we check by induction on a term $t$ without variables that $t$ is of this form for some $i$ and $j$, and (critically) that $i$ and $j$ are unique. For this, note that $0 = n^0 e^0(0)$. If $t$ is the (interpretation of the) term $n^i e^j(0)$, then $n(t)$ is $n^{i+1} e^j(0)$, and $e(t)$ is $n^{i} e^{j+1}(0)$. For the uniqueness part, suppose that $i$, $j$, $k$, and $\ell$ are natural numbers and

\[ n^{i} e^{j}(0) = n^{k} e^{\ell}(0) \]

We show that $i =k$ and $j = \ell$. Since $n$ and $e$ are one-to-one, either $i$ or $k$ is $0$, and similarly for $j$ and $\ell$. There are a few cases at this point. If both $i$ and $k$ are $0$, and also both $j$ and $\ell$ are $0$, then obviously $i =k$ and $j = \ell$. Without loss of generality, we may assume that $i > 0$. If $i > k$, then $n^{i -k} e^j(0) = e^{\ell}(0)$. This means that $e^{\ell}(0)$ is of the form $n(u)$ for some term $u$. So we contradict the fact that $0$ is not in the image of $n$. Similarly, we get a contradiction when $i< k$. We thus have $i = k$. We have $n^{i} e^{j}(0) = n^{i} e^{\ell}(0)$. Since $n$ is one-to-one, we have $e^{j}(0) = e^{\ell}(0)$. Exactly as above we get contradictions when $j > \ell$ and when $j < \ell$. So we have the case $j = \ell$. But then we have the desired conclusion: $i =k$ and $j = \ell$.

Let $f: G \to M$ be

\[ f(i,j) = n^i e^j(0). \]

From what we said above, $f$ is a one-to-one function from the quadrant onto the reachable submodel $\mathcal{M}_{reach}$ of $\mathcal{M}$. It is easy to check that $f$ preserves the interpretations of the function symbols, and thus it is an isomorphism $f: \mathcal{G} \cong \mathcal{M}_{reach}$.

Mapping tile sets to logic sentences#

Let $\mathcal{T}$ be a tile set. Recall that we had a signature $\Sigma$ consisting of $0$, $n$, and $e$. We now add to $\Sigma$ a relation symbol $T$ for each tile $t$ in $\mathcal{T}$.

The heart of the proof of Theorem 17 is to define a computable function $\varphi$ from tile sets to logic sentences in such a way as to have the following condition:

\[ \mbox{For all tile sets $\mathcal{T}$, $\mathcal{T}$ can tile the quadrant iff $\varphi(\mathcal{T})$.} \]

Here is the definition of $\varphi(\mathcal{T})$. Suppose that $\mathcal{T}$ has tiles $t_0$, $t_1$, $\ldots$, $t_m$. Then $\varphi(\mathcal{T})$ is the conjunction of sentences which say

$n$ and $e$ commute: $(\forall x)(n(e(x)) = e(n(x)))$.
Every $x$ gets exactly one tile:

\[ (\forall x)\bigvee_{1\leq i\leq m}\biggl(T_i(x)\wedge \neg\bigvee_{1\leq j\neq i\leq m} T_j(x) \biggr) \]

For all $x$, the tiles on $x$ and $n(x)$ match appropriately (see below).
For all $x$, the tiles on $x$ and $e(x)$ match appropriately (see below).
The tile on $0$ is $t_0$.

Example 4

Let us go back to our very first example of a pointed tile set. Call this tile set $\mathcal{T}$.

Here is point 2 for $\phi(\mathcal{T})$, saying that every point gets a unique tile:

\[\begin{split} \begin{array}{lll} (\forall x) \biggl( & &( T_1(x)\wedge\neg \bigvee_{j\neq 1} T_j(x) ) \\ & \vee & ( T_2(x)\wedge\neg \bigvee_{j\neq 2} T_j(x) ) \\ & \vee & ( T_3(x)\wedge\neg \bigvee_{j\neq 3} T_j(x) )\\ & \vee & ( T_4(x)\wedge\neg \bigvee_{j\neq 4} T_j(x) ) \\ & \vee &( T_5(x)\wedge\neg \bigvee_{j\neq 5} T_j(x) ) \\ & \vee & ( T_6(x)\wedge\neg \bigvee_{j\neq 6} T_j(x) ) \\ & \vee & ( T_7(x)\wedge\neg \bigvee_{j\neq 7} T_j(x) )\\ & \vee & ( T_8(x)\wedge\neg \bigvee_{j\neq 8} T_j(x) ) \biggr) \\ \end{array} \end{split}\]

For points 3, it is convenient to display the tiles:

Let us write them as

$ \begin{array}{@{\qquad}@{\qquad}@{\qquad}c@{\qquad}c@{\qquad}c} & & & t_1 & t_2 & t_3 & t_4 \\ & & & t_5 & t_6 & t_7 & t_8 \end{array} $

Here is how we would state point 3, that for all $x$, the tiles on $x$ and $n(x)$ match:

\[\begin{split} \begin{array}{lll} (\forall x) \biggl( & & T_1(x)\to (T_1(n(x))\vee T_3(n(x))\vee T_4(n(x))) \\ & \wedge & T_2(x)\to T_7(n(x)) \\ & \wedge & T_3(x)\to (T_1(n(x))\vee T_3(n(x))\vee T_4(n(x))) \\ & \wedge &T_4(x)\to (T_1(n(x))\vee T_3(n(x))\vee T_4(n(x))) \\ & \wedge & T_5(x)\to T_7(n(x)) \\ & \wedge & T_6(x)\to (T_6(n(x) \vee T_8(n(x))) \\ & \wedge & T_7(x)\to T_2(n(x)) \\ & \wedge & T_8(x)\to (T_1(n(x))\vee T_3(n(x))\vee T_4(n(x))) \biggr) \\ \end{array} \end{split}\]

Please note that this sentence may be computed from the tile set $\mathcal{T}$ because it only requires “local” information: which tiles can go on top of a given tile. In particular, one need now know whether $\mathcal{T}$ can tile the quadrant in order to construct the sentence above.

Point 5, pertaining to the distinuished tile of $\mathcal{T}$, would be $T_5(0)$.

Exercise 96

What should the disjunction $\bigvee \emptyset$ be in logic?
Suppose we were to add a new tile to our example tile set above with four completely new colors on the sides. Then nothing can go above this new tile, not even itself. Based on your definition of $\bigvee\emptyset$, what will our example sentence be? Is it correct?

Proof of the theorem#

We have defined $\varphi$ just above. We must check that $\mathcal{T}$ can tile the quadrant iff $\varphi(\mathcal{T})$ has a model. One direction is fairly direct: if $\mathcal{T}$ can tile the quadrant, then $\varphi(\mathcal{T})$ has a model. The model has as universe $N\times N$, the interpretations of $0$, $n$, and $e$ are as in the quadrant, and the interpretation of the symbol $T_i$ is the set of pairs $(i,j)$ such that tile $i$ goes on the point $(i,j)\in N\times N$.

In the other direction, suppose that we have any model $\mathcal{M}$ of $\varphi(\mathcal{T})$.
We need to tile the quadrant. Tile the square $(i,j)$ with the unique $t_a\in \mathcal{T}$ such that $T_a(n^j e^i(0))$ in $\mathcal{M}$. There is a unique such $t_a \in \mathcal{T}$ since $\mathcal{M}$ satisfies point 2 in the definition of $\varphi(\mathcal{T})$. We need to see that this tiling is proper. First of all, $0$ in the quadrant is $(0,0)$, and so we tile it with the unique $t_a$ such that $T_a(n^0 e^0(0))$; that is $T_a(0)$. But in this case $t_a$ is the distinguished tile $t^*$, as desired.

Let us check that the tiles on $(i,j)$ and $(i+1,j)$ match on the common edge. (The same kind of work applies to the tiles on $(i,j)$ and $(i,j+1)$, and it is rather easier.) The point is that in the quadrant, $e(i,j) = (i+1,j)$. Let $m$ be the interpretation of the term $n^j e^i(0)$ in $\mathcal{M}$. We claim that $e(m)$ is the interpretation of $n^{j} e^{i+1}(0)$. The reason is that in $\mathcal{M}$, the functions $n$ and $e$ commute. So

\[ e(n^j e^i(0)) = n e(n^{j-1} e^i(0)) = \cdots = n^j e (e^{i}(0)) = n^{j} e^{i+1}(0). \]

It follows that in $\mathcal{M}$, the tiles on $n^j e^i(0)$ and $ n^{j} e^{i+1}(0)$ match appropriately.

By construction, those are the same tiles as on $(i,j)$ and $(i+1,j)$ in the quadrant. So those tiles match.

Two improvements#

Exercise 97

Our proof of Theorem 17 used a function $\varphi$ from tile sets to first-order logic sentences with the property that we want: $\mathcal{T}$ can tile the quadrant iff $\varphi(\mathcal{T})$ has a model. This function has the property that the number of unary relation symbols in $\varphi(\mathcal{T})$ is the same as the number of tiles in $\mathcal{T}$.
Improve our proof of Theorem 17 by changing $\varphi$ so as to use a fixed finite signature $\Sigma$.

[Hint: Take $\Sigma$ to have the symbols $0$, $n$, and $e$ from before, and also a new relation symbol $Tile(x)$, and a new unary function symbol $on$. Instead of coding the quadrant, code the quadrant together with a separate finite set of tiles. The purpose of the function $on$ is to endode that a given tile is on a given square of the quadrant.]

Exercise 98

Here is another strengthening of Theorem 17. There is a fixed signature $\Sigma$ consisting of relation symbols of arity $1$ or $2$ and a function $\varphi$ from tile sets to first-order logic sentences in the language of $\Sigma$ such that for all tile sets $\mathcal{T}$:

$\varphi(\mathcal{T})$ has only three variables.
$\mathcal{T}$ can tile the quadrant iff $\varphi(\mathcal{T})$ has a model.

Validity in first-order logic#

A first-order logic sentence $\phi$ is valid if it is true in all models. This is the same thing as saying that $\neg\phi$ is not satisfiable. So if we let $Val_{FO}$ be the set of valid sentences, then

\[ K \leq_m Val_{FO} \]

Exercise 99

Prove this last fact, given what we have done above.

Naturally, we wish to know about the converse: is $Val_{FO}\leq_m K$? We show that it is, leaning on a very important property of first-order logic. This is that there is a proof system for it. That is there is a definition of a (formal) proof with the following properties:

Formal proofs are finite sequences of logic sentences, and the relation

\[ \mbox{$P$ is a proof of $\phi$} \]

is decidable.

$\phi\in VAL_{FO}$ if and only if for some $P$, $P$ is a proof of $\phi$.

Point 2 is called the Completeness Theorem of first-order logic. It says that a sentence is true in all models if and only if it has a formal proof.

It follows from the two points that the set $VAL_{FO}$ is $\Sigma_1$ and hence computably enumerable. Therefore $Val_{FO}\leq_m K$.

Trakhtentbrot’s Theorem#

The work which we have done so far show that whenever a first-order signature contains a binary relation sybmol, the validty problem is $\Sigma_1$-complete, and the satisfiabililty problem is $\Pi_1$-complete. We might ask about the finite versions of these. That is, we study the problem of whether a logic sentence has a finite model. The results here shows that this problem is $\Sigma_1$-complete.

Exercise 100

Use Exercise to show that the problem of determining whether a first-order logic sentence has a finite model is undecidable.

[Hint: you will not be able to use the functions $n$ and $e$ as we did above. This is due to the fact that in a finite rectangle it is not entirely clear what to do about those functions on the north and east edges of a rectangle. So you will need to fix this, either by making a decision on how to define $n$ and $e$ on the edges, or else by moving from functions to relations. Either way, there are a fair amount of details to work out and check in this problem.]