[HHR+25]: A unified semantics for universal quantifiers

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

Main finding

A single morpheme Q_∀ derives both distributive and non-distributive readings: the reading falls out from the algebraic structure of the restrictor (atoms → [+dist], a sum-closed/cumulative restrictor with a single maximal element → [−dist]). This derives the empirical Distributivity–Number Generalization (DNG): a singular count complement forces [+dist], a plural complement forces [−dist] — a strengthening of [Gil95]'s implicational universal (cf. also [Win01]). The distributive readings that [−dist] forms additionally allow come from a VP-level distributivity operator ([Lin87b]), not from the quantifier.

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

• ONE_∅: non-overlap (English every)
• ONE_AT: atomicity, stronger (English each) — following [FF20]

One-form languages (Dagara, Moore, Gourmantchema, Wolof, Syrian Arabic) use bare Q_∀, whose reading is fixed by complement number.

Relation to [HRSW25] (S&P)

The S&P paper (HaslingerEtAl2025.lean) shows distributivity ≠ maximality via tolerance. This NLLT paper shows distributivity ≠ number via Q_∀ + mereological structure. Complementary results from overlapping author sets; both consume Semantics/Plurality/Distributivity.lean substrate.

Theory-layer grounding

• UnifiedUniversal.lean: Q_∀, maxNonOverlap, DNG theorems.
• ONEModifiers.lean: ONE_∅, ONE_AT, English every/each decomposition.
• The 1-form/2-form UQProfile survey schema is study-local (single-paper data; the per-language forms derive from the determiner Fragments, not hand-typed).
• Bridge theorems connect Q_∀ to existing distMaximal/allViaForallH.

Cross-linguistic typology

The 1-form vs 2-form survey of [HHR+25] (1-form = its Table 2, 2-form = its Table 1). The schema is study-local — this is single-paper survey data — and the English/German forms are read off the determiner Fragments (every/all, jeder/alle) rather than restated.

inductive HaslingerHienEtAl2025.SystemType : Type

Whether a language lexicalizes one UQ lexeme whose reading is fixed by complement number (oneForm), or two distinct [+dist]/[−dist] forms (twoForm). [HHR+25]

• oneForm : SystemType

  Single UQ lexeme; reading determined by complement number.

• twoForm : SystemType

  Distinct [+dist] and [−dist] UQ lexemes.

@[implicit_reducible]

instance HaslingerHienEtAl2025.instDecidableEqSystemType : DecidableEq SystemType

Equations

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

def HaslingerHienEtAl2025.instReprSystemType.repr : SystemType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance HaslingerHienEtAl2025.instReprSystemType : Repr SystemType

Equations

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

structure HaslingerHienEtAl2025.UQProfile : Type

A language's DP-internal universal-quantifier inventory, as compiled in [HHR+25] (Table 1 for 2-form, Table 2 for 1-form languages).

• language : String

  Language name.

• family : String

  Genealogical family (the survey's label).

• systemType : SystemType

  1-form vs 2-form classification.

• distForm : String

  The [+dist] exponent; in 1-form languages, the sole UQ exponent.

• nonDistForm : String

  The [−dist] exponent; empty in 1-form languages.

• source : String

  Data provenance the survey attributes the row to.

def HaslingerHienEtAl2025.instReprUQProfile.repr : UQProfile → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance HaslingerHienEtAl2025.instReprUQProfile : Repr UQProfile

Equations

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

@[implicit_reducible]

instance HaslingerHienEtAl2025.instDecidableEqUQProfile : DecidableEq UQProfile

Equations

• HaslingerHienEtAl2025.instDecidableEqUQProfile = HaslingerHienEtAl2025.instDecidableEqUQProfile.decEq

def HaslingerHienEtAl2025.instDecidableEqUQProfile.decEq (x✝ x✝¹ : UQProfile) : Decidable (x✝ = x✝¹)

Equations

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

def HaslingerHienEtAl2025.UQProfile.isOneForm (p : UQProfile) : Prop

A 1-form language: one UQ lexeme, reading fixed by complement number.

Equations

• p.isOneForm = (p.systemType = HaslingerHienEtAl2025.SystemType.oneForm)

def HaslingerHienEtAl2025.UQProfile.isTwoForm (p : UQProfile) : Prop

A 2-form language: distinct [+dist]/[−dist] UQ lexemes.

Equations

• p.isTwoForm = (p.systemType = HaslingerHienEtAl2025.SystemType.twoForm)

@[implicit_reducible]

instance HaslingerHienEtAl2025.instDecidableIsOneForm (p : UQProfile) : Decidable p.isOneForm

Equations

• HaslingerHienEtAl2025.instDecidableIsOneForm p = id inferInstance

@[implicit_reducible]

instance HaslingerHienEtAl2025.instDecidableIsTwoForm (p : UQProfile) : Decidable p.isTwoForm

Equations

• HaslingerHienEtAl2025.instDecidableIsTwoForm p = id inferInstance

def HaslingerHienEtAl2025.typologicalSample : List UQProfile

Typological sample (inlined from the paper's Tables 1–2). The English/German [+dist]/[−dist] forms derive from the determiner Fragments; the rest are the survey's reported exponents.

Equations

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

theorem HaslingerHienEtAl2025.sample_size : typologicalSample.length = 15

The survey samples 15 languages.

theorem HaslingerHienEtAl2025.oneForm_count : (List.filter (fun (x : UQProfile) => x.systemType == SystemType.oneForm) typologicalSample).length = 5

1-form count (Table 2): Dagara, Moore, Gourmantchema, Wolof, Syrian Arabic.

theorem HaslingerHienEtAl2025.twoForm_count : (List.filter (fun (x : UQProfile) => x.systemType == SystemType.twoForm) typologicalSample).length = 10

2-form count (Table 1): English, German, Hindi, Russian, Imbabura Quichua, Turkish, Basque, Telugu, Hausa, Logoori.

theorem HaslingerHienEtAl2025.oneForm_twoForm_partition : (List.filter (fun (x : UQProfile) => x.systemType == SystemType.oneForm) typologicalSample).length + (List.filter (fun (x : UQProfile) => x.systemType == SystemType.twoForm) typologicalSample).length = typologicalSample.length

Every sampled language is either 1-form or 2-form — the classification is an exhaustive partition (no row is neither).

Finite model: the DNG on a 3-atom domain

Verify the DNG on a concrete flat 3-element domain (the SG case), where every element is an atom and distinct elements are disjoint.

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.

instance HaslingerHienEtAl2025.instIsAtomicDomainStudent : Mereology.IsAtomicDomain Student

The flat Student order is the canonical IsAtomicDomain: its atomicity and disjointness now come from the shared Mereology machinery, not bespoke proofs.

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

All Students are atoms — derived from the IsAtomicDomain instance.

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

Distinct Students don't overlap — derived from the IsAtomicDomain instance.

theorem HaslingerHienEtAl2025.dng_sg_concrete : 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 : ¬Quantification.UnifiedUniversal.QForall (fun (x : Student) => True) passed

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

Bridge to tolerance-based distributivity

Connect Q_∀ on atoms to distMaximal from Distributivity.lean. For an atomic restrictor P, Q_∀(P)(Q) reduces to ∀x, P(x) → Q(x) (by dng_atoms), which is exactly distMaximal P X w. The bridge is a semantic equivalence on the shared domain, not a definitional equality (different signatures: Q_∀ over PartialOrder, distMaximal over Finset Atom).

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.distMaximal P X w

Q_∀ on atoms is semantically equivalent to distMaximal: both say "Q holds of every atom in the restrictor."

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.allSatisfy P X w ↔ ∀ a ∈ X, P a w

Q_∀ on a cumulative restrictor is equivalent to allSatisfy over its atoms: both say "Q holds of every atom in the group."

English every/each/all decomposition

The English decomposition from [HHR+25] (eq. 79):

• 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} : Quantification.ONEModifiers.eachPresup P Q → 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 : Quantification.ONEModifiers.everyPresup P Q) : Quantification.UnifiedUniversal.QForall P Q

every entails all (ONE_∅ ⊂ no presupposition).

theorem HaslingerHienEtAl2025.every_is_distributive {α : Type u_1} [PartialOrder α] {P Q : α → Prop} (hONE : Quantification.ONEModifiers.ONE_empty P) : 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} : Quantification.ONEModifiers.eachPresup P Q → Quantification.ONEModifiers.everyPresup P Q ∧ Quantification.UnifiedUniversal.QForall P Q

The full chain: each ⊂ every ⊂ all.

German fragment consistency

Verify 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 a cumulative restrictor = allViaForallH
• jeweils (+dist, −max) = distTolerant (orthogonal to Q_∀)

theorem HaslingerHienEtAl2025.jeder_matches_ONE_prediction : 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 : German.Distributives.alleEntry.distMaxClass = Semantics.Plurality.Distributivity.DistMaxClass.nonDistMax

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

theorem HaslingerHienEtAl2025.german_dng_explained : German.Distributives.jederEntry.distMaxClass.isDistributive ∧ ¬German.Distributives.alleEntry.distMaxClass.isDistributive

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

English fragment consistency

Connect the Q_∀ decomposition to the English distributive Fragment's DistMaxClass and atomicity entries in Fragments/English/Distributives.lean, exactly as the German section derives from Fragments/German/Distributives.lean.

The NLLT decomposition predicts:

• each = Q_∀[ONE_∅[ONE_AT]] → [+dist] (atoms), [+max]
• every = Q_∀[ONE_∅] → [+dist] (non-overlap), [+max]
• all = bare Q_∀ → [−dist] (cumulative complement), [+max]

These predictions are read off the Fragment's entries (no local restipulation).

theorem HaslingerHienEtAl2025.each_matches_ONE_AT_prediction : English.Distributives.eachEntry.distMaxClass = Semantics.Plurality.Distributivity.DistMaxClass.distMax

English each's DistMaxClass matches the ONE_AT prediction (+dist, +max).

theorem HaslingerHienEtAl2025.every_matches_ONE_empty_prediction : English.Distributives.everyEntry.distMaxClass = Semantics.Plurality.Distributivity.DistMaxClass.distMax

English every's DistMaxClass matches the ONE_∅ prediction (+dist, +max).

theorem HaslingerHienEtAl2025.all_matches_bare_QForall_prediction : English.Distributives.allEntry.distMaxClass = Semantics.Plurality.Distributivity.DistMaxClass.nonDistMax

English all's DistMaxClass matches the bare Q_∀ prediction (−dist, +max).

theorem HaslingerHienEtAl2025.each_every_same_class_different_atomicity : English.Distributives.eachEntry.distMaxClass = English.Distributives.everyEntry.distMaxClass ∧ English.Distributives.eachEntry.atomicityPresup = true ∧ English.Distributives.everyEntry.atomicityPresup = false

each and every share a DistMaxClass (both +dist, +max), so this axis cannot separate them. The NLLT contrast lives in the atomicity presupposition (ONE_AT), recorded by the Fragment's atomicityPresup field — exactly the distinction that blocks each ten minutes below. [HHR+25] §6.2.

The *each ten minutes test

ONE_AT explains the ungrammaticality of each ten minutes: time intervals are not atoms, so the atomicity presupposition fails. every ten minutes is fine — intervals can be non-overlapping (satisfying ONE_∅) without being atomic. Following [FF20]; [HHR+25] §6.2.

theorem HaslingerHienEtAl2025.each_ten_minutes_blocked {α : Type u_1} [PartialOrder α] {P : α → Prop} (hNonAtomic : ∃ (x : α), P x ∧ ¬Mereology.Atom x) (hONE_AT : 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).

Bridge to the canonical generalized quantifier

On an atomic restrictor sort (Mereology.IsAtomicDomain α), Q_∀ is the canonical universal generalized quantifier every_sem (λR S. ∀x. R x → S x). The instance discharges both the atomicity and the disjointness conditions of QForall_eq_standardGQ, so the bridge is automatic — and *each ten minutes is exactly the case where the interval sort has no IsAtomicDomain instance. This snaps the mereological Q_∀ tower onto the shared ∀-denotation that the Barwise–Cooper every_sem, the Lindström everyDet.toGQ, and Sauerland's JE∘DER already meet at, with the atomicity presupposition realized as a typeclass on the sort rather than a side condition.

theorem HaslingerHienEtAl2025.QForall_eq_every_sem {α : Type u_1} [PartialOrder α] [Mereology.IsAtomicDomain α] {P Q : α → Prop} : Quantification.UnifiedUniversal.QForall P Q ↔ Quantification.every_sem P Q

On an atomic restrictor sort, Q_∀ is the canonical universal generalized quantifier every_sem. The [IsAtomicDomain α] instance is used — it discharges both hypotheses of QForall_eq_standardGQ. [HHR+25] eq. (30b).