Characters

A character is a function from contexts to contents, a content being an intension from worlds to extensions: the two-stage semantics of [Kap89], on which the linguistic meaning of an expression fixes, at each context of utterance, what the expression says there. A character is directly referential when its content at every context is rigid (Character.IsDirectlyReferential). Kaplan's rigidifier dthat makes a directly referential character out of any context-dependent choice of individual (Character.dthat): the pure indexicals are its instances at a coordinate of the context, and dthat of a description evaluated at the context world is Kaplan's dthat[the φ]. A proper name has the constant character (Character.const), rigid also as a function of the context in the sense of IsRigid.

Main definitions

• Character C W E, Content W E
• Character.IsDirectlyReferential
• Character.dthat, Character.const

References

• [Kap89]
• [Kri80]

@[reducible, inline]

abbrev Reference.Content (W : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

Content: an intension from worlds to extensions, what an expression says at a context.

Equations

• Reference.Content W E = (W → E)

@[reducible, inline]

abbrev Reference.Character (C : Type u_1) (W : Type u_2) (E : Type u_3) : Type (max (max u_1 u_3) u_2)

A Kaplanian character: the linguistic meaning of an expression, assigning a content to each context.

Equations

• Reference.Character C W E = (C → Reference.Content W E)

def Reference.Character.IsDirectlyReferential {C : Type u_1} {W : Type u_2} {E : Type u_3} (χ : Character C W E) : Prop

A character is directly referential when its content at every context is rigid.

Equations

• χ.IsDirectlyReferential = ∀ (c : C), Reference.IsRigid (χ c)

def Reference.Character.dthat {C : Type u_1} {W : Type u_2} {E : Type u_3} (f : C → E) : Character C W E

Kaplan's rigidifier: the character that at context c rigidly designates f c.

Equations

• Reference.Character.dthat f c x✝ = f c

def Reference.Character.const {C : Type u_1} {W : Type u_2} {E : Type u_3} (e : E) : Character C W E

The constant character at e: the character of a proper name for e.

Equations

• Reference.Character.const e x✝¹ x✝ = e

@[simp]

theorem Reference.Character.dthat_apply {C : Type u_1} {W : Type u_2} {E : Type u_3} (f : C → E) (c : C) (w : W) : dthat f c w = f c

@[simp]

theorem Reference.Character.const_apply {C : Type u_1} {W : Type u_2} {E : Type u_3} (e : E) (c : C) (w : W) : const e c w = e

theorem Reference.Character.dthat_isDirectlyReferential {C : Type u_1} {W : Type u_2} {E : Type u_3} (f : C → E) : (dthat f).IsDirectlyReferential

theorem Reference.Character.const_isDirectlyReferential {C : Type u_1} {W : Type u_2} {E : Type u_3} (e : E) : (const e).IsDirectlyReferential

theorem Reference.Character.dthat_ne {W : Type u_2} {E : Type u_3} {f : W → E} {w₀ w₁ : W} (h : f w₁ ≠ f w₀) : dthat f w₀ ≠ f

Rigidifying at a context differs from the description whenever the description varies.