The Semantics of Definiteness

[Don66] [Hei82] [Kam81] [Mor21] [Par87] [Rus05] [Sch09b] [BC81]

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

• Semantics.Definiteness.russellIotaList (the per-context referent selector, Russellian iota over a List E filtered by a Bool predicate), and
• Semantics.Presupposition.PartialProp.presupOfReferent (the combinator lifting a referent selector and a scope predicate into a PartialProp 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 [Hei82]
• 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 ([STCC99]) and context-sensitive attachment ([PV26])

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

A discourse context tracking salient/familiar entities.

[Hei82]: 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 (Semantics.Definiteness.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 {E : Type} (domain : List E) (restrictor : E → Prop) : (match List.filter (fun (x : 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 {α : Type u_1} (restrictor scope : α → Prop) (e : α) (h_restr : restrictor e) (h_unique : ∀ (x : α), restrictor x → x = e) : Quantification.every_sem 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 : 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 Quantification.Lexicon.QForce.definite = some Features.Definiteness.DefPresupType.uniqueness
• Semantics.Definiteness.qforceToPresupType x✝ = none

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

QForce.definite maps to uniqueness by default.

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

Map QForce to Definiteness.

Equations

• Semantics.Definiteness.qforceToDefiniteness Quantification.Lexicon.QForce.existential = Features.Definiteness.Definiteness.indefinite
• Semantics.Definiteness.qforceToDefiniteness Quantification.Lexicon.QForce.definite = Features.Definiteness.Definiteness.definite
• Semantics.Definiteness.qforceToDefiniteness Quantification.Lexicon.QForce.universal = Features.Definiteness.Definiteness.definite
• Semantics.Definiteness.qforceToDefiniteness Quantification.Lexicon.QForce.negative = Features.Definiteness.Definiteness.indefinite
• Semantics.Definiteness.qforceToDefiniteness 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 ([STCC99]): a scalar adjective is informative when a same-category competitor is present
• Context-sensitive attachment ([PV26]): 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.