English determiners

The quantificational determiners of English are the carrier QuantityWord. A word projects to a Quantifier record by QuantityWord.toQuantifier, which carries only what the readings leave open, the number the word selects and whether it selects mass nouns. The readings themselves are the Denotes instance, a set of Quantifier.GQ.Family per word: a word with one consensus reading denotes a singleton, so ⟦QuantityWord.all⟧ is {every}, and many, whose standard Barwise and Cooper leave to context, denotes ∅. Everything a reading fixes, its force, monotonicity, strength and conservativity, is a theorem about it, as in Studies/BarwiseCooper1981.lean. The articles, demonstratives and possessives are the other determiner kinds.

Main declarations

• QuantityWord: the quantificational determiners, with the six-word scale QuantityWord.scale of van Tiel, Franke and Sauerland inside it.
• QuantityWord.toQuantifier: a word as a determiner record.
• inventory: the English determiner inventory, and marking derives its cell in Moroney's typology of definite marking.

References

• [BC81]
• [Hor72]
• [vTFS21]
• [VF93]
• [Har14a]
• [JBG+25]
• [Sch09b]
• [Mor21]

Quantificational determiners

inductive English.Determiners.QuantityWord : Type

The quantificational determiners of English are the six-word quantity scale none, few, some, half, most and all, and every, each, many, both and neither.

• none_ : QuantityWord
• few : QuantityWord
• some_ : QuantityWord
• half : QuantityWord
• most : QuantityWord
• all : QuantityWord
• every : QuantityWord
• each : QuantityWord
• many : QuantityWord
• both : QuantityWord
• neither : QuantityWord

@[instance_reducible]

instance English.Determiners.instDecidableEqQuantityWord : DecidableEq QuantityWord

Equations

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

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

@[instance_reducible]

instance English.Determiners.instFintypeQuantityWord : Fintype QuantityWord

Equations

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

def English.Determiners.QuantityWord.form : QuantityWord → String

The form of a word is its spelling.

Equations

• English.Determiners.QuantityWord.none_.form = "none"
• English.Determiners.QuantityWord.few.form = "few"
• English.Determiners.QuantityWord.some_.form = "some"
• English.Determiners.QuantityWord.half.form = "half"
• English.Determiners.QuantityWord.most.form = "most"
• English.Determiners.QuantityWord.all.form = "all"
• English.Determiners.QuantityWord.every.form = "every"
• English.Determiners.QuantityWord.each.form = "each"
• English.Determiners.QuantityWord.many.form = "many"
• English.Determiners.QuantityWord.both.form = "both"
• English.Determiners.QuantityWord.neither.form = "neither"

def English.Determiners.QuantityWord.numberRestriction : QuantityWord → Option Number

The grammatical number a word selects is left open by the denotation, so every and all share a denotation and differ here. Both and neither select the dual, the core concept [−atomic, +minimal] of [Har14a], whose cardinality clause the denotation reflects ([JBG+25]).

Equations

• English.Determiners.QuantityWord.few.numberRestriction = some Number.plural
• English.Determiners.QuantityWord.most.numberRestriction = some Number.plural
• English.Determiners.QuantityWord.all.numberRestriction = some Number.plural
• English.Determiners.QuantityWord.many.numberRestriction = some Number.plural
• English.Determiners.QuantityWord.every.numberRestriction = some Number.singular
• English.Determiners.QuantityWord.each.numberRestriction = some Number.singular
• English.Determiners.QuantityWord.both.numberRestriction = some Number.dual
• English.Determiners.QuantityWord.neither.numberRestriction = some Number.dual
• English.Determiners.QuantityWord.none_.numberRestriction = none
• English.Determiners.QuantityWord.some_.numberRestriction = none
• English.Determiners.QuantityWord.half.numberRestriction = none

def English.Determiners.QuantityWord.selectsMass : QuantityWord → Bool

selectsMass w says whether w combines with mass nouns, which the denotation likewise leaves open.

Equations

• English.Determiners.QuantityWord.none_.selectsMass = true
• English.Determiners.QuantityWord.some_.selectsMass = true
• English.Determiners.QuantityWord.half.selectsMass = true
• English.Determiners.QuantityWord.most.selectsMass = true
• English.Determiners.QuantityWord.all.selectsMass = true
• English.Determiners.QuantityWord.few.selectsMass = false
• English.Determiners.QuantityWord.every.selectsMass = false
• English.Determiners.QuantityWord.each.selectsMass = false
• English.Determiners.QuantityWord.many.selectsMass = false
• English.Determiners.QuantityWord.both.selectsMass = false
• English.Determiners.QuantityWord.neither.selectsMass = false

def English.Determiners.QuantityWord.toQuantifier (w : QuantityWord) : Quantifier

The determiner record of a word carries its form, its number and its mass selection.

Equations

• w.toQuantifier = { form := w.form, numberRestriction := w.numberRestriction, selectsMass := w.selectsMass }

def English.Determiners.QuantityWord.scale : List QuantityWord

The six-word quantity scale of [vTFS21] runs from none to all; quantifier theories such as those of [BC81] and [VF93] are compared on it.

Equations

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

def English.Determiners.QuantityWord.toList : List QuantityWord

toList lists every word.

Equations

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

theorem English.Determiners.QuantityWord.mem_toList (w : QuantityWord) : w ∈ toList

The available readings

@[instance_reducible]

noncomputable instance English.Determiners.QuantityWord.instDenotesSetFamily : Semantics.Denotes QuantityWord (Set Quantifier.GQ.Family)

A word denotes the readings the literature makes available for it, as generalized quantifiers on every finite domain. None reads as no, some as Quantifier.GQ.some, all, every and each as every, most as most, few as few, half as half, both as both and neither as neither; many has no reading, since [BC81] leave its standard to context.

Equations

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

Articles, demonstratives and possessives

The articles and demonstratives are not quantifiers, since what they denote is definiteness and not a generalized quantifier.

def English.Determiners.the : Article

The is the definite article, syncretic over both strengths of [Sch09b].

Equations

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

def English.Determiners.a : Article

A is the singular indefinite article.

Equations

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

def English.Determiners.an : Article

An is the singular indefinite article, the allomorph of a before a vowel.

Equations

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

def English.Determiners.this : DemonstrativeDeterminer

This is the singular proximal demonstrative.

Equations

• English.Determiners.this = { form := "this", deixis := Person.first.participantSets }

def English.Determiners.that : DemonstrativeDeterminer

That is the singular distal demonstrative.

Equations

• English.Determiners.that = { form := "that", deixis := Person.first.participantSetsᶜ }

def English.Determiners.these : DemonstrativeDeterminer

These is the plural proximal demonstrative.

Equations

• English.Determiners.these = { form := "these", deixis := Person.first.participantSets }

def English.Determiners.those : DemonstrativeDeterminer

Those is the plural distal demonstrative.

Equations

• English.Determiners.those = { form := "those", deixis := Person.first.participantSetsᶜ }

def English.Determiners.my : PossessiveDeterminer

My is the first-person possessive determiner.

Equations

• English.Determiners.my = { form := "my" }

def English.Determiners.your : PossessiveDeterminer

Your is the second-person possessive determiner.

Equations

• English.Determiners.your = { form := "your" }

The inventory

def English.Determiners.allQuantifiers : List Quantifier

The quantificational determiners as records.

Equations

• English.Determiners.allQuantifiers = List.map English.Determiners.QuantityWord.toQuantifier English.Determiners.QuantityWord.toList

def English.Determiners.allArticles : List Article

The articles.

Equations

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

def English.Determiners.allDemonstratives : List DemonstrativeDeterminer

The demonstratives.

Equations

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

def English.Determiners.allPossessives : List PossessiveDeterminer

The possessive determiners.

Equations

• English.Determiners.allPossessives = [English.Determiners.my, English.Determiners.your]

def English.Determiners.inventory : Determiner.Inventory

The determiner inventory collects every kind of determiner.

Equations

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

theorem English.Determiners.marking : inventory.markingStrategy = Reference.MarkingStrategy.generallyMarked

English's inventory is in the .generallyMarked cell of [Mor21], since the syncretic the covers both use types of [Sch09b].