@cite{haslinger-etal-2025-nllt}: A Unified Semantics for Universal Quantifiers

@cite{haslinger-etal-2025-nllt}

Empirical data and theoretical verification for "A unified semantics for distributive and non-distributive universal quantifiers across languages" (NLLT 43, 2025).

Main Finding

A single morpheme Q_∀ can derive both distributive and non-distributive readings: the reading falls out from the algebraic structure of the restrictor (atoms → [+dist], CUM with max → [−dist]). This is the Distributivity-Number Generalization (DNG).

Two-form languages (English, German, Hindi) add a syntactic head ONE below Q_∀ that restricts the complement via presupposition:

• ONE_∅: non-overlap (English every)
• ONE_AT: atomicity (English each)

One-form languages (Dagara, Moore, Wolof, Arabic) use bare Q_∀.

Relation to @cite{haslinger-etal-2025} (S&P)

The S&P paper (existing HaslingerEtAl2025.lean) shows distributivity ≠ maximality via tolerance. This NLLT paper shows distributivity ≠ number via Q_∀ + mereological structure. Complementary results from overlapping author sets.

Theory-Layer Grounding

• UnifiedUniversal.lean: Q_∀, maxNonOverlap, DNG theorems
• ONEModifiers.lean: ONE_∅, ONE_AT, English every/each decomposition
• Bridge theorems below connect Q_∀ to existing distMaximal/allViaForallH

inductive HaslingerHienEtAl2025.UQSystemType : Type

Classification of UQ systems: 1-form (single UQ) vs 2-form (dist/non-dist split).

• oneForm : UQSystemType
• twoForm : UQSystemType

@[implicit_reducible]

instance HaslingerHienEtAl2025.instDecidableEqUQSystemType : DecidableEq UQSystemType

Equations

• HaslingerHienEtAl2025.instDecidableEqUQSystemType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance HaslingerHienEtAl2025.instReprUQSystemType : Repr UQSystemType

Equations

• HaslingerHienEtAl2025.instReprUQSystemType = { reprPrec := HaslingerHienEtAl2025.instReprUQSystemType.repr }

def HaslingerHienEtAl2025.instReprUQSystemType.repr : UQSystemType → ℕ → Std.Format

Equations

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

structure HaslingerHienEtAl2025.UQLanguageEntry : Type

A language's universal quantifier inventory.

• language : String
• systemType : UQSystemType
• distForm : String

  The [+dist] form (or the sole form in 1-form languages)

• nonDistForm : String

  The [−dist] form (empty in 1-form languages)

• family : String

  Language family

@[implicit_reducible]

instance HaslingerHienEtAl2025.instReprUQLanguageEntry : Repr UQLanguageEntry

Equations

• HaslingerHienEtAl2025.instReprUQLanguageEntry = { reprPrec := HaslingerHienEtAl2025.instReprUQLanguageEntry.repr }

def HaslingerHienEtAl2025.instReprUQLanguageEntry.repr : UQLanguageEntry → ℕ → Std.Format

Equations

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

def HaslingerHienEtAl2025.typologicalSample : List UQLanguageEntry

Typological sample from NLLT Table 1 and surrounding discussion.

Equations

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

theorem HaslingerHienEtAl2025.oneForm_count : (List.filter (fun (x : UQLanguageEntry) => x.systemType == UQSystemType.oneForm) typologicalSample).length = 6

1-form count

theorem HaslingerHienEtAl2025.twoForm_count : (List.filter (fun (x : UQLanguageEntry) => x.systemType == UQSystemType.twoForm) typologicalSample).length = 5

2-form count

Verify DNG on a concrete flat 3-element domain (SG case) and a small semilattice (PL case).

inductive HaslingerHienEtAl2025.Student : Type

Three students: a flat domain where every element is an atom.

• alice : Student
• bob : Student
• carol : Student

@[implicit_reducible]

instance HaslingerHienEtAl2025.instDecidableEqStudent : DecidableEq Student

Equations

• HaslingerHienEtAl2025.instDecidableEqStudent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def HaslingerHienEtAl2025.instReprStudent.repr : Student → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance HaslingerHienEtAl2025.instReprStudent : Repr Student

Equations

• HaslingerHienEtAl2025.instReprStudent = { reprPrec := HaslingerHienEtAl2025.instReprStudent.repr }

@[implicit_reducible]

instance HaslingerHienEtAl2025.instFintypeStudent : Fintype Student

Equations

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

@[implicit_reducible]

instance HaslingerHienEtAl2025.instPartialOrderStudent : PartialOrder Student

Flat discrete order: x ≤ y ↔ x = y. Every element is an atom.

Equations

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

def HaslingerHienEtAl2025.passed : Student → Prop

"passed the exam"

Equations

• HaslingerHienEtAl2025.passed HaslingerHienEtAl2025.Student.alice = True
• HaslingerHienEtAl2025.passed HaslingerHienEtAl2025.Student.bob = True
• HaslingerHienEtAl2025.passed HaslingerHienEtAl2025.Student.carol = False

theorem HaslingerHienEtAl2025.student_atoms (x : Student) : (fun (x : Student) => True) x → Mereology.Atom x

In a flat order, all elements are atoms.

theorem HaslingerHienEtAl2025.student_disjoint (x y : Student) : (fun (x : Student) => True) x → (fun (x : Student) => True) y → Mereology.Overlap x y → x = y

In a flat order, distinct elements don't overlap.

theorem HaslingerHienEtAl2025.dng_sg_concrete : Semantics.Quantification.UnifiedUniversal.QForall (fun (x : Student) => True) passed ↔ ∀ (x : Student), passed x

DNG-SG: Q_∀ on a flat domain distributes to each element.

theorem HaslingerHienEtAl2025.dng_sg_false : ¬Semantics.Quantification.UnifiedUniversal.QForall (fun (x : Student) => True) passed

Q_∀(student)(passed) is false: Carol didn't pass.

Connect Q_∀ on atoms to distMaximal from Distributivity.lean.

The key insight: for an atomic restrictor P, Q_∀(P)(Q) reduces to ∀x, P(x) → Q(x) (by dng_atoms). And distMaximal Q X w = true iff ∀a ∈ X, Q(a)(w) = true. These are the same universal structure.

The bridge is not a definitional equality (different type signatures: Q_∀ works over PartialOrder, distMaximal over Finset Atom × W → Bool) but a semantic equivalence on the shared domain.

theorem HaslingerHienEtAl2025.QForall_atoms_iff_distMaximal {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (X : Finset Atom) (w : W) : (∀ a ∈ X, P a w) ↔ Semantics.Plurality.Distributivity.distMaximal P X w

Q_∀ on atoms is semantically equivalent to distMaximal.

Both say: "Q holds of every atom in the restrictor." Q_∀ gets there via maxNonOverlap (trivial for atoms). distMaximal gets there via ∀a ∈ X, P(a)(w).

theorem HaslingerHienEtAl2025.QForall_cum_iff_allSatisfy {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (X : Finset Atom) (w : W) : Semantics.Plurality.Distributivity.allSatisfy P X w ↔ ∀ a ∈ X, P a w

Q_∀ on a CUM restrictor is semantically equivalent to allSatisfy applied to the maximal element (when it exists).

Both say: "Q holds of every atom in the group." The difference is structural: Q_∀ reaches this via maxNonOverlap selecting the unique max, while allSatisfy directly iterates.

The English decomposition from the paper: - all = Q_∀ (bare, no ONE) - every = Q_∀ + ONE_∅ - each = Q_∀ + ONE_∅ + ONE_AT

Verified: each ⊂ every ⊂ all in presuppositional strength. 

theorem HaslingerHienEtAl2025.each_stronger_than_every {α : Type u_1} [PartialOrder α] {P Q : α → Prop} : Semantics.Quantification.ONEModifiers.eachPresup P Q → Semantics.Quantification.ONEModifiers.everyPresup P Q

each entails every (ONE_AT ⊂ ONE_∅)

theorem HaslingerHienEtAl2025.every_stronger_than_all {α : Type u_1} [PartialOrder α] {P Q : α → Prop} (h : Semantics.Quantification.ONEModifiers.everyPresup P Q) : Semantics.Quantification.UnifiedUniversal.QForall P Q

every entails all (ONE_∅ ⊂ no presupposition)

theorem HaslingerHienEtAl2025.every_is_distributive {α : Type u_1} [PartialOrder α] {P Q : α → Prop} (hONE : Semantics.Quantification.ONEModifiers.ONE_empty P) : Semantics.Quantification.UnifiedUniversal.QForall P Q ↔ ∀ (x : α), P x → Q x

When ONE_∅ holds, Q_∀ distributes to atoms.

theorem HaslingerHienEtAl2025.presup_chain {α : Type u_1} [PartialOrder α] {P Q : α → Prop} : Semantics.Quantification.ONEModifiers.eachPresup P Q → Semantics.Quantification.ONEModifiers.everyPresup P Q ∧ Semantics.Quantification.UnifiedUniversal.QForall P Q

The full chain: each ⊂ every ⊂ all

Verify that the German fragment entries in Fragments/German/Distributives.lean are consistent with the Q_∀ decomposition.

- jeder (+dist, +max) = Q_∀[ONE_∅] on atoms = distMaximal ✓
- alle (-dist, +max) = bare Q_∀ on CUM = allViaForallH ✓
- jeweils (+dist, -max) = distTolerant (orthogonal to Q_∀) ✓ 

theorem HaslingerHienEtAl2025.jeder_matches_ONE_prediction : Fragments.German.Distributives.jederEntry.distMaxClass = Semantics.Plurality.Distributivity.DistMaxClass.distMax

German jeder's DistMaxClass matches the ONE_∅ prediction: [+dist] (ONE forces atom complement) and [+max] (atoms are vacuously maximal).

theorem HaslingerHienEtAl2025.alle_matches_bare_QForall : Fragments.German.Distributives.alleEntry.distMaxClass = Semantics.Plurality.Distributivity.DistMaxClass.nonDistMax

German alle's DistMaxClass matches bare Q_∀ prediction: [−dist] (no ONE, CUM complement → collective) and [+max].

theorem HaslingerHienEtAl2025.german_dng_explained : Fragments.German.Distributives.jederEntry.distMaxClass.isDistributive = true ∧ Fragments.German.Distributives.alleEntry.distMaxClass.isDistributive = false

The DNG explains the dist/non-dist split between jeder and alle: same Q_∀ semantics, different complement structure.

Connect the Q_∀ decomposition to the English fragment's DistMaxClass and semantic entries in Fragments/English/Determiners.lean.

The NLLT decomposition predicts:
- each = Q_∀[ONE_AT] → [+dist] (atoms), [+max] (atoms vacuously maximal)
- every = Q_∀[ONE_∅] → [+dist] (non-overlap), [+max]
- all = bare Q_∀ → [−dist] (CUM complement), [+max]

These predictions match the Fragment's DistMaxClass assignments. 

def HaslingerHienEtAl2025.each_distMaxClass : Semantics.Plurality.Distributivity.DistMaxClass

English each's DistMaxClass: +dist (ONE_AT forces atom complement), +max. The classification is local to this study because it lifts fragment lexical-class metadata into the @cite{haslinger-etal-2025-nllt} DistMaxClass typology, which is paper-specific.

Equations

• HaslingerHienEtAl2025.each_distMaxClass = Semantics.Plurality.Distributivity.DistMaxClass.distMax

def HaslingerHienEtAl2025.every_distMaxClass : Semantics.Plurality.Distributivity.DistMaxClass

English every's DistMaxClass: +dist (ONE_∅ forces non-overlap), +max.

Equations

• HaslingerHienEtAl2025.every_distMaxClass = Semantics.Plurality.Distributivity.DistMaxClass.distMax

def HaslingerHienEtAl2025.all_distMaxClass : Semantics.Plurality.Distributivity.DistMaxClass

English all's DistMaxClass: −dist (CUM complement), +max.

Equations

• HaslingerHienEtAl2025.all_distMaxClass = Semantics.Plurality.Distributivity.DistMaxClass.nonDistMax

def HaslingerHienEtAl2025.eachSem {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] : Finset Atom → W → Prop

English each: distributes via distMaximal.

Equations

• HaslingerHienEtAl2025.eachSem P = Semantics.Plurality.Distributivity.distMaximal P

theorem HaslingerHienEtAl2025.each_matches_ONE_AT_prediction : each_distMaxClass = Semantics.Plurality.Distributivity.DistMaxClass.distMax

English each's DistMaxClass matches the ONE_AT prediction: [+dist] (ONE_AT forces atom complement) and [+max].

theorem HaslingerHienEtAl2025.every_matches_ONE_empty_prediction : every_distMaxClass = Semantics.Plurality.Distributivity.DistMaxClass.distMax

English every's DistMaxClass matches the ONE_∅ prediction: [+dist] (ONE_∅ forces non-overlap) and [+max].

theorem HaslingerHienEtAl2025.all_matches_bare_QForall_prediction : all_distMaxClass = Semantics.Plurality.Distributivity.DistMaxClass.nonDistMax

English all's DistMaxClass matches bare Q_∀ prediction: [−dist] (no ONE, CUM complement → collective) and [+max].

theorem HaslingerHienEtAl2025.each_every_same_distmax_different_presup : each_distMaxClass = every_distMaxClass

The NLLT theory predicts each ⊂ every in presuppositional strength. Both share DistMaxClass (both are +dist, +max), but each additionally requires atomicity (ONE_AT). This distinction doesn't show up in DistMaxClass (which collapses each and every) but IS captured by the Q_∀+ONE decomposition.

theorem HaslingerHienEtAl2025.eachSem_is_distMaximal {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] : eachSem P = Semantics.Plurality.Distributivity.distMaximal P

eachSem = distMaximal is the computational counterpart of Q_∀[ONE_AT]: both distribute over atoms. Q_∀[ONE_AT] ⊢ ∀x, P(x) → Q(x) (by every_distributes), and distMaximal checks ∀a ∈ X, P(a)(w).

ONE_AT explains the ungrammaticality of *each ten minutes: time intervals are not atoms, so ONE_AT fails.

"Every ten minutes" is fine: intervals can be non-overlapping
(satisfying ONE_∅) without being atomic. 

theorem HaslingerHienEtAl2025.each_ten_minutes_blocked {α : Type u_1} [PartialOrder α] {P : α → Prop} (hNonAtomic : ∃ (x : α), P x ∧ ¬Mereology.Atom x) (hONE_AT : Semantics.Quantification.ONEModifiers.ONE_AT P) : False

ONE_AT rejects non-atomic predicates. every ten minutes is fine (ONE_∅ accepts non-overlapping intervals), but each ten minutes is out (ONE_AT requires atoms).