Determiner licensing

Determiner.licenses: does a declared List Determiner.Entry have the surface form needed to realize a given Description constructor? Kept separate from Determiner.lean so that marking-only Fragments do not transitively import the E/W-parameterized Description substrate.

def Determiner.licenses {E W : Type} (ds : List Entry) : Semantics.Definiteness.Description E W → Prop

Does the declared determiner set have the surface form needed to realize the given Description constructor? Bare nominals are always licensed; unique and anaphoric definites need a determiner exponing the corresponding presupposition type (MarksPresup); indefinite/demonstrative/possessive need a determiner of that kind.

Equations

• Determiner.licenses ds (Semantics.Definiteness.Description.bare restrictor) = True
• Determiner.licenses ds (Semantics.Definiteness.Description.indefinite restrictor) = ∃ e ∈ ds, e.IsIndefiniteArticle
• Determiner.licenses ds (Semantics.Definiteness.Description.unique restrictor situationIdx) = Determiner.MarksPresup ds Features.Definiteness.DefPresupType.uniqueness
• Determiner.licenses ds (Semantics.Definiteness.Description.anaphoric restrictor discourseIdx) = Determiner.MarksPresup ds Features.Definiteness.DefPresupType.familiarity
• Determiner.licenses ds (Semantics.Definiteness.Description.demonstrative restrictor deictic situationIdx discourseIdx) = ∃ e ∈ ds, e.IsDemonstrative
• Determiner.licenses ds (Semantics.Definiteness.Description.possessive restrictor possessor relation) = ∃ e ∈ ds, e.IsPossessive

@[implicit_reducible]

instance Determiner.instDecidableLicenses {E W : Type} (ds : List Entry) (k : Semantics.Definiteness.Description E W) : Decidable (licenses ds k)

Equations

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

An article's possible denotations

The deferred Article.denote: an article denotes the set of Descriptions its admissible strengths (Article.presupTypes) realize through Description.ofPresupType — a syncretic article (English the) denotes both the weak and the strong description, not a single one.

def Article.toDescriptions {E W : Type} (a : Article) (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (idx : ℕ) : List (Semantics.Definiteness.Description E W)

An article's possible (definite-description) denotations: the image of its admissible [Sch09b] strengths under Description.ofPresupType.

Equations

• a.toDescriptions R idx = List.map (fun (x : Features.Definiteness.DefPresupType) => Semantics.Definiteness.Description.ofPresupType x R idx) a.presupTypes

theorem Determiner.licenses_ofPresupType {E W : Type} (ds : List Entry) (p : Features.Definiteness.DefPresupType) (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (idx : ℕ) : licenses ds (Semantics.Definiteness.Description.ofPresupType p R idx) ↔ MarksPresup ds p

Licensing through ofPresupType is exactly MarksPresup: a determiner set licenses the weak/strong denotation of strength p iff some determiner expones a definite use of presupposition type p. The denotation pipeline (ofPresupType) and the inventory pipeline (MarksPresup) coincide by construction.

theorem Determiner.licenses_mem_toDescriptions {E W : Type} (a : Article) (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (idx : ℕ) (k : Semantics.Definiteness.Description E W) (hk : k ∈ a.toDescriptions R idx) : licenses [Entry.article a] k

An article licenses each of its own possible denotations.