202311292011

Tags : Logic

Ehrenfeucht-Fraïssé Game

---

Ehrenfeucht-Fraïssé Games are a nice tool to for describing expressiveness of logics over finite model.

Setup

There are two players, a spoiler and a duplicator. And the board consists of two structure $\mathfrak{A}$ and $\mathfrak{B}$. The goal of the spoiler is to show that the two structures are different, and the goal of the duplicator is to show that the two structures are the same.

Gameplay

In the classic Ehrenfeucht-Fraïssé Game, the players play a certain number of rounds, and each round consists of the following steps.

1. Spoiler picks a structure.
2. Then spoiler makes a move by picking a point in the structure.
3. the duplicator responds to the move by picking a point in the other structure.

An example game is given in Even is not FO-definable for Linear Orders.

Winning

After $n$ rounds of an Ehrenfeucht-Fraïssé Game, we have the move $\vec{a}=(a_1,a_2\dots a_n)$ and $\vec{b}=(b_1,b_2\dots b_n)$. And let $c_1,c_2\dots c_k$ be the set of constants in the language. We define $\overrightarrow{c^{\mathfrak{A}}}=c_1^{\mathfrak{A}}\dots c_k^{\mathfrak{A}}$ and $\overrightarrow{c^{\mathfrak{B}}}=c_1^{\mathfrak{B}}\dots c_k^{\mathfrak{B}}$ is the interpretation of the constants in the two structures $\mathfrak{B}$ and $\mathfrak{A}$.

With that machinery, we say that the spoiler failed to show that the two structures if $((\vec{a},\overrightarrow{c^{\mathfrak{A}}}),(\vec{b},\overrightarrow{c^{\mathfrak{B}}}))$ is a Partial Isomorphism.

And we say $\mathfrak{A}{\equiv }_n\mathfrak{B}$ if duplicator has a winning strategy in an $n$ round game.

---

The Application of Ehrenfeucht-Fraïssé Games is given by the Ehrenfeucht-Fraïssé Theorem which links it to first order logic

---

References

• Even is not FO-definable for Linear Orders
• Quantifier rank
• Ehrenfeucht-Fraïssé Theorem