English universal/distributive determiners

[HHR+25]

Fragment entries for the English DP-internal universal quantifiers each, every, and all, grounded in the theory-layer operators from Semantics/Plurality/. Parallel to Fragments/German/Distributives.lean.

Inventory

Form	Semantics	[±dist] / [±max]	ONE-stack ([HHR+25] eq. 79)
each	distMaximal	+dist, +max	Q_∀[ONE_∅[ONE_AT]] (atomicity presupposition)
every	distMaximal	+dist, +max	Q_∀[ONE_∅] (non-overlap presupposition)
all	allViaForallH	−dist, +max	bare Q_∀

each and every share their DistMaxClass (both +dist, +max) — the distinction between them is the atomicity presupposition (ONE_AT), which DistMaxClass does not record but the atomicityPresup field does. This is the contrast that blocks each ten minutes while allowing every ten minutes (intervals satisfy non-overlap but not atomicity).

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

⟦each⟧ = distMaximal: distribute P to every atom. The atomicity presupposition (ONE_AT) is a felicity condition, not part of the asserted content. [HHR+25] eq. (79c).

Equations

• English.Distributives.eachSem P = Semantics.Plurality.distMaximal P

def English.Distributives.everySem {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] : Finset Atom → W → Prop

⟦every⟧ = distMaximal: same asserted content as each; differs only in carrying the weaker non-overlap presupposition (ONE_∅). [HHR+25] eq. (79b).

Equations

• English.Distributives.everySem P = Semantics.Plurality.distMaximal P

def English.Distributives.allSem {Atom : Type u_1} {W : Type u_2} [Fintype Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : Prop

⟦all⟧ = allViaForallH: bare universal, maximization without distributive inferences. [HHR+25] eq. (79a); [KS21b] §5.3.

Equations

• English.Distributives.allSem P x w = Semantics.Plurality.Trivalent.allViaForallH P x w

structure English.Distributives.DistributiveEntry : Type

An English universal determiner with grounded distributivity classification. atomicityPresup records the ONE_AT (atomicity) felicity condition that distinguishes each from every — a distinction DistMaxClass collapses.

• form : String

  Surface form.

• gloss : String

  English gloss.

• atomicityPresup : Bool

  Carries the atomicity presupposition (ONE_AT)? each does, every does not.

• distMaxClass : Semantics.Plurality.Distributivity.DistMaxClass

  Distributivity/maximality classification.

@[implicit_reducible]

instance English.Distributives.instReprDistributiveEntry : Repr DistributiveEntry

Equations

• English.Distributives.instReprDistributiveEntry = { reprPrec := English.Distributives.instReprDistributiveEntry.repr }

def English.Distributives.instReprDistributiveEntry.repr : DistributiveEntry → ℕ → Std.Format

Equations

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

def English.Distributives.eachEntry : DistributiveEntry

each: +dist, +max, with the atomicity presupposition.

Equations

• English.Distributives.eachEntry = { form := "each", gloss := "each", atomicityPresup := true, distMaxClass := Semantics.Plurality.Distributivity.DistMaxClass.distMax }

def English.Distributives.everyEntry : DistributiveEntry

every: +dist, +max, with only the non-overlap presupposition.

Equations

• English.Distributives.everyEntry = { form := "every", gloss := "every", atomicityPresup := false, distMaxClass := Semantics.Plurality.Distributivity.DistMaxClass.distMax }

def English.Distributives.allEntry : DistributiveEntry

all: −dist, +max, bare Q_∀.

Equations

• English.Distributives.allEntry = { form := "all", gloss := "all", atomicityPresup := false, distMaxClass := Semantics.Plurality.Distributivity.DistMaxClass.nonDistMax }

theorem English.Distributives.each_eq_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.distMaximal P

each's semantics IS distMaximal.

theorem English.Distributives.every_eq_distMaximal {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] : everySem P = Semantics.Plurality.distMaximal P

every's semantics IS distMaximal (same asserted content as each).

theorem English.Distributives.all_iff_allSatisfy {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] [Fintype Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : allSem P x w ↔ Semantics.Plurality.allSatisfy P x w

all reduces to a simple universal check on atoms.

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

each and every share a DistMaxClass (both +dist, +max) but differ in the atomicity presupposition: this is the every-vs-each contrast that DistMaxClass alone cannot express. [HHR+25] §6.2.