Ehrenfeucht–Fraïssé games and finite-rank elementary equivalence

[UPSTREAM] candidate. Two structures are n-equivalent when they satisfy the same sentences of quantifier rank ≤ n, and elementarily equivalent when they are n-equivalent for every n. Duplicator wins the k-round Ehrenfeucht–Fraïssé game from a pair of tuples when she can answer every move for k rounds, back and forth, keeping the tuples alike. Such tuples satisfy the same formulas of quantifier rank ≤ k, and over a finite relational signature the converse holds, witnessed by Hintikka formulas. This is the rank-bounded counterpart of mathlib's IsExtensionPair.

Main definitions

• FirstOrder.Language.ElementarilyEquivalentUpTo: n-equivalence of structures.
• FirstOrder.Language.FODefinable: definability of a class of structures within a class.
• FirstOrder.Language.DuplicatorWins: duplicator wins the k-round game from a pair of tuples.
• FirstOrder.Language.hintikka: the rank-k Hintikka formula of a tuple.

Main results

• FirstOrder.Language.not_foDefinable_of_elementarilyEquivalentUpTo: the Ehrenfeucht–Fraïssé method for undefinability.
• FirstOrder.Language.DuplicatorWins.realize_iff: a winning position agrees on formulas of quantifier rank ≤ k.
• FirstOrder.Language.duplicatorWins_iff_realize_iff, FirstOrder.Language.elementarilyEquivalentUpTo_iff_duplicatorWins: the converse over a finite relational signature.
• FirstOrder.Language.foDefinable_iff_exists_elementarilyEquivalentUpTo: over a finite relational signature, a class is definable within K iff it is closed under n-equivalence within K for some n.

Implementation notes

Tuples are the bound variables of L.BoundedFormula Empty n, so the Fin.snoc in realize_all is a round of the game and sentences are the case n = 0. As in Hodges's back-and-forth systems, the atomic condition holds at every rank; Libkin states it at rank 0 only, which agrees on nonempty structures (duplicatorWins_succ_iff) but makes soundness fail on empty ones.

References

• [Lib04]
• [Hod93]

n-equivalence and definability

def FirstOrder.Language.ElementarilyEquivalentUpTo (L : Language) (n : ℕ) (M : Type w) (N : Type w') [L.Structure M] [L.Structure N] : Prop

Two structures are elementarily equivalent up to n, or n-equivalent, when they satisfy the same sentences of quantifier rank ≤ n.

Equations

• L.ElementarilyEquivalentUpTo n M N = ∀ (φ : L.Sentence), FirstOrder.Language.BoundedFormula.qr φ ≤ n → (M ⊨ φ ↔ N ⊨ φ)

def FirstOrder.«term_≅[_,_]_» : Lean.TrailingParserDescr

Two structures are elementarily equivalent up to n, or n-equivalent, when they satisfy the same sentences of quantifier rank ≤ n.

Equations

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

def FirstOrder.Language.FODefinable (L : Language) (K P : Set (CategoryTheory.Bundled L.Structure)) : Prop

A class P of structures is first-order definable within K when some sentence holds of exactly the members of P among the structures in K.

Equations

• L.FODefinable K P = ∃ (φ : L.Sentence), ∀ M ∈ K, M ∈ P ↔ ↑M ⊨ φ

theorem FirstOrder.Language.ElementarilyEquivalentUpTo.refl (L : Language) (n : ℕ) (M : Type w) [L.Structure M] : L.ElementarilyEquivalentUpTo n M M

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

theorem FirstOrder.Language.ElementarilyEquivalentUpTo.trans {L : Language} {M : Type w} {N : Type w'} {P : Type w''} [L.Structure M] [L.Structure N] [L.Structure P] {n : ℕ} (h₁ : L.ElementarilyEquivalentUpTo n M N) (h₂ : L.ElementarilyEquivalentUpTo n N P) : L.ElementarilyEquivalentUpTo n M P

theorem FirstOrder.Language.ElementarilyEquivalentUpTo.mono {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {k n : ℕ} (hkn : k ≤ n) (h : L.ElementarilyEquivalentUpTo n M N) : L.ElementarilyEquivalentUpTo k M N

theorem FirstOrder.Language.elementarilyEquivalent_iff_forall_elementarilyEquivalentUpTo {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] : L.ElementarilyEquivalent M N ↔ ∀ (n : ℕ), L.ElementarilyEquivalentUpTo n M N

ElementarilyEquivalent is n-equivalence at every rank.

theorem FirstOrder.Language.not_foDefinable_of_elementarilyEquivalentUpTo {L : Language} {K P : Set (CategoryTheory.Bundled L.Structure)} (h : ∀ (n : ℕ), ∃ M ∈ K, ∃ N ∈ K, L.ElementarilyEquivalentUpTo n ↑M ↑N ∧ M ∈ P ∧ N ∉ P) : ¬L.FODefinable K P

The Ehrenfeucht–Fraïssé method. If for every rank n some structure in K with property P is n-equivalent to one in K without it, then P is not definable within K, since a defining sentence would be fooled at its own quantifier rank.

The Ehrenfeucht–Fraïssé game

def FirstOrder.Language.DuplicatorWins (L : Language) {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] : ℕ → {n : ℕ} → (Fin n → M) → (Fin n → N) → Prop

Duplicator wins the k-round Ehrenfeucht–Fraïssé game from an n-tuple v of M and an n-tuple w of N when the tuples satisfy the same atomic formulas and, with k + 1 rounds left, every element of either structure (forth, back) has an answer in the other extending them to a position she wins with k rounds left.

Equations

• One or more equations did not get rendered due to their size.
• L.DuplicatorWins 0 x✝¹ x✝ = ∀ (φ : L.BoundedFormula Empty x✝²), φ.IsAtomic → (φ.Realize default x✝¹ ↔ φ.Realize default x✝)

theorem FirstOrder.Language.DuplicatorWins.zero {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {k n : ℕ} {v : Fin n → M} {w : Fin n → N} : L.DuplicatorWins k v w → L.DuplicatorWins 0 v w

theorem FirstOrder.Language.DuplicatorWins.realize_iff_of_isAtomic {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {k n : ℕ} {v : Fin n → M} {w : Fin n → N} (h : L.DuplicatorWins k v w) {φ : L.BoundedFormula Empty n} (hφ : φ.IsAtomic) : φ.Realize default v ↔ φ.Realize default w

theorem FirstOrder.Language.DuplicatorWins.forth {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {k n : ℕ} {v : Fin n → M} {w : Fin n → N} (h : L.DuplicatorWins (k + 1) v w) (a : M) : ∃ (b : N), L.DuplicatorWins k (Fin.snoc v a) (Fin.snoc w b)

theorem FirstOrder.Language.DuplicatorWins.back {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {k n : ℕ} {v : Fin n → M} {w : Fin n → N} (h : L.DuplicatorWins (k + 1) v w) (b : N) : ∃ (a : M), L.DuplicatorWins k (Fin.snoc v a) (Fin.snoc w b)

theorem FirstOrder.Language.DuplicatorWins.of_succ {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {k n : ℕ} {v : Fin n → M} {w : Fin n → N} : L.DuplicatorWins (k + 1) v w → L.DuplicatorWins k v w

theorem FirstOrder.Language.DuplicatorWins.antitone {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {n : ℕ} (v : Fin n → M) (w : Fin n → N) : Antitone fun (x : ℕ) => L.DuplicatorWins x v w

theorem FirstOrder.Language.DuplicatorWins.mono {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {k l n : ℕ} {v : Fin n → M} {w : Fin n → N} (hkl : k ≤ l) (h : L.DuplicatorWins l v w) : L.DuplicatorWins k v w

theorem FirstOrder.Language.DuplicatorWins.realize_iff {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {n : ℕ} {φ : L.BoundedFormula Empty n} {k : ℕ} {v : Fin n → M} {w : Fin n → N} : L.DuplicatorWins k v w → φ.qr ≤ k → (φ.Realize default v ↔ φ.Realize default w)

Tuples from which duplicator wins k rounds satisfy the same formulas of quantifier rank ≤ k. Atomic formulas agree by the atomic condition, and quantified ones by the back and forth moves.

theorem FirstOrder.Language.DuplicatorWins.elementarilyEquivalentUpTo {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {k : ℕ} (h : L.DuplicatorWins k default default) : L.ElementarilyEquivalentUpTo k M N

On the empty tuples, the rank-k relation gives k-equivalence.

theorem FirstOrder.Language.DuplicatorWins.symm {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {k n : ℕ} {v : Fin n → M} {w : Fin n → N} : L.DuplicatorWins k v w → L.DuplicatorWins k w v

theorem FirstOrder.Language.DuplicatorWins.trans {L : Language} {M : Type w} {N : Type w'} {P : Type w''} [L.Structure M] [L.Structure N] [L.Structure P] {k n : ℕ} {u : Fin n → M} {v : Fin n → N} {w : Fin n → P} : L.DuplicatorWins k u v → L.DuplicatorWins k v w → L.DuplicatorWins k u w

theorem FirstOrder.Language.Equiv.duplicatorWins {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] (f : L.Equiv M N) (k : ℕ) {n : ℕ} (v : Fin n → M) : L.DuplicatorWins k v (⇑f ∘ v)

An isomorphism is a winning strategy at every rank, answering a by f a and b by f.symm b.

theorem FirstOrder.Language.DuplicatorWins.refl {L : Language} {M : Type w} [L.Structure M] {n : ℕ} (k : ℕ) (v : Fin n → M) : L.DuplicatorWins k v v

theorem FirstOrder.Language.duplicatorWins_succ_iff {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {k n : ℕ} {v : Fin n → M} {w : Fin n → N} [Nonempty M] : L.DuplicatorWins (k + 1) v w ↔ (∀ (a : M), ∃ (b : N), L.DuplicatorWins k (Fin.snoc v a) (Fin.snoc w b)) ∧ ∀ (b : N), ∃ (a : M), L.DuplicatorWins k (Fin.snoc v a) (Fin.snoc w b)

On a nonempty structure the atomic condition at rank k + 1 follows from forth, so the relation is [Lib04]'s ≃ₖ₊₁ (p. 36) and [Hod93] Lemma 3.3.1.

Hintikka formulas and completeness

@[reducible, inline]

abbrev FirstOrder.Language.AtomIndex (L : Language) (n : ℕ) : Type v

AtomIndex n indexes the atomic formulas in n bound variables of a relational language, the equalities of two variables and the relation symbols applied to variables.

Equations

• L.AtomIndex n = (Fin n × Fin n ⊕ (R : (l : ℕ) × L.Relations l) × (Fin R.fst → Fin n))

def FirstOrder.Language.atom (L : Language) {n : ℕ} : L.AtomIndex n → L.BoundedFormula Empty n

The atomic formula with the given index.

Equations

• L.atom (Sum.inl (i, j)) = ((FirstOrder.Language.var ∘ Sum.inr) i).bdEqual ((FirstOrder.Language.var ∘ Sum.inr) j)
• L.atom (Sum.inr ⟨⟨fst, R⟩, f⟩) = R.boundedFormula fun (i : Fin fst) => (FirstOrder.Language.var ∘ Sum.inr) (f i)

instance FirstOrder.Language.instFiniteSigmaNatRelationsOfSymbols_linglib (L : Language) [Finite L.Symbols] : Finite ((l : ℕ) × L.Relations l)

theorem FirstOrder.Language.atom_isAtomic {L : Language} {n : ℕ} (i : L.AtomIndex n) : (L.atom i).IsAtomic

theorem FirstOrder.Language.BoundedFormula.IsAtomic.exists_eq_atom {L : Language} {n : ℕ} [L.IsRelational] {φ : L.BoundedFormula Empty n} (hφ : φ.IsAtomic) : ∃ (i : L.AtomIndex n), φ = L.atom i

In a relational language every atomic formula on bound variables is an atom.

noncomputable def FirstOrder.Language.atomicType (L : Language) {M : Type w} [L.Structure M] {n : ℕ} [Finite L.Symbols] (v : Fin n → M) : L.BoundedFormula Empty n

The atomic type of a tuple is the conjunction of the atoms it satisfies and the negations of the others.

Equations

• L.atomicType v = FirstOrder.Language.BoundedFormula.iInf fun (i : L.AtomIndex n) => if (L.atom i).Realize default v then L.atom i else (L.atom i).not

@[irreducible]

noncomputable def FirstOrder.Language.hintikkaSet (L : Language) [Finite L.Symbols] (k n : ℕ) : Finset (L.BoundedFormula Empty n)

hintikkaSet k n is the finite set of game-normal formulas of rank k in n variables. At rank 0 they are the atomic types. At rank k + 1 each joins an atomic type to a set X of rank-k formulas in n + 1 variables, saying that each member of X is realized by some extension and every extension realizes some member of X.

Equations

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

noncomputable def FirstOrder.Language.hintikka (L : Language) {M : Type w} [L.Structure M] [Finite L.Symbols] (k : ℕ) {n : ℕ} : (Fin n → M) → L.BoundedFormula Empty n

The rank-k Hintikka formula of v is the game-normal formula of rank k it satisfies.

Equations

• One or more equations did not get rendered due to their size.
• L.hintikka 0 x✝ = L.atomicType x✝

theorem FirstOrder.Language.realize_atomicType_iff {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {n : ℕ} [Finite L.Symbols] [L.IsRelational] (v : Fin n → M) (w : Fin n → N) : (L.atomicType v).Realize default w ↔ L.DuplicatorWins 0 v w

theorem FirstOrder.Language.qr_atomicType {L : Language} {M : Type w} [L.Structure M] {n : ℕ} [Finite L.Symbols] (v : Fin n → M) : (L.atomicType v).qr = 0

theorem FirstOrder.Language.qr_le_of_mem_hintikkaSet {L : Language} [Finite L.Symbols] {k n : ℕ} {θ : L.BoundedFormula Empty n} : θ ∈ L.hintikkaSet k n → θ.qr ≤ k

theorem FirstOrder.Language.hintikka_mem {L : Language} {M : Type w} [L.Structure M] [Finite L.Symbols] (k : ℕ) {n : ℕ} (v : Fin n → M) : L.hintikka k v ∈ L.hintikkaSet k n

theorem FirstOrder.Language.qr_hintikka_le {L : Language} {M : Type w} [L.Structure M] {n : ℕ} [Finite L.Symbols] (k : ℕ) (v : Fin n → M) : (L.hintikka k v).qr ≤ k

theorem FirstOrder.Language.eq_hintikka_of_realize {L : Language} {M : Type w} [L.Structure M] [Finite L.Symbols] {k n : ℕ} {θ : L.BoundedFormula Empty n} (u : Fin n → M) : θ ∈ L.hintikkaSet k n → θ.Realize default u → θ = L.hintikka k u

A tuple satisfies exactly one game-normal formula of each rank ([Hod93] Theorem 3.3.2 (a)), so any member of hintikkaSet k n it satisfies is its Hintikka formula.

theorem FirstOrder.Language.realize_hintikka_self {L : Language} {M : Type w} [L.Structure M] [Finite L.Symbols] [L.IsRelational] (k : ℕ) {n : ℕ} (v : Fin n → M) : (L.hintikka k v).Realize default v

theorem FirstOrder.Language.realize_hintikka_iff {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [Finite L.Symbols] [L.IsRelational] {k n : ℕ} (v : Fin n → M) (w : Fin n → N) : (L.hintikka k v).Realize default w ↔ L.DuplicatorWins k v w

The Hintikka formula of v holds of w iff duplicator wins k rounds from the tuples ([Hod93] Theorem 3.3.2 (b)).

theorem FirstOrder.Language.duplicatorWins_iff_realize_iff {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {k n : ℕ} [Finite L.Symbols] [L.IsRelational] (v : Fin n → M) (w : Fin n → N) : L.DuplicatorWins k v w ↔ ∀ (φ : L.BoundedFormula Empty n), φ.qr ≤ k → (φ.Realize default v ↔ φ.Realize default w)

Over a finite relational signature, duplicator wins k rounds from two tuples iff they satisfy the same formulas of quantifier rank ≤ k ([Lib04] Theorem 3.18).

theorem FirstOrder.Language.elementarilyEquivalentUpTo_iff_duplicatorWins {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {k : ℕ} [Finite L.Symbols] [L.IsRelational] : L.ElementarilyEquivalentUpTo k M N ↔ L.DuplicatorWins k default default

theorem FirstOrder.Language.foDefinable_iff_exists_elementarilyEquivalentUpTo {L : Language} [Finite L.Symbols] [L.IsRelational] {K P : Set (CategoryTheory.Bundled L.Structure)} : L.FODefinable K P ↔ ∃ (k : ℕ), ∀ M ∈ K, ∀ N ∈ K, L.ElementarilyEquivalentUpTo k ↑M ↑N → M ∈ P → N ∈ P

Over a finite relational signature, a class is first-order definable within K iff, for some k, it is closed under k-equivalence within K ([Lib04] Corollary 3.17). The defining sentence is the disjunction of the rank-k Hintikka sentences of its members.