Demonstrations

structure Semantics.Reference.Demonstratives.Demonstration (C : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

A demonstration: an act that presents an individual in a context.

@cite{kaplan-1989} §IX: "A demonstration is, roughly, a visual presentation of a local object discriminated by a pointing." The demonstration provides the manner of presentation — different demonstrations of the same object constitute different modes of presentation.

• demonstratum : C → Option E

  Given a context, yield the demonstrated object (if any).

• description : String

  Description of the manner of presentation (for documentation).

def Semantics.Reference.Demonstratives.Demonstration.succeeds {C : Type u_1} {E : Type u_2} (d : Demonstration C E) (c : C) : Prop

A demonstration succeeds in context c if it yields a demonstratum.

Equations

• d.succeeds c = (d.demonstratum c ≠ none)

def Semantics.Reference.Demonstratives.vacuousDemonstration {C : Type u_1} {E : Type u_2} : Demonstration C E

A vacuous demonstration: always fails (hallucination, empty pointing).

Equations

• Semantics.Reference.Demonstratives.vacuousDemonstration = { demonstratum := fun (x : C) => none, description := "vacuous" }

def Semantics.Reference.Demonstratives.constantDemonstration {C : Type u_1} {E : Type u_2} (e : E) (desc : String) : Demonstration C E

A constant demonstration: always yields the same individual.

Equations

• Semantics.Reference.Demonstratives.constantDemonstration e desc = { demonstratum := fun (x : C) => some e, description := desc }

True Demonstratives

structure Semantics.Reference.Demonstratives.TrueDemonstrative (C : Type u_1) (W : Type u_2) (E : Type u_3) : Type (max (max u_1 u_2) u_3)

A true demonstrative: a demonstrative expression completed by a demonstration.

@cite{kaplan-1989} §XV: "that [pointing at Venus in the evening] is bright." The demonstration completes the character; without it, "that" is incomplete.

• demonstration : Demonstration C E

  The associated demonstration

• sortal : Option (E → W → Bool)

  Optional sortal restriction (e.g., "that planet")

def Semantics.Reference.Demonstratives.TrueDemonstrative.character {C : Type u_1} {W : Type u_2} {E : Type u_3} [Inhabited E] (td : TrueDemonstrative C W E) : C → Core.Intension W E

The character of a true demonstrative: in each context, rigidly designate the demonstratum (if the demonstration succeeds).

If the demonstration fails, the content is a trivially rigid intension returning a default entity.

Equations

• td.character c = match td.demonstration.demonstratum c with | some e => Core.Intension.rigid e | none => Core.Intension.rigid default

theorem Semantics.Reference.Demonstratives.demo_directlyReferential {C : Type u_1} {W : Type u_2} {E : Type u_3} [Inhabited E] (td : TrueDemonstrative C W E) : Basic.isDirectlyReferential td.character

Principle 2 (@cite{kaplan-1989} §XVI): Complete demonstratives are directly referential — at every context, their content is rigid.

theorem Semantics.Reference.Demonstratives.demo_character_varies {C : Type u_1} {W : Type u_2} {E : Type u_3} [Inhabited E] [Inhabited W] (td : TrueDemonstrative C W E) (c₁ c₂ : C) (e₁ e₂ : E) (h₁ : td.demonstration.demonstratum c₁ = some e₁) (h₂ : td.demonstration.demonstratum c₂ = some e₂) (hne : e₁ ≠ e₂) : td.character c₁ ≠ td.character c₂

Different demonstrations in different contexts yield different contents.

If the demonstratum differs between two contexts, the contents differ.

Demonstrative Frege Puzzle (§IX.ii-iv)

structure Semantics.Reference.Demonstratives.DemoFregePuzzle (C : Type u_1) (W : Type u_2) (E : Type u_3) : Type (max (max u_1 u_2) u_3)

The Demonstrative Frege Puzzle: "that [Hes] = that [Phos]" is informative even though both demonstrations pick out the same object (Venus).

The two demonstrations constitute different manners of presentation. The identity is informative because the characters differ (different demonstrations), even though the contents coincide.

• demo₁ : TrueDemonstrative C W E

  First demonstrative (e.g., "that" + pointing at evening star)

• demo₂ : TrueDemonstrative C W E

  Second demonstrative (e.g., "that" + pointing at morning star)

• sharedObject : E

  The shared demonstratum (Venus)

• context : C

  Context in which both demonstrations succeed with the same object

• demo₁_yields : self.demo₁.demonstration.demonstratum self.context = some self.sharedObject

  First demonstration yields the shared object

• demo₂_yields : self.demo₂.demonstration.demonstratum self.context = some self.sharedObject

  Second demonstration yields the shared object

• demonstrations_differ : self.demo₁.demonstration.description ≠ self.demo₂.demonstration.description

  The demonstrations themselves differ (different descriptions)

theorem Semantics.Reference.Demonstratives.fregePuzzle_same_content {C : Type u_1} {W : Type u_2} {E : Type u_3} [Inhabited E] (fp : DemoFregePuzzle C W E) : fp.demo₁.character fp.context = fp.demo₂.character fp.context

In a Frege puzzle configuration, the contents coincide: both demos yield the same rigid intension at the shared context.

Bridges

def Semantics.Reference.Demonstratives.TrueDemonstrative.toReferringExpression {C : Type u_1} {W : Type u_2} {E : Type u_3} [Inhabited E] (td : TrueDemonstrative C W E) : Basic.ReferringExpression C W E

Wrap a TrueDemonstrative as a ReferringExpression for integration with the Reference/Basic.lean types.

Equations

• td.toReferringExpression = { character := td.character, profile := { designation := true, singularProp := true, referentialUse := true } }

Bridge to RSA Reference Games

Demonstrations connect to RSA reference games:

• A demonstration is analogous to a pointing gesture in a reference game
• L0 (literal listener) ≈ attributive interpretation (resolves via description)
• S1 (pragmatic speaker) ≈ referential interpretation (chooses expression to single out the intended referent)

See RSA.FrankGoodman2012 for a reference game implementation.