De Re and De Dicto

Modal sentences involving referring expressions are ambiguous when the expression takes wide scope (de re) or narrow scope (de dicto) relative to the modal operator. We formalize both readings.

def Semantics.Reference.Kripke.deDicto {W : Type u_1} {E : Type u_2} (P : E → W → Prop) (t : Core.Intension W E) (w : W) : Prop

De dicto evaluation: predicate and term both evaluated at world w. This is the narrow-scope reading: the term is inside the modal operator.

"The president might have lost" (de dicto) = at some world w, whoever is president at w lost at w.

Equations

• Semantics.Reference.Kripke.deDicto P t w = P (t w) w

def Semantics.Reference.Kripke.deRe {W : Type u_1} {E : Type u_2} (P : E → W → Prop) (t : Core.Intension W E) (w₀ w : W) : Prop

De re evaluation: the term is evaluated at a fixed world w₀ (the "actual" world), while the predicate is evaluated at w. This is the wide-scope reading: the term scopes over the modal operator.

"The president might have lost" (de re) = at some world w, the actual president (Nixon) lost at w.

Equations

• Semantics.Reference.Kripke.deRe P t w₀ w = P (t w₀) w

The Scope-Rigidity Equivalence

Kripke's central insight formalized as a biconditional: a designator is rigid if and only if it is scope-inert (de re = de dicto for all predicates).

The forward direction says rigid designators eliminate scope ambiguity. The backward direction says scope-invariance FORCES rigidity — there is no other way to be scope-inert. The proof of the backward direction constructs the identity predicate as witness.

theorem Semantics.Reference.Kripke.rigid_iff_scope_invariant {W : Type u_1} {E : Type u_2} (t : Core.Intension W E) (w₀ : W) : t.IsRigid ↔ ∀ (P : E → W → Prop) (w : W), deRe P t w₀ w ↔ deDicto P t w

Main theorem. A designator is rigid if and only if de re and de dicto evaluations coincide for every predicate at every world.

Forward: names (rigid) are scope-inert. "Nixon might have lost" is unambiguous — both scope configurations yield the same proposition.

Backward: if a designator is scope-inert for ALL predicates, it must be rigid. We witness this by the identity predicate λ e _ => e = t w₀, which discriminates any referent shift.

Non-Rigidity Creates Scope Ambiguity

theorem Semantics.Reference.Kripke.nonrigid_creates_ambiguity {W : Type u_1} {E : Type u_2} (t : Core.Intension W E) (w₀ w₁ : W) (hShift : t w₁ ≠ t w₀) : ∃ (P : E → W → Prop), deRe P t w₀ w₁ ∧ ¬deDicto P t w₁

If a term shifts reference between two worlds, there exists a predicate for which de re and de dicto readings diverge.

The witness predicate is "being identical to the actual-world referent." At the shifted world, the actual referent satisfies this trivially but the shifted referent does not. This is constructive: from the mere fact that a term is non-rigid, we build the scope ambiguity.

theorem Semantics.Reference.Kripke.nonrigid_scope_sensitive {W : Type u_1} {E : Type u_2} (t : Core.Intension W E) (w₀ w₁ : W) (hShift : t w₁ ≠ t w₀) : ¬∀ (P : E → W → Prop) (w : W), deRe P t w₀ w ↔ deDicto P t w

Equivalent form: non-rigidity implies the scope-invariance property fails. Contrapositive of the backward direction of rigid_iff_scope_invariant.

The Modal Argument

Kripke's argument against the description theory of names. The formal core chains two lemmas from Core.Intension: varying_not_rigid (descriptions are non-rigid) and rigid_neq_nonrigid (rigid ≠ non-rigid).

theorem Semantics.Reference.Kripke.modal_argument {W : Type u_1} {E : Type u_2} (name desc : Core.Intension W E) (hRigid : name.IsRigid) (w₁ w₂ : W) (hVaries : desc w₁ ≠ desc w₂) : name ≠ desc

Kripke's modal argument. If a name rigidly designates an entity and the associated description varies across worlds, the name is not synonymous with the description.

This is the formal refutation of the Frege-Russell description theory of names. The proof chains varying_not_rigid and rigid_neq_nonrigid from Core.Intension.

theorem Semantics.Reference.Kripke.properName_neq_description {C : Type u_1} {W : Type u_2} {E : Type u_3} (e : E) (c : C) (desc : Core.Intension W E) (w₁ w₂ : W) (hVaries : desc w₁ ≠ desc w₂) : (Basic.properName e).character c ≠ desc

The modal argument instantiated for proper names: no proper name is synonymous with a non-rigid description.

Bridges properName from Reference/Basic.lean to the modal argument.

Essential and Accidental Properties

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

An essential property of entity e: true at every possible world.

Equations

• Semantics.Reference.Kripke.IsEssential e P = ∀ (w : W), P e w

def Semantics.Reference.Kripke.IsAccidental {W : Type u_1} {E : Type u_2} (e : E) (P : E → W → Prop) : Prop

An accidental property of entity e: true at some worlds but not others.

Equations

• Semantics.Reference.Kripke.IsAccidental e P = ((∃ (w : W), P e w) ∧ ∃ (w : W), ¬P e w)

theorem Semantics.Reference.Kripke.essential_rigid_necessary {W : Type u_1} {E : Type u_2} (e : E) (P : E → W → Prop) (name : Core.Intension W E) (hRigid : name.IsRigid) (hEss : IsEssential e P) (w₀ : W) (hRef : name w₀ = e) (w : W) : P (name w) w

Rigid designators preserve essential properties in modal contexts.

If P is essential to e, and name is a rigid designator of e, then ∀ w, P(name(w), w). Necessity "attaches to things" (Kripke), and rigid designators transparently transmit this necessity.

theorem Semantics.Reference.Kripke.nonrigid_loses_essential {W : Type u_1} {E : Type u_2} (_e : E) (P : E → W → Prop) (desc : Core.Intension W E) (w₁ : W) (hNotP : ¬P (desc w₁) w₁) : ¬∀ (w : W), P (desc w) w

Non-rigid designators can "lose" essential properties. Even if P is essential to e, a description that shifts to denote someone else at w₁ may fail P at w₁. This is why descriptions yield wrong modal predictions.

Reference-Fixing ≠ Synonymy

theorem Semantics.Reference.Kripke.rigidification_not_synonymy {W : Type u_1} {E : Type u_2} (desc : Core.Intension W E) (w₀ w₁ : W) (hVaries : desc w₁ ≠ desc w₀) : KaplanLD.dthatW desc w₀ ≠ desc

Rigidifying a non-rigid description (via dthat) yields a rigid designator that is NOT identical to the original description.

Linguistically: fixing the reference of "Hesperus" via "the bright star in the evening sky" makes "Hesperus" rigidly designate Venus, but "Hesperus" does NOT mean "the bright star in the evening sky." The description is contingent; the name (after rigidification) is rigid.

This follows from the modal argument: dthatW desc w₀ is rigid (by dthatW_isRigid), desc is non-rigid (it varies), so they differ.

Strong Rigidity

def Semantics.Reference.Kripke.IsStronglyRigid {W : Type u_1} {E : Type u_2} (exists_ : E → W → Prop) (f : Core.Intension W E) : Prop

Strong rigidity: the designator is rigid AND its designatum necessarily exists. Numbers are strongly rigid (2 exists at every world); people are not (Nixon might not have existed).

@cite{kripke-1980}: a strongly rigid designator designates an object that exists in every possible world.

Equations

• Semantics.Reference.Kripke.IsStronglyRigid exists_ f = (f.IsRigid ∧ ∀ (w : W), exists_ (f w) w)

theorem Semantics.Reference.Kripke.stronglyRigid_isRigid {W : Type u_1} {E : Type u_2} {exists_ : E → W → Prop} {f : Core.Intension W E} (h : IsStronglyRigid exists_ f) : f.IsRigid

Strongly rigid designators are rigid.

theorem Semantics.Reference.Kripke.rigid_stronglyRigid {W : Type u_1} {E : Type u_2} {exists_ : E → W → Prop} (e : E) (hExists : ∀ (w : W), exists_ e w) : IsStronglyRigid exists_ (Core.Intension.rigid e)

rigid e is strongly rigid whenever e necessarily exists.