Kripke (1980): Naming and Necessity

This file formalizes the modal argument of [Kri80]. A designator is rigid exactly when the de re and the de dicto reading of every predication of it coincide (isRigid_iff_deRe_iff_deDicto): a name eliminates the scope ambiguity that a description creates, and a designator that varies between two worlds is separated from its actual-world referent by the identity predicate (exists_deRe_not_deDicto). A description that varies is therefore not synonymous with a rigid name (modal_argument), and fixing a name's reference by a description, Kaplan's dthat, does not make the two synonymous (Character.dthat_ne). Necessity attaches to things: a rigid designator of e carries e's essential properties to every world (IsEssential.of_isRigid), and a strongly rigid designator designates something that exists at every world (IsStronglyRigid).

References

• [Kri80]
• [Kap89]

def Kripke1980.deDicto {W : Type u_1} {E : Type u_2} (P : E → W → Prop) (t : W → E) (w : W) : Prop

The de dicto reading: the designator is evaluated at the world of the predication.

Equations

• Kripke1980.deDicto P t w = P (t w) w

def Kripke1980.deRe {W : Type u_1} {E : Type u_2} (P : E → W → Prop) (t : W → E) (w₀ w : W) : Prop

The de re reading: the designator is evaluated at the actual world w₀.

Equations

• Kripke1980.deRe P t w₀ w = P (t w₀) w

theorem Kripke1980.isRigid_iff_deRe_iff_deDicto {W : Type u_1} {E : Type u_2} (t : W → E) (w₀ : W) : Reference.IsRigid t ↔ ∀ (P : E → W → Prop) (w : W), deRe P t w₀ w ↔ deDicto P t w

A designator is rigid iff every predication of it reads the same de re and de dicto.

theorem Kripke1980.exists_deRe_not_deDicto {W : Type u_1} {E : Type u_2} {t : W → E} {w₀ w₁ : W} (h : t w₁ ≠ t w₀) : ∃ (P : E → W → Prop), deRe P t w₀ w₁ ∧ ¬deDicto P t w₁

A designator that varies is separated by the predicate of being its actual referent.

theorem Kripke1980.modal_argument {W : Type u_1} {E : Type u_2} {name desc : W → E} {w₁ w₂ : W} (h : Reference.IsRigid name) (hv : desc w₁ ≠ desc w₂) : name ≠ desc

The modal argument: a rigid name is not a description that varies.

def Kripke1980.IsEssential {W : Type u_1} {E : Type u_2} (e : E) (P : E → W → Prop) : Prop

An essential property of e holds of it at every world.

Equations

• Kripke1980.IsEssential e P = ∀ (w : W), P e w

theorem Kripke1980.IsEssential.of_isRigid {W : Type u_1} {E : Type u_2} {t : W → E} {P : E → W → Prop} {w₀ : W} {e : E} (hP : IsEssential e P) (ht : Reference.IsRigid t) (h : t w₀ = e) (w : W) : P (t w) w

A rigid designator of e carries e's essential properties to every world.

def Kripke1980.IsStronglyRigid {W : Type u_1} {E : Type u_2} (exists_ : E → W → Prop) (t : W → E) : Prop

A strongly rigid designator is rigid and designates something that exists at every world, as a numeral does and a name of a person does not.

Equations

• Kripke1980.IsStronglyRigid exists_ t = (Reference.IsRigid t ∧ ∀ (w : W), exists_ (t w) w)

theorem Kripke1980.isStronglyRigid_const {W : Type u_1} {E : Type u_2} {e : E} {exists_ : E → W → Prop} (h : ∀ (w : W), exists_ e w) : IsStronglyRigid exists_ fun (x : W) => e