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 (@cite{donnellan-1966}). 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 referent can vary across worlds.

Equations

• Semantics.Reference.Donnellan.attributiveContent domain restrictor w = match List.filter (fun (e : E) => restrictor e w) domain with | [e] => some e | x => none

def Semantics.Reference.Donnellan.definitePrProp {W : Type u_1} {E : Type u_2} (domain : List E) (restrictor predicate : E → W → Bool) : Core.Presupposition.PrProp W

Attributive semantics wrapped in PrProp: existence and uniqueness are presupposed, the assertion is the predicate applied to the unique satisfier.

Factored as presupOfReferent ∘ attributiveContent: the referent selector is attributiveContent (Russellian iota at each world), and the canonical PrProp.presupOfReferent combinator lifts it to a presupposition+assertion bundle. This is the single source of truth for definite descriptions in the library; familiarity-based, anaphoric, and discourse-restricted variants all use presupOfReferent with different referent selectors.

Equations

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

theorem Semantics.Reference.Donnellan.definitePrProp_eq_presupOfReferent {W : Type u_1} {E : Type u_2} (domain : List E) (restrictor predicate : E → W → Bool) : definitePrProp domain restrictor predicate = Core.Presupposition.PrProp.presupOfReferent (attributiveContent domain restrictor) predicate

Unfolding lemma: definitePrProp is presupOfReferent applied to attributiveContent. By definition.

@[simp]

theorem Semantics.Reference.Donnellan.definitePrProp_presup {W : Type u_1} {E : Type u_2} (domain : List E) (restrictor predicate : E → W → Bool) (w : W) : (definitePrProp domain restrictor predicate).presup w = ((attributiveContent domain restrictor w).isSome = true)

Direct presupposition characterization: definitePrProp presupposes that attributiveContent returns some referent.

Referential Semantics

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

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

@cite{donnellan-1966}: 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 = Core.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 @cite{almog-2014}'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 = match List.filter (fun (e : E) => restrictor e w) domain with | [e] => some e | x => none

Connection to TypeShifting.iota: the attributive semantics of "the φ" is Partee's iota applied at each world. Both compute the unique satisfier of a predicate in a domain.

TypeShifting.iota domain P returns the unique e with P e = true. attributiveContent domain restrictor w returns the unique e with restrictor e w = true. These coincide when we fix the world parameter.