Almog (2014): Referential Mechanics

This file formalizes the formal core of [Alm14]. Rigid designation and directly referential content are separated by Kaplan's dthat: dthat[the φ] designates rigidly and so is scope-inert (dthat_deRe_iff_deDicto), yet two descriptions that co-denote at the context world rigidify to one content (dthat_eq_dthat_of_eq), so rigidity alone leaves the informativeness of an identity unexplained, while a structured singular proposition keeps the individuals apart (SingularProposition.mk_ne_mk_of_ne). Co-referential rigid designators have the same content, IsRigid.eq_of_apply_eq, which is the book's "no entailments" thesis: direct reference assigns Cicero is Cicero and Cicero is Tully one proposition and is silent on whether it is necessary or believed. Donnellan's referential use is a different mechanism from rigidification: reference fixed by contact with the object before any description is deployed is the constant character, and it diverges from dthat of the description whenever the description misfits (const_ne_dthat_of_ne). The Russell–Partee– Kaplan challenge is the type gap between referential and quantificational subjects: the Montague lift Quantifier.NP.individual is injective (Quantifier.NP.individual_injective) but the universal quantifier is not in its image (not_exists_individual_eq_forall), so a subject of type E cannot serve every philosopher.

Implementation notes

The book's taxonomy of three mechanisms of direct reference (designation, singular proposition, referential use), whose pairwise independence it argues expression by expression, is not formalized: a profile assigned to an expression by fiat is not derivable from its semantics, so nothing would be proved about it.

References

• [Alm14]
• [Kap89]
• [Kri80]
• [Don66]

Rigidity without singularity

theorem Almog2014.dthat_deRe_iff_deDicto {W : Type u_1} {E : Type u_2} {desc : W → E} {c w₀ w : W} (P : E → W → Prop) : Kripke1980.deRe P (Reference.Character.dthat desc c) w₀ w ↔ Kripke1980.deDicto P (Reference.Character.dthat desc c) w

dthat of a description is scope-inert.

theorem Almog2014.dthat_eq_dthat_of_eq {W : Type u_1} {E : Type u_2} {desc₁ desc₂ : W → E} {c : W} (h : desc₁ c = desc₂ c) : Reference.Character.dthat desc₁ c = Reference.Character.dthat desc₂ c

Descriptions that co-denote at the context world rigidify to one content.

structure Almog2014.SingularProposition (W : Type u_3) (E : Type u_4) : Type (max u_3 u_4)

A singular proposition: a structured pair of an individual and a property.

• individual : E

  The individual the proposition is about.

• property : E → W → Prop

  The property predicated of it.

def Almog2014.SingularProposition.flatten {W : Type u_1} {E : Type u_2} (p : SingularProposition W E) : W → Prop

The unstructured proposition a singular proposition determines.

Equations

• p.flatten = p.property p.individual

theorem Almog2014.SingularProposition.mk_ne_mk_of_ne {W : Type u_1} {E : Type u_2} {a b : E} {P : E → W → Prop} (h : a ≠ b) : { individual := a, property := P } ≠ { individual := b, property := P }

Singular propositions about distinct individuals are distinct, whatever their unstructured propositions: the Frege puzzle is dissolved by structure.

Referential use is not rigidification

theorem Almog2014.const_ne_dthat_of_ne {W : Type u_1} {E : Type u_2} {desc : W → E} {c : W} {intended : E} (h : desc c ≠ intended) : Reference.Character.const intended c ≠ Reference.Character.dthat desc c

Reference fixed on an intended individual differs from dthat of a description that misfits it.

The Russell–Partee–Kaplan challenge

theorem Almog2014.not_exists_individual_eq_forall {E : Type u_2} (a b : E) (hab : a ≠ b) : ¬∃ (e : E), Quantifier.NP.individual e = fun (P : E → Prop) => ∀ (x : E), P x

The universal quantifier is not the lift of an individual: no subject of type E serves every φ.