Context and Character

structure Semantics.Reference.Basic.Context (W : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

A Kaplanian context of utterance.

Contexts supply the parameters that indexicals depend on: who is speaking, what world is actual, etc. Following @cite{kaplan-1989}, characters are functions from contexts to contents.

• agent : E

  The agent of the context (the speaker)

• world : W

  The world of the context (the actual world)

@[reducible, inline]

abbrev Semantics.Reference.Basic.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: a function from contexts to contents (intensions).

Characters represent the linguistic meaning of an expression — what any competent speaker knows. Content (= intension) represents what is said on a particular occasion of use.

Equations

• Semantics.Reference.Basic.Character C W E = (C → Core.Intension W E)

@[reducible, inline]

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

Content is just an intension — a function from worlds to extensions.

Equations

• Semantics.Reference.Basic.Content W E = Core.Intension W E

Referential Profile (@cite{almog-2014})

structure Semantics.Reference.Basic.ReferentialProfile : Type

@cite{almog-2014}'s three independent mechanisms of direct reference, represented as a three-dimensional Boolean profile.

Each dimension is a distinct way that an expression can refer:

• designation: The expression rigidly designates its referent (Kripke)
• singularProp: The content is a structured singular proposition (Kaplan)
• referentialUse: The speaker uses the expression to pick out a particular individual, regardless of the expression's descriptive content (Donnellan)

The three dimensions are logically independent: any of the 2³ = 8 combinations is coherent, and @cite{almog-2014} argues each is linguistically attested.

• designation : Bool

  Kripke: the expression rigidly designates its referent

• singularProp : Bool

  Kaplan: the content is a structured ⟨individual, property⟩ pair

• referentialUse : Bool

  Donnellan: the speaker has a cognitive fix on a particular individual

instance Semantics.Reference.Basic.instDecidableEqReferentialProfile : DecidableEq ReferentialProfile

Equations

• Semantics.Reference.Basic.instDecidableEqReferentialProfile = Semantics.Reference.Basic.instDecidableEqReferentialProfile.decEq

def Semantics.Reference.Basic.instDecidableEqReferentialProfile.decEq (x✝ x✝¹ : ReferentialProfile) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

def Semantics.Reference.Basic.instBEqReferentialProfile.beq : ReferentialProfile → ReferentialProfile → Bool

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Reference.Basic.instBEqReferentialProfile.beq x✝¹ x✝ = false

instance Semantics.Reference.Basic.instBEqReferentialProfile : BEq ReferentialProfile

Equations

• Semantics.Reference.Basic.instBEqReferentialProfile = { beq := Semantics.Reference.Basic.instBEqReferentialProfile.beq }

instance Semantics.Reference.Basic.instReprReferentialProfile : Repr ReferentialProfile

Equations

• Semantics.Reference.Basic.instReprReferentialProfile = { reprPrec := Semantics.Reference.Basic.instReprReferentialProfile.repr }

def Semantics.Reference.Basic.instReprReferentialProfile.repr : ReferentialProfile → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

structure Semantics.Reference.Basic.ReferringExpression (C : Type u_1) (W : Type u_2) (E : Type u_3) : Type (max (max u_1 u_2) u_3)

A referring expression bundles a character with its referential profile.

• character : Character C W E

  The expression's character (linguistic meaning)

• profile : ReferentialProfile

  Which direct-reference mechanisms the expression exhibits

Direct Reference Properties

def Semantics.Reference.Basic.isDirectlyReferential {C : Type u_1} {W : Type u_2} {E : Type u_3} (char : Character C W E) : Prop

An expression is directly referential iff its content is rigid at every context.

@cite{kaplan-1989}: "For directly referential terms, the referent determines the content; once we fix the referent, the content is just the referent itself."

Equations

• Semantics.Reference.Basic.isDirectlyReferential char = ∀ (c : C), (char c).IsRigid

def Semantics.Reference.Basic.constantCharacter {C : Type u_1} {W : Type u_2} {E : Type u_3} (char : Character C W E) : Prop

A character is constant iff it assigns the same content at every context.

Proper names have constant character: "Aristotle" picks out the same intension regardless of who utters it or when.

Equations

• Semantics.Reference.Basic.constantCharacter char = ∀ (c₁ c₂ : C), char c₁ = char c₂

Proper Names

def Semantics.Reference.Basic.properName {C : Type u_1} {W : Type u_2} {E : Type u_3} (e : E) : ReferringExpression C W E

A proper name for entity e: constant character, rigid content.

"Aristotle" ↦ at every context, the intension λw. e (the constant function returning e). This is the paradigm case of direct reference via the designation mechanism.

Equations

• Semantics.Reference.Basic.properName e = { character := fun (x : C) => Core.Intension.rigid e, profile := { designation := true, singularProp := true, referentialUse := false } }

theorem Semantics.Reference.Basic.properName_constantCharacter {C : Type u_1} {W : Type u_2} {E : Type u_3} (e : E) : constantCharacter (properName e).character

Proper names have constant character.

theorem Semantics.Reference.Basic.properName_isDirectlyReferential {C : Type u_1} {W : Type u_2} {E : Type u_3} (e : E) : isDirectlyReferential (properName e).character

Proper names are directly referential.

theorem Semantics.Reference.Basic.properName_content_eq_rigid {C : Type u_1} {W : Type u_2} {E : Type u_3} (e : E) (c : C) : (properName e).character c = Core.Intension.rigid e

The content of a proper name equals rigid e, connecting to Core.Intension.

De Jure vs De Facto Rigidity

def Semantics.Reference.Basic.IsDeJureRigid {C : Type u_1} {W : Type u_2} {E : Type u_3} (expr : ReferringExpression C W E) : Prop

De jure rigidity: the expression is rigid by mechanism — its linguistic meaning guarantees rigidity. Proper names and indexicals are de jure rigid.

Cf. @cite{kripke-1980}: "one meter" is de facto rigid (happens to pick out the same length at every world) but not de jure rigid (its character involves a description).

Equations

• Semantics.Reference.Basic.IsDeJureRigid expr = (expr.profile.designation = true ∧ Semantics.Reference.Basic.isDirectlyReferential expr.character)

def Semantics.Reference.Basic.IsDeFactoRigid {C : Type u_1} {W : Type u_2} {E : Type u_3} (expr : ReferringExpression C W E) (c : C) : Prop

De facto rigidity: the expression happens to have rigid content at the actual context, but not by mechanism. "The smallest prime" is de facto rigid (it's 2 at every world) but its character is descriptive.

Equations

• Semantics.Reference.Basic.IsDeFactoRigid expr c = ((expr.character c).IsRigid ∧ expr.profile.designation = false)

theorem Semantics.Reference.Basic.properName_deJureRigid {C : Type u_1} {W : Type u_2} {E : Type u_3} (e : E) : IsDeJureRigid (properName e)

Proper names are de jure rigid.

theorem Semantics.Reference.Basic.properNames_corefer_coextensional {C : Type u_1} {W : Type u_2} {E : Type u_3} (e₁ e₂ : E) (c : C) (w : W) (h : ((properName e₁).character c).CoRefer ((properName e₂).character c) w) : ((properName e₁).character c).CoExtensional ((properName e₂).character c)

Two proper names that co-refer are co-extensional (Kripke's argument).

Bridge to Core.Intension.rigid_identity_necessary: if "Hesperus" and "Phosphorus" are both proper names and co-refer at the actual world, they have the same content.

Bridge to KContext

def Semantics.Reference.Basic.Context.toKContext {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : Context W E) (addr : E) (p : P) (t : T) : Core.Context.KContext W E P T

Lift a simple Context W E to a full KContext W E P T by supplying trivial time and position.

This allows existing code using the two-component context to interoperate with the full Kaplanian context.

Equations

• c.toKContext addr p t = { agent := c.agent, addressee := addr, world := c.world, time := t, position := p }