Interpretation of Nominal Descriptions

@cite{coppock-beaver-2015} @cite{hanink-2021} @cite{schwarz-2009} @cite{patel-grosz-grosz-2017} @cite{sharvy-1980}

Maps NominalKind F to a referent in Option F.Entity, 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 Core/Nominal/Maximality.lean:

• bare and unique ↦ russellIota (order-free uniqueness; languages with mereological structure can opt into sharvyMax instead by providing a [PartialOrder F.Entity] 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 Core.Nominal.interpret {F : Logic.Intensional.Frame} (k : NominalKind F) (g : Assignment F.Entity) (gs : Logic.Intensional.Variables.SitAssignment F) : Option F.Entity

Denotation of a NominalKind at a bi-assignment, as Option F.Entity. none is presupposition failure or inapplicability.

Equations

• Core.Nominal.interpret (Core.Nominal.NominalKind.bare R) g gs = Core.Nominal.russellIota fun (x : F.Denot Core.Logic.Intensional.Ty.e) => R g gs x
• Core.Nominal.interpret (Core.Nominal.NominalKind.indefinite restrictor) g gs = none
• Core.Nominal.interpret (Core.Nominal.NominalKind.unique R situationIdx) g gs = Core.Nominal.russellIota fun (x : F.Denot Core.Logic.Intensional.Ty.e) => R g gs x
• Core.Nominal.interpret (Core.Nominal.NominalKind.anaphoric R d) g gs = if R g gs (g d) then some (g d) else none
• Core.Nominal.interpret (Core.Nominal.NominalKind.demonstrative R deictic situationIdx d) g gs = if R g gs (g d) then some (g d) else none
• Core.Nominal.interpret (Core.Nominal.NominalKind.possessive R possessor rel) g gs = Core.Nominal.russellIota fun (x : F.Denot Core.Logic.Intensional.Ty.e) => R g gs x ∧ rel g gs (possessor g gs) x

@[simp]

theorem Core.Nominal.interpret_bare {F : Logic.Intensional.Frame} (R : Logic.Intensional.Variables.DenotGS F Logic.Intensional.Ty.et) (g : Assignment F.Entity) (gs : Logic.Intensional.Variables.SitAssignment F) : interpret (NominalKind.bare R) g gs = russellIota fun (x : F.Denot Logic.Intensional.Ty.e) => R g gs x

@[simp]

theorem Core.Nominal.interpret_indefinite {F : Logic.Intensional.Frame} (R : Logic.Intensional.Variables.DenotGS F Logic.Intensional.Ty.et) (g : Assignment F.Entity) (gs : Logic.Intensional.Variables.SitAssignment F) : interpret (NominalKind.indefinite R) g gs = none

@[simp]

theorem Core.Nominal.interpret_unique {F : Logic.Intensional.Frame} (R : Logic.Intensional.Variables.DenotGS F Logic.Intensional.Ty.et) (sIdx : ℕ) (g : Assignment F.Entity) (gs : Logic.Intensional.Variables.SitAssignment F) : interpret (NominalKind.unique R sIdx) g gs = russellIota fun (x : F.Denot Logic.Intensional.Ty.e) => R g gs x

theorem Core.Nominal.interpret_anaphoric {F : Logic.Intensional.Frame} (R : Logic.Intensional.Variables.DenotGS F Logic.Intensional.Ty.et) (d : ℕ) (g : Assignment F.Entity) (gs : Logic.Intensional.Variables.SitAssignment F) : interpret (NominalKind.anaphoric R d) g gs = if R g gs (g d) then some (g d) else none

theorem Core.Nominal.interpret_demonstrative {F : Logic.Intensional.Frame} (R : Logic.Intensional.Variables.DenotGS F Logic.Intensional.Ty.et) (deictic : Deixis.Feature) (sIdx d : ℕ) (g : Assignment F.Entity) (gs : Logic.Intensional.Variables.SitAssignment F) : interpret (NominalKind.demonstrative R deictic sIdx d) g gs = if R g gs (g d) then some (g d) else none

@[simp]

theorem Core.Nominal.interpret_possessive {F : Logic.Intensional.Frame} (R : Logic.Intensional.Variables.DenotGS F Logic.Intensional.Ty.et) (possessor : Logic.Intensional.Variables.DenotGS F Logic.Intensional.Ty.e) (rel : Logic.Intensional.Variables.DenotGS F Logic.Intensional.Ty.eet) (g : Assignment F.Entity) (gs : Logic.Intensional.Variables.SitAssignment F) : interpret (NominalKind.possessive R possessor rel) g gs = russellIota fun (x : F.Denot Logic.Intensional.Ty.e) => R g gs x ∧ rel g gs (possessor g gs) x

theorem Core.Nominal.interpret_bare_eq_unique {F : Logic.Intensional.Frame} (R : Logic.Intensional.Variables.DenotGS F Logic.Intensional.Ty.et) (sIdx : ℕ) (g : Assignment F.Entity) (gs : Logic.Intensional.Variables.SitAssignment F) : interpret (NominalKind.bare R) g gs = interpret (NominalKind.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 Core.Nominal.interpret_demonstrative_eq_anaphoric {F : Logic.Intensional.Frame} (R : Logic.Intensional.Variables.DenotGS F Logic.Intensional.Ty.et) (deictic : Deixis.Feature) (sIdx d : ℕ) (g : Assignment F.Entity) (gs : Logic.Intensional.Variables.SitAssignment F) : interpret (NominalKind.demonstrative R deictic sIdx d) g gs = interpret (NominalKind.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 Core.Nominal.interpret_unique_index_irrelevant {F : Logic.Intensional.Frame} (R : Logic.Intensional.Variables.DenotGS F Logic.Intensional.Ty.et) (sIdx₁ sIdx₂ : ℕ) (g : Assignment F.Entity) (gs : Logic.Intensional.Variables.SitAssignment F) : interpret (NominalKind.unique R sIdx₁) g gs = interpret (NominalKind.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 Core.Nominal.interpret_unique_witness_satisfies {F : Logic.Intensional.Frame} (R : Logic.Intensional.Variables.DenotGS F Logic.Intensional.Ty.et) (sIdx : ℕ) (e : F.Entity) (g : Assignment F.Entity) (gs : Logic.Intensional.Variables.SitAssignment F) (h : interpret (NominalKind.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 Core.Nominal.interpret_unique_eq_some_of_existsUnique {F : Logic.Intensional.Frame} (R : Logic.Intensional.Variables.DenotGS F Logic.Intensional.Ty.et) (sIdx : ℕ) (g : Assignment F.Entity) (gs : Logic.Intensional.Variables.SitAssignment F) (e : F.Entity) (hSat : R g gs e) (hUniq : ∀ (y : F.Denot Logic.Intensional.Ty.e), R g gs y → y = e) : interpret (NominalKind.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_existsUnique → Option.isSome_iff_exists → russellIota_witness_satisfies → case analysis.

theorem Core.Nominal.interpret_unique_eq_some_choose {F : Logic.Intensional.Frame} (R : Logic.Intensional.Variables.DenotGS F Logic.Intensional.Ty.et) (sIdx : ℕ) (g : Assignment F.Entity) (gs : Logic.Intensional.Variables.SitAssignment F) (hExU : existsUnique fun (x : F.Denot Logic.Intensional.Ty.e) => R g gs x) : interpret (NominalKind.unique R sIdx) g gs = some (Exists.choose ⋯)

Specialization of interpret_unique_eq_some_of_existsUnique to a packaged existsUnique hypothesis, with the witness extracted. The first projection of existsUnique gives the entity; the second proves uniqueness.

theorem Core.Nominal.interpret_anaphoric_witness_is_indexed {F : Logic.Intensional.Frame} (R : Logic.Intensional.Variables.DenotGS F Logic.Intensional.Ty.et) (d : ℕ) (g : Assignment F.Entity) (gs : Logic.Intensional.Variables.SitAssignment F) (e : F.Entity) (h : interpret (NominalKind.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 Core.Nominal.interpret_anaphoric_isSome_iff {F : Logic.Intensional.Frame} (R : Logic.Intensional.Variables.DenotGS F Logic.Intensional.Ty.et) (d : ℕ) (g : Assignment F.Entity) (gs : Logic.Intensional.Variables.SitAssignment F) : (interpret (NominalKind.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.