Nominal descriptions

A Description E W is a definite description over entities E at situations W: a bare noun read by the covert iota, the weak (uniqueness) and strong (familiarity) articles of Schwarz, a deictic demonstrative, and a possessive. Its denotation ⟦k⟧ g s, relative to an entity assignment and a resource situation, is the partial individual the description picks out, none when the uniqueness presupposition fails. Every constructor is a Russellian iota over a restrictor at the situation; the strong article and the demonstrative are the iota over the restrictor conjoined with identity to the indexed entity, so the anaphoric index selects the referent while the situation only decides definedness (denote_anaphoric_eq_some_iff, denote_anaphoric_rigid), whereas the weak article's referent covaries with the situation. The possessive is the iota over the restrictor relationalized by the possession relation, Barker's Possession.π, at the possessor.

Main definitions

• Restrictor E W: a property of entities at a situation, relative to an assignment.
• Description E W, Description.denote: the descriptions and their partial individual.
• Description.kind, Description.ofStrength: the Frame-free kind and the description an article strength realizes.

Main results

• denote_unique_eq_some_iff, denote_anaphoric_eq_some_iff, denote_possessive_isSome_iff: the referent conditions of the three iotas.
• denote_bare_eq_unique, denote_demonstrative_eq_anaphoric: the covert iota is the weak article, and deixis filters without selecting.

Implementation notes

The resource situation is a Reader argument of the denotation, as the assignment is: a situation pronoun binding it, as Hanink proposes, is composition above the description, fun gs ↦ ⟦k⟧ g (gs n), not a field of it. Indefinites do not denote a partial individual and are not descriptions; Description.Kind.indefinite records them for inventory typology only. A demonstrative's deictic content and the presupposition it imposes belong to the determiner (DemonstrativeDeterminer.denote), not to the description.

References

• [Sch09b]
• [CB15]
• [PGG17]
• [Han21]
• [Mor21]
• [Rus05]
• [Sha80]
• [Bar11]

@[reducible, inline]

abbrev Reference.Restrictor (E W : Type) : Type

A restrictor is a property of entities at a situation, relative to an entity assignment.

Equations

• Reference.Restrictor E W = (Assignment E → W → E → Prop)

inductive Reference.Description (E W : Type) : Type

The definite descriptions are distinguished by form: the covert iota of a bare noun, the weak and strong articles of [Sch09b], a deictic demonstrative, and a possessive.

• bare {E W : Type} (restrictor : Restrictor E W) : Description E W

  A bare noun read by the covert iota ([Chi98], [Day04]).

• unique {E W : Type} (restrictor : Restrictor E W) : Description E W

  The weak article is [CB15]'s uniqueness definite.

• anaphoric {E W : Type} (restrictor : Restrictor E W) (discourseIdx : ℕ) : Description E W

  The strong article is the familiarity definite whose antecedent is the discourseIdx-th entity of the assignment.

• demonstrative {E W : Type} (restrictor : Restrictor E W) (discourseIdx : ℕ) : Description E W

  A deictic demonstrative ([Mor21]) is the strong article in its form, its deictic content being the determiner's.

• possessive {E W : Type} (restrictor : Restrictor E W) (possessor : Assignment E → W → E) (relation : Assignment E → W → E → E → Prop) : Description E W

  A possessive picks the unique satisfier of the restrictor that stands in relation to the possessor.

The Frame-free kind

def Reference.Description.kind {E W : Type} : Description E W → Kind

The kind of a description, its constructor with the payload erased.

Equations

• (Reference.Description.bare restrictor).kind = Reference.Description.Kind.bare
• (Reference.Description.unique restrictor).kind = Reference.Description.Kind.unique
• (Reference.Description.anaphoric restrictor discourseIdx).kind = Reference.Description.Kind.anaphoric
• (Reference.Description.demonstrative restrictor discourseIdx).kind = Reference.Description.Kind.demonstrative
• (Reference.Description.possessive restrictor possessor relation).kind = Reference.Description.Kind.possessive

def Reference.Description.ofStrength {E W : Type} (p : Strength) (R : Restrictor E W) (idx : ℕ) : Description E W

An article strength realizes the weak article over a restrictor for uniqueness and the strong article for familiarity, idx being the strong article's anaphoric index.

Equations

• Reference.Description.ofStrength Reference.Description.Strength.uniqueness R idx = Reference.Description.unique R
• Reference.Description.ofStrength Reference.Description.Strength.familiarity R idx = Reference.Description.anaphoric R idx

@[simp]

theorem Reference.Description.kind_ofStrength {E W : Type} (R : Restrictor E W) (p : Strength) (idx : ℕ) : (ofStrength p R idx).kind = p.toKind

The denotation

noncomputable def Reference.Description.denote {E W : Type} : Description E W → Assignment E → W → Option E

The partial individual a description picks out at an assignment and a resource situation: the Russellian iota over its restrictor at the situation, conjoined for the strong article and the demonstrative with identity to the indexed entity ([Sch09b]) and relationalized for the possessive by the possession relation to the possessor.

Equations

• (Reference.Description.bare R).denote x✝¹ x✝ = Reference.iota (R x✝¹ x✝)
• (Reference.Description.unique R).denote x✝¹ x✝ = Reference.iota (R x✝¹ x✝)
• (Reference.Description.anaphoric R d).denote x✝¹ x✝ = Reference.iota fun (x : E) => R x✝¹ x✝ x ∧ x = x✝¹ d
• (Reference.Description.demonstrative R d).denote x✝¹ x✝ = Reference.iota fun (x : E) => R x✝¹ x✝ x ∧ x = x✝¹ d
• (Reference.Description.possessive R possessor rel).denote x✝¹ x✝ = Reference.iota (Possession.π (R x✝¹ x✝) (rel x✝¹ x✝) (possessor x✝¹ x✝))

@[instance_reducible]

noncomputable instance Reference.Description.instDenotesForallAssignmentForallOption {E W : Type} : Semantics.Denotes (Description E W) (Assignment E → W → Option E)

Equations

• Reference.Description.instDenotesForallAssignmentForallOption = { denote := Reference.Description.denote }

@[simp]

theorem Reference.Description.denote_bare {E W : Type} (R : Restrictor E W) (g : Assignment E) (s : W) : Semantics.Denotes.denote (bare R) g s = iota (R g s)

@[simp]

theorem Reference.Description.denote_unique {E W : Type} (R : Restrictor E W) (g : Assignment E) (s : W) : Semantics.Denotes.denote (unique R) g s = iota (R g s)

@[simp]

theorem Reference.Description.denote_anaphoric {E W : Type} (R : Restrictor E W) (d : ℕ) (g : Assignment E) (s : W) : Semantics.Denotes.denote (anaphoric R d) g s = iota fun (x : E) => R g s x ∧ x = g d

@[simp]

theorem Reference.Description.denote_demonstrative {E W : Type} (R : Restrictor E W) (d : ℕ) (g : Assignment E) (s : W) : Semantics.Denotes.denote (demonstrative R d) g s = iota fun (x : E) => R g s x ∧ x = g d

@[simp]

theorem Reference.Description.denote_possessive {E W : Type} (R : Restrictor E W) (possessor : Assignment E → W → E) (rel : Assignment E → W → E → E → Prop) (g : Assignment E) (s : W) : Semantics.Denotes.denote (possessive R possessor rel) g s = iota (Possession.π (R g s) (rel g s) (possessor g s))

theorem Reference.Description.denote_bare_eq_unique {E W : Type} (R : Restrictor E W) : Semantics.Denotes.denote (bare R) = Semantics.Denotes.denote (unique R)

The covert iota of a bare noun is the weak article; the two differ in form, not meaning.

theorem Reference.Description.denote_demonstrative_eq_anaphoric {E W : Type} (R : Restrictor E W) (d : ℕ) : Semantics.Denotes.denote (demonstrative R d) = Semantics.Denotes.denote (anaphoric R d)

A demonstrative denotes as the strong article with the same index, so deixis, a presupposition on the referent, filters it without selecting it.

Referent conditions

theorem Reference.Description.denote_unique_eq_some_iff {E W : Type} (R : Restrictor E W) (g : Assignment E) (s : W) {x : E} : Semantics.Denotes.denote (unique R) g s = some x ↔ R g s x ∧ ∀ (y : E), R g s y → y = x

The weak article denotes x iff x is the unique satisfier of the restrictor at the situation.

theorem Reference.Description.denote_bare_eq_some_iff {E W : Type} (R : Restrictor E W) (g : Assignment E) (s : W) {x : E} : Semantics.Denotes.denote (bare R) g s = some x ↔ R g s x ∧ ∀ (y : E), R g s y → y = x

The covert iota denotes x iff x is the unique satisfier of the restrictor at the situation.

theorem Reference.Description.denote_unique_isSome_iff {E W : Type} (R : Restrictor E W) (g : Assignment E) (s : W) : (Semantics.Denotes.denote (unique R) g s).isSome = true ↔ ∃! x : E, R g s x

The weak article is defined iff the restrictor has a unique satisfier at the situation.

theorem Reference.Description.denote_anaphoric_eq_some_iff {E W : Type} (R : Restrictor E W) (d : ℕ) (g : Assignment E) (s : W) {x : E} : Semantics.Denotes.denote (anaphoric R d) g s = some x ↔ R g s (g d) ∧ x = g d

The strong article denotes x iff x is its antecedent and the restrictor holds of the antecedent at the situation: the index selects, the situation only decides definedness.

theorem Reference.Description.denote_anaphoric_isSome_iff {E W : Type} (R : Restrictor E W) (d : ℕ) (g : Assignment E) (s : W) : (Semantics.Denotes.denote (anaphoric R d) g s).isSome = true ↔ R g s (g d)

The strong article is defined iff the restrictor holds of its antecedent at the situation.

theorem Reference.Description.denote_anaphoric_rigid {E W : Type} (R : Restrictor E W) (d : ℕ) (g : Assignment E) (s : W) {x : E} {s' : W} {x' : E} (h : Semantics.Denotes.denote (anaphoric R d) g s = some x) (h' : Semantics.Denotes.denote (anaphoric R d) g s' = some x') : x = x'

The strong article's referent does not covary with the situation: wherever it is defined, it is the antecedent.

theorem Reference.Description.denote_possessive_isSome_iff {E W : Type} (R : Restrictor E W) (possessor : Assignment E → W → E) (rel : Assignment E → W → E → E → Prop) (g : Assignment E) (s : W) : (Semantics.Denotes.denote (possessive R possessor rel) g s).isSome = true ↔ ∃! x : E, R g s x ∧ rel g s (possessor g s) x

The possessive is defined iff exactly one satisfier of the restrictor stands in the possession relation to the possessor.