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

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 $n$ is odd, make the same definition but switch the roles of $A$ and $B$, selecting $b’ _ {n+1}$ to be the first element such that…

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 so 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 } 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)$.

@todo, come back to this.

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$, $\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)$

iff

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

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}$ 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}’$ 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 $B \models \varphi (\pmb b \parallel b’)$ by the assumption. By the definition of $\varphi$ we therefore have (@todo)

\[(\mathcal A, \pmb a \parallel a') \equiv_k (\mathcal B, \pmb b \parallel b')\]

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.