English Determiners

[Hor72] [BC81]

English-specific determiner lexicon. Each entry is marked like a Pronoun (a decidable record carrying only the morphosyntax synonyms diverge on) and typed by the standard determiner taxonomy in Syntax/Determiner/Basic.lean:

• the genuinely quantificational words (every, some, no, most, few, half, all, each, many, both, neither) are Syntax.Determiner.Quantifier;
• the definites/indefinites (the, a, an) are Articles and the demonstratives (this, that, these, those) are DemonstrativeDeterminers.

A determiner's denotation is a generalized quantifier supplied externally — the marked record carries no GQ, exactly as Pronoun carries no referent. For the six-word quantity scale the form↦GQ map is QuantityWord.gqDenotation (Semantics/Quantification); everything a meaning fixes (force, monotonicity, strength, conservativity) is a theorem about that denotation, not a stored field (see Studies/BarwiseCooper1981.lean).

The cross-paper typological labels (B&C Table II strength/monotonicity, K&S force) are kept as the textbook-consensus QuantityWord.entry : QuantityWord.Metadata metadata table (a small local record over the Quantification.Lexicon enums), consumed by GQT and exceptive studies that need the descriptive classification rather than the denotation.

Scope

This file carries descriptive lexical data, its projection to GQ denotations, and the typological metadata table. Per-paper model parameters (GQT thresholds, prototype-theory prototypes/spreads) and theory-bridge theorems live elsewhere:

• Compositional GQ denotations (every_sem, both_sem, neither_sem, …): Semantics/Quantification/Quantifier.lean.
• GQT/PT meaning operators consuming numerical parameters: Studies/VanTielEtAl2021.lean (gqtMeaning, van Tiel's threshold scale-model), Semantics/Probabilistic/PrototypeTheory.lean (ptMeaning).
• Per-paper parameter values: Studies/VanTielEtAl2021.lean.

Quantificational determiners

Marked Quantifier records: form, the selectional numberRestriction (root Number), and selectsMass. The meaning leaves these open — every and all can share a denotation yet differ in numberRestriction.

def English.Determiners.none_ : Quantifier

"none" — negative, accepts mass NPs.

Equations

• English.Determiners.none_ = { form := "none", selectsMass := true }

def English.Determiners.few : Quantifier

"few" — proportional, plural.

Equations

• English.Determiners.few = { form := "few", numberRestriction := some Number.plural }

def English.Determiners.some_ : Quantifier

"some" — existential, accepts mass NPs.

Equations

• English.Determiners.some_ = { form := "some", selectsMass := true }

def English.Determiners.half : Quantifier

"half" — proportional, accepts mass NPs.

Equations

• English.Determiners.half = { form := "half", selectsMass := true }

def English.Determiners.most : Quantifier

"most" — proportional, plural, accepts mass NPs.

Equations

• English.Determiners.most = { form := "most", numberRestriction := some Number.plural, selectsMass := true }

def English.Determiners.all : Quantifier

"all" — universal, plural, accepts mass NPs.

Equations

• English.Determiners.all = { form := "all", numberRestriction := some Number.plural, selectsMass := true }

def English.Determiners.every : Quantifier

"every" — universal, singular.

Equations

• English.Determiners.every = { form := "every", numberRestriction := some Number.singular }

def English.Determiners.each : Quantifier

"each" — universal, distributive, singular.

Equations

• English.Determiners.each = { form := "each", numberRestriction := some Number.singular }

def English.Determiners.many : Quantifier

"many" — proportional, plural.

Equations

• English.Determiners.many = { form := "many", numberRestriction := some Number.plural }

def English.Determiners.both : Quantifier

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

numberRestriction := some .dual carries the dual core concept ([Har14a] [−atomic, +minimal]); the cardinality clause |R| ≥ 2 on the denotation side reflects the Harbour dualPredOnLattice reading ([JBG+25]).

Equations

• English.Determiners.both = { form := "both", numberRestriction := some Number.dual }

def English.Determiners.neither : Quantifier

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

Equations

• English.Determiners.neither = { form := "neither", numberRestriction := some Number.dual }

Articles and demonstratives

The definites/indefinites and demonstratives are not quantifiers: their denotation is definiteness, not a generalized quantifier.

def English.Determiners.the : Article

"the" — definite article, syncretic over both [Sch09b] strengths.

Equations

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

def English.Determiners.a : Article

"a" — indefinite article, singular.

Equations

• English.Determiners.a = { form := "a", definiteness := Features.Definiteness.Definiteness.indefinite, exponent := Determiner.Exponent.dedicatedMorpheme }

def English.Determiners.an : Article

"an" — indefinite article, singular (phonological allomorph of a).

Equations

• English.Determiners.an = { form := "an", definiteness := Features.Definiteness.Definiteness.indefinite, exponent := Determiner.Exponent.dedicatedMorpheme }

def English.Determiners.this : DemonstrativeDeterminer

"this" — proximal demonstrative determiner, singular.

Equations

• English.Determiners.this = { form := "this", deictic := Features.Deixis.Feature.proximal }

def English.Determiners.that : DemonstrativeDeterminer

"that" — distal demonstrative determiner, singular.

Equations

• English.Determiners.that = { form := "that", deictic := Features.Deixis.Feature.distal }

def English.Determiners.these : DemonstrativeDeterminer

"these" — proximal demonstrative determiner, plural.

Equations

• English.Determiners.these = { form := "these", deictic := Features.Deixis.Feature.proximal }

def English.Determiners.those : DemonstrativeDeterminer

"those" — distal demonstrative determiner, plural.

Equations

• English.Determiners.those = { form := "those", deictic := Features.Deixis.Feature.distal }

Numerical Determiners

[BC81] [vdPLvM+23]

Parameterized by a numerical threshold n. These are the class of determiners [vdPLvM+23] show satisfy all three semantic universals (and have low MDL).

structure English.Determiners.NumericalDetEntry : Type

Numerical determiner entry.

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

  The numerical threshold

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

Equations

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

@[implicit_reducible]

instance English.Determiners.instReprNumericalDetEntry : Repr NumericalDetEntry

Equations

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

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

Equations

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

@[implicit_reducible]

instance English.Determiners.instBEqNumericalDetEntry : BEq NumericalDetEntry

Equations

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

def 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 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 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 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 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.

The Canonical Quantity Scale

[BC81] [vTFS21]

The 6-element ⟨none, few, some, half, most, all⟩ scale used cross-paper to evaluate quantifier theories — empirical implicature studies ([vTFS21]), GQ universals ([BC81]), and polarity bridges ([VF93]).

inductive English.Determiners.QuantityWord : Type

The canonical 6-element quantity scale.

• none_ : QuantityWord
• few : QuantityWord
• some_ : QuantityWord
• half : QuantityWord
• most : QuantityWord
• all : QuantityWord

@[implicit_reducible]

instance English.Determiners.instReprQuantityWord : Repr QuantityWord

Equations

• English.Determiners.instReprQuantityWord = { reprPrec := English.Determiners.instReprQuantityWord.repr }

def English.Determiners.instReprQuantityWord.repr : QuantityWord → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance English.Determiners.instDecidableEqQuantityWord : DecidableEq QuantityWord

Equations

• English.Determiners.instDecidableEqQuantityWord x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance English.Determiners.instInhabitedQuantityWord : Inhabited QuantityWord

Equations

• English.Determiners.instInhabitedQuantityWord = { default := English.Determiners.instInhabitedQuantityWord.default }

@[implicit_reducible]

instance English.Determiners.instFintypeQuantityWord : Fintype QuantityWord

Equations

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

structure English.Determiners.QuantityWord.Metadata : Type

B&C Table II typological metadata: the textbook-consensus descriptive labels (force, monotonicity, weak/strong strength) a quantity word carries. A small local record over the Quantification.Lexicon enums — not the lexical marking (that is Quantifier, above) and not the denotation (that is QuantityWord.gqDenotation).

• qforce : QForce

  Quantificational force.

• monotonicity : Monotonicity

  Monotonicity (typological label).

• strength : Strength

  Weak/strong (B&C Table II).

@[implicit_reducible]

instance English.Determiners.QuantityWord.instReprMetadata : Repr Metadata

Equations

• English.Determiners.QuantityWord.instReprMetadata = { reprPrec := English.Determiners.QuantityWord.instReprMetadata.repr }

def English.Determiners.QuantityWord.instReprMetadata.repr : Metadata → ℕ → Std.Format

Equations

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

def English.Determiners.QuantityWord.instBEqMetadata.beq : Metadata → Metadata → Bool

Equations

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

@[implicit_reducible]

instance English.Determiners.QuantityWord.instBEqMetadata : BEq Metadata

Equations

• English.Determiners.QuantityWord.instBEqMetadata = { beq := English.Determiners.QuantityWord.instBEqMetadata.beq }

@[implicit_reducible]

instance English.Determiners.QuantityWord.instDecidableEqMetadata : DecidableEq Metadata

Equations

• English.Determiners.QuantityWord.instDecidableEqMetadata = English.Determiners.QuantityWord.instDecidableEqMetadata.decEq

def English.Determiners.QuantityWord.instDecidableEqMetadata.decEq (x✝ x✝¹ : Metadata) : Decidable (x✝ = x✝¹)

Equations

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

def English.Determiners.QuantityWord.entry : QuantityWord → Metadata

B&C Table II typological metadata for each quantity word: force, monotonicity, and weak/strong strength. This is the textbook-consensus descriptive classification ([BC81] Table II, [vdPLvM+23] for half), not the denotation — the denotation is QuantityWord.gqDenotation, and the properties this table labels are theorems about it (Studies/BarwiseCooper1981.lean). Consumed by the GQT model ([vTFS21]) and the exceptive-licensing bridge ([VF93]) that want the descriptive label.

Equations

• English.Determiners.QuantityWord.none_.entry = { qforce := Quantification.Lexicon.QForce.negative, monotonicity := Quantification.Lexicon.Monotonicity.decreasing }
• English.Determiners.QuantityWord.few.entry = { qforce := Quantification.Lexicon.QForce.proportional, monotonicity := Quantification.Lexicon.Monotonicity.decreasing }
• English.Determiners.QuantityWord.some_.entry = { qforce := Quantification.Lexicon.QForce.existential }
• English.Determiners.QuantityWord.half.entry = { qforce := Quantification.Lexicon.QForce.proportional, monotonicity := Quantification.Lexicon.Monotonicity.nonMonotone }
• English.Determiners.QuantityWord.most.entry = { qforce := Quantification.Lexicon.QForce.proportional, strength := Quantification.Lexicon.Strength.strong }
• English.Determiners.QuantityWord.all.entry = { qforce := Quantification.Lexicon.QForce.universal, strength := Quantification.Lexicon.Strength.strong }

def English.Determiners.QuantityWord.monotonicity (q : QuantityWord) : Monotonicity

Convenience accessor.

Equations

• q.monotonicity = q.entry.monotonicity

def English.Determiners.QuantityWord.toList : List QuantityWord

All quantity words as a list.

Equations

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

noncomputable def English.Determiners.QuantityWord.gqDenotation (q : QuantityWord) {α : Type u_1} [Fintype α] : Quantification.GQ α

Canonical model-theoretic generalized-quantifier denotation (B&C-style), built on every_sem/some_sem/no_sem/etc. from Quantification.Quantifier.

Equations

• English.Determiners.QuantityWord.none_.gqDenotation = Quantification.no_sem
• English.Determiners.QuantityWord.some_.gqDenotation = Quantification.some_sem
• English.Determiners.QuantityWord.all.gqDenotation = Quantification.every_sem
• English.Determiners.QuantityWord.most.gqDenotation = Quantification.most_sem
• English.Determiners.QuantityWord.few.gqDenotation = Quantification.few_sem
• English.Determiners.QuantityWord.half.gqDenotation = Quantification.half_sem

Lexicon Access

def English.Determiners.allQuantifiers : List Quantifier

All quantificational determiner entries (excluding definites).

Equations

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

def English.Determiners.allArticles : List Article

All article entries.

Equations

• English.Determiners.allArticles = [English.Determiners.the, English.Determiners.a, English.Determiners.an]

def English.Determiners.allDemonstratives : List DemonstrativeDeterminer

All demonstrative-determiner entries.

Equations

• English.Determiners.allDemonstratives = [English.Determiners.this, English.Determiners.that, English.Determiners.these, English.Determiners.those]

def English.Determiners.inventory : List Determiner.Entry

The full inventory as a heterogeneous List Determiner.Entry (the per-language form a Fragment declares).

Equations

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