Interpretation of Nominal Descriptions

[CB15] [Han21] [Sch09b] [PGG17] [Sha80]

Maps Description E W to a referent in Option E, relative to a (entity, situation) bi-assignment. none represents either presupposition failure (no unique satisfier; no satisfying antecedent at the discourse index) or inapplicability (indefinites do not denote a single entity at this layer — they need separate existential-closure machinery).

The interpretation composes the operators in Semantics/Definiteness/Maximality.lean:

• bare and unique ↦ russellIota (order-free uniqueness; languages with mereological structure can opt into sharvyMax instead by providing a [PartialOrder E] instance and using a separate plural-aware interpreter)
• anaphoric and demonstrative ↦ entity-assignment lookup, accepted iff the restrictor holds of the indexed entity
• possessive ↦ russellIota of the restrictor conjoined with the possession relation applied to the possessor

A handful of agreement theorems wire the constructors together: bare and unique collapse on a shared restrictor (the default Core reading is weak/ uniqueness); demonstrative and anaphoric agree when they share restrictor and discourse index (the deictic feature is for presupposition checking, not referent selection).

noncomputable def Semantics.Definiteness.interpret {E W : Type} (k : Description E W) (g : Core.Assignment E) (gs : Intensional.Variables.SitAssignment W) : Option E

Denotation of a Description at a bi-assignment, as Option E. none is presupposition failure or inapplicability.

Equations

• Semantics.Definiteness.interpret (Semantics.Definiteness.Description.bare R) g gs = Semantics.Definiteness.russellIota fun (x : E) => R g gs x
• Semantics.Definiteness.interpret (Semantics.Definiteness.Description.indefinite restrictor) g gs = none
• Semantics.Definiteness.interpret (Semantics.Definiteness.Description.unique R situationIdx) g gs = Semantics.Definiteness.russellIota fun (x : E) => R g gs x
• Semantics.Definiteness.interpret (Semantics.Definiteness.Description.anaphoric R d) g gs = if R g gs (g d) then some (g d) else none
• Semantics.Definiteness.interpret (Semantics.Definiteness.Description.demonstrative R deictic situationIdx d) g gs = if R g gs (g d) then some (g d) else none
• Semantics.Definiteness.interpret (Semantics.Definiteness.Description.possessive R possessor rel) g gs = Semantics.Definiteness.russellIota fun (x : E) => R g gs x ∧ rel g gs (possessor g gs) x

@[simp]

theorem Semantics.Definiteness.interpret_bare {E W : Type} (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (g : Core.Assignment E) (gs : Intensional.Variables.SitAssignment W) : interpret (Description.bare R) g gs = russellIota fun (x : Intensional.Denot E W Intensional.Ty.e) => R g gs x

@[simp]

theorem Semantics.Definiteness.interpret_indefinite {E W : Type} (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (g : Core.Assignment E) (gs : Intensional.Variables.SitAssignment W) : interpret (Description.indefinite R) g gs = none

@[simp]

theorem Semantics.Definiteness.interpret_unique {E W : Type} (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (sIdx : ℕ) (g : Core.Assignment E) (gs : Intensional.Variables.SitAssignment W) : interpret (Description.unique R sIdx) g gs = russellIota fun (x : Intensional.Denot E W Intensional.Ty.e) => R g gs x

theorem Semantics.Definiteness.interpret_anaphoric {E W : Type} (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (d : ℕ) (g : Core.Assignment E) (gs : Intensional.Variables.SitAssignment W) : interpret (Description.anaphoric R d) g gs = if R g gs (g d) then some (g d) else none

theorem Semantics.Definiteness.interpret_demonstrative {E W : Type} (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (deictic : Features.Deixis.Feature) (sIdx d : ℕ) (g : Core.Assignment E) (gs : Intensional.Variables.SitAssignment W) : interpret (Description.demonstrative R deictic sIdx d) g gs = if R g gs (g d) then some (g d) else none

@[simp]

theorem Semantics.Definiteness.interpret_possessive {E W : Type} (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (possessor : Intensional.Variables.DenotGS E W Intensional.Ty.e) (rel : Intensional.Variables.DenotGS E W Intensional.Ty.eet) (g : Core.Assignment E) (gs : Intensional.Variables.SitAssignment W) : interpret (Description.possessive R possessor rel) g gs = russellIota fun (x : Intensional.Denot E W Intensional.Ty.e) => R g gs x ∧ rel g gs (possessor g gs) x

theorem Semantics.Definiteness.interpret_bare_eq_unique {E W : Type} (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (sIdx : ℕ) (g : Core.Assignment E) (gs : Intensional.Variables.SitAssignment W) : interpret (Description.bare R) g gs = interpret (Description.unique R sIdx) g gs

Bare nouns and weak/uniqueness definites agree on referent selection when they share a restrictor — the default Core reading is uniqueness. Languages whose bare nouns shift to ∃ or kind readings override this via fragment-specific interpreters.

theorem Semantics.Definiteness.interpret_demonstrative_eq_anaphoric {E W : Type} (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (deictic : Features.Deixis.Feature) (sIdx d : ℕ) (g : Core.Assignment E) (gs : Intensional.Variables.SitAssignment W) : interpret (Description.demonstrative R deictic sIdx d) g gs = interpret (Description.anaphoric R d) g gs

The deictic feature on a demonstrative does not affect referent selection: demonstratives and anaphoric definites pick the same entity when they share restrictor and discourse index. The deictic content is a presupposition filter, not a selector.

theorem Semantics.Definiteness.interpret_unique_index_irrelevant {E W : Type} (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (sIdx₁ sIdx₂ : ℕ) (g : Core.Assignment E) (gs : Intensional.Variables.SitAssignment W) : interpret (Description.unique R sIdx₁) g gs = interpret (Description.unique R sIdx₂) g gs

The situation index on a unique description does not affect the interpretation as written: the restrictor R already takes the full situation assignment, so the index records which pronoun is bound but does not change what is computed by the operator.

theorem Semantics.Definiteness.interpret_unique_witness_satisfies {E W : Type} (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (sIdx : ℕ) (e : E) (g : Core.Assignment E) (gs : Intensional.Variables.SitAssignment W) (h : interpret (Description.unique R sIdx) g gs = some e) : R g gs e

Whatever entity the interpretation returns, the restrictor holds of it. Stated for .unique (the operator-driven case); the analogue for .bare follows by interpret_bare_eq_unique.

theorem Semantics.Definiteness.interpret_unique_eq_some_of_existsUnique {E W : Type} (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (sIdx : ℕ) (g : Core.Assignment E) (gs : Intensional.Variables.SitAssignment W) (e : E) (hSat : R g gs e) (hUniq : ∀ (y : Intensional.Denot E W Intensional.Ty.e), R g gs y → y = e) : interpret (Description.unique R sIdx) g gs = some e

Witness-extraction shortcut: when an entity satisfies the restrictor and is the unique satisfier, .unique returns it. Closes the standard Russellian-iota extraction in one line — without it, every concrete interpret_* instance needs the six-step ritual of interpret_unique → russellIota_isSome_iff_exists_unique → Option.isSome_iff_exists → russellIota_witness_satisfies → case analysis.

theorem Semantics.Definiteness.interpret_unique_eq_some_choose {E W : Type} (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (sIdx : ℕ) (g : Core.Assignment E) (gs : Intensional.Variables.SitAssignment W) (hExU : ∃! x : Intensional.Denot E W Intensional.Ty.e, R g gs x) : interpret (Description.unique R sIdx) g gs = some (Exists.choose hExU)

Specialization of interpret_unique_eq_some_of_existsUnique to a packaged ∃! hypothesis, with the witness extracted via Exists.choose.

theorem Semantics.Definiteness.interpret_anaphoric_witness_is_indexed {E W : Type} (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (d : ℕ) (g : Core.Assignment E) (gs : Intensional.Variables.SitAssignment W) (e : E) (h : interpret (Description.anaphoric R d) g gs = some e) : e = g d

An anaphoric definite that returns a witness must return the indexed entity — it never picks anything else.

theorem Semantics.Definiteness.interpret_anaphoric_isSome_iff {E W : Type} (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (d : ℕ) (g : Core.Assignment E) (gs : Intensional.Variables.SitAssignment W) : (interpret (Description.anaphoric R d) g gs).isSome = true ↔ R g gs (g d)

An anaphoric definite returns a witness iff the restrictor holds of the indexed entity.

theorem Semantics.Definiteness.interpret_possessive_isSome_iff_exists_unique {E W : Type} (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (possessor : Intensional.Variables.DenotGS E W Intensional.Ty.e) (rel : Intensional.Variables.DenotGS E W Intensional.Ty.eet) (g : Core.Assignment E) (gs : Intensional.Variables.SitAssignment W) : (interpret (Description.possessive R possessor rel) g gs).isSome = true ↔ ∃! x : Intensional.Denot E W Intensional.Ty.e, R g gs x ∧ rel g gs (possessor g gs) x

A possessive definite returns a referent iff its π-modified restrictor has a unique satisfier — the typed-world form of the relational definite's uniqueness presupposition (Relational.iotaPresupposition, = ∃!).

theorem Semantics.Definiteness.interpret_anaphoric_eq_unique_of_existsUnique {E W : Type} (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (sIdx i : ℕ) (g : Core.Assignment E) (gs : Intensional.Variables.SitAssignment W) (hSat : R g gs (g i)) (hUniq : ∀ (y : Intensional.Denot E W Intensional.Ty.e), R g gs y → y = g i) : interpret (Description.anaphoric R i) g gs = interpret (Description.unique R sIdx) g gs

[PGG17]'s "DEM = PER + index": the strong article (anaphoric at index i) and the weak article (unique) over a shared restrictor pick the same referent exactly when the indexed entity g i is the unique satisfier of R. The hypotheses are load-bearing — off this condition the strong (the indexed entity) and weak (the unique satisfier) articles diverge, PG&G's point that the strong article is anaphoric in a way the weak one is not.