ONE Modifiers for Distributive Universal Quantifiers

[HHR+25]

In 2-form languages (English, German, Hindi, ...), distributive [+dist] UQ forms contain an additional syntactic head ONE below Q_∀ that restricts the complement to atomic or non-overlapping individuals.

Two variants:

• ONE_∅: presupposes non-overlap among restrictor elements. English every = Q_∀[ONE_∅].
• ONE_AT: presupposes atomicity (stronger than non-overlap). English each = Q_∀[ONE_∅[ONE_AT]].

Non-distributive [−dist] forms like all are bare Q_∀ with no ONE.

The ONE_AT atomicity presupposition explains why each ten minutes is ungrammatical: intervals are not atoms, so ONE_AT fails.

ONE Presuppositional Modifiers

structure Quantification.ONEModifiers.ONE_empty {α : Type u_1} [PartialOrder α] (P : α → Prop) : Prop

ONE_∅: presupposes that the restrictor contains at least two elements and that no two distinct elements overlap.

[HHR+25] eq. (75a): blocks plural complements (which contain overlapping sums) and forces [+dist] readings.

• has_two : ∃ (x : α) (y : α), P x ∧ P y ∧ x ≠ y

  At least two distinct elements in P

• pairwise_disjoint (x y : α) : P x → P y → Mereology.Overlap x y → x = y

  Pairwise non-overlap: distinct P-elements share no part

structure Quantification.ONEModifiers.ONE_AT {α : Type u_1} [PartialOrder α] (P : α → Prop) : Prop

ONE_AT: presupposes that the restrictor contains at least two elements and that all elements are atoms.

[HHR+25] eq. (75b): additionally blocks degree-interval predicates like ten minutes (which are non-atomic). This distinguishes each from every.

• has_two : ∃ (x : α) (y : α), P x ∧ P y ∧ x ≠ y

  At least two distinct elements in P

• all_atomic (x : α) : P x → Mereology.Atom x

  All P-elements are atoms

theorem Quantification.ONEModifiers.ONE_AT_implies_ONE_empty {α : Type u_1} [PartialOrder α] {P : α → Prop} (h : ONE_AT P) : ONE_empty P

ONE_AT implies ONE_∅: atoms are pairwise non-overlapping.

If x and y are both atoms and Overlap(x, y), then ∃z, z ≤ x ∧ z ≤ y. By atomicity of x: z = x. By atomicity of y: z = y. Hence x = y.

English UQ Decomposition

@[reducible, inline]

abbrev Quantification.ONEModifiers.allSem {α : Type u_1} [PartialOrder α] (P Q : α → Prop) : Prop

all = Q_∀: bare universal quantifier, no ONE modifier. Non-distributive with PL complements, distributive with SG complements. [HHR+25] eq. (79a).

Equations

• Quantification.ONEModifiers.allSem = Quantification.UnifiedUniversal.QForall

def Quantification.ONEModifiers.everyPresup {α : Type u_1} [PartialOrder α] (P Q : α → Prop) : Prop

every = Q_∀ + ONE_∅: universal quantifier with non-overlap presupposition. Always distributive (since ONE_∅ ensures all elements are maxNonOverlap). [HHR+25] eq. (79b).

Equations

• Quantification.ONEModifiers.everyPresup P Q = (Quantification.ONEModifiers.ONE_empty P ∧ Quantification.UnifiedUniversal.QForall P Q)

def Quantification.ONEModifiers.eachPresup {α : Type u_1} [PartialOrder α] (P Q : α → Prop) : Prop

each = Q_∀ + ONE_∅ + ONE_AT: universal quantifier with atomicity presupposition. Always distributive, and restricted to atomic predicates. [HHR+25] eq. (79c).

Equations

• Quantification.ONEModifiers.eachPresup P Q = (Quantification.ONEModifiers.ONE_AT P ∧ Quantification.UnifiedUniversal.QForall P Q)

theorem Quantification.ONEModifiers.each_entails_every {α : Type u_1} [PartialOrder α] {P Q : α → Prop} (h : eachPresup P Q) : everyPresup P Q

each entails every: ONE_AT is stronger than ONE_∅.

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

When ONE_empty holds, QForall reduces to pointwise universal. This is the core semantic consequence of the ONE_∅ presupposition.

theorem Quantification.ONEModifiers.ONE_AT_of_isAtomicDomain {α : Type u_1} [PartialOrder α] [Mereology.IsAtomicDomain α] {P : α → Prop} (h2 : ∃ (x : α) (y : α), P x ∧ P y ∧ x ≠ y) : ONE_AT P

On an atomic restrictor sort (Mereology.IsAtomicDomain), every restrictor satisfies ONE_AT's atomicity for free, so the presupposition reduces to the |P| > 1 cardinality condition. This connects the sort-level Mereology.IsAtomicDomain typeclass to the predicate-level ONE_AT structure — they are the same atomicity at two granularities, not parallel notions.