Realizing Lindström quantifiers as GQ denotations

A determiner, a Lindström quantifier of type ⟨1,1⟩, is an isomorphism-invariant class of structures for the monadic language with two predicate symbols, the restrictor pred 0 and the scope pred 1. Det.toGQ realizes it as a generalized-quantifier denotation GQ α: a pair of predicates (A, B) becomes the structure (α, A, B), and the quantifier holds of (A, B) when that structure is in the class. Quantity invariance is then a theorem about every realized determiner, and the determiners defined by the sentences for every, some and no realize the denotations of Quantification/Basic.lean.

The language is Language.monadic (Fin 2), so the monadic Ehrenfeucht–Fraïssé results apply to determiners directly: foDefinable_iff_exists_min_encard_eq is van Benthem's characterization of the first-order definable determiners as those invariant under agreement of the four Venn region sizes up to a threshold.

Main definitions

• Det, Det.toGQ: determiners and their realization as GQ α denotations.
• everyDet, someDet, noDet: the determiners of the square of opposition.

Main results

• Det.realize_quantityInvariant: every realized determiner satisfies Quantifier.GQ.QuantityInvariant, the type-⟨1,1⟩ form of Mostowski's permutation invariance.
• everyDet_toGQ, someDet_toGQ, noDet_toGQ: the realizations are every, GQ.some, no.
• toGQ_compl: realization carries the complement of a class to GQ outer negation.
• someDet_holds_eq_compl, noDet_toGQ_eq_innerNeg, someDet_toGQ_eq_dual: the no and some corners as the complement, inner negation and dual of every.

References

• [BC81]
• [DF23]
• [Mos57]
• [vB84]

The realization functor

@[reducible, inline]

abbrev Quantifier.Lindstrom.Det : Type (u + 1)

A determiner is a Lindström quantifier of type ⟨1,1⟩, an iso-invariant class of structures for the monadic language with a restrictor and a scope predicate.

Equations

• Quantifier.Lindstrom.Det = (FirstOrder.Language.monadic (Fin 2)).LindstromQuantifier

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

Q.toGQ α holds of (A, B) iff the structure (α, A, B) is in the class Q.

Equations

• Q.toGQ α A B = ({ α := α, str := FirstOrder.Language.monadicStructure α ![A, B] } ∈ Q.holds)

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

Every realized Lindström quantifier satisfies QuantityInvariant, so q A B is invariant under a bijective relabelling of the domain. This is the type-⟨1,1⟩ form of Mostowski's permutation invariance, derived from iso_inv rather than stipulated on the denotation.

The Aristotelian determiners

def Quantifier.Lindstrom.everyDet : Det

The determiner every, defined by ∀x (U x → V x).

Equations

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

def Quantifier.Lindstrom.someDet : Det

The determiner some, defined by ∃x (U x ∧ V x).

Equations

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

def Quantifier.Lindstrom.noDet : Det

The determiner no, defined by ∀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, GQ.some, no) are exactly the realizations of the Lindström classes above.

theorem Quantifier.Lindstrom.everyDet_toGQ (α : Type u) : everyDet.toGQ α = GQ.every

theorem Quantifier.Lindstrom.someDet_toGQ (α : Type u) : someDet.toGQ α = GQ.some

theorem Quantifier.Lindstrom.noDet_toGQ (α : Type u) : noDet.toGQ α = GQ.no

The square of opposition

The relations of the square live on GQ α in Quantification/Basic.lean: every_contradicts_notEvery and no_contradicts_some, and a_e_contrary and subalternation_a_i, which need a non-empty restrictor, an instance of the logic-sensitivity Demey and Frijters describe. This section shows that realization carries the class-level structure to the GQ duality operators. Outer negation is the complement of the class (toGQ_compl), the corners no and some are the inner negation and the dual of every (noDet_toGQ_eq_innerNeg, someDet_toGQ_eq_dual), and the contradictory diagonal between no and some is the class-level fact some = ¬ no (someDet_holds_eq_compl).

theorem Quantifier.Lindstrom.someDet_holds_eq_compl : someDet.holds = noDet.holdsᶜ

As iso-invariant classes, some is the complement of no, since ∃x. Ux ∧ Vx is the negation of ∀x. Ux → ¬Vx. Its image under toGQ is Quantifier.GQ.no_contradicts_some.

theorem Quantifier.Lindstrom.toGQ_compl (Q : Det) (α : Type u) : Qᶜ.toGQ α = (Q.toGQ α)ᶜ

Realization carries the complement of an iso-invariant class to GQ outer negation. With everyDet this realizes the contradictory diagonal between A and O as Quantifier.GQ.every_contradicts_notEvery.

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

At the E corner, no realizes the inner negation of every.

theorem Quantifier.Lindstrom.someDet_toGQ_eq_dual (α : Type u) : someDet.toGQ α = (everyDet.toGQ α).dual

At the I corner, some realizes the dual of every.