The Ehrenfeucht–Fraïssé game on monadic structures

[UPSTREAM] candidate. A language is monadic when its only symbols are unary relation symbols, so each element of a structure has a unary type, the set of symbols holding of it. On monadic structures the Ehrenfeucht–Fraïssé game is decided by counting: duplicator answers a played element by its partner and a fresh element by a fresh element of the same type, which is possible while, for each type, the unplayed elements on the two sides are equinumerous or both at least the number of rounds left. Conversely, spoiler wins when a type is scarcer on one side, so two structures for a finite monadic signature are t-equivalent exactly when, for each unary type, their elements of that type are equinumerous or both at least t, the first-order case of Peters and Westerståhl's Theorem 13. With the Hintikka characterization of definability, this makes a class first-order definable iff it is invariant under these counts up to some threshold, which is van Benthem's characterization of the first-order definable determiners.

Main definitions

• FirstOrder.Language.IsMonadic: the language has only unary relation symbols.
• FirstOrder.Language.monadic, FirstOrder.Language.monadicStructure: the monadic language on an index type and the structure given by a family of predicates.
• FirstOrder.Language.unaryType: the unary relation symbols holding of an element.
• FirstOrder.Language.MonadicMatch: tuples with the same equality pattern and unary types.

Main results

• FirstOrder.Language.MonadicMatch.duplicatorWins: the counting strategy wins the game.
• FirstOrder.Language.DuplicatorWins.min_encard_eq: conversely, any winning position satisfies the counting condition.
• FirstOrder.Language.elementarilyEquivalentUpTo_iff_min_encard_eq, FirstOrder.Language.elementarilyEquivalentUpTo_monadicStructure_iff: the t-equivalence criterion.
• FirstOrder.Language.foDefinable_iff_exists_min_encard_eq: a class of structures for a finite monadic signature is definable within K iff it is invariant under agreement of the unary type counts up to some threshold.

References

• [PW06]
• [vB84]

class FirstOrder.Language.IsMonadic (L : Language) : Prop

A language is monadic when its only symbols are unary relation symbols.

• isEmpty_functions (n : ℕ) : IsEmpty (L.Functions n)
• isEmpty_relations (n : ℕ) : n ≠ 1 → IsEmpty (L.Relations n)

@[instance 100]

instance FirstOrder.Language.IsMonadic.isRelational (L : Language) [L.IsMonadic] : L.IsRelational

inductive FirstOrder.Language.monadicRel (ι : Type v) : ℕ → Type v

The relation symbols of the monadic language on ι, one unary symbol for each i : ι.

• pred {ι : Type v} (i : ι) : monadicRel ι 1

def FirstOrder.Language.monadic (ι : Type v) : Language

The monadic language with one unary relation symbol for each i : ι.

Equations

• FirstOrder.Language.monadic ι = { Functions := fun (x : ℕ) => Empty, Relations := FirstOrder.Language.monadicRel ι }

instance FirstOrder.Language.instIsMonadicMonadic {ι : Type v} : (Language.monadic ι).IsMonadic

instance FirstOrder.Language.instFiniteSymbolsMonadic {ι : Type v} [Finite ι] : Finite (Language.monadic ι).Symbols

def FirstOrder.Language.unaryType (L : Language) {M : Type w} [L.Structure M] (a : M) : L.Relations 1 → Prop

The unary type of a is the set of unary relation symbols that hold of it.

Equations

• L.unaryType a R = FirstOrder.Language.Structure.RelMap R ![a]

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

Two tuples match when they have the same equality pattern and corresponding entries have the same unary type, so that they form a partial isomorphism between monadic structures.

• eq_iff (i j : Fin n) : v i = v j ↔ w i = w j
• unaryType_eq (i : Fin n) : L.unaryType (v i) = L.unaryType (w i)

@[instance_reducible]

def FirstOrder.Language.monadicStructure (M : Type w) {ι : Type v} (P : ι → M → Prop) : (Language.monadic ι).Structure M

The structure on M interpreting each symbol pred i as the predicate P i.

Equations

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

@[simp]

theorem FirstOrder.Language.relMap_monadicStructure {M : Type w} {ι : Type v} {P : ι → M → Prop} (i : ι) (x : Fin 1 → M) : Structure.RelMap (monadicRel.pred i) x ↔ P i (x 0)

theorem FirstOrder.Language.unaryType_monadicStructure_eq_iff {M : Type w} {ι : Type v} {P : ι → M → Prop} (a : M) (S : (Language.monadic ι).Relations 1 → Prop) : (Language.monadic ι).unaryType a = S ↔ ∀ (i : ι), P i a ↔ S (monadicRel.pred i)

def FirstOrder.Language.monadicStructureEquiv {M : Type w} {N : Type w'} {ι : Type v} {P : ι → M → Prop} {Q : ι → N → Prop} (e : M ≃ N) (h : ∀ (i : ι) (x : M), Q i (e x) ↔ P i x) : (Language.monadic ι).Equiv M N

A bijection carrying each predicate P i to Q i is an isomorphism of the monadic structures.

Equations

• FirstOrder.Language.monadicStructureEquiv e h = { toEquiv := e, map_fun' := ⋯, map_rel' := ⋯ }

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

theorem FirstOrder.Language.MonadicMatch.snoc {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {n : ℕ} {v : Fin n → M} {w : Fin n → N} (h : L.MonadicMatch v w) {a : M} {b : N} (heq : ∀ (i : Fin n), v i = a ↔ w i = b) (hab : L.unaryType a = L.unaryType b) : L.MonadicMatch (Fin.snoc v a) (Fin.snoc w b)

theorem FirstOrder.Language.MonadicMatch.exists_snoc {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {n : ℕ} {v : Fin n → M} {w : Fin n → N} {j : ℕ} (h : L.MonadicMatch v w) (hc : ∀ (S : L.Relations 1 → Prop), min (↑(j + 1)) (L.unaryType ⁻¹' {S} \ Set.range v).encard = min (↑(j + 1)) (L.unaryType ⁻¹' {S} \ Set.range w).encard) (a : M) : ∃ (b : N), L.MonadicMatch (Fin.snoc v a) (Fin.snoc w b) ∧ ∀ (S : L.Relations 1 → Prop), min (↑j) (L.unaryType ⁻¹' {S} \ Set.range (Fin.snoc v a)).encard = min (↑j) (L.unaryType ⁻¹' {S} \ Set.range (Fin.snoc w b)).encard

In the forth move of the counting strategy, a played element is answered by its partner and a fresh element of type S by a fresh element of type S, which exists because the fresh elements of type S are equinumerous on the two sides or both at least j + 1.

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

Matched tuples in a monadic language satisfy the same atomic formulas, which are equalities and unary predications of variables.

theorem FirstOrder.Language.MonadicMatch.duplicatorWins {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [L.IsMonadic] {j n : ℕ} {v : Fin n → M} {w : Fin n → N} : L.MonadicMatch v w → (∀ (S : L.Relations 1 → Prop), min (↑j) (L.unaryType ⁻¹' {S} \ Set.range v).encard = min (↑j) (L.unaryType ⁻¹' {S} \ Set.range w).encard) → L.DuplicatorWins j v w

In a monadic language the counting strategy wins j rounds from matched tuples when, for every unary type, the unplayed elements of that type are equinumerous on the two sides or both at least j.

theorem FirstOrder.Language.elementarilyEquivalentUpTo_of_min_encard_eq {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [L.IsMonadic] {t : ℕ} (h : ∀ (S : L.Relations 1 → Prop), min (↑t) (L.unaryType ⁻¹' {S}).encard = min (↑t) (L.unaryType ⁻¹' {S}).encard) : L.ElementarilyEquivalentUpTo t M N

Two structures for a monadic language are t-equivalent when, for every unary type, their elements of that type are equinumerous or both at least t ([PW06] Theorem 13 with condition (13.7), first-order case).

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

Tuples from which duplicator wins match, since equalities and unary predications of variables are atomic formulas.

theorem FirstOrder.Language.DuplicatorWins.exists_mem_sdiff_range {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {n : ℕ} {v : Fin n → M} {w : Fin n → N} {k : ℕ} (h : L.DuplicatorWins (k + 1) v w) {S : L.Relations 1 → Prop} {a : M} (ha : a ∈ L.unaryType ⁻¹' {S} \ Set.range v) : ∃ b ∈ L.unaryType ⁻¹' {S} \ Set.range w, L.DuplicatorWins k (Fin.snoc v a) (Fin.snoc w b)

A forth move answers a fresh element of type S by a fresh element of type S.

theorem FirstOrder.Language.DuplicatorWins.min_encard_eq {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] {j n : ℕ} {v : Fin n → M} {w : Fin n → N} : L.DuplicatorWins j v w → ∀ (S : L.Relations 1 → Prop), min (↑j) (L.unaryType ⁻¹' {S} \ Set.range v).encard = min (↑j) (L.unaryType ⁻¹' {S} \ Set.range w).encard

At a winning position for j rounds, the unplayed elements of each unary type are equinumerous on the two sides or both at least j.

theorem FirstOrder.Language.elementarilyEquivalentUpTo_iff_min_encard_eq {L : Language} {M : Type w} {N : Type w'} [L.Structure M] [L.Structure N] [L.IsMonadic] [Finite L.Symbols] {t : ℕ} : L.ElementarilyEquivalentUpTo t M N ↔ ∀ (S : L.Relations 1 → Prop), min (↑t) (L.unaryType ⁻¹' {S}).encard = min (↑t) (L.unaryType ⁻¹' {S}).encard

Two structures for a finite monadic signature are t-equivalent iff, for every unary type, their elements of that type are equinumerous or both at least t ([PW06] Theorem 13 with condition (13.7), first-order case).

theorem FirstOrder.Language.foDefinable_iff_exists_min_encard_eq {L : Language} [L.IsMonadic] [Finite L.Symbols] {K P : Set (CategoryTheory.Bundled L.Structure)} : L.FODefinable K P ↔ ∃ (n : ℕ), ∀ M ∈ K, ∀ N ∈ K, (∀ (S : L.Relations 1 → Prop), min (↑n) (L.unaryType ⁻¹' {S}).encard = min (↑n) (L.unaryType ⁻¹' {S}).encard) → M ∈ P → N ∈ P

A class of structures for a finite monadic signature is first-order definable within K iff, for some threshold n, it is invariant within K under agreement of the unary type counts up to n; for two unary predicates this is [vB84] Theorem 6.1.

theorem FirstOrder.Language.elementarilyEquivalentUpTo_monadicStructure_iff {M : Type w} {N : Type w'} {ι : Type v} [Finite ι] {P : ι → M → Prop} {Q : ι → N → Prop} {t : ℕ} : (Language.monadic ι).ElementarilyEquivalentUpTo t M N ↔ ∀ (S : ι → Prop), min ↑t {x : M | ∀ (i : ι), P i x ↔ S i}.encard = min ↑t {y : N | ∀ (i : ι), Q i y ↔ S i}.encard

Two monadic structures (M, P) and (N, Q) over a finite index type are t-equivalent iff each part of the partition by the predicates, the elements satisfying exactly the predicates selected by S, has the same size in both or at least t elements in both ([PW06] Theorem 13 with condition (13.7), first-order case).