Ehrenfeucht–Fraïssé games on finite structures

The graded back-and-forth refinement between two structures (Ehrenfeucht 1961; Ebbinghaus–Flum 1995, ch. 2), and the one lemma the whole inexpressibility toolkit rests on: surviving n rounds implies agreeing on every sentence of quantifier rank at most n (DescriptiveComplexity.realize_efStage), so a property distinguishing two structures the duplicator can play forever is not first-order.

A position (DescriptiveComplexity.PartialIso) is a pair of tuples of equal length, one on each side, satisfying the same equalities between coordinates and the same base relations at every selection of coordinates – agreement on the atomic type (DescriptiveComplexity.atomicAgreeOn) read across two structures. A round appends one element, chosen on either side by the spoiler and answered on the other by the duplicator, and DescriptiveComplexity.efStage L n is the set of positions from which the duplicator survives n of them.

The stages are not an instance of the abstract pebble refinement (DescriptiveComplexity.Invariant.Pebble), although the two chains look alike: there the two tuples live in the same structure and a round replaces one of k fixed pebbles, here they live in two different structures – the spoiler's move is a quantifier over one of them, the duplicator's answer a quantifier over the other – and a round appends a coordinate, so a position is not a point of a fixed relation but of a family indexed by the number of rounds already played. What the two do share is the measure they are graded by, DescriptiveComplexity.qdepth, and the shape of the proof: the atomic case is settled by the position, the quantifier case by one round of the game. The vocabulary is relational, as everywhere in this library, so that atomic formulas read coordinates rather than terms (DescriptiveComplexity.exists_eq_var_of_isRelational).

Positions

def DescriptiveComplexity.PartialIso (L : FirstOrder.Language) {M N : Type} [L.Structure M] [L.Structure N] {j : ℕ} (a : Fin j → M) (b : Fin j → N) : Prop

A legal position of the Ehrenfeucht–Fraïssé game: two tuples of equal length, one on each side, satisfying the same equalities between their coordinates and the same base relations at every selection of coordinates. Equivalently, matching coordinate to coordinate is a partial isomorphism.

This is DescriptiveComplexity.atomicAgreeOn read across two structures, and over the whole vocabulary: unlike the ≡ᵏ layer, which must restrict to the symbols a definition mentions to stay definable, a game plays against one sentence at a time and nothing here has to be defined by a formula.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.PartialIso.symm {L : FirstOrder.Language} {M N : Type} [L.Structure M] [L.Structure N] {j : ℕ} {a : Fin j → M} {b : Fin j → N} (h : PartialIso L a b) : PartialIso L b a

A legal position read from the other side is legal.

The refinement chain

def DescriptiveComplexity.efStage (L : FirstOrder.Language) {M N : Type} [L.Structure M] [L.Structure N] : ℕ → {j : ℕ} → (Fin j → M) → (Fin j → N) → Prop

The stages of the Ehrenfeucht–Fraïssé refinement: efStage L n a b says that from the position (a, b) the duplicator survives n further rounds – the position is legal, and whichever element the spoiler appends on either side, the duplicator can append one on the other and survive n - 1 more rounds.

The chain descends (DescriptiveComplexity.efStage_le), so the stage index is a budget: a position surviving n rounds survives fewer.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.efStage L 0 x✝¹ x✝ = DescriptiveComplexity.PartialIso L x✝¹ x✝

theorem DescriptiveComplexity.efStage.partialIso {L : FirstOrder.Language} {M N : Type} [L.Structure M] [L.Structure N] {j : ℕ} {a : Fin j → M} {b : Fin j → N} {n : ℕ} : efStage L n a b → PartialIso L a b

A position from which the duplicator survives any number of rounds is legal.

theorem DescriptiveComplexity.efStage.forth {L : FirstOrder.Language} {M N : Type} [L.Structure M] [L.Structure N] {n j : ℕ} {a : Fin j → M} {b : Fin j → N} (h : efStage L (n + 1) a b) (c : M) : ∃ (d : N), efStage L n (Fin.snoc a c) (Fin.snoc b d)

The spoiler moves on the left: from a position surviving n + 1 rounds, an element appended on the left is answered on the right.

theorem DescriptiveComplexity.efStage.back {L : FirstOrder.Language} {M N : Type} [L.Structure M] [L.Structure N] {n j : ℕ} {a : Fin j → M} {b : Fin j → N} (h : efStage L (n + 1) a b) (d : N) : ∃ (c : M), efStage L n (Fin.snoc a c) (Fin.snoc b d)

The spoiler moves on the right: from a position surviving n + 1 rounds, an element appended on the right is answered on the left.

theorem DescriptiveComplexity.efStage_succ_le {L : FirstOrder.Language} {M N : Type} [L.Structure M] [L.Structure N] (n : ℕ) {j : ℕ} {a : Fin j → M} {b : Fin j → N} : efStage L (n + 1) a b → efStage L n a b

The refinement chain descends: surviving one more round is a stronger requirement.

theorem DescriptiveComplexity.efStage_le {L : FirstOrder.Language} {M N : Type} [L.Structure M] [L.Structure N] {n j : ℕ} {a : Fin j → M} {b : Fin j → N} {m : ℕ} (hmn : m ≤ n) (h : efStage L n a b) : efStage L m a b

The refinement chain descends, monotonically.

theorem DescriptiveComplexity.efStage.symm {L : FirstOrder.Language} {M N : Type} [L.Structure M] [L.Structure N] {n j : ℕ} {a : Fin j → M} {b : Fin j → N} : efStage L n a b → efStage L n b a

Positions surviving n rounds, read from the other side.

n-round equivalence of structures

def DescriptiveComplexity.EFEquiv (L : FirstOrder.Language) (M N : Type) [L.Structure M] [L.Structure N] (n : ℕ) : Prop

n-round equivalence: the duplicator survives n rounds of the Ehrenfeucht–Fraïssé game on M and N played from the empty position.

Equations

• DescriptiveComplexity.EFEquiv L M N n = DescriptiveComplexity.efStage L n default default

theorem DescriptiveComplexity.EFEquiv.symm {L : FirstOrder.Language} {M N : Type} [L.Structure M] [L.Structure N] {n : ℕ} (h : EFEquiv L M N n) : EFEquiv L N M n

n-round equivalence is symmetric.

theorem DescriptiveComplexity.EFEquiv.mono {L : FirstOrder.Language} {M N : Type} [L.Structure M] [L.Structure N] {n m : ℕ} (hmn : m ≤ n) (h : EFEquiv L M N n) : EFEquiv L M N m

n-round equivalence is antitone in the number of rounds.

The methodology lemma

theorem DescriptiveComplexity.realize_efStage {L : FirstOrder.Language} {M N : Type} [L.Structure M] [L.Structure N] [L.IsRelational] {j : ℕ} (φ : L.BoundedFormula Empty j) {n : ℕ} : qdepth φ ≤ n → ∀ {a : Fin j → M} {b : Fin j → N}, efStage L n a b → (φ.Realize default a ↔ φ.Realize default b)

The Ehrenfeucht–Fraïssé method. A formula whose quantifier rank fits in the duplicator's remaining budget cannot separate the two sides of a position: each quantifier spends one round of the game, and atomic formulas are decided by the position itself.

The free-variable context is empty (Empty): the tuples of the position play the role of the free variables, exactly as the bound variables of Mathlib's FirstOrder.Language.BoundedFormula are read off the valuation tuple.

theorem DescriptiveComplexity.realize_sentence_of_efEquiv {L : FirstOrder.Language} {M N : Type} [L.Structure M] [L.Structure N] {n : ℕ} [L.IsRelational] (h : EFEquiv L M N n) (φ : L.Sentence) (hφ : qdepth φ ≤ n) : M ⊨ φ ↔ N ⊨ φ

The methodology lemma: n-round equivalent structures satisfy the same sentences of quantifier rank at most n. Everything the inexpressibility toolkit proves is a contrapositive of this.