Determiners

This file defines the determiner as a lexical object and the determiner inventory of a language. The base Determiner carries only a surface form, and the four specializations Article, DemonstrativeDeterminer, Quantifier and PossessiveDeterminer extend it. An inventory is a list of Determiner.Entry occurrences, and the typologies of definiteness marking are derived from it rather than declared. An entry marks an article strength when one of the definite uses it obligatorily expones calls for that strength, and a language's [moroney-2021] cell and [schwarz-2009] article system are theorems about its inventory, discharged by decide.

Main declarations

• Determiner is the base record, and Determiner.toWord realizes it as a word.
• Article records definiteness, the exponent and the definite uses the article obligatorily expones; DemonstrativeDeterminer, Quantifier and PossessiveDeterminer are the other specializations.
• Determiner.Entry is an occurrence of one of the four kinds in an inventory, Entry.kind is its kind together with an article's definiteness, and Entry.Marks says which strengths it marks.
• Determiner.Inventory is a language's declared inventory. Inventory.Marks and Inventory.IsSyncretic lift the entry predicates, and Inventory.markingStrategy and Inventory.articleType derive the typological cells, each characterized by an _iff lemma.
• Determiner.Inventory.Realizes says that the inventory carries a form for a kind of nominal description.
• Article.strengths is the set of strengths an article admits.

Implementation notes

This file is the Frame-free lexical layer. The denotations of articles, demonstratives and possessives are in Semantics/Reference/Determiner.lean, and the generalized-quantifier denotation of a Quantifier is supplied by its consumers. Inventory is a def rather than an abbrev so that its operations resolve by dot notation; its membership is the list's, and facts about one-entry inventories go through Inventory.marks_singleton. Realizes is inventory data and neither licensing nor felicity. A kind can be expressed without a determiner realizing it, as Shan anaphoric definites are by bare nouns ([moroney-2021]), and which form a context selects is pragmatics ([jenks-2018]).

References

• [schwarz-2009]
• [moroney-2021]
• [jenks-2018]

structure Determiner : Type

A determiner is a D head with a surface form, a representative morpheme or a construction label. The specializations extend it.

• form : String

  The surface form.

@[instance_reducible]

instance instDecidableEqDeterminer : DecidableEq Determiner

Equations

• instDecidableEqDeterminer = instDecidableEqDeterminer.decEq

def instDecidableEqDeterminer.decEq (x✝ x✝¹ : Determiner) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqDeterminer.decEq { form := a } { form := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def instReprDeterminer.repr : Determiner → ℕ → Std.Format

Equations

• instReprDeterminer.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "form" ++ Std.Format.text " := " ++ (Std.Format.nest 8 (repr x✝.form)).group) " }"

@[instance_reducible]

instance instReprDeterminer : Repr Determiner

Equations

• instReprDeterminer = { reprPrec := instReprDeterminer.repr }

def Determiner.toWord (d : Determiner) : Morphology.Word

A determiner is realized as a bare word of category DET.

Equations

• d.toWord = { form := d.form, cat := UD.UPOS.DET }

inductive Determiner.Exponent : Type

An article is exponed by a dedicated morpheme, a classifier construction, a demonstrative form or a bare noun. Whether the form marks definiteness is a matter of the uses it expones, not of its exponent.

• dedicatedMorpheme : Exponent

  A dedicated article morpheme, as English the and German der.

• classifierPhrase : Exponent

  A bare classifier phrase, as the Cantonese definite [Clf-N].

• numeralClassifier : Exponent

  A numeral-classifier phrase, as the Cantonese indefinite [jat-Clf-N].

• demonstrativeForm : Exponent

  A demonstrative form, as Mandarin anaphoric na.

• bareNoun : Exponent

  A bare noun whose reading a covert type shift fixes.

@[instance_reducible]

instance Determiner.instDecidableEqExponent : DecidableEq Exponent

Equations

• Determiner.instDecidableEqExponent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Determiner.instReprExponent.repr : Exponent → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Determiner.instReprExponent : Repr Exponent

Equations

• Determiner.instReprExponent = { reprPrec := Determiner.instReprExponent.repr }

The specializations

structure Articleextends Determiner : Type

An article is the definite or indefinite determiner. Its uses are the definite uses it obligatorily expones, and they are empty for an indefinite.

• form : String
• definiteness : Reference.Definiteness

  The article is definite or indefinite.

• exponent : Determiner.Exponent

  The exponent of the article.

• uses : Finset Reference.DefiniteUse

  The definite uses the article obligatorily expones.

def instDecidableEqArticle.decEq (x✝ x✝¹ : Article) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance instDecidableEqArticle : DecidableEq Article

Equations

• instDecidableEqArticle = instDecidableEqArticle.decEq

structure DemonstrativeDeterminerextends Determiner : Type

A demonstrative determiner carries a deictic feature. Its definiteUses are the definite uses it obligatorily expones, as Mandarin na expones the anaphoric use, and they are empty for a demonstrative that merely can be used anaphorically.

• form : String
• deictic : Reference.Deixis

  The deictic feature.

• definiteUses : Finset Reference.DefiniteUse

  The definite uses the demonstrative obligatorily expones.

def instDecidableEqDemonstrativeDeterminer.decEq (x✝ x✝¹ : DemonstrativeDeterminer) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance instDecidableEqDemonstrativeDeterminer : DecidableEq DemonstrativeDeterminer

Equations

• instDecidableEqDemonstrativeDeterminer = instDecidableEqDemonstrativeDeterminer.decEq

@[instance_reducible]

instance instDemonstrativeDemonstrativeDeterminer : Demonstrative DemonstrativeDeterminer

The demonstrative determiner shares the Demonstrative capability with the demonstrative pronoun.

Equations

• instDemonstrativeDemonstrativeDeterminer = { deixis := DemonstrativeDeterminer.deictic }

structure Quantifierextends Determiner : Type

A quantificational determiner records only what its generalized-quantifier denotation leaves open, the grammatical number it selects and whether it selects mass nouns, since synonymous determiners such as every and all differ there. Everything the denotation fixes, its force, monotonicity, strength and conservativity, is a theorem about the denotation, which the consumers supply.

• form : String
• numberRestriction : Option Number

  The grammatical number the determiner selects, or none when it is number-neutral.

• selectsMass : Bool

  The determiner selects mass nouns.

@[instance_reducible]

instance instDecidableEqQuantifier : DecidableEq Quantifier

Equations

• instDecidableEqQuantifier = instDecidableEqQuantifier.decEq

def instDecidableEqQuantifier.decEq (x✝ x✝¹ : Quantifier) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance instReprQuantifier : Repr Quantifier

Equations

• instReprQuantifier = { reprPrec := instReprQuantifier.repr }

def instReprQuantifier.repr : Quantifier → ℕ → Std.Format

Equations

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

structure PossessiveDeterminerextends Determiner : Type

A possessive determiner denotes a definite through a possession relation.

• form : String

def instDecidableEqPossessiveDeterminer.decEq (x✝ x✝¹ : PossessiveDeterminer) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqPossessiveDeterminer.decEq { toDeterminer := a } { toDeterminer := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance instDecidableEqPossessiveDeterminer : DecidableEq PossessiveDeterminer

Equations

• instDecidableEqPossessiveDeterminer = instDecidableEqPossessiveDeterminer.decEq

def instReprPossessiveDeterminer.repr : PossessiveDeterminer → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance instReprPossessiveDeterminer : Repr PossessiveDeterminer

Equations

• instReprPossessiveDeterminer = { reprPrec := instReprPossessiveDeterminer.repr }

Entries

inductive Determiner.Entry : Type

An entry of an inventory is an occurrence of one of the four kinds of determiner.

• article (a : Article) : Entry
• demonstrative (d : DemonstrativeDeterminer) : Entry
• quantifier (q : Quantifier) : Entry
• possessive (p : PossessiveDeterminer) : Entry

def Determiner.instDecidableEqEntry.decEq (x✝ x✝¹ : Entry) : Decidable (x✝ = x✝¹)

Equations

• Determiner.instDecidableEqEntry.decEq (Determiner.Entry.article a) (Determiner.Entry.article b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Determiner.instDecidableEqEntry.decEq (Determiner.Entry.article a) (Determiner.Entry.demonstrative d) = isFalse ⋯
• Determiner.instDecidableEqEntry.decEq (Determiner.Entry.article a) (Determiner.Entry.quantifier q) = isFalse ⋯
• Determiner.instDecidableEqEntry.decEq (Determiner.Entry.article a) (Determiner.Entry.possessive p) = isFalse ⋯
• Determiner.instDecidableEqEntry.decEq (Determiner.Entry.demonstrative d) (Determiner.Entry.article a) = isFalse ⋯
• Determiner.instDecidableEqEntry.decEq (Determiner.Entry.demonstrative a) (Determiner.Entry.demonstrative b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Determiner.instDecidableEqEntry.decEq (Determiner.Entry.demonstrative d) (Determiner.Entry.quantifier q) = isFalse ⋯
• Determiner.instDecidableEqEntry.decEq (Determiner.Entry.demonstrative d) (Determiner.Entry.possessive p) = isFalse ⋯
• Determiner.instDecidableEqEntry.decEq (Determiner.Entry.quantifier q) (Determiner.Entry.article a) = isFalse ⋯
• Determiner.instDecidableEqEntry.decEq (Determiner.Entry.quantifier q) (Determiner.Entry.demonstrative d) = isFalse ⋯
• Determiner.instDecidableEqEntry.decEq (Determiner.Entry.quantifier a) (Determiner.Entry.quantifier b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Determiner.instDecidableEqEntry.decEq (Determiner.Entry.quantifier q) (Determiner.Entry.possessive p) = isFalse ⋯
• Determiner.instDecidableEqEntry.decEq (Determiner.Entry.possessive p) (Determiner.Entry.article a) = isFalse ⋯
• Determiner.instDecidableEqEntry.decEq (Determiner.Entry.possessive p) (Determiner.Entry.demonstrative d) = isFalse ⋯
• Determiner.instDecidableEqEntry.decEq (Determiner.Entry.possessive p) (Determiner.Entry.quantifier q) = isFalse ⋯
• Determiner.instDecidableEqEntry.decEq (Determiner.Entry.possessive a) (Determiner.Entry.possessive b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Determiner.instDecidableEqEntry : DecidableEq Entry

Equations

• Determiner.instDecidableEqEntry = Determiner.instDecidableEqEntry.decEq

inductive Determiner.Entry.Kind : Type

The kind of an entry records an article's definiteness and nothing else.

• article (d : Reference.Definiteness) : Kind
• demonstrative : Kind
• quantifier : Kind
• possessive : Kind

@[instance_reducible]

instance Determiner.Entry.instDecidableEqKind : DecidableEq Kind

Equations

• Determiner.Entry.instDecidableEqKind = Determiner.Entry.instDecidableEqKind.decEq

def Determiner.Entry.instDecidableEqKind.decEq (x✝ x✝¹ : Kind) : Decidable (x✝ = x✝¹)

Equations

• Determiner.Entry.instDecidableEqKind.decEq (Determiner.Entry.Kind.article a) (Determiner.Entry.Kind.article b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Determiner.Entry.instDecidableEqKind.decEq (Determiner.Entry.Kind.article d) Determiner.Entry.Kind.demonstrative = isFalse ⋯
• Determiner.Entry.instDecidableEqKind.decEq (Determiner.Entry.Kind.article d) Determiner.Entry.Kind.quantifier = isFalse ⋯
• Determiner.Entry.instDecidableEqKind.decEq (Determiner.Entry.Kind.article d) Determiner.Entry.Kind.possessive = isFalse ⋯
• Determiner.Entry.instDecidableEqKind.decEq Determiner.Entry.Kind.demonstrative (Determiner.Entry.Kind.article d) = isFalse ⋯
• Determiner.Entry.instDecidableEqKind.decEq Determiner.Entry.Kind.demonstrative Determiner.Entry.Kind.demonstrative = isTrue ⋯
• Determiner.Entry.instDecidableEqKind.decEq Determiner.Entry.Kind.demonstrative Determiner.Entry.Kind.quantifier = isFalse Determiner.Entry.instDecidableEqKind.decEq._proof_8
• Determiner.Entry.instDecidableEqKind.decEq Determiner.Entry.Kind.demonstrative Determiner.Entry.Kind.possessive = isFalse Determiner.Entry.instDecidableEqKind.decEq._proof_9
• Determiner.Entry.instDecidableEqKind.decEq Determiner.Entry.Kind.quantifier (Determiner.Entry.Kind.article d) = isFalse ⋯
• Determiner.Entry.instDecidableEqKind.decEq Determiner.Entry.Kind.quantifier Determiner.Entry.Kind.demonstrative = isFalse Determiner.Entry.instDecidableEqKind.decEq._proof_11
• Determiner.Entry.instDecidableEqKind.decEq Determiner.Entry.Kind.quantifier Determiner.Entry.Kind.quantifier = isTrue ⋯
• Determiner.Entry.instDecidableEqKind.decEq Determiner.Entry.Kind.quantifier Determiner.Entry.Kind.possessive = isFalse Determiner.Entry.instDecidableEqKind.decEq._proof_12
• Determiner.Entry.instDecidableEqKind.decEq Determiner.Entry.Kind.possessive (Determiner.Entry.Kind.article d) = isFalse ⋯
• Determiner.Entry.instDecidableEqKind.decEq Determiner.Entry.Kind.possessive Determiner.Entry.Kind.demonstrative = isFalse Determiner.Entry.instDecidableEqKind.decEq._proof_14
• Determiner.Entry.instDecidableEqKind.decEq Determiner.Entry.Kind.possessive Determiner.Entry.Kind.quantifier = isFalse Determiner.Entry.instDecidableEqKind.decEq._proof_15
• Determiner.Entry.instDecidableEqKind.decEq Determiner.Entry.Kind.possessive Determiner.Entry.Kind.possessive = isTrue ⋯

@[instance_reducible]

instance Determiner.Entry.instReprKind : Repr Kind

Equations

• Determiner.Entry.instReprKind = { reprPrec := Determiner.Entry.instReprKind.repr }

def Determiner.Entry.instReprKind.repr : Kind → ℕ → Std.Format

Equations

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

def Determiner.Entry.kind : Entry → Kind

The kind of an entry.

Equations

• (Determiner.Entry.article a).kind = Determiner.Entry.Kind.article a.definiteness
• (Determiner.Entry.demonstrative d).kind = Determiner.Entry.Kind.demonstrative
• (Determiner.Entry.quantifier q).kind = Determiner.Entry.Kind.quantifier
• (Determiner.Entry.possessive p).kind = Determiner.Entry.Kind.possessive

def Determiner.Entry.definiteUses : Entry → Finset Reference.DefiniteUse

The definite uses an entry obligatorily expones are an article's uses and a demonstrative's definiteUses; a quantifier or possessive expones none.

Equations

• (Determiner.Entry.article a).definiteUses = a.uses
• (Determiner.Entry.demonstrative d).definiteUses = d.definiteUses
• (Determiner.Entry.quantifier q).definiteUses = ∅
• (Determiner.Entry.possessive p).definiteUses = ∅

def Determiner.Entry.Marks (e : Entry) (p : Reference.Description.Strength) : Prop

An entry marks an article strength when some definite use it expones calls for it.

Equations

• e.Marks p = ∃ u ∈ e.definiteUses, u.strength = p

@[instance_reducible]

instance Determiner.Entry.instDecidableMarks (e : Entry) (p : Reference.Description.Strength) : Decidable (e.Marks p)

Equations

• e.instDecidableMarks p = id inferInstance

def Determiner.Entry.IsSyncretic (e : Entry) : Prop

An entry is syncretic when it marks both strengths, as English the does.

Equations

• e.IsSyncretic = (e.Marks Reference.Description.Strength.uniqueness ∧ e.Marks Reference.Description.Strength.familiarity)

@[instance_reducible]

instance Determiner.Entry.instDecidableIsSyncretic (e : Entry) : Decidable e.IsSyncretic

Equations

• e.instDecidableIsSyncretic = id inferInstance

Inventories

def Determiner.Inventory : Type

A language's declared determiner inventory is a list of entries. It is a def so that the operations below resolve by dot notation.

Equations

• Determiner.Inventory = List Determiner.Entry

@[instance_reducible]

instance Determiner.Inventory.instMembershipEntry : Membership Entry Inventory

Equations

• Determiner.Inventory.instMembershipEntry = { mem := Determiner.Inventory.instMembershipEntry._aux_1 }

@[instance_reducible]

instance Determiner.Inventory.instDecidableEq : DecidableEq Inventory

Equations

• Determiner.Inventory.instDecidableEq = Determiner.Inventory.instDecidableEq._aux_1

@[instance_reducible]

instance Determiner.Inventory.instDecidableExistsEntryAndMemOfDecidablePred (ds : Inventory) (p : Entry → Prop) [DecidablePred p] : Decidable (∃ e ∈ ds, p e)

Equations

• ds.instDecidableExistsEntryAndMemOfDecidablePred p = List.decidableBEx p ds

def Determiner.Inventory.Marks (ds : Inventory) (p : Reference.Description.Strength) : Prop

An inventory marks an article strength when some entry marks it.

Equations

• ds.Marks p = ∃ e ∈ ds, e.Marks p

@[instance_reducible]

instance Determiner.Inventory.instDecidableMarks (ds : Inventory) (p : Reference.Description.Strength) : Decidable (ds.Marks p)

Equations

• ds.instDecidableMarks p = id inferInstance

theorem Determiner.Inventory.marks_singleton (e : Entry) (p : Reference.Description.Strength) : Marks [e] p ↔ e.Marks p

A one-entry inventory marks a strength iff the entry marks it.

def Determiner.Inventory.IsSyncretic (ds : Inventory) : Prop

An inventory is syncretic when a single entry marks both strengths, which separates the generally marked cell from the bipartite one.

Equations

• ds.IsSyncretic = ∃ e ∈ ds, e.IsSyncretic

@[instance_reducible]

instance Determiner.Inventory.instDecidableIsSyncretic (ds : Inventory) : Decidable ds.IsSyncretic

Equations

• ds.instDecidableIsSyncretic = id inferInstance

The marking typology

A language's [moroney-2021] cell is a theorem about its inventory, and each cell is characterized by its markingStrategy_eq_*_iff lemma. If uniqueness and familiarity are both marked by one form, or uniqueness alone is marked, the cell is .generallyMarked; if they are marked by distinct forms, it is .bipartite; if familiarity alone is marked, for instance by a demonstrative, it is .markedAnaphoric; and if neither is marked, it is .unmarked.

def Determiner.Inventory.markingStrategy (ds : Inventory) : Reference.MarkingStrategy

The [moroney-2021] definiteness-marking cell derived from an inventory.

Equations

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

theorem Determiner.Inventory.markingStrategy_eq_generallyMarked_iff {ds : Inventory} : ds.markingStrategy = Reference.MarkingStrategy.generallyMarked ↔ ds.Marks Reference.Description.Strength.uniqueness ∧ (ds.IsSyncretic ∨ ¬ds.Marks Reference.Description.Strength.familiarity)

theorem Determiner.Inventory.markingStrategy_eq_bipartite_iff {ds : Inventory} : ds.markingStrategy = Reference.MarkingStrategy.bipartite ↔ ds.Marks Reference.Description.Strength.uniqueness ∧ ds.Marks Reference.Description.Strength.familiarity ∧ ¬ds.IsSyncretic

theorem Determiner.Inventory.markingStrategy_eq_markedAnaphoric_iff {ds : Inventory} : ds.markingStrategy = Reference.MarkingStrategy.markedAnaphoric ↔ ¬ds.Marks Reference.Description.Strength.uniqueness ∧ ds.Marks Reference.Description.Strength.familiarity

theorem Determiner.Inventory.markingStrategy_eq_unmarked_iff {ds : Inventory} : ds.markingStrategy = Reference.MarkingStrategy.unmarked ↔ ¬ds.Marks Reference.Description.Strength.uniqueness ∧ ¬ds.Marks Reference.Description.Strength.familiarity

def Determiner.Inventory.articleType (ds : Inventory) : Reference.ArticleType

The [schwarz-2009] article system of an inventory is the coarsening MarkingStrategy.articleType of its marking cell.

Equations

• ds.articleType = ds.markingStrategy.articleType

Realization

def Determiner.Inventory.Realizes (ds : Inventory) : Reference.Description.Kind → Prop

An inventory realizes a kind of nominal description when it carries a form for it. A bare nominal needs no determiner, a unique or anaphoric definite needs an entry marking its strength, and an indefinite, demonstrative or possessive needs an entry of that kind.

Equations

• ds.Realizes Reference.Description.Kind.bare = True
• ds.Realizes Reference.Description.Kind.indefinite = ∃ e ∈ ds, e.kind = Determiner.Entry.Kind.article Reference.Definiteness.indefinite
• ds.Realizes Reference.Description.Kind.unique = ds.Marks Reference.Description.Strength.uniqueness
• ds.Realizes Reference.Description.Kind.anaphoric = ds.Marks Reference.Description.Strength.familiarity
• ds.Realizes Reference.Description.Kind.demonstrative = ∃ e ∈ ds, e.kind = Determiner.Entry.Kind.demonstrative
• ds.Realizes Reference.Description.Kind.possessive = ∃ e ∈ ds, e.kind = Determiner.Entry.Kind.possessive

@[instance_reducible]

instance Determiner.Inventory.instDecidablePredKindRealizes (ds : Inventory) : DecidablePred ds.Realizes

Equations

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

theorem Determiner.Inventory.realizes_toKind (ds : Inventory) (p : Reference.Description.Strength) : ds.Realizes p.toKind ↔ ds.Marks p

An inventory realizes the kind of an article strength iff it marks that strength.

Article strengths

def Article.strengths (a : Article) : Finset Reference.Description.Strength

The strengths an article admits are those its uses call for. A syncretic article such as English the admits both, and a weak or strong article admits one.

Equations

• a.strengths = Finset.image Reference.DefiniteUse.strength a.uses

theorem Article.mem_strengths_iff_marks (a : Article) (p : Reference.Description.Strength) : p ∈ a.strengths ↔ (Determiner.Entry.article a).Marks p

An article admits a strength iff, as an entry, it marks that strength.