Donnellan (1966): Reference and Definite Descriptions

Donnellan distinguishes two uses of a definite description. Used attributively, the φ denotes at each world whoever uniquely satisfies φ there, the Russellian iota taken pointwise (attributive, attributive_eq_some_iff), and as a nominal denotation its only presupposition is that the iota is defined (attributiveNominal, attributiveNominal_resolve_eq_one_iff). Used referentially, it denotes the individual the speaker has in mind whatever the world: the constant character (Character.const), whose content is rigid. The two uses come apart in Donnellan's scene of the man with the martini: when the intended referent fails the description at a world where someone else uniquely satisfies it, the attributive use denotes that other individual and the referential use the intended one (attributive_ne_const_of_misfit).

Implementation notes

Whether the referential use is semantic or pragmatic, the dispute with Kripke, is not decided here: the file gives Donnellan's truth conditions for each use.

References

• [Don66]
• [Kri77]
• [Rus05]

noncomputable def Donnellan1966.attributive {W : Type u_1} {E : Type u_2} (φ : E → W → Prop) : W → Option E

The attributive use, which picks out at each world the unique satisfier of the description there.

Equations

• Donnellan1966.attributive φ w = Reference.iota fun (x : E) => φ x w

theorem Donnellan1966.attributive_eq_some_iff {W : Type u_1} {E : Type u_2} {φ : E → W → Prop} {w : W} {e : E} : attributive φ w = some e ↔ φ e w ∧ ∀ (x : E), φ x w → x = e

noncomputable def Donnellan1966.attributiveNominal {W : Type u_1} {E : Type u_2} (φ : E → W → Prop) : Reference.Nominal Unit W E

The attributive use as a nominal denotation, whose selector is the pointwise iota and which presupposes nothing beyond the iota's definedness.

Equations

• Donnellan1966.attributiveNominal φ = Reference.Nominal.ofReferent (Donnellan1966.attributive φ)

theorem Donnellan1966.attributiveNominal_resolve_eq_one_iff {W : Type u_1} {E : Type u_2} {φ : E → W → Prop} {w : W} {e : E} (ψ : E → W → Prop) (h : attributive φ w = some e) : (attributiveNominal φ).resolve ψ () w = 1 ↔ ψ e w

Where the description picks out e, the attributive use of the φ is ψ is true iff ψ e.

theorem Donnellan1966.attributive_ne_const_of_misfit {W : Type u_1} {E : Type u_2} {φ : E → W → Prop} {w : W} {e intended : E} (h : attributive φ w = some e) (hne : e ≠ intended) : attributive φ w ≠ some (Reference.Character.const intended () w)

In Donnellan's scene the description uniquely fits e at w while the speaker intends someone else, so the attributive use denotes e and the referential use, the constant character at the intended referent, does not.