Indexicals

def Semantics.Reference.Kaplan.indexical {W : Type u_1} {E : Type u_2} (charFn : Basic.Context W E → E) : Basic.ReferringExpression (Basic.Context W E) W E

An indexical expression: its character varies with context (unlike proper names), but its content at each context is rigid.

Example: "I" has a different content when uttered by Alice vs Bob, but once we fix the context, the content rigidly picks out the agent.

Equations

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

def Semantics.Reference.Kaplan.pronI {W : Type u_1} {E : Type u_2} : Basic.ReferringExpression (Basic.Context W E) W E

"I": picks out the agent of the context.

Equations

• Semantics.Reference.Kaplan.pronI = Semantics.Reference.Kaplan.indexical fun (c : Semantics.Reference.Basic.Context W E) => c.agent

theorem Semantics.Reference.Kaplan.pronI_directlyReferential {W : Type u_1} {E : Type u_2} : Basic.isDirectlyReferential pronI.character

"I" is directly referential: at every context, its content is rigid.

def Semantics.Reference.Kaplan.pronYou {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} : Basic.ReferringExpression (Core.Context.KContext W E P T) W E

"You": picks out the addressee of the context (Speas & Tenny's HEARER).

Parallel to pronI but uses the full KContext (which has addressee) rather than the simple Context (which only has agent and world).

Equations

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

theorem Semantics.Reference.Kaplan.pronYou_directlyReferential {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} : Basic.isDirectlyReferential pronYou.character

"You" is directly referential: at every context, its content is rigid.

theorem Semantics.Reference.Kaplan.indexical_character_varies {W : Type u_1} {E : Type u_2} [Inhabited W] (charFn : Basic.Context W E → E) (c₁ c₂ : Basic.Context W E) (h : charFn c₁ ≠ charFn c₂) : (indexical charFn).character c₁ ≠ (indexical charFn).character c₂

Indexicals have non-constant character (in general).

"I" said by Alice ≠ "I" said by Bob: the character varies.

Singular Propositions

structure Semantics.Reference.Kaplan.SingularProposition (W : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

A singular proposition: a structured pair ⟨individual, property⟩.

Where unstructured propositions are sets of worlds (W → Bool), singular propositions retain the identity of the individual. This is essential for solving the Frege puzzle: ⟨Hesperus, bright⟩ ≠ ⟨Phosphorus, bright⟩ even when "Hesperus is bright" and "Phosphorus is bright" are true at exactly the same worlds.

• individual : E

  The individual the proposition is about

• property : E → W → Bool

  The property predicated of the individual

def Semantics.Reference.Kaplan.SingularProposition.eval {W : Type u_1} {E : Type u_2} (sp : SingularProposition W E) (w : W) : Bool

Evaluate a singular proposition at a world.

Equations

• sp.eval w = sp.property sp.individual w

def Semantics.Reference.Kaplan.SingularProposition.flatten {W : Type u_1} {E : Type u_2} (sp : SingularProposition W E) : W → Bool

Flatten a singular proposition to an unstructured proposition (W → Bool).

Equations

• sp.flatten w = sp.property sp.individual w

theorem Semantics.Reference.Kaplan.SingularProposition.structured_distinguishes_unstructured {W : Type u_1} {E : Type u_2} (a b : E) (P : E → W → Bool) (hab : a ≠ b) (_hflat : { individual := a, property := P }.flatten = { individual := b, property := P }.flatten) : { individual := a, property := P } ≠ { individual := b, property := P }

Two singular propositions with the same property but different individuals produce the same unstructured content iff the property can't distinguish them.

This is the formal Frege puzzle: ⟨a, P⟩ and ⟨b, P⟩ may flatten to the same W → Bool, yet remain distinct as structured propositions because a ≠ b.

Bridge to Attitude/Intensional

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

Montague's up operator (constant intension) coincides with the character of a proper name: both produce rigid e.

This connects the PTQ-style up (in Attitude/Intensional.lean) to the Kaplanian constantCharacter of a proper name.

Kaplan's Logical Truth: "I am here now"

theorem Semantics.Reference.Kaplan.i_am_here_now_logically_true {W : Type u_1} {E : Type u_2} (here : Basic.Context W E → E → W → Bool) (hCtx : ∀ (c : Basic.Context W E), here c c.agent c.world = true) (c : Basic.Context W E) : here c c.agent c.world = true

"I am here now" is a logical truth in the logic of demonstratives: at every context, the content is true at the world of the context.

It is NOT necessary — there are worlds where the agent is elsewhere. This distinguishes logical truth (true at every context) from necessity (true at every world).

Indexicals as Tower Access Patterns

Connects the character/content theory above to the ContextTower infrastructure. Each pure indexical is an AccessPattern reading from the origin (speech-act context) with a projection to the relevant coordinate. Kaplan's thesis that English indexicals are invariant under embedding operators becomes a corollary of origin_stable.

def Semantics.Reference.Kaplan.pronI_access {W' : Type u_1} {E' : Type u_2} {P' : Type u_3} {T' : Type u_4} : Core.Context.AccessPattern (Core.Context.KContext W' E' P' T') E'

"I" — first person pronoun. Reads the agent from the speech-act context.

@cite{kaplan-1989}: the character of "I" is the function that maps every context to the agent of that context. In tower terms, "I" reads from the origin (depth 0), projecting KContext.agent.

Equations

• Semantics.Reference.Kaplan.pronI_access = { depth := Core.Context.DepthSpec.origin, project := Core.Context.KContext.agent }

def Semantics.Reference.Kaplan.pronYou_access {W' : Type u_1} {E' : Type u_2} {P' : Type u_3} {T' : Type u_4} : Core.Context.AccessPattern (Core.Context.KContext W' E' P' T') E'

"you" — second person pronoun. Reads the addressee from the speech-act context.

Following @cite{speas-tenny-2003}, the addressee is a coordinate of the Kaplanian context. "You" reads from the origin, projecting KContext.addressee.

Equations

• Semantics.Reference.Kaplan.pronYou_access = { depth := Core.Context.DepthSpec.origin, project := Core.Context.KContext.addressee }

def Semantics.Reference.Kaplan.opNow_access {W' : Type u_1} {E' : Type u_2} {P' : Type u_3} {T' : Type u_4} : Core.Context.AccessPattern (Core.Context.KContext W' E' P' T') T'

"now" — temporal indexical. Reads the time from the speech-act context.

@cite{kaplan-1989} §VI: N (now) is a content operator that shifts the evaluation time to the context time. As an access pattern, "now" reads KContext.time from the origin.

Equations

• Semantics.Reference.Kaplan.opNow_access = { depth := Core.Context.DepthSpec.origin, project := Core.Context.KContext.time }

def Semantics.Reference.Kaplan.opHere_access {W' : Type u_1} {E' : Type u_2} {P' : Type u_3} {T' : Type u_4} : Core.Context.AccessPattern (Core.Context.KContext W' E' P' T') P'

"here" — spatial indexical. Reads the position from the speech-act context.

Equations

• Semantics.Reference.Kaplan.opHere_access = { depth := Core.Context.DepthSpec.origin, project := Core.Context.KContext.position }

def Semantics.Reference.Kaplan.opActually_access {W' : Type u_1} {E' : Type u_2} {P' : Type u_3} {T' : Type u_4} : Core.Context.AccessPattern (Core.Context.KContext W' E' P' T') W'

"actually" — modal indexical. Reads the world from the speech-act context.

@cite{kaplan-1989} §VI: A (actually) shifts the evaluation world to the context world. As an access pattern, "actually" reads KContext.world from the origin.

Equations

• Semantics.Reference.Kaplan.opActually_access = { depth := Core.Context.DepthSpec.origin, project := Core.Context.KContext.world }

@[simp]

theorem Semantics.Reference.Kaplan.pronI_depth {W' : Type u_1} {E' : Type u_2} {P' : Type u_3} {T' : Type u_4} : pronI_access.depth = Core.Context.DepthSpec.origin

@[simp]

theorem Semantics.Reference.Kaplan.pronYou_depth {W' : Type u_1} {E' : Type u_2} {P' : Type u_3} {T' : Type u_4} : pronYou_access.depth = Core.Context.DepthSpec.origin

@[simp]

theorem Semantics.Reference.Kaplan.opNow_depth {W' : Type u_1} {E' : Type u_2} {P' : Type u_3} {T' : Type u_4} : opNow_access.depth = Core.Context.DepthSpec.origin

@[simp]

theorem Semantics.Reference.Kaplan.opHere_depth {W' : Type u_1} {E' : Type u_2} {P' : Type u_3} {T' : Type u_4} : opHere_access.depth = Core.Context.DepthSpec.origin

@[simp]

theorem Semantics.Reference.Kaplan.opActually_depth {W' : Type u_1} {E' : Type u_2} {P' : Type u_3} {T' : Type u_4} : opActually_access.depth = Core.Context.DepthSpec.origin

theorem Semantics.Reference.Kaplan.pronI_shift_invariant {W' : Type u_1} {E' : Type u_2} {P' : Type u_3} {T' : Type u_4} (t : Core.Context.ContextTower (Core.Context.KContext W' E' P' T')) (σ : Core.Context.ContextShift (Core.Context.KContext W' E' P' T')) : pronI_access.resolve (t.push σ) = pronI_access.resolve t

"I" is invariant under any tower push. This is the formal content of Kaplan's thesis for the first person pronoun: no embedding operator (attitude verb, temporal shift, mood operator) changes what "I" refers to.

"John said that I am happy" => "I" = the actual speaker, not John.

theorem Semantics.Reference.Kaplan.pronYou_shift_invariant {W' : Type u_1} {E' : Type u_2} {P' : Type u_3} {T' : Type u_4} (t : Core.Context.ContextTower (Core.Context.KContext W' E' P' T')) (σ : Core.Context.ContextShift (Core.Context.KContext W' E' P' T')) : pronYou_access.resolve (t.push σ) = pronYou_access.resolve t

"you" is invariant under any tower push.

theorem Semantics.Reference.Kaplan.opNow_shift_invariant {W' : Type u_1} {E' : Type u_2} {P' : Type u_3} {T' : Type u_4} (t : Core.Context.ContextTower (Core.Context.KContext W' E' P' T')) (σ : Core.Context.ContextShift (Core.Context.KContext W' E' P' T')) : opNow_access.resolve (t.push σ) = opNow_access.resolve t

"now" is invariant under any tower push.

theorem Semantics.Reference.Kaplan.opHere_shift_invariant {W' : Type u_1} {E' : Type u_2} {P' : Type u_3} {T' : Type u_4} (t : Core.Context.ContextTower (Core.Context.KContext W' E' P' T')) (σ : Core.Context.ContextShift (Core.Context.KContext W' E' P' T')) : opHere_access.resolve (t.push σ) = opHere_access.resolve t

"here" is invariant under any tower push.

theorem Semantics.Reference.Kaplan.opActually_shift_invariant {W' : Type u_1} {E' : Type u_2} {P' : Type u_3} {T' : Type u_4} (t : Core.Context.ContextTower (Core.Context.KContext W' E' P' T')) (σ : Core.Context.ContextShift (Core.Context.KContext W' E' P' T')) : opActually_access.resolve (t.push σ) = opActually_access.resolve t

"actually" is invariant under any tower push.

def Semantics.Reference.Kaplan.IsKaplanCompliant {C : Type u_5} {R : Type u_6} (ap : Core.Context.AccessPattern C R) : Prop

Kaplan's thesis as a tower property: an access pattern is Kaplan-compliant iff its depth is .origin. This means it reads from the speech-act context and is unaffected by any embedding operators.

Equations

• Semantics.Reference.Kaplan.IsKaplanCompliant ap = (ap.depth = Core.Context.DepthSpec.origin)

theorem Semantics.Reference.Kaplan.kaplansThesisTower {W' : Type u_1} {E' : Type u_2} {P' : Type u_3} {T' : Type u_4} : IsKaplanCompliant pronI_access ∧ IsKaplanCompliant pronYou_access ∧ IsKaplanCompliant opNow_access ∧ IsKaplanCompliant opHere_access ∧ IsKaplanCompliant opActually_access

All English pure indexicals are Kaplan-compliant: they all read from the origin (speech-act context).

This is the tower formulation of @cite{kaplan-1989} §VIII: natural language (English) operators cannot shift the context of utterance. In tower terms, English indexicals have depth =.origin, so embedding (pushing shifts) has no effect on their resolution.

theorem Semantics.Reference.Kaplan.pronI_root {W' : Type u_1} {E' : Type u_2} {P' : Type u_3} {T' : Type u_4} (c : Core.Context.KContext W' E' P' T') : pronI_access.resolve (Core.Context.ContextTower.root c) = c.agent

In a root tower, "I" resolves to the context's agent.

theorem Semantics.Reference.Kaplan.pronYou_root {W' : Type u_1} {E' : Type u_2} {P' : Type u_3} {T' : Type u_4} (c : Core.Context.KContext W' E' P' T') : pronYou_access.resolve (Core.Context.ContextTower.root c) = c.addressee

In a root tower, "you" resolves to the context's addressee.

theorem Semantics.Reference.Kaplan.opNow_root {W' : Type u_1} {E' : Type u_2} {P' : Type u_3} {T' : Type u_4} (c : Core.Context.KContext W' E' P' T') : opNow_access.resolve (Core.Context.ContextTower.root c) = c.time

In a root tower, "now" resolves to the context's time.

theorem Semantics.Reference.Kaplan.opHere_root {W' : Type u_1} {E' : Type u_2} {P' : Type u_3} {T' : Type u_4} (c : Core.Context.KContext W' E' P' T') : opHere_access.resolve (Core.Context.ContextTower.root c) = c.position

In a root tower, "here" resolves to the context's position.

theorem Semantics.Reference.Kaplan.opActually_root {W' : Type u_1} {E' : Type u_2} {P' : Type u_3} {T' : Type u_4} (c : Core.Context.KContext W' E' P' T') : opActually_access.resolve (Core.Context.ContextTower.root c) = c.world

In a root tower, "actually" resolves to the context's world.