Use Modes

inductive Semantics.Reference.Donnellan.UseMode : Type

The two uses of definite descriptions.

• attributive: The speaker means "whoever uniquely satisfies the description". Content is descriptive (non-rigid in general).
• referential: The speaker has a particular individual in mind. What is said is about that individual ([Don66]). The interpretive status of this (pragmatic vs. semantic) is disputed; see module docstring.

• attributive : UseMode
• referential : UseMode

@[implicit_reducible]

instance Semantics.Reference.Donnellan.instDecidableEqUseMode : DecidableEq UseMode

Equations

• Semantics.Reference.Donnellan.instDecidableEqUseMode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Reference.Donnellan.instReprUseMode.repr : UseMode → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Reference.Donnellan.instReprUseMode : Repr UseMode

Equations

• Semantics.Reference.Donnellan.instReprUseMode = { reprPrec := Semantics.Reference.Donnellan.instReprUseMode.repr }

Definite Descriptions

structure Semantics.Reference.Donnellan.DefiniteDescription (W : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

A definite description with a specified use mode.

The same surface form "the man drinking a martini" can be used attributively (whoever is drinking a martini) or referentially (that guy over there, whom I happen to identify via the description).

• restrictor : E → W → Bool

  The restrictor property (e.g., "man drinking a martini")

• useMode : UseMode

  How the description is being used

• intendedRef : Option E

  The speaker's intended referent (only relevant for referential use)

Attributive Semantics

def Semantics.Reference.Donnellan.attributiveContent {W : Type u_1} {E : Type u_2} (domain : List E) (restrictor : E → W → Bool) : W → Option E

Attributive content: at each world, the unique satisfier of the restrictor.

This is the Russellian analysis: "the φ" denotes, at world w, the unique entity satisfying φ at w — the canonical iota russellIotaList applied pointwise. The referent can vary across worlds.

Equations

• Semantics.Reference.Donnellan.attributiveContent domain restrictor w = Semantics.Definiteness.russellIotaList domain fun (e : E) => restrictor e w

def Semantics.Reference.Donnellan.definiteNominal {W : Type u_1} {E : Type u_2} (domain : List E) (restrictor : E → W → Bool) : NominalDenot Unit W E

The definite description as a NominalDenot: the selector is the Russellian iota (attributiveContent); there is no intrinsic presupposition beyond definedness of that selector.

This is the single source of truth for definite descriptions in the library; familiarity-based, anaphoric, and discourse-restricted variants are NominalDenots with different selectors, and pronouns add a φ-feature presup (see PersonalPronoun.denote).

Equations

• Semantics.Reference.Donnellan.definiteNominal domain restrictor = Semantics.Reference.NominalDenot.ofReferent (Semantics.Reference.Donnellan.attributiveContent domain restrictor)

Referential Semantics

def Semantics.Reference.Donnellan.referentialContent {W : Type u_1} {E : Type u_2} (intended : E) : Intensional.Intension W E

Referential content: truth conditions fixed to the speaker's intended referent, regardless of which world we evaluate at.

[Don66]: in referential use, what is said is about the intended individual. "The man drinking a martini is happy" (referential, about Jones) is true iff Jones is happy — even if Jones isn't drinking a martini.

Note: modeling this as rigid intended captures Donnellan's claim about truth conditions. Whether this represents the expression's semantic content or merely the speaker's reference is the Kripke 1977 vs Donnellan dispute — see module docstring.

Equations

• Semantics.Reference.Donnellan.referentialContent intended = Intensional.Intension.rigid intended

def Semantics.Reference.Donnellan.referentialExpression {C : Type u_1} {W : Type u_2} {E : Type u_3} (intended : E) : Basic.ReferringExpression C W E

A referential definite description as a ReferringExpression.

The profile ⟨false, false, true⟩ records:

• designation = false: not a rigid designator by linguistic type (it is a description, not a name or indexical)
• singularProp = false: per [Alm14]'s reading of Donnellan (Ch 3, §2.12), referential use gives a "proposition-free" account, not a structured ⟨individual, property⟩ pair
• referentialUse = true: the speaker has a cognitive fix on the referent

Equations

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

Donnellan Divergence

structure Semantics.Reference.Donnellan.DonnellanDivergence (W : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

Donnellan's divergence scenario: attributive and referential uses come apart when the description fails to apply to the intended referent.

Classic example: "The man drinking a martini is happy."

• The speaker intends Jones (who is actually drinking water).
• Attributive: whoever IS drinking a martini — picks out Smith.
• Referential: Jones — the speaker's intended referent.

When the description misfits, the two uses yield different truth values.

• world : W

  The world where divergence occurs

• restrictor : E → W → Bool

  The restrictor (e.g., "man drinking a martini")

• predicate : E → W → Bool

  The predicate (e.g., "is happy")

• intended : E

  Who the speaker intends

• actualSatisfier : E

  Who actually uniquely satisfies the description

• misfit : self.intended ≠ self.actualSatisfier

  The description picks out someone other than the intended referent

• intendedFails : self.restrictor self.intended self.world = false

  The intended referent doesn't satisfy the description

• satisfierSucceeds : self.restrictor self.actualSatisfier self.world = true

  The actual satisfier does satisfy the description

theorem Semantics.Reference.Donnellan.donnellanDivergence {W : Type u_1} {E : Type u_2} (d : DonnellanDivergence W E) (_hPred : d.predicate d.intended d.world ≠ d.predicate d.actualSatisfier d.world) : referentialContent d.intended d.world ≠ d.actualSatisfier

When divergence occurs, referential and attributive uses evaluate differently (assuming the predicate distinguishes the two individuals).

Bridge to Partee's Type-Shifting Triangle

theorem Semantics.Reference.Donnellan.attributive_is_pointwise_iota {W : Type u_1} {E : Type u_2} (domain : List E) (restrictor : E → W → Bool) (w : W) : attributiveContent domain restrictor w = Definiteness.russellIotaList domain fun (e : E) => restrictor e w

attributiveContent is the canonical Russellian iota russellIotaList applied pointwise: "the φ" picks, at each world w, the unique e in the domain with restrictor e w = true.