Lindström generalized quantifiers

[UPSTREAM] candidate. A (Lindström 1966; Mostowski 1957 for type ⟨1⟩) generalized quantifier over a language L is an isomorphism-invariant class of L-structures: the field holds, a Set (Bundled L.Structure) closed under L-isomorphism. The iso-invariance (Mostowski's QUANT / permutation invariance, in its general type-⟨1ⁿ⟩ form) is part of the type, not a side condition checked on a denotation.

This is the same shape as mathlib's FirstOrder.Language.age (an iso-invariant Set (Bundled L.Structure); cf. age.is_equiv_invariant) — a thin layer over Bundled/≃[L], not a new framework. The first-order definability of such a class is decided by the Ehrenfeucht–Fraïssé apparatus in this directory (not_foDefinable_of_nEquiv); its per-model realization (a determiner denotation) and the linguistic generalized-quantifier API live downstream in Semantics.Quantification.

Main definitions

• FirstOrder.Language.LindstromQuantifier — an iso-invariant class of L-structures.
• BooleanAlgebra (LindstromQuantifier L) — the Boolean algebra of generalized quantifiers (Qᶜ outer negation, Q ⊓ R/Q ⊔ R conjunction/disjunction, ⊤/⊥ the trivial quantifiers), obtained by pulling the powerset algebra back along the injective holds; holdsHom bundles that embedding as a BoundedLatticeHom.

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

A (Lindström) generalized quantifier over L: an isomorphism-invariant class of L-structures. The defining closure under L-isomorphism is built into the type.

• 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 (Mostowski QUANT, general form).

theorem FirstOrder.Language.LindstromQuantifier.ext_iff {L : Language} {x y : L.LindstromQuantifier} : x = y ↔ x.holds = y.holds

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.

@[implicit_reducible]

instance FirstOrder.Language.LindstromQuantifier.instLE {L : Language} : LE L.LindstromQuantifier

Equations

• FirstOrder.Language.LindstromQuantifier.instLE = { le := fun (Q R : L.LindstromQuantifier) => Q.holds ≤ R.holds }

@[implicit_reducible]

instance FirstOrder.Language.LindstromQuantifier.instLT {L : Language} : LT L.LindstromQuantifier

Equations

• FirstOrder.Language.LindstromQuantifier.instLT = { lt := fun (Q R : L.LindstromQuantifier) => Q.holds < R.holds }

@[implicit_reducible]

instance FirstOrder.Language.LindstromQuantifier.instMax {L : Language} : Max L.LindstromQuantifier

Equations

• FirstOrder.Language.LindstromQuantifier.instMax = { max := fun (Q R : L.LindstromQuantifier) => { holds := Q.holds ∪ R.holds, iso_inv := ⋯ } }

@[implicit_reducible]

instance FirstOrder.Language.LindstromQuantifier.instMin {L : Language} : Min L.LindstromQuantifier

Equations

• FirstOrder.Language.LindstromQuantifier.instMin = { min := fun (Q R : L.LindstromQuantifier) => { holds := Q.holds ∩ R.holds, iso_inv := ⋯ } }

@[implicit_reducible]

instance FirstOrder.Language.LindstromQuantifier.instTop {L : Language} : Top L.LindstromQuantifier

Equations

• FirstOrder.Language.LindstromQuantifier.instTop = { top := { holds := Set.univ, iso_inv := ⋯ } }

@[implicit_reducible]

instance FirstOrder.Language.LindstromQuantifier.instBot {L : Language} : Bot L.LindstromQuantifier

Equations

• FirstOrder.Language.LindstromQuantifier.instBot = { bot := { holds := ∅, iso_inv := ⋯ } }

@[implicit_reducible]

instance FirstOrder.Language.LindstromQuantifier.instCompl {L : Language} : Compl L.LindstromQuantifier

Equations

• FirstOrder.Language.LindstromQuantifier.instCompl = { compl := fun (Q : L.LindstromQuantifier) => { holds := Q.holdsᶜ, iso_inv := ⋯ } }

@[implicit_reducible]

instance FirstOrder.Language.LindstromQuantifier.instSDiff {L : Language} : SDiff L.LindstromQuantifier

Equations

• FirstOrder.Language.LindstromQuantifier.instSDiff = { sdiff := fun (Q R : L.LindstromQuantifier) => { holds := Q.holds \ R.holds, iso_inv := ⋯ } }

@[implicit_reducible]

instance FirstOrder.Language.LindstromQuantifier.instHImp {L : Language} : HImp L.LindstromQuantifier

Equations

• FirstOrder.Language.LindstromQuantifier.instHImp = { himp := fun (Q R : L.LindstromQuantifier) => { holds := Q.holds ⇨ R.holds, iso_inv := ⋯ } }

theorem FirstOrder.Language.LindstromQuantifier.holds_injective {L : Language} : Function.Injective holds

@[implicit_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

• FirstOrder.Language.LindstromQuantifier.instBooleanAlgebra = Function.Injective.booleanAlgebra FirstOrder.Language.LindstromQuantifier.holds ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[simp]

theorem FirstOrder.Language.LindstromQuantifier.holds_sup {L : Language} (Q R : L.LindstromQuantifier) : (Q ⊔ R).holds = Q.holds ∪ R.holds

@[simp]

theorem FirstOrder.Language.LindstromQuantifier.holds_inf {L : Language} (Q R : L.LindstromQuantifier) : (Q ⊓ R).holds = Q.holds ∩ R.holds

@[simp]

theorem FirstOrder.Language.LindstromQuantifier.holds_compl {L : Language} (Q : L.LindstromQuantifier) : Qᶜ.holds = Q.holdsᶜ

@[simp]

theorem FirstOrder.Language.LindstromQuantifier.holds_top {L : Language} : ⊤.holds = Set.univ

@[simp]

theorem FirstOrder.Language.LindstromQuantifier.holds_bot {L : Language} : ⊥.holds = ∅

def FirstOrder.Language.LindstromQuantifier.holdsHom {L : Language} : BoundedLatticeHom L.LindstromQuantifier (Set (CategoryTheory.Bundled L.Structure))

holds bundled: the embedding of the generalized-quantifier Boolean algebra into the powerset algebra Set (Bundled L.Structure) is a BoundedLatticeHom (it also preserves ᶜ, see holds_compl) — the Lindström analogue of Core.Order.holdsHom.

Equations

• FirstOrder.Language.LindstromQuantifier.holdsHom = { toFun := FirstOrder.Language.LindstromQuantifier.holds, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }