Haslinger, Hien, Rosina, Schmitt and Wurm (2025): A unified semantics for universal quantifiers

This file formalizes the single universal quantifier of Haslinger, Hien, Rosina, Schmitt and Wurm and the two presuppositional heads it combines with. The quantifier Q∀ applies its scope to every element of its restrictor that contains each restrictor element it overlaps. Whether the result distributes falls out of the restrictor's part structure. A restrictor of pairwise non-overlapping elements, such as the denotation of a singular count noun, makes Q∀ the ordinary universal quantifier, and a sum-closed plural restrictor with a largest element makes it a claim about that largest sum. This is the authors' Distributivity–Number Generalization, which strengthens the implicational universal of Gil. In two-form languages such as English and German a head ONE below the quantifier presupposes that the restrictor has more than one element and either is pairwise non-overlapping (English every) or consists of atoms (each, German jeder), following Fassi Fehri. The heads are partial identities on restrictors, so a presupposition failure is undefinedness rather than falsity.

Main definitions

• MaxNonOverlap, QForall: the quantifier's domain condition and the quantifier Q∀.
• oneEmpty, oneAt: the heads ONE_∅ and ONE_AT as partial functions on restrictors.
• over, every, each, jeder: the quantifier over a head, and the English and German structures as partial propositions.

Main results

• qForall_iff_of_disjoint, qForall_iff_of_supClosed: the two halves of the generalization.
• each_le_every: each is defined on fewer restrictors than every and agrees where both are.
• dng, qForall_twoStudents: the generalization on one algebra of students, and the vacuity of Q∀ over two students when three students are salient.
• every_tenMinutes_dom, each_tenMinutes_undefined: consecutive ten-minute intervals meet the presupposition of every and fail that of each.
• one_iff_singular: the English forms carrying a ONE head are the ones the fragment records as selecting the singular.
• judgment_rows: the paper's ten minutes judgments are the definedness predictions.

Implementation notes

The null individual is IsBot, the overlap relation Mereology.Overlap, and non-overlap of a restrictor Mereology.DisjointPred. The heads are PFun.res of the identity on the restrictors meeting their presupposition, and a structure applied to a restrictor and a scope is a Part Prop, defined when the head is. Time is measured in minutes, so ten minutes denotes the consecutive half-open intervals of ℕ. The survey of universal quantifiers in the paper's first two tables is not formalized here, since a survey of lexemes has no data format in the library.

References

• [HHR+25]
• [Gil95]
• [FF20]

The quantifier

def HaslingerHienEtAl2025.MaxNonOverlap {α : Type u_1} [PartialOrder α] (P : Set α) (x : α) : Prop

MaxNonOverlap P x says that x is a P-element containing every P-element it overlaps, the domain condition of the quantifier.

Equations

• HaslingerHienEtAl2025.MaxNonOverlap P x = (x ∈ P ∧ ∀ y ∈ P, Mereology.Overlap x y → y ≤ x)

def HaslingerHienEtAl2025.QForall {α : Type u_1} [PartialOrder α] (P Q : Set α) : Prop

The single universal quantifier Q∀ says that the scope holds of every maximal non-overlapping element of the restrictor.

Equations

• HaslingerHienEtAl2025.QForall P Q = ∀ (x : α), HaslingerHienEtAl2025.MaxNonOverlap P x → x ∈ Q

theorem HaslingerHienEtAl2025.MaxNonOverlap.mem {α : Type u_1} {P : Set α} {x : α} [PartialOrder α] (h : MaxNonOverlap P x) : x ∈ P

theorem HaslingerHienEtAl2025.MaxNonOverlap.maximal {α : Type u_1} {P : Set α} {x : α} [PartialOrder α] (hx : ¬IsBot x) (h : MaxNonOverlap P x) : Maximal (fun (x : α) => x ∈ P) x

A non-null maximal non-overlapping element is maximal in P.

theorem HaslingerHienEtAl2025.maxNonOverlap_iff_of_disjoint {α : Type u_1} {P : Set α} {x : α} [PartialOrder α] (h : Mereology.DisjointPred Mereology.Overlap P) : MaxNonOverlap P x ↔ x ∈ P

On a pairwise non-overlapping restrictor every element is maximal non-overlapping.

theorem HaslingerHienEtAl2025.qForall_iff_of_disjoint {α : Type u_1} {P Q : Set α} [PartialOrder α] (h : Mereology.DisjointPred Mereology.Overlap P) : QForall P Q ↔ ∀ x ∈ P, x ∈ Q

The singular half of the generalization says that on a pairwise non-overlapping restrictor the quantifier is the ordinary universal.

theorem HaslingerHienEtAl2025.qForall_iff_every {α : Type u_1} {P Q : Set α} [PartialOrder α] (h : Mereology.DisjointPred Mereology.Overlap P) : QForall P Q ↔ Quantifier.GQ.every P Q

On a pairwise non-overlapping restrictor the quantifier is the generalized quantifier every.

theorem HaslingerHienEtAl2025.maxNonOverlap_of_supClosed {α : Type u_1} {P : Set α} [SemilatticeSup α] {m : α} (hP : SupClosed P) (hm : Maximal (fun (x : α) => x ∈ P) m) : MaxNonOverlap P m

On a sum-closed restrictor a maximal element is maximal non-overlapping.

theorem HaslingerHienEtAl2025.maxNonOverlap_iff_of_supClosed {α : Type u_1} {P : Set α} {x : α} [SemilatticeSup α] {m : α} (h0 : ∀ x ∈ P, ¬IsBot x) (hP : SupClosed P) (hm : Maximal (fun (x : α) => x ∈ P) m) : MaxNonOverlap P x ↔ x = m

On a sum-closed restrictor without the null individual, the maximal non-overlapping element is the maximal element.

theorem HaslingerHienEtAl2025.qForall_iff_of_supClosed {α : Type u_1} {P Q : Set α} [SemilatticeSup α] {m : α} (h0 : ∀ x ∈ P, ¬IsBot x) (hP : SupClosed P) (hm : Maximal (fun (x : α) => x ∈ P) m) : QForall P Q ↔ m ∈ Q

The plural half of the generalization says that on a sum-closed restrictor without the null individual the quantifier applies the scope to the largest sum.

The heads ONE_∅ and ONE_AT

def HaslingerHienEtAl2025.OneEmptyDom {α : Type u_1} [PartialOrder α] (P : Set α) : Prop

The presupposition of ONE_∅ is that the restrictor has more than one element and no two of them overlap.

Equations

• HaslingerHienEtAl2025.OneEmptyDom P = (P.Nontrivial ∧ Mereology.DisjointPred Mereology.Overlap P)

def HaslingerHienEtAl2025.OneAtDom {α : Type u_1} [PartialOrder α] (P : Set α) : Prop

The presupposition of ONE_AT is that the restrictor has more than one element, all of them atoms.

Equations

• HaslingerHienEtAl2025.OneAtDom P = (P.Nontrivial ∧ ∀ x ∈ P, Mereology.Atom x)

theorem HaslingerHienEtAl2025.OneAtDom.oneEmptyDom {α : Type u_1} {P : Set α} [PartialOrder α] (h : OneAtDom P) : OneEmptyDom P

Distinct atoms never overlap, so the presupposition of ONE_AT entails that of ONE_∅.

def HaslingerHienEtAl2025.oneEmpty {α : Type u_1} [PartialOrder α] : Set α →. Set α

The head ONE_∅ is the identity on the restrictors meeting its presupposition.

Equations

• HaslingerHienEtAl2025.oneEmpty = PFun.res id {P : Set α | HaslingerHienEtAl2025.OneEmptyDom P}

def HaslingerHienEtAl2025.oneAt {α : Type u_1} [PartialOrder α] : Set α →. Set α

The head ONE_AT is the identity on the restrictors meeting its presupposition.

Equations

• HaslingerHienEtAl2025.oneAt = PFun.res id {P : Set α | HaslingerHienEtAl2025.OneAtDom P}

def HaslingerHienEtAl2025.over {α : Type u_1} [PartialOrder α] (h : Set α →. Set α) (P Q : Set α) : Part Prop

The quantifier over a head is defined when the head is defined on the restrictor, and is then the quantifier over the head's output.

Equations

• HaslingerHienEtAl2025.over h P Q = Part.map (fun (x : Set α) => HaslingerHienEtAl2025.QForall x Q) (h P)

def HaslingerHienEtAl2025.every {α : Type u_1} [PartialOrder α] (P Q : Set α) : Part Prop

English every is the quantifier over ONE_∅.

Equations

• HaslingerHienEtAl2025.every P Q = HaslingerHienEtAl2025.over HaslingerHienEtAl2025.oneEmpty P Q

def HaslingerHienEtAl2025.each {α : Type u_1} [PartialOrder α] (P Q : Set α) : Part Prop

English each is the quantifier over ONE_∅ over ONE_AT.

Equations

• HaslingerHienEtAl2025.each P Q = HaslingerHienEtAl2025.over (HaslingerHienEtAl2025.oneEmpty.comp HaslingerHienEtAl2025.oneAt) P Q

def HaslingerHienEtAl2025.jeder {α : Type u_1} [PartialOrder α] (P Q : Set α) : Part Prop

German jeder is the quantifier over ONE_AT alone, since German lacks ONE_∅.

Equations

• HaslingerHienEtAl2025.jeder P Q = HaslingerHienEtAl2025.over HaslingerHienEtAl2025.oneAt P Q

theorem HaslingerHienEtAl2025.every_dom {α : Type u_1} {P Q : Set α} [PartialOrder α] : (every P Q).Dom ↔ OneEmptyDom P

theorem HaslingerHienEtAl2025.jeder_dom {α : Type u_1} {P Q : Set α} [PartialOrder α] : (jeder P Q).Dom ↔ OneAtDom P

theorem HaslingerHienEtAl2025.each_dom {α : Type u_1} {P Q : Set α} [PartialOrder α] : (each P Q).Dom ↔ OneAtDom P

theorem HaslingerHienEtAl2025.each_le_every {α : Type u_1} {P Q : Set α} [PartialOrder α] : each P Q ≤ every P Q

Each is defined on fewer restrictors than every, and where both are defined they agree, since the presupposition of each entails that of every and both leave the bare quantifier.

theorem HaslingerHienEtAl2025.every_get_iff {α : Type u_1} {P Q : Set α} [PartialOrder α] (h : (every P Q).Dom) : (every P Q).get h ↔ ∀ x ∈ P, x ∈ Q

Under its presupposition every is the ordinary universal quantifier.

theorem HaslingerHienEtAl2025.each_get_iff {α : Type u_1} {P Q : Set α} [PartialOrder α] (h : (each P Q).Dom) : (each P Q).get h ↔ ∀ x ∈ P, x ∈ Q

Under its presupposition each is the ordinary universal quantifier.

Decidability on finite carriers

@[instance_reducible]

instance HaslingerHienEtAl2025.instDecidableOverlap_studies {α : Type u_1} [PartialOrder α] [Fintype α] [DecidableLE α] [DecidablePred IsBot] (x y : α) : Decidable (Mereology.Overlap x y)

Equations

• HaslingerHienEtAl2025.instDecidableOverlap_studies x y = Fintype.decidableExistsFintype

@[instance_reducible]

instance HaslingerHienEtAl2025.instDecidableAtom_studies {α : Type u_1} [PartialOrder α] [Fintype α] [DecidableLE α] [DecidablePred IsBot] (x : α) : Decidable (Mereology.Atom x)

Equations

• HaslingerHienEtAl2025.instDecidableAtom_studies x = { decide := decide ¬IsBot x && decide (∀ ⦃y : α⦄, ¬IsBot y → y ≤ x → x ≤ y), reflects_decide := ⋯ }

@[instance_reducible]

instance HaslingerHienEtAl2025.instDecidableMaximalMemSet_studies {α : Type u_1} {P : Set α} [PartialOrder α] [Fintype α] [DecidableLE α] [DecidablePred fun (x : α) => x ∈ P] (x : α) : Decidable (Maximal (fun (x : α) => x ∈ P) x)

Equations

• HaslingerHienEtAl2025.instDecidableMaximalMemSet_studies x = { decide := decide (x ∈ P) && decide (∀ ⦃y : α⦄, y ∈ P → x ≤ y → y ≤ x), reflects_decide := ⋯ }

@[instance_reducible]

instance HaslingerHienEtAl2025.instDecidablePredMaxNonOverlap {α : Type u_1} {P : Set α} [PartialOrder α] [Fintype α] [DecidableLE α] [DecidablePred IsBot] [DecidablePred fun (x : α) => x ∈ P] : DecidablePred (MaxNonOverlap P)

Equations

• HaslingerHienEtAl2025.instDecidablePredMaxNonOverlap x = { decide := decide (x ∈ P) && decide (∀ y ∈ P, Mereology.Overlap x y → y ≤ x), reflects_decide := ⋯ }

@[instance_reducible]

instance HaslingerHienEtAl2025.instDecidableQForall {α : Type u_1} {P Q : Set α} [PartialOrder α] [Fintype α] [DecidableLE α] [DecidablePred IsBot] [DecidablePred fun (x : α) => x ∈ P] [DecidablePred fun (x : α) => x ∈ Q] : Decidable (QForall P Q)

Equations

• HaslingerHienEtAl2025.instDecidableQForall = { decide := decide (∀ a ∈ Finset.univ, (fun (x : α) => HaslingerHienEtAl2025.MaxNonOverlap P x → x ∈ Q) a), reflects_decide := ⋯ }

@[instance_reducible]

instance HaslingerHienEtAl2025.instDecidableNontrivial_studies {α : Type u_1} {P : Set α} [Fintype α] [DecidableEq α] [DecidablePred fun (x : α) => x ∈ P] : Decidable P.Nontrivial

Equations

• HaslingerHienEtAl2025.instDecidableNontrivial_studies = { decide := decide (∃ a ∈ Finset.univ, (fun (x : α) => x ∈ P ∧ ∃ y ∈ P, x ≠ y) a), reflects_decide := ⋯ }

@[instance_reducible]

instance HaslingerHienEtAl2025.instDecidableOverlapPredOverlap_studies {α : Type u_1} {P : Set α} [PartialOrder α] [Fintype α] [DecidableEq α] [DecidableLE α] [DecidablePred IsBot] [DecidablePred fun (x : α) => x ∈ P] : Decidable (Mereology.OverlapPred Mereology.Overlap P)

Equations

• HaslingerHienEtAl2025.instDecidableOverlapPredOverlap_studies = { decide := decide (∃ a ∈ Finset.univ, (fun (x : α) => x ∈ P ∧ ∃ y ∈ P, x ≠ y ∧ Mereology.Overlap x y) a), reflects_decide := ⋯ }

@[instance_reducible]

instance HaslingerHienEtAl2025.instDecidableDisjointPredOverlap_studies {α : Type u_1} {P : Set α} [PartialOrder α] [Fintype α] [DecidableEq α] [DecidableLE α] [DecidablePred IsBot] [DecidablePred fun (x : α) => x ∈ P] : Decidable (Mereology.DisjointPred Mereology.Overlap P)

Equations

• HaslingerHienEtAl2025.instDecidableDisjointPredOverlap_studies = { decide := !decide (Mereology.OverlapPred Mereology.Overlap P), reflects_decide := ⋯ }

@[instance_reducible]

instance HaslingerHienEtAl2025.instDecidableOneEmptyDom {α : Type u_1} {P : Set α} [PartialOrder α] [Fintype α] [DecidableEq α] [DecidableLE α] [DecidablePred IsBot] [DecidablePred fun (x : α) => x ∈ P] : Decidable (OneEmptyDom P)

Equations

• HaslingerHienEtAl2025.instDecidableOneEmptyDom = { decide := decide P.Nontrivial && decide (Mereology.DisjointPred Mereology.Overlap P), reflects_decide := ⋯ }

@[instance_reducible]

instance HaslingerHienEtAl2025.instDecidableOneAtDom {α : Type u_1} {P : Set α} [PartialOrder α] [Fintype α] [DecidableEq α] [DecidableLE α] [DecidablePred IsBot] [DecidablePred fun (x : α) => x ∈ P] : Decidable (OneAtDom P)

Equations

• HaslingerHienEtAl2025.instDecidableOneAtDom = { decide := decide P.Nontrivial && decide (∀ x ∈ P, Mereology.Atom x), reflects_decide := ⋯ }

Three students

inductive HaslingerHienEtAl2025.Student : Type

Three salient students; a plurality is a nonempty finset and the null individual is ∅.

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

@[instance_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.

@[instance_reducible]

instance HaslingerHienEtAl2025.instReprStudent : Repr Student

Equations

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

@[instance_reducible]

instance HaslingerHienEtAl2025.instFintypeStudent : Fintype Student

Equations

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

@[instance_reducible]

instance HaslingerHienEtAl2025.instInhabitedStudent : Inhabited Student

Equations

• HaslingerHienEtAl2025.instInhabitedStudent = { default := HaslingerHienEtAl2025.instInhabitedStudent.default }

def HaslingerHienEtAl2025.students : Set (Finset Student)

The plural restrictor students holds of the nonempty pluralities and is closed under sum.

Equations

• HaslingerHienEtAl2025.students = {s : Finset HaslingerHienEtAl2025.Student | s.Nonempty}

def HaslingerHienEtAl2025.student : Set (Finset Student)

The singular restrictor student holds of the atoms.

Equations

• HaslingerHienEtAl2025.student = {s : Finset HaslingerHienEtAl2025.Student | s.card = 1}

def HaslingerHienEtAl2025.twoStudents : Set (Finset Student)

The restrictor two students holds of the pairs.

Equations

• HaslingerHienEtAl2025.twoStudents = {s : Finset HaslingerHienEtAl2025.Student | s.card = 2}

def HaslingerHienEtAl2025.met : Set (Finset Student)

The collective scope met, true of the whole group only.

Equations

• HaslingerHienEtAl2025.met = {s : Finset HaslingerHienEtAl2025.Student | s = Finset.univ}

@[instance_reducible]

instance HaslingerHienEtAl2025.instDecidablePredFinsetStudentMemSetStudents : DecidablePred fun (x : Finset Student) => x ∈ students

Equations

• HaslingerHienEtAl2025.instDecidablePredFinsetStudentMemSetStudents s = { decide := decide (∃ a ∈ s, true = true), reflects_decide := ⋯ }

@[instance_reducible]

instance HaslingerHienEtAl2025.instDecidablePredFinsetStudentMemSetStudent : DecidablePred fun (x : Finset Student) => x ∈ student

Equations

• HaslingerHienEtAl2025.instDecidablePredFinsetStudentMemSetStudent s = { decide := s.card.beq 1, reflects_decide := ⋯ }

@[instance_reducible]

instance HaslingerHienEtAl2025.instDecidablePredFinsetStudentMemSetTwoStudents : DecidablePred fun (x : Finset Student) => x ∈ twoStudents

Equations

• HaslingerHienEtAl2025.instDecidablePredFinsetStudentMemSetTwoStudents s = { decide := s.card.beq 2, reflects_decide := ⋯ }

@[instance_reducible]

instance HaslingerHienEtAl2025.instDecidablePredFinsetStudentMemSetMet : DecidablePred fun (x : Finset Student) => x ∈ met

Equations

• HaslingerHienEtAl2025.instDecidablePredFinsetStudentMemSetMet s = { decide := decide (s.val = Finset.univ.val), reflects_decide := ⋯ }

theorem HaslingerHienEtAl2025.dng : QForall students met ∧ ¬QForall student met

The Distributivity–Number Generalization on one algebra, where the collective scope holds under the plural restrictor and fails under the singular one.

theorem HaslingerHienEtAl2025.qForall_students_iff (Q : Set (Finset Student)) : QForall students Q ↔ Finset.univ ∈ Q

In the model the plural half says that the quantifier over students is a claim about the sum of all the students.

theorem HaslingerHienEtAl2025.qForall_student_iff (Q : Set (Finset Student)) : QForall student Q ↔ ∀ s ∈ student, s ∈ Q

In the model the singular half says that the quantifier over student is the ordinary universal.

theorem HaslingerHienEtAl2025.maximal_twoStudents (s : Finset Student) : s ∈ twoStudents → Maximal (fun (x : Finset Student) => x ∈ twoStudents) s

Every pair of students is a maximal element of two students.

theorem HaslingerHienEtAl2025.not_maxNonOverlap_twoStudents (s : Finset Student) : ¬MaxNonOverlap twoStudents s

Yet every pair overlaps another pair, so no pair is maximal non-overlapping.

theorem HaslingerHienEtAl2025.qForall_twoStudents (Q : Set (Finset Student)) : QForall twoStudents Q

With three salient students the quantifier over two students is vacuous, so the reading on which every pair of students satisfies the scope is unavailable.

theorem HaslingerHienEtAl2025.not_oneEmptyDom_students : ¬OneEmptyDom students

ONE_∅ rejects the plural restrictor, whose pluralities overlap.

theorem HaslingerHienEtAl2025.oneAtDom_student : OneAtDom student

ONE_AT accepts the singular restrictor.

Ten minutes

def HaslingerHienEtAl2025.tenMinutes : Set (Set ℕ)

The coerced denotation of ten minutes holds of the consecutive ten-minute intervals, with time measured in minutes.

Equations

• HaslingerHienEtAl2025.tenMinutes = Set.range fun (k : ℕ) => Set.Ico (10 * k) (10 * k + 10)

theorem HaslingerHienEtAl2025.tenMinutes_nontrivial : tenMinutes.Nontrivial

theorem HaslingerHienEtAl2025.tenMinutes_disjoint : Mereology.DisjointPred Mereology.Overlap tenMinutes

theorem HaslingerHienEtAl2025.oneEmptyDom_tenMinutes : OneEmptyDom tenMinutes

theorem HaslingerHienEtAl2025.not_atom_tenMinutes (I : Set ℕ) : I ∈ tenMinutes → ¬Mereology.Atom I

An interval of ten minutes is the sum of shorter intervals, so it is not an atom.

theorem HaslingerHienEtAl2025.not_oneAtDom_tenMinutes : ¬OneAtDom tenMinutes

theorem HaslingerHienEtAl2025.every_tenMinutes_dom (Q : Set (Set ℕ)) : (every tenMinutes Q).Dom

Every ten minutes is defined.

theorem HaslingerHienEtAl2025.each_tenMinutes_undefined (Q : Set (Set ℕ)) : ¬(each tenMinutes Q).Dom

Each ten minutes is a presupposition failure.

theorem HaslingerHienEtAl2025.jeder_tenMinutes_undefined (Q : Set (Set ℕ)) : ¬(jeder tenMinutes Q).Dom

German jede zehn Minuten is a presupposition failure, since jeder carries ONE_AT.

The English and German forms

inductive HaslingerHienEtAl2025.Structure : Type

A universal quantifier form realizes one of four structures, namely the bare quantifier, the quantifier over ONE_∅, the quantifier over ONE_∅ and ONE_AT, or the quantifier over ONE_AT alone, as in German.

• bare : Structure
• nonOverlap : Structure
• atomic : Structure
• atomicOnly : Structure

@[instance_reducible]

instance HaslingerHienEtAl2025.instDecidableEqStructure : DecidableEq Structure

Equations

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

@[instance_reducible]

instance HaslingerHienEtAl2025.instReprStructure : Repr Structure

Equations

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

def HaslingerHienEtAl2025.instReprStructure.repr : Structure → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance HaslingerHienEtAl2025.instFintypeStructure : Fintype Structure

Equations

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

def HaslingerHienEtAl2025.Structure.head {α : Type u_1} [PartialOrder α] : Structure → Set α →. Set α

The head a structure spells out.

Equations

• HaslingerHienEtAl2025.Structure.bare.head = ↑id
• HaslingerHienEtAl2025.Structure.nonOverlap.head = HaslingerHienEtAl2025.oneEmpty
• HaslingerHienEtAl2025.Structure.atomic.head = HaslingerHienEtAl2025.oneEmpty.comp HaslingerHienEtAl2025.oneAt
• HaslingerHienEtAl2025.Structure.atomicOnly.head = HaslingerHienEtAl2025.oneAt

def HaslingerHienEtAl2025.english : English.Determiners.QuantityWord → Option Structure

The English universal determiners all, every and each.

Equations

• HaslingerHienEtAl2025.english English.Determiners.QuantityWord.all = some HaslingerHienEtAl2025.Structure.bare
• HaslingerHienEtAl2025.english English.Determiners.QuantityWord.every = some HaslingerHienEtAl2025.Structure.nonOverlap
• HaslingerHienEtAl2025.english English.Determiners.QuantityWord.each = some HaslingerHienEtAl2025.Structure.atomic
• HaslingerHienEtAl2025.english x✝ = none

theorem HaslingerHienEtAl2025.one_iff_singular (w : English.Determiners.QuantityWord) (s : Structure) : english w = some s → (s ≠ Structure.bare ↔ w.numberRestriction = some Number.singular)

At the lexicon the generalization says that the English forms carrying a ONE head are exactly the universal determiners the fragment records as selecting the singular.

theorem HaslingerHienEtAl2025.structure_dom_tenMinutes (s : Structure) (Q : Set (Set ℕ)) : (over s.head tenMinutes Q).Dom ↔ s = Structure.bare ∨ s = Structure.nonOverlap

Which structures are defined on the intervals of ten minutes.

@[instance_reducible]

instance HaslingerHienEtAl2025.instDecidableDomOverSetNatHeadTenMinutes (s : Structure) (Q : Set (Set ℕ)) : Decidable (over s.head tenMinutes Q).Dom

Equations

• HaslingerHienEtAl2025.instDecidableDomOverSetNatHeadTenMinutes s Q = decidable_of_iff (s = HaslingerHienEtAl2025.Structure.bare ∨ s = HaslingerHienEtAl2025.Structure.nonOverlap) ⋯

def HaslingerHienEtAl2025.structureTable : List (String × Structure)

The structure names of the example rows.

Equations

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

theorem HaslingerHienEtAl2025.judgment_rows (row : Datum) : row ∈ Examples.all → ∃ (s : Structure), row.parse? "structure" structureTable = some s ∧ (row.judgment = Judgment.acceptable ↔ (over s.head tenMinutes Set.univ).Dom)

The paper's judgments on universal quantifiers with ten minutes are the definedness predictions, since a form is acceptable just in case its structure is defined on the intervals.