Hintikka formulas and the Ehrenfeucht–Fraïssé theorem

For a language with finitely many relation symbols, the rank-n type of a k-tuple is finite combinatorial data (Cslib.Logic.FO.RankType): its atomic diagram and, if n > 0, the set of rank-(n - 1) types of its one-point extensions. Two tuples have the same rank-n type exactly when Duplicator wins the n-round Ehrenfeucht–Fraïssé game between them (rankType_eq_iff), and every rank-n type is defined by a Hintikka formula of quantifier rank at most n (realize_hintikka, quantifierRank_hintikka_le). Together with the easy direction DuplicatorWins.realize_iff, this gives the Ehrenfeucht–Fraïssé theorem: for a relational language with finitely many relation symbols, Duplicator wins the n-round game from (a, b) exactly when a and b satisfy the same formulas of quantifier rank at most n.

The hypothesis [Finite (Σ l, L.Relations l)] (finitely many relation symbols of all arities) is used only by the Hintikka direction duplicatorWins_of_forall_realize_iff, which does not need L.IsRelational; the easy direction needs L.IsRelational and no finiteness. The structures themselves are arbitrary, finite or infinite.

Formulas are stated as L.BoundedFormula Empty k, whose k bound variables are the pebbles. duplicatorWins_iff_forall_formula restates the theorem for formulas φ : L.Formula (Fin k) whose free variables name the pebbles; the translation between the two forms preserves quantifier rank (quantifierRank_relabel, quantifierRank_toFormula).

To show that a property of finite structures is not first-order definable, exhibit for each n two structures, one with the property and one without, on which Duplicator wins the n-round game (DuplicatorWins.realize_iff). For linear orders this is carried out in CslibFrontier.Logics.FirstOrder.EhrenfeuchtFraisse.FiniteLinearOrder.

Main definitions

• Cslib.Logic.FO.AtomicIndex: the atomic formulas in k variables, as indices.
• Cslib.Logic.FO.RankType, Cslib.Logic.FO.rankType: rank-n types and the type of a tuple.
• Cslib.Logic.FO.atomicDiagram, Cslib.Logic.FO.hintikka: the defining formulas of atomic types and of rank-n types.

Main results

• Cslib.Logic.FO.rankType_eq_iff: equal rank-n types are exactly winning positions of the n-round game.
• Cslib.Logic.FO.realize_hintikka, Cslib.Logic.FO.quantifierRank_hintikka_le: the Hintikka formula of a type defines it and has quantifier rank at most n.
• Cslib.Logic.FO.duplicatorWins_of_forall_realize_iff: Ehrenfeucht–Fraïssé, hard direction.
• Cslib.Logic.FO.duplicatorWins_iff_forall_realize_iff, Cslib.Logic.FO.duplicatorWins_iff_forall_formula, Cslib.Logic.FO.duplicatorWins_iff_forall_sentence: the Ehrenfeucht–Fraïssé theorem.
• Cslib.Logic.FO.exists_finite_quantifierRank_le_realize_iff: there are finitely many formulas of quantifier rank at most n in k variables up to logical equivalence.
• Cslib.Logic.FO.elementarilyEquivalent_iff_forall_duplicatorWins: elementary equivalence is winning every finite game.

References

• A. Ehrenfeucht, An application of games to the completeness problem for formalized theories
• R. Fraïssé, Sur quelques classifications des systèmes de relations
• L. Libkin, Elements of Finite Model Theory, Chapter 3 (the Ehrenfeucht–Fraïssé theorem and rank-k types).
• H.-D. Ebbinghaus and J. Flum, Finite Model Theory, Chapter 2.

Atomic types

@[reducible, inline]

abbrev Cslib.Logic.FO.AtomicIndex (L : FirstOrder.Language) (k : ℕ) : Type v

The atomic formulas in k variables of a relational language, as indices: an equation xᵢ = xⱼ, or a relation symbol applied to a tuple of variables.

instance Cslib.Logic.FO.AtomicIndex.finite {L : FirstOrder.Language} [Finite ((l : ℕ) × L.Relations l)] (k : ℕ) : Finite (AtomicIndex L k)

def Cslib.Logic.FO.AtomicIndex.formula {L : FirstOrder.Language} {k : ℕ} : AtomicIndex L k → L.BoundedFormula Empty k

The atomic formula xᵢ = xⱼ or R(x_{f 0}, …) with index i, the variables being the bound variables of a formula with no free variables.

def Cslib.Logic.FO.AtomicIndex.Holds {L : FirstOrder.Language} {M : Type w} [L.Structure M] {k : ℕ} (a : Fin k → M) : AtomicIndex L k → Prop

The atomic fact with index i holds of the tuple a.

@[simp]

theorem Cslib.Logic.FO.AtomicIndex.holds_inl {L : FirstOrder.Language} {M : Type w} [L.Structure M] {k : ℕ} (a : Fin k → M) (i j : Fin k) : Holds a (Sum.inl { down := (i, j) }) ↔ a i = a j

@[simp]

theorem Cslib.Logic.FO.AtomicIndex.holds_inr {L : FirstOrder.Language} {M : Type w} [L.Structure M] {k l : ℕ} (a : Fin k → M) (R : L.Relations l) (f : Fin l → Fin k) : Holds a (Sum.inr ⟨⟨l, R⟩, f⟩) ↔ FirstOrder.Language.Structure.RelMap R (a ∘ f)

@[simp]

theorem Cslib.Logic.FO.AtomicIndex.realize_formula {L : FirstOrder.Language} {M : Type w} [L.Structure M] {k : ℕ} (i : AtomicIndex L k) (a : Fin k → M) : i.formula.Realize default a ↔ Holds a i

@[simp]

theorem Cslib.Logic.FO.AtomicIndex.quantifierRank_formula {L : FirstOrder.Language} {k : ℕ} (i : AtomicIndex L k) : quantifierRank i.formula = 0

theorem Cslib.Logic.FO.partialIso_iff_holds {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {k : ℕ} {a : Fin k → M} {b : Fin k → N} : PartialIso L a b ↔ ∀ (i : AtomicIndex L k), AtomicIndex.Holds a i ↔ AtomicIndex.Holds b i

A position is a partial isomorphism exactly when both tuples satisfy the same atomic formulas.

Rank types

def Cslib.Logic.FO.RankType (L : FirstOrder.Language) : ℕ → ℕ → Type v

The rank-n types of k-tuples, as combinatorial data: a rank-0 type is a set of atomic facts, and a rank-(n + 1) type is a set of atomic facts together with the set of rank-n types of the one-point extensions. The body is exposed: statements about types use its shape.

instance Cslib.Logic.FO.RankType.finite {L : FirstOrder.Language} [Finite ((l : ℕ) × L.Relations l)] (n k : ℕ) : Finite (RankType L n k)

For finitely many relation symbols, there are finitely many rank-n types of k-tuples.

def Cslib.Logic.FO.rankType {L : FirstOrder.Language} {M : Type w} [L.Structure M] (n : ℕ) {k : ℕ} : (Fin k → M) → RankType L n k

The rank-n type of a tuple.

theorem Cslib.Logic.FO.rankType_zero {L : FirstOrder.Language} {M : Type w} [L.Structure M] {k : ℕ} (a : Fin k → M) : rankType 0 a = {i : AtomicIndex L k | AtomicIndex.Holds a i}

theorem Cslib.Logic.FO.RankType.succ_ext_iff {L : FirstOrder.Language} {n k : ℕ} {T T' : RankType L (n + 1) k} : T = T' ↔ T.1 = T'.1 ∧ T.2 = T'.2

Equality of rank-(n + 1) types is componentwise.

theorem Cslib.Logic.FO.rankType_succ {L : FirstOrder.Language} {M : Type w} [L.Structure M] {n k : ℕ} (a : Fin k → M) : rankType (n + 1) a = ({i : AtomicIndex L k | AtomicIndex.Holds a i}, Set.range fun (c : M) => rankType n (Fin.snoc a c))

theorem Cslib.Logic.FO.rankType_eq_iff {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {n k : ℕ} {a : Fin k → M} {b : Fin k → N} : rankType n a = rankType n b ↔ DuplicatorWins L n a b

Two tuples have the same rank-n type exactly when Duplicator wins the n-round game.

Hintikka formulas

noncomputable def Cslib.Logic.FO.atomicDiagram {L : FirstOrder.Language} [Finite ((l : ℕ) × L.Relations l)] {k : ℕ} (T : Set (AtomicIndex L k)) : L.BoundedFormula Empty k

The conjunction of the atomic facts in T and the negations of those not in T.

theorem Cslib.Logic.FO.realize_atomicDiagram {L : FirstOrder.Language} {M : Type w} [L.Structure M] [Finite ((l : ℕ) × L.Relations l)] {k : ℕ} (T : Set (AtomicIndex L k)) (a : Fin k → M) : (atomicDiagram T).Realize default a ↔ {i : AtomicIndex L k | AtomicIndex.Holds a i} = T

theorem Cslib.Logic.FO.quantifierRank_atomicDiagram {L : FirstOrder.Language} [Finite ((l : ℕ) × L.Relations l)] {k : ℕ} (T : Set (AtomicIndex L k)) : quantifierRank (atomicDiagram T) = 0

noncomputable def Cslib.Logic.FO.hintikka {L : FirstOrder.Language} [Finite ((l : ℕ) × L.Relations l)] {n k : ℕ} : RankType L n k → L.BoundedFormula Empty k

The Hintikka formula of a rank-n type: a formula of quantifier rank at most n satisfied exactly by the tuples of that type. For n + 1 it states the atomic diagram, that every rank-n type of the type is realized by a one-point extension, and that every one-point extension realizes one of them.

theorem Cslib.Logic.FO.realize_hintikka {L : FirstOrder.Language} {M : Type w} [L.Structure M] [Finite ((l : ℕ) × L.Relations l)] {n k : ℕ} (T : RankType L n k) (a : Fin k → M) : (hintikka T).Realize default a ↔ rankType n a = T

theorem Cslib.Logic.FO.quantifierRank_hintikka_le {L : FirstOrder.Language} [Finite ((l : ℕ) × L.Relations l)] {n k : ℕ} (T : RankType L n k) : quantifierRank (hintikka T) ≤ n

The Ehrenfeucht–Fraïssé theorem

theorem Cslib.Logic.FO.duplicatorWins_of_forall_realize_iff {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [Finite ((l : ℕ) × L.Relations l)] {n k : ℕ} {a : Fin k → M} {b : Fin k → N} (h : ∀ (φ : L.BoundedFormula Empty k), quantifierRank φ ≤ n → (φ.Realize default a ↔ φ.Realize default b)) : DuplicatorWins L n a b

Ehrenfeucht–Fraïssé, hard direction. For a language with finitely many relation symbols, if a and b satisfy the same formulas of quantifier rank at most n, then Duplicator wins the n-round game from (a, b). Only the Hintikka formula of the type of a is used.

theorem Cslib.Logic.FO.duplicatorWins_iff_forall_realize_iff {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [L.IsRelational] [Finite ((l : ℕ) × L.Relations l)] {n k : ℕ} {a : Fin k → M} {b : Fin k → N} : DuplicatorWins L n a b ↔ ∀ (φ : L.BoundedFormula Empty k), quantifierRank φ ≤ n → (φ.Realize default a ↔ φ.Realize default b)

The Ehrenfeucht–Fraïssé theorem [Lib04]. For a relational language with finitely many relation symbols, Duplicator wins the n-round game from (a, b) exactly when a and b satisfy the same formulas of quantifier rank at most n.

theorem Cslib.Logic.FO.duplicatorWins_iff_forall_formula {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [L.IsRelational] [Finite ((l : ℕ) × L.Relations l)] {n k : ℕ} {a : Fin k → M} {b : Fin k → N} : DuplicatorWins L n a b ↔ ∀ (φ : L.Formula (Fin k)), quantifierRank φ ≤ n → (φ.Realize a ↔ φ.Realize b)

The Ehrenfeucht–Fraïssé theorem for formulas with free variables. For a relational language with finitely many relation symbols, Duplicator wins the n-round game from (a, b) exactly when a and b satisfy the same formulas φ : L.Formula (Fin k) of quantifier rank at most n.

theorem Cslib.Logic.FO.duplicatorWins_iff_forall_sentence {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [L.IsRelational] [Finite ((l : ℕ) × L.Relations l)] {n : ℕ} {a : Fin 0 → M} {b : Fin 0 → N} : DuplicatorWins L n a b ↔ ∀ (φ : L.Sentence), quantifierRank φ ≤ n → (M ⊨ φ ↔ N ⊨ φ)

The Ehrenfeucht–Fraïssé theorem for sentences. For a relational language with finitely many relation symbols, Duplicator wins the n-round game on M and N exactly when M and N satisfy the same sentences of quantifier rank at most n.

Consequences

theorem Cslib.Logic.FO.exists_finite_quantifierRank_le_realize_iff {L : FirstOrder.Language} [L.IsRelational] [Finite ((l : ℕ) × L.Relations l)] (n k : ℕ) : ∃ (F : Set (L.BoundedFormula Empty k)), F.Finite ∧ (∀ ψ ∈ F, quantifierRank ψ ≤ n) ∧ ∀ (φ : L.BoundedFormula Empty k), quantifierRank φ ≤ n → ∃ ψ ∈ F, ∀ (M : Type w) [inst : L.Structure M] (a : Fin k → M), φ.Realize default a ↔ ψ.Realize default a

For a relational language with finitely many relation symbols, there are only finitely many formulas of quantifier rank at most n in k variables up to logical equivalence: each is equivalent, in every structure, to a disjunction of Hintikka formulas.

theorem Cslib.Logic.FO.elementarilyEquivalent_iff_forall_duplicatorWins {L : FirstOrder.Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [L.IsRelational] [Finite ((l : ℕ) × L.Relations l)] {a : Fin 0 → M} {b : Fin 0 → N} : L.ElementarilyEquivalent M N ↔ ∀ (n : ℕ), DuplicatorWins L n a b

For a relational language with finitely many relation symbols, two structures are elementarily equivalent exactly when Duplicator wins the n-round game on them for every n.