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]$.

(Ehrenfeucht-Fraïssé)

Let $\mA$ and $\mB$ be $\sigma$-structures. Then $\mA \equiv_n \mB$ if and only if $\mA$ and $\mB$ agree on all FO$[n]$-sentences.

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}\}$.

- Suppose the spoiler chooses $a_i \in A.$
- If $a_i = a_j$ for some $j < i$, then the duplicator chooses $b_i = b_j$.
- 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}\}$).

- Suppose instead the spoiler chooses $b_i \in B$.
- If $b_i = b_j$ for some $j < i$, then the duplicator chooses $a_i = a_j$.
- 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.