Finite Model Theory/FO EFM

The method for employing Ehrenfeucht-Fraisse-Games for (in-)expressibility-proofs is given by the following:

Theorem

Let P be a property of finite σ-structures. Then the following are equivalent

• P is not expressible in FO
• for every k ${\displaystyle \in \mathbb {N} }$ there exist two finite σ-structures ${\displaystyle {\mathfrak {A}}_{k}}$ and ${\displaystyle {\mathfrak {B}}_{k}}$, such that the following are both satisfied
• ${\displaystyle {\mathfrak {A}}_{k}\equiv _{k}{\mathfrak {B}}_{k}}$
• ${\displaystyle {\mathfrak {A}}_{k}}$ has P and ${\displaystyle {\mathfrak {B}}_{k}}$ does not have P

Remarks

• Thus using the EFM works roughly as follows:
• choose a k
• construct two structures - one with the property, one without - that are big enough s.t. the duplicator wins the k-ary EFG
• show that this can be expanded with k
• So, a non-expressible property (i.e. the effort to check it) must be somehow 'expandable' with k

Examples

• To begin pick two linear orders say A ={1, 2, 3, 4} and B ={1, 2, 3, 4, 5}. For a two-move Ehrenfeucht game D is to win, obviously. This gives us two structures that satisfy the above conditions for k = 2 and the Property having even cardinality (that A has and B doesn't). Now we have to expand this over all k ${\displaystyle \in \mathbb {N} }$. From the above example we adopt that in a linear order of cardinality ${\displaystyle 2^{k}}$ or higher D has a winning strategy. Thus we choose the cardinalities depending on k as |A| = ${\displaystyle 2^{k}}$ and |B| = ${\displaystyle 2^{k}}$+1. So we have found an even A and an odd B for every k, where D has a winning strategy. Thus (by the corollary) having even/odd cardinality is a property that can not be expressed in FO for finite σ-structures of linear order.