Generalized Quantifier Definitions

@cite{barwise-cooper-1981} @cite{keenan-stavi-1986} @cite{peters-westerstahl-2006} @cite{van-benthem-1984}

Model-agnostic property definitions, operations, and type shifts for generalized quantifier denotations.

A GQ denotation is a function (α → Bool) → (α → Bool) → Bool mapping a restrictor and a scope to a truth value. The properties defined here (conservativity, monotonicity, duality, intersection condition, symmetry) are purely logical — they hold at the Bool-function level and require no model infrastructure.

The theory-specific module Semantics.Lexical.Determiner.Quantifier defines concrete denotations (every_sem, some_sem, etc.) and proves they satisfy these properties.

Contents

• §1 Property definitions: all predicates on GQs, grouped by source
• §2 Operations: duality, Boolean algebra, type shifts
• §3 Mathlib bridge: connection to Monotone/Antitone

@[reducible, inline]

abbrev Core.Quantification.GQ (α : Type u_1) : Type u_1

Generalized quantifier denotation: restrictor → scope → truth value.

Equations

• Core.Quantification.GQ α = ((α → Bool) → (α → Bool) → Bool)

def Core.Quantification.Conservative {α : Type u_1} (q : GQ α) : Prop

Conservativity: Q(A, B) = Q(A, A ∩ B).

Only the elements of B that are also in A matter for the quantifier's truth value. Also called "lives on" (B&C) or "intersectivity". All simple (lexicalized) determiners are conservative.

Equations

• Core.Quantification.Conservative q = ∀ (R S : α → Bool), q R S = q R fun (x : α) => R x && S x

def Core.Quantification.ScopeUpwardMono {α : Type u_1} (q : GQ α) : Prop

Scope-upward-monotone: if B ⊆ B' and Q(A,B), then Q(A,B').

Equivalent to ∀ R, Monotone (q R) under pointwise Bool ordering (see scopeUpMono_iff_monotone). This connects to Semantics.Entailment.Polarity.IsUpwardEntailing = Monotone.

Equations

• Core.Quantification.ScopeUpwardMono q = ∀ (R S S' : α → Bool), (∀ (x : α), S x = true → S' x = true) → q R S = true → q R S' = true

def Core.Quantification.ScopeDownwardMono {α : Type u_1} (q : GQ α) : Prop

Scope-downward-monotone: if B ⊆ B' and Q(A,B'), then Q(A,B).

Equivalent to ∀ R, Antitone (q R) under pointwise Bool ordering (see scopeDownMono_iff_antitone).

Equations

• Core.Quantification.ScopeDownwardMono q = ∀ (R S S' : α → Bool), (∀ (x : α), S x = true → S' x = true) → q R S' = true → q R S = true

def Core.Quantification.IntersectionCondition {α : Type u_1} (q : GQ α) : Prop

Intersection condition: Q(A,B) depends only on A∩B. B&C §4.8, p.189.

Equations

• Core.Quantification.IntersectionCondition q = ∀ (R S R' S' : α → Bool), (∀ (x : α), (R x && S x) = (R' x && S' x)) → q R S = q R' S'

def Core.Quantification.QSymmetric {α : Type u_1} (q : GQ α) : Prop

Symmetric: Q(A,B) = Q(B,A). B&C p.210; equivalent to intersection condition by Theorem C5.

Equations

• Core.Quantification.QSymmetric q = ∀ (R S : α → Bool), q R S = q S R

def Core.Quantification.RestrictorUpwardMono {α : Type u_1} (q : GQ α) : Prop

Restrictor-upward-monotone (persistent): if A ⊆ A' then Q(A,B) → Q(A',B). Linked to weak determiners and there-insertion. B&C §4.9, p.193.

Equations

• Core.Quantification.RestrictorUpwardMono q = ∀ (R R' S : α → Bool), (∀ (x : α), R x = true → R' x = true) → q R S = true → q R' S = true

def Core.Quantification.RestrictorDownwardMono {α : Type u_1} (q : GQ α) : Prop

Restrictor-downward-monotone (anti-persistent).

Equations

• Core.Quantification.RestrictorDownwardMono q = ∀ (R R' S : α → Bool), (∀ (x : α), R x = true → R' x = true) → q R' S = true → q R S = true

def Core.Quantification.PositiveStrong {α : Type u_1} (q : GQ α) : Prop

Positive strong: Q(A,A) for all A. P&W Ch.6: "every", "most", "the".

Equations

• Core.Quantification.PositiveStrong q = ∀ (R : α → Bool), q R R = true

def Core.Quantification.NegativeStrong {α : Type u_1} (q : GQ α) : Prop

Negative strong: ¬Q(A,A) for all A. "Neither".

Equations

• Core.Quantification.NegativeStrong q = ∀ (R : α → Bool), q R R = false

def Core.Quantification.Extension {α : Type u_1} (_q : GQ α) : Prop

Extension (EXT): Q(A,B) depends only on A and B, not on the ambient universe M. In model-theoretic GQ theory (where Q^M takes a universe), EXT must be stated as an additional axiom. For GQ α, EXT holds trivially since there is no universe parameter — it's a design theorem.

Significance: EXT + CONS characterize "well-behaved" determiners. See vanBenthem_cons_ext.

Reference: Peters & Westerståhl Ch.4 Def 4.1.

Equations

• Core.Quantification.Extension _q = True

def Core.Quantification.CONS2 {α : Type u_1} (q : GQ α) : Prop

Second conservativity: Q(A,B) = Q(A∩B, B). P&W Ch.6.

Equations

• Core.Quantification.CONS2 q = ∀ (R S : α → Bool), q R S = q (fun (x : α) => R x && S x) S

def Core.Quantification.Existential {α : Type u_1} (q : GQ α) : Prop

Existential property: Q(A,B) = Q(A∩B, everything). P&W Ch.6. Characterizes determiners that are felicitous in there-sentences.

Equations

• Core.Quantification.Existential q = ∀ (R S : α → Bool), q R S = q (fun (x : α) => R x && S x) fun (x : α) => true

def Core.Quantification.UpSEMon {α : Type u_1} (q : GQ α) : Prop

↑_SE Mon (@cite{peters-westerstahl-2006} §5.5): Q(A,B) & A⊆A' & A\B=A'\B → Q(A',B). On the number triangle: if Q(k,m) then Q(k',m) for k' ≥ k. Enlarging A by adding elements of B preserves Q.

Equations

• Core.Quantification.UpSEMon q = ∀ (R S R' : α → Bool), (∀ (x : α), R x = true → R' x = true) → (∀ (x : α), R' x = true → S x = false → R x = true) → q R S = true → q R' S = true

def Core.Quantification.UpSWMon {α : Type u_1} (q : GQ α) : Prop

↑_SW Mon (@cite{peters-westerstahl-2006} §5.5): Q(A,B) & A⊆A' & A∩B=A'∩B → Q(A',B). On the number triangle: if Q(k,m) then Q(k,m') for m' ≥ m. Enlarging A by adding elements outside B preserves Q. This is property (p) from P&W §5.2: half of the EXT condition.

Equations

• Core.Quantification.UpSWMon q = ∀ (R S R' : α → Bool), (∀ (x : α), R x = true → R' x = true) → (∀ (x : α), R' x = true → S x = true → R x = true) → q R S = true → q R' S = true

def Core.Quantification.DownNWMon {α : Type u_1} (q : GQ α) : Prop

↓_NW Mon (@cite{peters-westerstahl-2006} §5.5): Q(A,B) & A'⊆A & A\B=A'\B → Q(A',B). On the number triangle: if Q(k,m) then Q(k',m) for k' ≤ k. Shrinking A by removing elements of B preserves Q.

Equations

• Core.Quantification.DownNWMon q = ∀ (R S R' : α → Bool), (∀ (x : α), R' x = true → R x = true) → (∀ (x : α), R x = true → S x = false → R' x = true) → q R S = true → q R' S = true

def Core.Quantification.DownNEMon {α : Type u_1} (q : GQ α) : Prop

↓_NE Mon (@cite{peters-westerstahl-2006} §5.5): Q(A,B) & A'⊆A & A∩B=A'∩B → Q(A',B). On the number triangle: if Q(k,m) then Q(k,m') for m' ≤ m. Shrinking A by removing elements outside B preserves Q.

Equations

• Core.Quantification.DownNEMon q = ∀ (R S R' : α → Bool), (∀ (x : α), R' x = true → R x = true) → (∀ (x : α), R x = true → S x = true → R' x = true) → q R S = true → q R' S = true

def Core.Quantification.Smooth {α : Type u_1} (q : GQ α) : Prop

Smooth (@cite{peters-westerstahl-2006} §5.6): Q is ↓_NE Mon and ↑_SE Mon. Smooth quantifiers are Mon↑ (Prop 9). Under ISOM, smooth quantifiers have smooth monotonicity functions f where f(n) ≤ f(n+1) ≤ f(n)+1 (Prop 10). Most natural language Mon↑ determiners are smooth: all proportional quantifiers, "some", "all", "most", etc.

Equations

• Core.Quantification.Smooth q = (Core.Quantification.DownNEMon q ∧ Core.Quantification.UpSEMon q)

def Core.Quantification.CoSmooth {α : Type u_1} (q : GQ α) : Prop

Co-smooth (@cite{peters-westerstahl-2006} §5.6): Q's inner negation is smooth. Equivalently, ↓_NW Mon and ↑_SW Mon. "no" and "fewer than half" are co-smooth.

Equations

• Core.Quantification.CoSmooth q = (Core.Quantification.DownNWMon q ∧ Core.Quantification.UpSWMon q)

def Core.Quantification.LeftAntiAdditive {α : Type u_1} (q : GQ α) : Prop

Left anti-additive: Q(A∪B, C) ↔ Q(A,C) ∧ Q(B,C). P&W §5.9.

Equations

• Core.Quantification.LeftAntiAdditive q = ∀ (R R' S : α → Bool), q (fun (x : α) => R x || R' x) S = (q R S && q R' S)

def Core.Quantification.RightAntiAdditive {α : Type u_1} (q : GQ α) : Prop

Right anti-additive: Q(A, B∪C) ↔ Q(A,B) ∧ Q(A,C). P&W §5.9.

Equations

• Core.Quantification.RightAntiAdditive q = ∀ (R S S' : α → Bool), (q R fun (x : α) => S x || S' x) = (q R S && q R S')

def Core.Quantification.QTransitive {α : Type u_1} (q : GQ α) : Prop

Transitive: Q(A,B) ∧ Q(B,C) → Q(A,C). @cite{van-benthem-1984} §3.1. "all" is the prime transitive quantifier (inclusion is transitive).

Equations

• Core.Quantification.QTransitive q = ∀ (A B C : α → Bool), q A B = true → q B C = true → q A C = true

def Core.Quantification.QAntisymmetric {α : Type u_1} (q : GQ α) : Prop

Antisymmetric: Q(A,B) ∧ Q(B,A) → A = B (extensionally). @cite{van-benthem-1984} §3.1: "all" (inclusion) is antisymmetric.

Equations

• Core.Quantification.QAntisymmetric q = ∀ (A B : α → Bool), q A B = true → q B A = true → A = B

def Core.Quantification.QLinear {α : Type u_1} (q : GQ α) : Prop

Linear (connected): Q(A,B) ∨ Q(B,A) for all A, B. @cite{van-benthem-1984} §3.1: "not all" (non-inclusion) is linear.

Equations

• Core.Quantification.QLinear q = ∀ (A B : α → Bool), q A B = true ∨ q B A = true

def Core.Quantification.QuasiReflexive {α : Type u_1} (q : GQ α) : Prop

Quasi-reflexive: Q(A,B) → Q(A,A). @cite{van-benthem-1984} §3.1. "some" is quasi-reflexive: overlap implies non-emptiness.

Equations

• Core.Quantification.QuasiReflexive q = ∀ (A B : α → Bool), q A B = true → q A A = true

def Core.Quantification.QuasiUniversal {α : Type u_1} (q : GQ α) : Prop

Quasi-universal: Q(A,A) → Q(A,B) for all B. @cite{van-benthem-1984} §3.1. "no" is quasi-universal: if A∩A = ∅ then A∩B = ∅ for all B.

Equations

• Core.Quantification.QuasiUniversal q = ∀ (A B : α → Bool), q A A = true → q A B = true

def Core.Quantification.AlmostConnected {α : Type u_1} (q : GQ α) : Prop

Almost-connected: Q(A,B) → Q(A,C) ∨ Q(C,B) for all C. @cite{van-benthem-1984} §3.1: equivalent to transitivity of ¬Q. "not all" is almost-connected.

Equations

• Core.Quantification.AlmostConnected q = ∀ (A B C : α → Bool), q A B = true → q A C = true ∨ q C B = true

def Core.Quantification.Variety {α : Type u_1} (q : GQ α) : Prop

VAR (Variety): Q is non-trivial — it both accepts and rejects some pair. @cite{van-benthem-1984} §2: rules out degenerate quantifiers like "at least 2" on singleton domains. Used as hypothesis in most uniqueness theorems.

Equations

• Core.Quantification.Variety q = ((∃ (A : α → Bool) (B : α → Bool), q A B = true) ∧ ∃ (A : α → Bool) (B : α → Bool), q A B = false)

inductive Core.Quantification.DoubleMono : Type

Double monotonicity type (@cite{van-benthem-1984} §4.2). The logical Square of Opposition maps to four double-monotonicity types: all = ↓MON↑, some = ↑MON↑, no = ↓MON↓, not all = ↑MON↓.

• upUp : DoubleMono
• downUp : DoubleMono
• upDown : DoubleMono
• downDown : DoubleMono

instance Core.Quantification.instDecidableEqDoubleMono : DecidableEq DoubleMono

Equations

• Core.Quantification.instDecidableEqDoubleMono x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Quantification.instReprDoubleMono.repr : DoubleMono → ℕ → Std.Format

Equations

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

instance Core.Quantification.instReprDoubleMono : Repr DoubleMono

Equations

• Core.Quantification.instReprDoubleMono = { reprPrec := Core.Quantification.instReprDoubleMono.repr }

def Core.Quantification.instBEqDoubleMono.beq : DoubleMono → DoubleMono → Bool

Equations

• Core.Quantification.instBEqDoubleMono.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Quantification.instBEqDoubleMono : BEq DoubleMono

Equations

• Core.Quantification.instBEqDoubleMono = { beq := Core.Quantification.instBEqDoubleMono.beq }

def Core.Quantification.RightContinuous {α : Type u_1} (q : GQ α) : Prop

Right continuity (CONT): if Q(A,B₁) and Q(A,B₂) hold and B₁ ⊆ B ⊆ B₂, then Q(A,B). @cite{van-benthem-1984} §4.3: all right-monotone quantifiers are continuous. "precisely one" is continuous but non-monotone.

Equations

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

def Core.Quantification.Filtrating {α : Type u_1} (q : GQ α) : Prop

Filtrating: Q(A,B) ∧ Q(A,C) → Q(A, B∩C). @cite{van-benthem-1984} Thm 4.4.2: "all" is the only filtrating quantifier (under VAR*). This is because filtrating ↔ filter (closure under ∩), and only the principal filter at A (= inclusion) satisfies CONSERV.

Equations

• Core.Quantification.Filtrating q = ∀ (A B C : α → Bool), q A B = true → q A C = true → (q A fun (x : α) => B x && C x) = true

def Core.Quantification.QuantityInvariant {α : Type u_1} (q : GQ α) : Prop

QUANT (Isomorphism closure): Q is invariant under permutations of the domain. Model-agnostic version: Q(A,B) depends only on the pointwise Boolean pattern, not on which specific elements satisfy A and B.

This is the type ⟨1,1⟩ (binary) generalization of @cite{mostowski-1957}'s permutation invariance. Mostowski's original condition applies to type ⟨1⟩ (unary) quantifiers; the extension to binary determiners is due to @cite{van-benthem-1984} (building on Lindström 1966).

The model-specific version in Semantics.Lexical.Determiner.Quantifier.Quantity uses cardinalities directly, which requires FiniteModel. This version captures the same intuition without model infrastructure.

@cite{van-benthem-1984} §2: CONSERV + QUANT together reduce Q's behavior to pairs (a, b) where a = |A \ B| and b = |A ∩ B|.

Equations

• Core.Quantification.QuantityInvariant q = ∀ (A B A' B' : α → Bool) (f : α → α), Function.Bijective f → (∀ (x : α), A (f x) = A' x) → (∀ (x : α), B (f x) = B' x) → q A B = q A' B'

def Core.Quantification.outerNeg {α : Type u_1} (q : GQ α) : GQ α

Outer negation: (~Q)(A,B) = ¬Q(A,B) (B&C §4.11). Example: ~every = not-every ("Not every student passed").

Equations

• Core.Quantification.outerNeg q R S = !q R S

def Core.Quantification.innerNeg {α : Type u_1} (q : GQ α) : GQ α

Inner negation: (Q~)(A,B) = Q(A, ¬B) (B&C §4.11). Example: every~ = every...not ("Every student didn't pass").

Equations

• Core.Quantification.innerNeg q R S = q R fun (x : α) => !S x

def Core.Quantification.dualQ {α : Type u_1} (q : GQ α) : GQ α

Dual: Q̌ = ~(Q~) = ¬Q(A, ¬B) (B&C §4.11). Example: every̌ = some, somě = every.

Equations

• Core.Quantification.dualQ q = Core.Quantification.outerNeg (Core.Quantification.innerNeg q)

def Core.Quantification.gqMeet {α : Type u_1} (f g : GQ α) : GQ α

Meet of two GQ denotations: (f ∧ g)(A,B) = f(A,B) ∧ g(A,B). K&S (20): conjunction of dets, e.g., "both John's and Mary's". Also: "between n and m" = (at least n) ∧ (at most m).

Equations

• Core.Quantification.gqMeet f g R S = (f R S && g R S)

def Core.Quantification.gqJoin {α : Type u_1} (f g : GQ α) : GQ α

Join of two GQ denotations: (f ∨ g)(A,B) = f(A,B) ∨ g(A,B). K&S (24): disjunction of dets, e.g., "either John's or Mary's".

Equations

• Core.Quantification.gqJoin f g R S = (f R S || g R S)

def Core.Quantification.adjRestrict {α : Type u_1} (q : GQ α) (adj : α → Bool) : GQ α

Restriction of a GQ by a restricting function (adjective/relative clause). K&S (66): h_f(s) = h(f(s)). In our representation, the adjective narrows the restrictor: "tall student" = student ∧ tall.

Equations

• Core.Quantification.adjRestrict q adj R S = q (fun (x : α) => R x && adj x) S

@[reducible, inline]

abbrev Core.Quantification.NPQ (α : Type u_2) : Type u_2

NP denotation (type ⟨1⟩): a property of properties. This is the model-agnostic version of Ty.ett from TypeShifting.lean. P&W §2.1: an NP like "every student" denotes a set of sets.

Equations

• Core.Quantification.NPQ α = ((α → Bool) → Bool)

def Core.Quantification.restrict {α : Type u_1} (q : GQ α) (A : α → Bool) : NPQ α

Restriction: given a GQ Q and restrictor A, produce the type ⟨1⟩ quantifier Q^[A] (P&W §3.2.2). restrict Q A B = Q A B.

Equations

• Core.Quantification.restrict q A = q A

def Core.Quantification.LivesOn {α : Type u_1} (Q : NPQ α) (A : α → Bool) : Prop

A type ⟨1⟩ quantifier Q "lives on" A iff Q(B) = Q(A ∩ B) for all B. P&W §3.2.2: the restricted quantifier depends only on elements of A.

Equations

• Core.Quantification.LivesOn Q A = ∀ (B : α → Bool), Q B = Q fun (x : α) => A x && B x

def Core.Quantification.individual {α : Type u_1} (a : α) : NPQ α

Montagovian individual: the type ⟨1⟩ quantifier I_a = {X : a ∈ X}. P&W §3.2.3: an entity lifts to the principal ultrafilter it generates.

Equations

• Core.Quantification.individual a P = P a

theorem Core.Quantification.bool_le_iff_imp (a b : Bool) : a ≤ b ↔ a = true → b = true

theorem Core.Quantification.scopeUpMono_iff_monotone {α : Type u_1} (q : GQ α) : ScopeUpwardMono q ↔ ∀ (R : α → Bool), Monotone (q R)

ScopeUpwardMono q is ∀ R, Monotone (q R) under pointwise Bool ordering. This bridges GQ-level monotonicity to Mathlib's Monotone, which is what Polarity.lean uses (IsUpwardEntailing = Monotone).

theorem Core.Quantification.scopeDownMono_iff_antitone {α : Type u_1} (q : GQ α) : ScopeDownwardMono q ↔ ∀ (R : α → Bool), Antitone (q R)

ScopeDownwardMono q is ∀ R, Antitone (q R) under pointwise Bool ordering.