Documentation

Linglib.Core.ModelTheory.Lindstrom

Lindström generalized quantifiers #

[UPSTREAM] candidate. A generalized quantifier over a language L, in Lindström's sense, is a class of L-structures closed under isomorphism, so the invariance Mostowski imposed on quantifiers is part of the type rather than a side condition on a denotation. These classes form a Boolean subalgebra of the powerset of Bundled L.Structure. Each sentence defines one, its class of models, and the Ehrenfeucht–Fraïssé results in this directory decide which classes arise this way, the classes Lindström writes EC.

Main definitions #

Implementation notes #

Lindström restricts quantifiers to classes of relational structures; here L may have function symbols, which costs nothing since isomorphism invariance is the only condition.

References #

source
structure FirstOrder.Language.LindstromQuantifier (L : Language) :
Type (max (max u v) (w + 1))

A Lindström quantifier over L is a class of L-structures closed under L-isomorphism.

  • holds : Set (CategoryTheory.Bundled L.Structure)

    The class of structures the quantifier holds of.

  • iso_inv {M N : CategoryTheory.Bundled L.Structure} : Nonempty (L.Equiv ↑M ↑N) → (M ∈ self.holds ↔ N ∈ self.holds)

    The class is closed under L-isomorphism.

Instances For
    source
    theorem FirstOrder.Language.LindstromQuantifier.ext_iff {L : Language} {x y : L.LindstromQuantifier} :
    x = y ↔ x.holds = y.holds
    source
    theorem FirstOrder.Language.LindstromQuantifier.ext {L : Language} {x y : L.LindstromQuantifier} (holds : x.holds = y.holds) :
    x = y

    Boolean-algebra structure #

    The iso-invariant classes are a sub-Boolean-algebra of Set (Bundled L.Structure) — closed under complement, finite meet/join, ⊤ (all structures) and ⊥ (none), because L-isomorphism is an equivalence. holds is the injective embedding, so the algebra is pulled back along it: Qᶜ is outer negation (every ↦ not-every), Q ⊓ R/Q ⊔ R are conjunction/disjunction.

    source
    @[instance_reducible]
    instance FirstOrder.Language.LindstromQuantifier.instLE {L : Language} :
    LE L.LindstromQuantifier
    Equations
    source
    @[instance_reducible]
    instance FirstOrder.Language.LindstromQuantifier.instLT {L : Language} :
    LT L.LindstromQuantifier
    Equations
    source
    @[instance_reducible]
    instance FirstOrder.Language.LindstromQuantifier.instMax {L : Language} :
    Max L.LindstromQuantifier
    Equations
    source
    @[instance_reducible]
    instance FirstOrder.Language.LindstromQuantifier.instMin {L : Language} :
    Min L.LindstromQuantifier
    Equations
    source
    @[instance_reducible]
    instance FirstOrder.Language.LindstromQuantifier.instTop {L : Language} :
    Top L.LindstromQuantifier
    Equations
    source
    @[instance_reducible]
    instance FirstOrder.Language.LindstromQuantifier.instBot {L : Language} :
    Bot L.LindstromQuantifier
    Equations
    source
    @[instance_reducible]
    instance FirstOrder.Language.LindstromQuantifier.instCompl {L : Language} :
    Compl L.LindstromQuantifier
    Equations
    source
    @[instance_reducible]
    instance FirstOrder.Language.LindstromQuantifier.instSDiff {L : Language} :
    SDiff L.LindstromQuantifier
    Equations
    source
    @[instance_reducible]
    instance FirstOrder.Language.LindstromQuantifier.instHImp {L : Language} :
    HImp L.LindstromQuantifier
    Equations
    source
    theorem FirstOrder.Language.LindstromQuantifier.holds_injective {L : Language} :
    Function.Injective holds
    source
    @[instance_reducible]
    instance FirstOrder.Language.LindstromQuantifier.instBooleanAlgebra {L : Language} :
    BooleanAlgebra L.LindstromQuantifier

    The Boolean algebra of generalized quantifiers over L, pulled back along the injective holds embedding into the powerset algebra Set (Bundled L.Structure).

    Equations
    source
    @[simp]
    theorem FirstOrder.Language.LindstromQuantifier.holds_sup {L : Language} (Q R : L.LindstromQuantifier) :
    (Q ⊔ R).holds = Q.holds ∪ R.holds
    source
    @[simp]
    theorem FirstOrder.Language.LindstromQuantifier.holds_inf {L : Language} (Q R : L.LindstromQuantifier) :
    (Q ⊓ R).holds = Q.holds ∩ R.holds
    source
    @[simp]
    theorem FirstOrder.Language.LindstromQuantifier.holds_compl {L : Language} (Q : L.LindstromQuantifier) :
    Qᶜ.holds = Q.holdsᶜ
    source
    @[simp]
    theorem FirstOrder.Language.LindstromQuantifier.holds_top {L : Language} :
    ⊤.holds = Set.univ
    source
    @[simp]
    theorem FirstOrder.Language.LindstromQuantifier.holds_bot {L : Language} :
    ⊥.holds = ∅
    source
    def FirstOrder.Language.LindstromQuantifier.holdsHom {L : Language} :
    BoundedLatticeHom L.LindstromQuantifier (Set (CategoryTheory.Bundled L.Structure))

    holdsHom is the embedding of the quantifiers into the powerset algebra Set (Bundled L.Structure) as a bounded lattice homomorphism; it also preserves complements (holds_compl).

    Equations
    Instances For
      source
      def FirstOrder.Language.LindstromQuantifier.ofSentence {L : Language} (φ : L.Sentence) :
      L.LindstromQuantifier

      The quantifier defined by a sentence holds of exactly the models of the sentence.

      Equations
      Instances For
        source
        @[simp]
        theorem FirstOrder.Language.LindstromQuantifier.mem_holds_ofSentence {L : Language} {φ : L.Sentence} {M : CategoryTheory.Bundled L.Structure} :
        M ∈ (ofSentence φ).holds ↔ ↑M ⊨ φ