This note was motivated by questions 1(c) and 1(d) on the first homework assignment for Dan Suciu's special topics class on database theory, offered at Berkeley in Fall 2023.

The Problem

Let $\sigma$ consist only of unary relation symbols (no constants or functions). Let $\phi$ be a $\sigma$-sentence. Show that the satisfiability of $\phi$ is decidable, and that satisfiability coincides with finite satisfiability.

Preliminaries

We assume the reader is familiar with the basics of first-order logic (FO) and model theory. In particular, we assume familiarity with the notions of structure, sentence, satisfiability, finite satisfiability, and decidability. We will briefly cover the Ehrenfeucht-Fraïssé game and theorem here.

Partial Isomorphism

Fix a relational signature $\sigma$ possibly with constants. Let $\mA$ and $\mB$ be $\sigma$-structures. A partial isomorphism between $\mA$ and $\mB$ is a bijection $f : A' \to B'$ between some $A' \subseteq A$ and $B' \subseteq B$ such that:

• if $c^A \in A'$ where $c$ is a constant in $\sigma$, then $f(c^A) = c^B$, and
• $R^A(a_1,\dots,a_n)$ if and only if $R^B(f(a_1),\dots,f(a_n))$, where $R \in \sigma$ is a relation of arity $n$ and $a_i \in A'$.

It is useful to define a partial isomorphism by a pair of vectors $(\vec{a}, \vec{b})$ where $\vec{a} = (a_1,\dots,a_n)$ and $\vec{b} = (b_1,\dots,b_n)$ are vectors of (possibly repeated) elements of $A$ and $B$ respectively. In particular, $(\vec{a}, \vec{b})$ defines a partial isomorphism if and only if:

• if $a_{i} = a_j$ for some $j < i$, then $b_{i} = b_j$, and
• if $a_{i} = c^A$ then $b_{i} = c^B$, and
• $R^A(a_{i_1},\dots,a_{i_n})$ if and only if $R^B(b_{i_1},\dots,b_{i_n})$ where each $i_k \in [n]$.

Quantifier Rank

The quantifier rank of a formula $\phi$ is denoted $\qr(\phi)$ and defined recursively by:

• $\qr(\phi) = 0$ if $\phi$ is atomic,
• $\qr(\phi_1 \land \phi_2) = \qr(\phi_1 \lor \phi_2) = \max(\qr(\phi_1), \qr(\phi_1))$,
• $\qr(\lnot \phi) = \qr(\phi)$,
• $\qr(\exists x.\phi) = \qr(\forall x.\phi) = \qr(\phi) + 1$.

The set of all $\sigma$-sentences of quantifier rank at most $n$ is denoted FO$[n]$.

The Ehrenfeucht-Fraïssé Game

Let $\sigma = (R_1,\dots,R_m, c_1,\dots)$ be a relational signature possibly with constants. Let $\mA$ and $\mB$ be $\sigma$-structures. The Ehrenfeucht-Fraïssé (EF) game $G_n(\mA,\mB)$ is a two-player game played over $n$ rounds. In each round $i \in [n]$, the players (called spoiler and duplicator) do the following:

• the spoiler chooses some $a_i \in A$ or $b_i \in B$,
• the duplicator responds with some $b_i \in B$ or $a_i \in A$ respectively.

The duplicator wins if and only if the vectors $\vec{a} = (a_1,\dots,a_n)$ and $\vec{b} = (b_1,\dots,b_n)$ form a partial isomorphism between $\mA$ and $\mB$. If the duplicator always has a winning strategy for $G_n(\mA,\mB)$, then we write $\mA \equiv_n \mB$.

The remarkable power of EF games is captured by the EF theorem, which allows us to characterize $\equiv_n$ in terms of FO$[n]$.

The proof is too involved to be included here, but can be found in [1].

The Solution

First, note that finite satisfiability implies satisfiability, so it suffices to show the other direction. Let $\sigma = (U_1, \dots, U_m)$ be a relational signature with $m$ unary relation symbols. Let $\phi$ be a $\sigma$-sentence. Our goal is to show the following: if $\mA$ is an infinite $\sigma$-structure such that $\mA \models \phi$, then there exists a finite $\mB$ such that $\mB \models \phi$. Letting $n = \qr(\phi)$, our goal indeed follows from the EF theorem so long as we can show that $\mA \equiv_n \mB$ for some finite $\mB$.

Constructing $\mB$

Before we begin, we need to introduce some notation.

Let $a \in A$ and $d \in I = \{0, 1, \dots, 2^m - 1\}$. Let $d[j]$ denote the $j$th bit of $d$ when written in binary. We can now construct a mapping \[\beta: A \to I,\quad \beta(a) = \sum_{j=1}^m 2^{j-1} \mathbf{1}\{R_j^A(a)\}.\] Equivalently, $\beta(a)[j]$ is 1 if and only if $R_j^A(a)$. Given $d \in I$, we can consider all $a$ such that $\beta(a) = d$. Let \[\gamma: I \to 2^A,\quad \gamma(d) = \{a \in A \mid \beta(a) = d\},\] and let $\kappa(d) = \min(|\gamma(d)|, n)$. Intuitively, $\kappa(d)$ counts the number of times the specific relational membership pattern/bit-string $d$ occurs in $A$, except that we cap the count at $n$.

We can now start piecing together $\mB$. First, we define the domain \[ B = \{(\ell, d) \in \{1, \dots, n\} \times I \mid \ell \leq \kappa(d)\}. \] Then we define $U_j^B$ by $(\ell, d) \in U_j^B$ if and only if $d[j] = 1$. Note that $|B| \leq n 2^m$, and $|R_j^B| \leq |R_j^A|$ for all $j$ (with equality when $|R_j^A| \leq n$). That's it!

Playing the EF game

Let $(\vec{a}, \vec{b}) = ((a_1, \dots, a_{i-1}), (b_1, \dots, b_{i-1}))$ be the (possibly) empty choices made before the $i$th round. Let $L_B: I \to 2^{\{1, \dots, n\}}$ be defined by $L_B(d) = \{\ell \in \{1, \dots, \kappa(d)\} \mid (\ell, d) \in \vec{b}\}$. In other words, $L_B(d)$ is the set of indices $\ell$ such that the pair $(\ell, d)$ has already been chosen in $\vec{b}$. Symmetrically, let $L_A: I \to 2^A$ be defined by $L_A(d) = \{a' \in A \mid \beta(a') = d \text{ and } a' \in \vec{a}\}$.

1. Suppose the spoiler chooses $a_i \in A.$
   1. If $a_i = a_j$ for some $j < i$, then the duplicator chooses $b_i = b_j$.
   2. Otherwise, choose $b_i = (\ell, d)$ where $d = \beta(a_i)$ and $\ell \in \{1, \dots, \kappa(d)\} \setminus L_B(d)$. Note that this is always possible: if $L_B(d) = \{1, \dots, \kappa(d)\}$, then either $i > n$ (impossible) or all $a$ such that $\beta(a) = d$ have already been chosen (which violates the assumption that $a_i \notin \{a_1, \dots, a_{i-1}\}$).
2. Suppose instead the spoiler chooses $b_i \in B$.
   1. If $b_i = b_j$ for some $j < i$, then the duplicator chooses $a_i = a_j$.
   2. Otherwise, let $b_i = (\ell, d) \in B$, and choose $a_i = a \in \gamma(d) \setminus L_A(d)$. Again, this is always possible: if $L_A(d) = \gamma(d)$, then either $i > n$ (impossible) or else all $(\ell', d) \in B$ have already been chosen.

The fact that $(\vec{a}, \vec{b})$ is a partial isomorphism should be clear, as the choice of $a_i$ or $b_i$ is always made to match the corresponding membership pattern chosen by the spoiler. From this it follows that $\mA \equiv_n \mB$.

Wrapping up

We have shown that $\mA \equiv_n \mB$ for some finite $\mB$. By the EF theorem, it follows that $\mA \models \phi$ if and only if $\mB \models \phi$. This means that satisfiability coincides with finite satisfiability.

To show decidability, notice that we can just enumerate all finite $\mB$ (both domain and relations) and check if $\mB \models \phi$. (Checking $\mB \models \phi$ can be done by iterating over all $|B|^n$ assignments of variables in $\phi$ and evaluating the matrix, assuming $\phi$ is in prenex normal form.)

References

[1] Leonid Libkin, Elements of Finite Model Theory, Springer, 2004.