The Semantics of Definiteness

@cite{donnellan-1966} @cite{heim-1982} @cite{kamp-1981} @cite{moroney-2021} @cite{partee-1987} @cite{russell-1905} @cite{schwarz-2009} @cite{barwise-cooper-1981}

Connective tissue between definite-description denotations and the rest of the library. The denotational layer itself lives in two canonical pieces:

• Core.Nominal.russellIotaList (the per-context referent selector, Russellian iota over a List E filtered by a Bool predicate), and
• Core.Presupposition.PrProp.presupOfReferent (the combinator lifting a referent selector and a scope predicate into a PrProp W).

All variants — uniqueness-based, familiarity-based, anaphoric (ι^x), discourse-restricted, situation-relative — are obtained by composing these two pieces with different referent-selector arguments. There are no named wrappers (the_uniq, the_fam, the_anaphoric) at the library level; consumer files compose the two canonical pieces directly, optionally with a file-local convenience definition where one is used repeatedly.

This module retains:

• DiscourseContext — the file-card record from @cite{heim-1982}
• qforceToPresupType / qforceToDefiniteness — bridges from the English Determiner fragment to the definiteness type vocabulary
• the_is_every_on_singletons — the classical observation that ⟦the⟧ agrees with ⟦every⟧ on singleton restrictors
• modifierNecessary — abstract predicate capturing referential necessity of a modifier, shared between contrastive inference (@cite{sedivy-etal-1999}) and context-sensitive attachment (@cite{paape-vasishth-2026})

structure Semantics.Definiteness.DiscourseContext (E : Type) : Type

A discourse context tracking salient/familiar entities.

@cite{heim-1982}: the context is a set of "file cards" — entities that have been introduced into the discourse and are available for anaphoric reference. Familiarity-based definites (Schwarz's strong article) are evaluated by running the canonical Russellian-iota selector (Core.Nominal.russellIotaList) over dc.salient rather than the full domain.

• salient : List E

  Entities currently salient/familiar in discourse

theorem Semantics.Definiteness.definite_presup_iff_iota {m : Core.Logic.Intensional.Frame} (domain : List m.Entity) (restrictor : m.Denot Core.Logic.Intensional.Ty.et) : (match List.filter (fun (x : m.Denot Core.Logic.Intensional.Ty.e) => decide (restrictor x)) domain with | [head] => true | x => false) = (Composition.TypeShifting.iota domain restrictor).isSome

The uniqueness presupposition of a definite description holds iff Partee's iota succeeds on the same domain and restrictor. Both check that domain.filter restrictor is a singleton; one returns Bool (the presupposition flag), the other returns Option E (the witness).

theorem Semantics.Definiteness.the_is_every_on_singletons (m : Core.Logic.Intensional.Frame) [Fintype m.Entity] (restrictor scope : m.Entity → Prop) (e : m.Entity) (h_restr : restrictor e) (h_unique : ∀ (x : m.Entity), restrictor x → x = e) : Quantification.Quantifier.every_sem m restrictor scope ↔ scope e

⟦the⟧ agrees with ⟦every⟧ when the restrictor is a singleton.

When exactly one entity satisfies the restrictor, "the φ is ψ" and "every φ is ψ" have the same truth value. This is the classical observation that the definite article is a universal quantifier restricted to singletons.

def Semantics.Definiteness.qforceToPresupType : Theories.Semantics.Quantification.Lexicon.QForce → Option Features.Definiteness.DefPresupType

English "the" is QForce.definite — its denotation is given by composing presupOfReferent with russellIotaList domain restrictor (uniqueness-based, since English is ArticleType.weakOnly). The familiarity reading arises pragmatically (accommodation) rather than structurally.

Equations

• Semantics.Definiteness.qforceToPresupType Theories.Semantics.Quantification.Lexicon.QForce.definite = some Features.Definiteness.DefPresupType.uniqueness
• Semantics.Definiteness.qforceToPresupType x✝ = none

theorem Semantics.Definiteness.definite_is_uniqueness : qforceToPresupType Theories.Semantics.Quantification.Lexicon.QForce.definite = some Features.Definiteness.DefPresupType.uniqueness

QForce.definite maps to uniqueness by default.

def Semantics.Definiteness.qforceToDefiniteness : Theories.Semantics.Quantification.Lexicon.QForce → Features.Definiteness.Definiteness

Map QForce to Definiteness.

Equations

• Semantics.Definiteness.qforceToDefiniteness Theories.Semantics.Quantification.Lexicon.QForce.existential = Features.Definiteness.Definiteness.indefinite
• Semantics.Definiteness.qforceToDefiniteness Theories.Semantics.Quantification.Lexicon.QForce.definite = Features.Definiteness.Definiteness.definite
• Semantics.Definiteness.qforceToDefiniteness Theories.Semantics.Quantification.Lexicon.QForce.universal = Features.Definiteness.Definiteness.definite
• Semantics.Definiteness.qforceToDefiniteness Theories.Semantics.Quantification.Lexicon.QForce.negative = Features.Definiteness.Definiteness.indefinite
• Semantics.Definiteness.qforceToDefiniteness Theories.Semantics.Quantification.Lexicon.QForce.proportional = Features.Definiteness.Definiteness.indefinite

def Semantics.Definiteness.modifierNecessary {E : Type} (domain : List E) (restrictor modifier : E → Bool) : Bool

A modifier is referentially necessary in a domain when the bare restrictor fails to uniquely identify a referent but the modified (intersected) restrictor succeeds.

This captures the shared mechanism underlying:

• Contrastive inference (@cite{sedivy-etal-1999}): a scalar adjective is informative when a same-category competitor is present
• Context-sensitive attachment (@cite{paape-vasishth-2026}): an RC modifier is pragmatically licensed when multiple potential referents make the bare definite ambiguous

In both cases, the modifier rescues a failed uniqueness presupposition.

Equations

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