Realizing Lindström quantifiers as GQ denotations

[BC81] [Mos57] [vB84] [DKVD24] [DF23]

A FirstOrder.Language.LindstromQuantifier is an isomorphism-invariant class of L-structures (Mostowski's QUANT built into the type). This file realizes one over the monadic language L_UV (two unary predicates U, V) as a linguistic generalized-quantifier denotation GQ α = (α → Prop) → (α → Prop) → Prop: a pair of predicates (A, B) becomes the structure (α, A, B), and the quantifier holds of (A, B) iff it holds of that structure (Det.toGQ).

The headline is Det.realize_quantityInvariant: the project's existing predicate Quantification.QuantityInvariant — invariance of q A B under a bijective relabelling of the domain — is a theorem about every realized Lindström quantifier, not a side condition. It falls straight out of iso_inv, because a bijection f with A (f x) ↔ A' x and B (f x) ↔ B' x is exactly an L_UV-isomorphism (α, A, B) ≃[L_UV] (α, A', B') (with the map f⁻¹). This is the general-form (Lindström/van Benthem, type ⟨1,1⟩) of Mostowski's permutation invariance.

everyDet/someDet/noDet are the determiner classes for the Aristotelian core, and everyDet_toGQ/someDet_toGQ/noDet_toGQ show the GQ denotations the codebase already uses (every_sem, some_sem, no_sem) are precisely their realizations.

The final section grounds the square of opposition in the model theory. The square has a single home — the Aristotelian.IsContradictory/… relations, instantiated on GQ α in Quantification.Basic. Rather than restate them on a new carrier, toGQ is shown to be the [DKVD24] Aristotelian morphism carrying the class-level Boolean structure onto the GQ duality operators (toGQ_compl realizes outerNeg; noDet/someDet realize the inner-negation/dual corners), so the GQ square is the image of the model-theoretic one. Existential-import/logic-sensitivity ([DF23]) lives with the relations at the GQ layer (Quantification.a_e_contrary).

The general LindstromQuantifier layer is [UPSTREAM]-adjacent; this file is the linguistic realization functor on top of it.

Main definitions

• L_UV — the monadic language with two unary relation symbols U, V.
• structOfAB A B — the L_UV-structure (α, A, B).
• Det := LindstromQuantifier L_UV and Det.toGQ — the realization functor.
• everyDet/someDet/noDet — the Aristotelian determiner classes.

Main results

• Det.realize_quantityInvariant — every realized Lindström quantifier satisfies Quantification.QuantityInvariant.
• everyDet_toGQ/someDet_toGQ/noDet_toGQ — realizations are every_sem/some_sem/ no_sem.
• toGQ_compl — toGQ is the Aristotelian morphism: it carries the Boolean complement of a class to GQ outerNeg.
• someDet_holds_eq_compl/noDet_toGQ_eq_innerNeg/someDet_toGQ_eq_dualQ — the no/some corners as the complement/inner-negation/dual images of the model-theoretic structure.

L_UV/uvRel/uRel/vRel are re-derived in Studies.BarwiseCooper1981 (its Appendix-C Fraïssé argument predates this substrate); that copy will be deduped against this one in a follow-up.

The monadic language L_UV

inductive Quantification.uvRel : ℕ → Type

The two unary relation symbols of L_UV: restrictor U and scope V.

• U : uvRel 1
• V : uvRel 1

@[implicit_reducible]

instance Quantification.instDecidableEqUvRel {a✝ : ℕ} : DecidableEq (uvRel a✝)

Equations

• Quantification.instDecidableEqUvRel = Quantification.instDecidableEqUvRel.decEq

def Quantification.instDecidableEqUvRel.decEq {a✝ : ℕ} (x✝ x✝¹ : uvRel a✝) : Decidable (x✝ = x✝¹)

Equations

• Quantification.instDecidableEqUvRel.decEq Quantification.uvRel.U Quantification.uvRel.U = isTrue Quantification.instDecidableEqUvRel.decEq._proof_1
• Quantification.instDecidableEqUvRel.decEq Quantification.uvRel.U Quantification.uvRel.V = isFalse Quantification.instDecidableEqUvRel.decEq._proof_2
• Quantification.instDecidableEqUvRel.decEq Quantification.uvRel.V Quantification.uvRel.U = isFalse Quantification.instDecidableEqUvRel.decEq._proof_3
• Quantification.instDecidableEqUvRel.decEq Quantification.uvRel.V Quantification.uvRel.V = isTrue Quantification.instDecidableEqUvRel.decEq._proof_4

def Quantification.L_UV : FirstOrder.Language

The monadic language of generalized determiners: no function symbols, two unary relation symbols U, V.

Equations

• Quantification.L_UV = { Functions := fun (x : ℕ) => Empty, Relations := Quantification.uvRel }

@[reducible, inline]

abbrev Quantification.uRel : L_UV.Relations 1

The restrictor symbol U.

Equations

• Quantification.uRel = Quantification.uvRel.U

@[reducible, inline]

abbrev Quantification.vRel : L_UV.Relations 1

The scope symbol V.

Equations

• Quantification.vRel = Quantification.uvRel.V

@[reducible]

def Quantification.structOfAB {α : Type u} (A B : α → Prop) : L_UV.Structure α

The L_UV-structure (α, A, B): U is interpreted as A, V as B, and there are no function symbols.

Equations

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

@[simp]

theorem Quantification.structOfAB_relMap_U {α : Type u} (A B : α → Prop) (v : Fin 1 → α) : FirstOrder.Language.Structure.RelMap uRel v ↔ A (v 0)

@[simp]

theorem Quantification.structOfAB_relMap_V {α : Type u} (A B : α → Prop) (v : Fin 1 → α) : FirstOrder.Language.Structure.RelMap vRel v ↔ B (v 0)

The realization functor

@[reducible, inline]

abbrev Quantification.Det : Type (u + 1)

A determiner (type-⟨1,1⟩ Lindström quantifier): an iso-invariant class of L_UV-structures.

Equations

• Quantification.Det = Quantification.L_UV.LindstromQuantifier

def Quantification.Det.toGQ (Q : Det) (α : Type u) : GQ α

Realize a determiner as a GQ α denotation: (A, B) holds iff the structure (α, A, B) is in the quantifier's class.

Equations

• Q.toGQ α A B = ({ α := α, str := Quantification.structOfAB A B } ∈ Q.holds)

@[simp]

theorem Quantification.Det.toGQ_apply (Q : Det) {α : Type u} (A B : α → Prop) : Q.toGQ α A B ↔ { α := α, str := structOfAB A B } ∈ Q.holds

theorem Quantification.Det.realize_quantityInvariant (Q : Det) {α : Type u} : QuantityInvariant (Q.toGQ α)

Headline. Every realized Lindström quantifier satisfies the project's QuantityInvariant predicate: q A B is invariant under a bijective relabelling of the domain. This is the type-⟨1,1⟩ Mostowski/Lindström permutation invariance ([Mos57] [vB84]), recovered here as a consequence of iso_inv — not stipulated on the denotation.

The Aristotelian determiner classes

def Quantification.everyDet : Det

every: ∀ x, U x → V x.

Equations

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

def Quantification.someDet : Det

some: ∃ x, U x ∧ V x.

Equations

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

def Quantification.noDet : Det

no: ∀ x, U x → ¬ V x.

Equations

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

Theory-hub tie-ins

The GQ denotations the codebase already uses (every_sem, some_sem, no_sem) are exactly the realizations of the Lindström classes above.

theorem Quantification.everyDet_toGQ (α : Type u) : everyDet.toGQ α = every_sem

everyDet realizes every_sem: ⟦every⟧ = λR S. ∀x. R x → S x.

theorem Quantification.someDet_toGQ (α : Type u) : someDet.toGQ α = some_sem

someDet realizes some_sem: ⟦some⟧ = λR S. ∃x. R x ∧ S x.

theorem Quantification.noDet_toGQ (α : Type u) : noDet.toGQ α = no_sem

noDet realizes no_sem: ⟦no⟧ = λR S. ∀x. R x → ¬ S x.

The square of opposition: toGQ realizes it from the model theory

The square of opposition has a single home. Its relations are the Aristotelian.IsContradictory/IsContrary/IsSubaltern of [DS18a], instantiated on GQ α in Quantification.Basic (the working layer): every_contradicts_notEvery, no_contradicts_some, and the existential-import-gated a_e_contrary/subalternation_a_i (contrariety and subalternation need a non-empty restrictor — the logic-sensitivity of [DF23]). This section does not restate them on a new carrier; it shows the realization functor toGQ is the [DKVD24] Aristotelian morphism carrying the class-level Boolean structure onto those GQ duality operators, so the GQ square is the image of the model-theoretic one.

Concretely: outerNeg is realized by the Boolean complement of the iso-invariant class (toGQ_compl); the E/I corners no/some are the inner-negation and dual images of every (noDet_toGQ_eq_innerNeg, someDet_toGQ_eq_dualQ); and the no/some contradictory diagonal is the class-level fact some = ¬ no (someDet_holds_eq_compl) pushed through the morphism.

theorem Quantification.someDet_holds_eq_compl : someDet.holds = noDet.holdsᶜ

some is the Boolean complement of no as iso-invariant classes: ∃x. Ux ∧ Vx is the negation of ∀x. Ux → ¬Vx. The model-theoretic source of the no/some contradictory diagonal — toGQ-image is Quantification.no_contradicts_some.

theorem Quantification.toGQ_compl (Q : Det) (α : Type u) : Qᶜ.toGQ α = outerNeg (Q.toGQ α)

The Aristotelian morphism (outer negation). toGQ carries the Boolean complement of an iso-invariant class to GQ outer negation: (¬Q).toGQ = outerNeg Q.toGQ ([DKVD24]). With everyDet, this realizes the A/O contradictory diagonal as Quantification.every_contradicts_notEvery.

theorem Quantification.noDet_toGQ_eq_innerNeg (α : Type u) : noDet.toGQ α = innerNeg (everyDet.toGQ α)

The E corner: no realizes the inner negation of every (every…not = no).

theorem Quantification.someDet_toGQ_eq_dualQ (α : Type u) : someDet.toGQ α = dualQ (everyDet.toGQ α)

The I corner: some realizes the dual of every (every̌ = some).