Unified Semantics for Universal Quantification

@cite{haslinger-etal-2025-nllt}

A single lexical meaning for universal quantifiers across languages, from "A unified semantics for distributive and non-distributive universal quantifiers across languages" (NLLT 43, 2025).

Core Idea

The morpheme Q_∀ applies its scope predicate to every maximal non-overlapping element of the restrictor denotation. Whether the result is distributive or non-distributive falls out from the algebraic structure of the noun denotation:

• Singular NP (atoms only): every element is maximal and non-overlapping → Q_∀ distributes over each atom. [+dist]
• Plural NP (closed under sum): one maximal element = the sum → Q_∀ applies scope to the sum. [−dist]

This is the Distributivity-Number Generalization (DNG).

Architecture

Q_∀ is defined abstractly over PartialOrder using Mereology.Overlap, Mereology.Atom, and Mereology.isMaximal. A decidable Finset-based variant is provided for computational verification.

The connection to the standard GQ every_sem (in Quantifier.lean) and to the tolerance-based distMaximal (in Distributivity.lean) is established via bridge theorems, not by replacement.

def Semantics.Quantification.UnifiedUniversal.maxNonOverlap {α : Type u_1} [PartialOrder α] (P : α → Prop) (x : α) : Prop

An element x is maximal non-overlapping in P iff x ∈ P and every P-element that overlaps x is a part of x.

This is the condition in @cite{haslinger-etal-2025-nllt} eq. (70): P(x) ∧ ¬∃y[P(y) ∧ ∃z[z ⊑ x ∧ z ⊑ y] ∧ y ⊄ x].

Equivalently: x absorbs all overlapping P-elements. In a singular NP denotation (atoms only), every atom satisfies this. In a plural NP denotation (closed under sum), only the maximal sum does.

Equations

• Semantics.Quantification.UnifiedUniversal.maxNonOverlap P x = (P x ∧ ∀ (y : α), P y → Mereology.Overlap x y → y ≤ x)

def Semantics.Quantification.UnifiedUniversal.QForall {α : Type u_1} [PartialOrder α] (P Q : α → Prop) : Prop

Q_∀: the unified universal quantifier.

⟦Q_∀⟧ = λP.λQ.∀x[maxNonOverlap(P, x) → Q(x)]

Q_∀ applies the scope predicate Q to every maximal non-overlapping element of the restrictor P. @cite{haslinger-etal-2025-nllt} eq. (70).

When P = ⟦student⟧ (atoms {a,b,c}): Q_∀(P)(Q) = Q(a) ∧ Q(b) ∧ Q(c) — distributive

When P = ⟦student-PL⟧ (closed under ⊔, max = a⊔b⊔c): Q_∀(P)(Q) = Q(a⊔b⊔c) — non-distributive (maximization)

Equations

• Semantics.Quantification.UnifiedUniversal.QForall P Q = ∀ (x : α), Semantics.Quantification.UnifiedUniversal.maxNonOverlap P x → Q x

theorem Semantics.Quantification.UnifiedUniversal.maxNonOverlap_imp_isMaximal {α : Type u_1} [PartialOrder α] {P : α → Prop} {x : α} (h : maxNonOverlap P x) : Mereology.isMaximal P x

maxNonOverlap implies isMaximal: if x absorbs all overlapping P-elements, it is certainly maximal (no proper P-extension).

theorem Semantics.Quantification.UnifiedUniversal.maxNonOverlap_of_atom {α : Type u_1} [PartialOrder α] {P : α → Prop} {x : α} (hPx : P x) (_hAtom : Mereology.Atom x) (hDisj : ∀ (y : α), P y → Mereology.Overlap x y → y = x) : maxNonOverlap P x

For atoms with a disjointness property, maxNonOverlap reduces to membership in P.

The hypothesis hDisj says distinct P-atoms don't overlap. This holds in any atomic Boolean algebra (or distributive lattice where atoms are join-prime).

theorem Semantics.Quantification.UnifiedUniversal.maxNonOverlap_of_cum_maximal {α : Type u_1} [SemilatticeSup α] {P : α → Prop} (hCum : Mereology.CUM P) {x : α} (hMax : Mereology.isMaximal P x) : maxNonOverlap P x

In a CUM predicate, an element that is isMaximal is also maxNonOverlap. CUM ensures all P-elements join into the max, so any P-element overlapping max is necessarily ≤ max.

Proof: if y ∈ P overlaps x, then x ⊔ y ∈ P (by CUM), and x ≤ x ⊔ y, so x = x ⊔ y (by maximality), hence y ≤ x.

theorem Semantics.Quantification.UnifiedUniversal.dng_atoms {α : Type u_1} [PartialOrder α] {P Q : α → Prop} (hAtoms : ∀ (x : α), P x → Mereology.Atom x) (hDisj : ∀ (x y : α), P x → P y → Mereology.Overlap x y → x = y) : QForall P Q ↔ ∀ (x : α), P x → Q x

DNG for singular complements (atoms).

When every P-element is an atom and distinct P-atoms don't overlap, Q_∀(P)(Q) reduces to universal quantification: ∀x, P(x) → Q(x).

This is the [+dist] case: @cite{haslinger-etal-2025-nllt} eq. (30b).

theorem Semantics.Quantification.UnifiedUniversal.dng_cum {α : Type u_1} [SemilatticeSup α] {P Q : α → Prop} (hCum : Mereology.CUM P) {m : α} (hMax : Mereology.isMaximal P m) (hOnly : ∀ (x' : α), maxNonOverlap P x' → x' = m) : QForall P Q ↔ Q m

DNG for plural complements (CUM with a maximal element).

When P is CUM and has a maximal element m, Q_∀(P)(Q) reduces to Q(m).

This is the [−dist] case: @cite{haslinger-etal-2025-nllt} eq. (30a). The unique maximal element of a CUM predicate is the join of all P-elements — the "maximal plurality."

theorem Semantics.Quantification.UnifiedUniversal.maxNonOverlap_unique_of_cum {α : Type u_1} [SemilatticeSup α] {P : α → Prop} (hCum : Mereology.CUM P) {x y : α} (hx : maxNonOverlap P x) (hy : maxNonOverlap P y) : x = y

In a CUM predicate, maxNonOverlap elements are unique (= the max).

This derives hOnly for dng_cum: if P is CUM, any two maxNonOverlap elements must be equal (both are isMaximal, and CUM predicates have at most one maximal element).

theorem Semantics.Quantification.UnifiedUniversal.dng_cum' {α : Type u_1} [SemilatticeSup α] {P Q : α → Prop} (hCum : Mereology.CUM P) {m : α} (hMax : Mereology.isMaximal P m) : QForall P Q ↔ Q m

Combined DNG-PL: for CUM predicates with a maximal element, Q_∀(P)(Q) ↔ Q(m), without needing to supply hOnly separately.

theorem Semantics.Quantification.UnifiedUniversal.QForall_eq_standardGQ {α : Type u_1} [PartialOrder α] {P Q : α → Prop} (hAtoms : ∀ (x : α), P x → Mereology.Atom x) (hDisj : ∀ (x y : α), P x → P y → Mereology.Overlap x y → x = y) : QForall P Q ↔ ∀ (x : α), P x → Q x

Q_∀ on an atomic restrictor is equivalent to the standard generalized quantifier ∀x[P(x) → Q(x)], which is the denotation of every_sem in Quantifier.lean.

This theorem bridges the mereological Q_∀ to the flat-domain GQ: the two coincide when the restrictor has no mereological structure (all elements are atoms with no overlap).

@[implicit_reducible]

instance Semantics.Quantification.UnifiedUniversal.decidableOverlap {α : Type u_1} [Fintype α] [PartialOrder α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (x y : α) : Decidable (Mereology.Overlap x y)

Decidable overlap on a finite type with decidable ≤.

Equations

• Semantics.Quantification.UnifiedUniversal.decidableOverlap x y = Fintype.decidableExistsFintype

def Semantics.Quantification.UnifiedUniversal.maxNonOverlapB {α : Type u_1} [Fintype α] [PartialOrder α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (P : α → Bool) (x : α) : Bool

Bool-valued maxNonOverlap for computation.

Equations

• Semantics.Quantification.UnifiedUniversal.maxNonOverlapB P x = (P x && decide (∀ (y : α), P y = true → Mereology.Overlap x y → y ≤ x))

def Semantics.Quantification.UnifiedUniversal.QForallDec {α : Type u_1} [Fintype α] [PartialOrder α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (P Q : α → Bool) : Bool

Computable Q_∀ over a Fintype.

Equations

• Semantics.Quantification.UnifiedUniversal.QForallDec P Q = decide (∀ (x : α), Semantics.Quantification.UnifiedUniversal.maxNonOverlapB P x = true → Q x = true)