English Determiners

@cite{horn-1972} @cite{barwise-cooper-1981}

English-specific determiner lexicon. The shared QuantifierEntry structure (and the QForce/Monotonicity/Strength enums) lives in Theories/Semantics/Quantification/Lexicon.lean; this file is the English instantiation and a small numerical-determiner sublexicon.

Scope

This file carries only descriptive lexical data — facts a reference grammar of English would record. Per-paper model parameters (GQT thresholds, prototype-theory prototypes/spreads), compositional denotations, scalar-paradigm projections, and theory-bridge theorems all live elsewhere:

• Canonical 6-element ⟨none, few, some, half, most, all⟩ paradigm and its B&C-style GQ denotation table: Phenomena/Quantification/Inventory.lean.
• Compositional GQ denotations (every_sem, both_sem, neither_sem, …): Theories/Semantics/Quantification/Quantifier.lean.
• GQT/PT meaning operators consuming numerical parameters: Theories/Semantics/Quantification/Quantifier.lean (gqtMeaning), Theories/Semantics/Probabilistic/PrototypeTheory.lean (ptMeaning).
• Per-paper parameter values: Phenomena/ScalarImplicatures/Studies/VanTielEtAl2021.lean.

def Fragments.English.Determiners.none_ : QuantifierEntry

Equations

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

def Fragments.English.Determiners.few : QuantifierEntry

Equations

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

def Fragments.English.Determiners.some_ : QuantifierEntry

Equations

• Fragments.English.Determiners.some_ = { form := "some", qforce := Theories.Semantics.Quantification.Lexicon.QForce.existential, allowsMass := true }

def Fragments.English.Determiners.half : QuantifierEntry

Equations

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

def Fragments.English.Determiners.most : QuantifierEntry

"most" - more than half

Equations

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

def Fragments.English.Determiners.all : QuantifierEntry

"all" - everything satisfies

Equations

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

def Fragments.English.Determiners.every : QuantifierEntry

"every" - universal, singular

Equations

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

def Fragments.English.Determiners.each : QuantifierEntry

"each" - universal, distributive

Equations

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

def Fragments.English.Determiners.many : QuantifierEntry

"many" - a large number

Equations

• Fragments.English.Determiners.many = { form := "many", qforce := Theories.Semantics.Quantification.Lexicon.QForce.proportional, numberRestriction := some Number.pl }

Numerical Determiners

@cite{barwise-cooper-1981} @cite{van-de-pol-etal-2023}

Parameterized by a numerical threshold n. These are the class of determiners @cite{van-de-pol-etal-2023} show satisfy all three semantic universals (and have low MDL).

structure Fragments.English.Determiners.NumericalDetEntry : Type

Numerical determiner entry.

• form : String
• qforce : QForce
• monotonicity : Monotonicity
• threshold : ℕ

  The numerical threshold

@[implicit_reducible]

instance Fragments.English.Determiners.instReprNumericalDetEntry : Repr NumericalDetEntry

Equations

• Fragments.English.Determiners.instReprNumericalDetEntry = { reprPrec := Fragments.English.Determiners.instReprNumericalDetEntry.repr }

def Fragments.English.Determiners.instReprNumericalDetEntry.repr : NumericalDetEntry → ℕ → Std.Format

Equations

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

def Fragments.English.Determiners.instBEqNumericalDetEntry.beq : NumericalDetEntry → NumericalDetEntry → Bool

Equations

• One or more equations did not get rendered due to their size.
• Fragments.English.Determiners.instBEqNumericalDetEntry.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Fragments.English.Determiners.instBEqNumericalDetEntry : BEq NumericalDetEntry

Equations

• Fragments.English.Determiners.instBEqNumericalDetEntry = { beq := Fragments.English.Determiners.instBEqNumericalDetEntry.beq }

def Fragments.English.Determiners.atLeast (n : ℕ) : NumericalDetEntry

"at least n" — upward monotone in scope, conservative, quantity

Equations

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

def Fragments.English.Determiners.atMost (n : ℕ) : NumericalDetEntry

"at most n" — downward monotone in scope, conservative, quantity

Equations

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

def Fragments.English.Determiners.exactlyN (n : ℕ) : NumericalDetEntry

"exactly n" — non-monotone (neither UE nor DE), conservative, quantity

Equations

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

def Fragments.English.Determiners.moreThan (n : ℕ) : NumericalDetEntry

"more than n" — upward monotone, conservative, quantity

Equations

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

def Fragments.English.Determiners.fewerThan (n : ℕ) : NumericalDetEntry

"fewer than n" — downward monotone, conservative, quantity

Equations

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

Definite Determiners (less relevant for quantity scales)

def Fragments.English.Determiners.the : QuantifierEntry

Equations

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

def Fragments.English.Determiners.this : QuantifierEntry

Equations

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

def Fragments.English.Determiners.that : QuantifierEntry

Equations

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

def Fragments.English.Determiners.these : QuantifierEntry

Equations

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

def Fragments.English.Determiners.those : QuantifierEntry

Equations

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

def Fragments.English.Determiners.a : QuantifierEntry

Equations

• Fragments.English.Determiners.a = { form := "a", qforce := Theories.Semantics.Quantification.Lexicon.QForce.existential, numberRestriction := some Number.sg }

def Fragments.English.Determiners.an : QuantifierEntry

Equations

• Fragments.English.Determiners.an = { form := "an", qforce := Theories.Semantics.Quantification.Lexicon.QForce.existential, numberRestriction := some Number.sg }

def Fragments.English.Determiners.both : QuantifierEntry

"both" - universal dual, presupposes exactly 2. K&S (83a): [_Det each of the two] ⇒ both. Compositional denotation both_sem lives in Theories.Semantics.Quantification.Quantifier.

numberRestriction := some .du carries the dual core concept (@cite{harbour-2014} [−atomic, +minimal]); the cardinality clause |R| ≥ 2 on the denotation side reflects the Harbour dualPredOnLattice reading (@cite{jeretic-bassi-gonzalez-yatsushiro-meyer-sauerland-2025}).

Equations

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

def Fragments.English.Determiners.neither : QuantifierEntry

"neither" - negative dual, presupposes exactly 2. K&S (83b): [_Det (not one) of the two] ⇒ neither. Compositional denotation neither_sem lives in Theories.Semantics.Quantification.Quantifier.

Equations

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

Lexicon Access

def Fragments.English.Determiners.allQuantifiers : List QuantifierEntry

All quantifier entries (excluding definites).

Equations

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

def Fragments.English.Determiners.allDeterminers : List QuantifierEntry

All determiner entries (including definites).

Equations

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

def Fragments.English.Determiners.lookup (form : String) : Option QuantifierEntry

Lookup by form.

Equations

• Fragments.English.Determiners.lookup form = List.find? (fun (d : Theories.Semantics.Quantification.Lexicon.QuantifierEntry) => d.form == form) Fragments.English.Determiners.allDeterminers