Notes - Logic and Proof MT24, Ehrenfeucht-Fraïssé games

Overall idea: Build up two enumerations of the orderings which have the desired properties, switching between making one enumeration and then the other. Since the ordering is unbounded and dense, we always have “enough” elements that we can match up elements from each of the orderings.

Let

\[\begin{aligned} &a _ 1, a _ 2, a _ 3, \ldots \\\\ &b _ 1, b _ 2, b _ 3, \ldots \end{aligned}\]

are two enumerations of the elements of $A$ and $B$ without repetitions. We aim to find two new enumerations

\[\begin{aligned} &a' _ 1, a' _ 2, a' _ 3, \ldots \\\\ &b' _ 1, b' _ 2, b' _ 3, \ldots \end{aligned}\]

such that for any pair of indices $i$ and $j$,

\[a _ i' < a _ j' \iff b _ i' < b _ j'\]

Then the bijection can be defined by $f(a _ i’) = b _ i’$ for each $i$.

To do this, define $a _ i’$ and $b _ i’$ by strong induction.

Suppose we have defined

\[\begin{aligned} &a' _ 1, a' _ 2, \ldots, a' _ n \\\\ &b' _ 1, b' _ 2, \ldots, b' _ n \end{aligned}\]

We consider two cases.

If $n$ is even, define $a’ _ {n+1}$ to be the first element of the original enumeration $a _ 1, a _ 2, \ldots$ that does not appear among $a _ 1’, \ldots, a _ n’$. Then define $b’ _ {n+1}$ such that $a _ i’ < a’ _ {n+1}$ if and only if $b _ i’ < b’ _ {n+1}$ for $1 \le i \le n$. This is possible because $(B, <)$ is a dense linear order: if there exists some $j$ such that $a _ i’ < a _ {n+1}’ < a _ j’$, then by density, there must be a corresponding $b’ _ {n+1}$ between $b _ i’$ and $b _ j’$. If there is no such $a _ i’$ and $b _ j’$, then we can take $b _ {n+1}’$ to be very big or small, using the fact that the ordering is unbounded.

If $n$ is odd, make the same definition but switch the roles of $A$ and $B$.

Proceeding this way, we obtain the new enumeration with the desired properties, and then can define $f$ as necessary.

The definition is by induction on $k$.

• $k = 0$: $(\mathcal A, \pmb a) \sim _ 0 (\mathcal B, \pmb b)$ iff for any atomic $\sigma$-formula $\varphi$ with free variables among $x _ 1, \ldots, x _ m$, $\mathcal A \models \varphi(\pmb a)$ iff $\mathcal B \models \varphi (\pmb b)$.
• $k > 0$: $(\mathcal A, \pmb a) \sim _ {k+1} (\mathcal B, \pmb b)$ iff:
  • for all $a’ \in A$, there exists $b’ \in B$ such that $(\mathcal A, \pmb a \parallel a’) \sim _ k (\mathcal B, \pmb b \parallel b’)$, and
  • for all $b’ \in B$, there exists $a’ \in A$ such that $(\mathcal A, \pmb a \parallel a’) \sim _ k (\mathcal B, \pmb b \parallel b’)$.

It is a game between two players:

• Spoiler, who aims to show that $\mathcal A$ and $\mathcal B$ are different
• Duplicator, who aims to show that $\mathcal A$ and $\mathcal B$ are not that different

The game consists of $k$ rounds. In each round $1 \le i \le k$, Spoiler picks an element $a \in A$ or $b \in B$ and Duplicator responds with an element of the other structure.

After $k$ rounds, this produces tuples $\pmb a’ \in A^k$ and $\pmb b’ \in B^k$ of elements chosen by each player.

Duplicator wins if for all atomic formulas $\varphi(x _ 1, \ldots, x _ {m+k})$,

\[\mathcal A \models \varphi(\pmb a \parallel \pmb a') \text{ iff } \mathcal B \models \varphi(\pmb b \parallel \pmb b')\]

A function that takes a configuration of the game $\big((\mathcal A, \pmb a), (\mathcal B, \pmb b)\big)$ and a move of Spoiler, and outputs a response.

• $(\mathcal A, \pmb a) \sim _ k (\mathcal B, \pmb b)$

iff

• Duplicator has a winning strategy in $G _ k\big((\mathcal A, \pmb a), (\mathcal B, b)\big)$.

This follows straightforwardly from the definitions. Recall that $(\mathcal A, \pmb a) \sim _ k (\mathcal B, \pmb b)$ is defined inductively via:

• $k = 0$: $(\mathcal A, \pmb a) \sim _ 0 (\mathcal B, \pmb b)$ iff for any atomic $\sigma$-formula $\varphi$ with free variables among $x _ 1, \ldots, x _ m$, $\mathcal A \models \varphi(\pmb a)$ iff $\mathcal B \models \varphi (\pmb b)$.
• $k > 0$: $(\mathcal A, \pmb a) \sim _ {k+1} (\mathcal B, \pmb b)$ iff:
  • for all $a’ \in A$, there exists $b’ \in B$ such that $(\mathcal A, \pmb a \parallel a’) \sim _ k (\mathcal B, \pmb b \parallel b’)$, and
  • for all $b’ \in B$, there exists $a’ \in A$ such that $(\mathcal A, \pmb a \parallel a’) \sim _ k (\mathcal B, \pmb b \parallel b’)$.

The characterisations are equivalent when $k = 0$. Then note:

• Duplicator has a winning strategy in $G _ {k+1}((\mathcal A, \pmb a), (\mathcal B, \pmb b))$, iff
• For every move of Spoiler, Duplicator has a winning strategy in $G _ {k}((\mathcal A, \pmb a), (\mathcal B, \pmb b))$, iff
• $(\mathcal A, \pmb a) \sim _ {k+1} (\mathcal B, \pmb b)$

The set of $\sigma$-formulas in free variables $x _ 1, \ldots, x _ m$ that have maximum quantifier depth $k$.

Induct on the quantifier depth $k$.

Base case: $k = 0$. In this case, every formula in $\text{FO} _ {k, m}^\sigma$ is a boolean combination of atomic formulas in the free variables $x _ 1, \ldots, x _ m$, of which there are only finitely many.

Inductive step: $k > 0$.

Note that every formula in $\text{FO} _ {k+1, m}^\sigma$ is a boolean combination of formulas of the form

\[\exists x _ {m+1} \varphi\]

where $\varphi \in \text{FO} _ {k, m+1}^\sigma$. But then by the induction hypothesis, there are only finitely many choices of $\varphi$ up to logical equivalence.

Since $\varphi \equiv \varphi$ implies $\exists x _ {m+1} \varphi \equiv \exists x _ {m+1} \varphi’$, the result follows.

For all formulas $\varphi \in \text{FO} _ {k, m}^\sigma$ (first-order formulas of depth $k$ with $m$ free variables), $\mathcal A \models \varphi(\pmb a)$ iff $\mathcal B \models \varphi(\pmb b)$.

Suppose:

• $\sigma$ is a signature
• $\mathcal A$ is a $\sigma$-structure
• $\mathcal B$ is a $\sigma$-structure
• $\pmb a, \pmb b$ are $m$-tuples
• $k, m \in \mathbb N _ {\ge 0}$

Then:

• $(\mathcal A, \pmb a) \equiv _ k (\mathcal B, \pmb b)$ (agree on all first-order formulas with quantifier depth $k$)

iff

• $(\mathcal A, \pmb a) \sim _ k (\mathcal B, \pmb b)$ (“inductively similar”, equivalent to Duplicator having a winning strategy in corresponding Ehrenfeucht-Fraïssé game).

Recall the definitions:

$(\mathcal A, \pmb a) \equiv _ k (\mathcal B, \pmb b)$ means that for all formulas $\varphi \in \text{FO} _ {k, m}^\sigma$, $\mathcal A \models \varphi(\pmb a)$ iff $\mathcal B \models \varphi(\pmb b)$.

and

$(\mathcal A, \pmb a) \sim _ k (\mathcal B, \pmb b)$ is defined inductively, like so:

• $k = 0$: $(\mathcal A, \pmb a) \sim _ 0 (\mathcal B, \pmb b)$ iff for any atomic $\sigma$-formula $\varphi$ with free variables among $x _ 1, \ldots, x _ m$, $\mathcal A \models \varphi(\pmb a)$ iff $\mathcal B \models \varphi (\pmb b)$.
• $k > 0$: $(\mathcal A, \pmb a) \sim _ {k+1} (\mathcal B, \pmb b)$ iff:
  • for all $a’ \in A$, there exists $b’ \in B$ such that $(\mathcal A, \pmb a \parallel a’) \sim _ k (\mathcal B, \pmb b \parallel b’)$, and
  • for all $b’ \in B$, there exists $a’ \in A$ such that $(\mathcal A, \pmb a \parallel a’) \sim _ k (\mathcal B, \pmb b \parallel b’)$.

We proceed by induction on $k$.

Base case $k = 0$: This is trivial, since $\sim _ 0$ and $\equiv _ 0$ have the same definition.

Inductive step $k > 0$:

For the forward direction, suppose that

\[(\mathcal A, \pmb a) \equiv _ {k+1} (\mathcal B, \pmb b)\]

we aim to show that

\[(\mathcal A, \pmb a) \sim _ {k+1} (\mathcal B, \pmb b)\]

To do this, pick some $a’ \in A$. The definition requires us to find some $b’ \in B$ such that

\[(\mathcal A, \pmb a \parallel a') \sim _ k (\mathcal B, \pmb b \parallel b')\]

Let

• $\psi _ 1, \psi _ 2, \ldots, \psi _ {\ell _ 1} \in \text{FO}^\sigma _ {k, m+1}$ be an enumeration of all formulas up to logical equivalence that are satisfied by $(\mathcal A, \pmb a \parallel a’)$
• $\psi _ 1’, \psi _ 2’, \ldots, \psi _ {\ell _ 2}’ \in \text{FO}^\sigma _ {k, m+1}$ be an enumeration of all formulas up to logical equivalence that are not satisfied by $(\mathcal A, \pmb a \parallel a’)$.

Define

\[\varphi := \bigwedge^{\ell _ 1} _ {i = 1} \psi _ i \land \bigwedge^{\ell _ 2} _ {i = 1} \lnot \psi _ i'\]

Then $\mathcal A \models (\exists x _ {m+1} \varphi)(\pmb a)$ (just take $x _ {m+1}$ to be $a’$). Since $(\exists x _ {m+1} \varphi) \in \text{FO} _ {k+1, m}$, we have that $\mathcal B \models \varphi (\pmb b \parallel b’)$ by the assumption. By the definition of $\varphi$ we therefore have

\[(\mathcal A, \pmb a \parallel a') \equiv _ k (\mathcal B, \pmb b \parallel b')\]

since otherwise $\mathcal A$ and $\mathcal B$ would disagree on one of the conjuncts in $\varphi$. But then by the inductive hypothesis,

\[(\mathcal A, \pmb a \parallel a') \sim _ k (\mathcal B, \pmb b \parallel b')\]

and thus

\[(\mathcal A, \pmb a) \sim _ {k+1} (\mathcal B, \pmb b)\]

as required. The definition of $\sim _ {k+1}$ also requires we show that for all $b’ \in B$ there exists $a’ \in A$ with $(\mathcal A, \pmb a \parallel a’) \sim _ k (\mathcal B, \pmb b \parallel b’)$, but this is immediate since the above argument is symmetric.

For the backward direction, suppose that

\[(\mathcal A, \pmb a) \sim _ {k+1} (\mathcal B, \pmb b)\]

and we aim to show that

\[(\mathcal A, \pmb a) \equiv _ {k+1} (\mathcal B, \pmb b)\]

Consider some formula $(\exists x _ {m+1} \varphi) \in \text{FO} _ {k+1, m}^\sigma$, and suppose that

\[\mathcal A \models (\exists x _ {m+1} \varphi)(\pmb a)\]

Then there exists $a’ \in A$ such that

\[\mathcal A \models \varphi(\pmb a \parallel a')\]

Since by assumption $(\mathcal A, \pmb a) \sim _ {k+1} (\mathcal B, \pmb b)$, there exists $b’$ such that

\[(\mathcal A, \pmb a \parallel a') \sim _ k (\mathcal B, \pmb b \parallel b')\]

By the inductive hypothesis, it follows that

\[(\mathcal A, \pmb a \parallel a') \equiv _ k (\mathcal B, \pmb b \parallel b')\]

which implies that

\[\mathcal B \models \varphi(\pmb b \parallel b')\]

Hence $B \models (\exists x _ {m+1} \varphi)(\pmb b)$. Since every formula in $\text{FO} _ {k+1,m}^\sigma$ is a boolean combination of formulas $\exists x _ {m+1} \varphi$ for $\varphi \in \text{FO} _ {k, m+1}^\sigma$, we conclude that $(\mathcal A, \pmb a) \equiv _ {k+1} (\mathcal B, \pmb b)$. The definition of $\equiv _ {k+1}$ also requires us to show that $\mathcal B \models \varphi(\pmb b)$ implies $\mathcal A \models \varphi(\pmb a)$, but again this is immediate from symmetry.