Documentation

Linglib.Core.ModelTheory.BijectiveGame

First-order logic with monadic quantifiers and the bijective game #

[UPSTREAM] candidate. Adding every monadic Lindström quantifier to first-order logic gives the logic FO(Mon). Besides atomic formulas and connectives, a quantifier Q over m predicates binds one variable in m formulas, and holds when the domain, with the predicates read as the formulas' extensions, belongs to Q. Hella's bijective game is the matching Ehrenfeucht–Fraïssé game: each round duplicator commits to a bijection between the domains, spoiler picks an element, and its image answers it. If duplicator wins k rounds, the two positions satisfy the same FO(Mon) formulas of quantifier rank ≤ k, since a bijection matching the formulas' extensions is an isomorphism of the monadic structures they carve out, which no quantifier can tell apart.

Main definitions #

Main results #

References #

source
inductive FirstOrder.Language.MonFormula (L : Language) :
ℕ → Type (max u v (w + 1))

Formulas of first-order logic with all monadic quantifiers, FO(Mon), with n free variables. Besides equations and relations between terms, falsity and implication, a monadic quantifier Q over m predicates binds a new variable in m formulas.

Instances For
    source
    def FirstOrder.Language.MonFormula.Realize {L : Language} {M : Type w} [L.Structure M] {n : ℕ} :
    L.MonFormula n → (Fin n → M) → Prop

    Satisfaction of a formula of FO(Mon) under an assignment of its free variables. A monadic quantifier holds when the domain, each predicate read as the extension of the corresponding formula in the bound variable, belongs to the quantifier.

    Equations
    Instances For
      source
      def FirstOrder.Language.MonFormula.qr {L : Language} {n : ℕ} :
      L.MonFormula n → ℕ

      The quantifier rank of a formula of FO(Mon), the greatest nesting depth of quantifiers.

      Equations
      Instances For
        source
        def FirstOrder.Language.MonDefinable (L : Language) (K P : Set (CategoryTheory.Bundled L.Structure)) :
        Prop

        A class P of structures is definable in FO(Mon) within K when some sentence of FO(Mon) holds of exactly the members of P among the structures in K.

        Equations
        Instances For

          The bijective game #

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

          Duplicator wins the k-round bijective 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, she has a bijection g between the domains such that each element a of M and its image g a extend the tuples to a position she wins with k rounds left.

          Equations
          Instances For
            source
            theorem FirstOrder.Language.DuplicatorWinsBijective.duplicatorWins_zero {L : Language} {M N : Type w} [L.Structure M] [L.Structure N] {k n : ℕ} {v : Fin n → M} {w : Fin n → N} :
            L.DuplicatorWinsBijective k v w → L.DuplicatorWins 0 v w
            source
            theorem FirstOrder.Language.DuplicatorWinsBijective.realize_iff {L : Language} {M N : Type w} [L.Structure M] [L.Structure N] {n : ℕ} {φ : L.MonFormula n} {k : ℕ} {v : Fin n → M} {w : Fin n → N} :
            L.DuplicatorWinsBijective k v w → φ.qr ≤ k → (φ.Realize v ↔ φ.Realize w)

            A position from which duplicator wins k rounds of the bijective game satisfies the same formulas of FO(Mon) of quantifier rank ≤ k.

            source
            theorem FirstOrder.Language.not_monDefinable_of_duplicatorWinsBijective {L : Language} {K P : Set (CategoryTheory.Bundled L.Structure)} (h : ∀ (k : ℕ), ∃ M ∈ K, ∃ N ∈ K, L.DuplicatorWinsBijective k default default ∧ M ∈ P ∧ N ∉ P) :
            ¬L.MonDefinable K P

            The bijective game method for undefinability in FO(Mon). If for every number of rounds duplicator wins the bijective game between some structure in K with property P and one in K without it, then P is not definable in FO(Mon) within K.

            Successor graphs of permutations #

            The successor graph of a permutation σ joins each element x to σ x. Duplicator wins r rounds of the bijective game between the successor graphs of two permutations of equinumerous finite sets whose cycles all have length at least 2 ^ r. With k rounds left she keeps the chosen points matched displacement by displacement up to 2 ^ k: the j-th point lies d steps along σ from the i-th exactly when the same holds along τ. In each round she translates the points near the chosen ones along τ and matches the remaining points by counting.

            source
            theorem FirstOrder.Language.duplicatorWinsBijective_successor {M N : Type w} {σ : Equiv.Perm M} {τ : Equiv.Perm N} [Fintype M] [Fintype N] (hcard : Fintype.card M = Fintype.card N) (r : ℕ) (hσ : ∀ (x : M) (d : ℤ), |d| < 2 ^ r → (σ ^ d) x = x → d = 0) (hτ : ∀ (x : N) (d : ℤ), |d| < 2 ^ r → (τ ^ d) x = x → d = 0) :
            Language.graph.DuplicatorWinsBijective r default default

            Duplicator wins r rounds of the bijective game between the successor graphs of two permutations of equinumerous finite sets whose cycles all have length at least 2 ^ r.