Kaplan's theory of indexicality

The three tenets of [Kap89] as [Sch11b] states them, over any context type with its coordinates given as projections. Interpretation is relativized to a context, so a sentence's character holds at a context when its content is true at that context's world (Character.HoldsAt), and a character is a priori when it holds at every context (Character.IsAPriori) and necessary when its content is true at every world (Character.IsNecessary); the two come apart because contexts are finer than worlds: when every context is proper, its agent existing at its world, I exist is a priori (Kaplan.isAPriori_existsAgent) without being necessary (Kaplan.not_isNecessary_existsAgent), and when every context is located I am here now is a priori (Kaplan.isAPriori_locatedAgent). The English pure indexicals read a coordinate of the speech-act context: as access patterns on the context tower they are AccessPattern.origin of a coordinate (Kaplan.I, Kaplan.you, Kaplan.now, Kaplan.here, Kaplan.actually), hence invariant under every embedding shift (AccessPattern.stable_origin), which is Kaplan's thesis for English. An access pattern is a character over towers with rigid content (AccessPattern.toCharacter), and an origin pattern at a root tower is Character.dthat of its coordinate (AccessPattern.origin_toCharacter_root): the tower analysis at depth zero is Kaplan's. An access pattern stable under every shift is Kaplan-compliant (AccessPattern.IsKaplanCompliant); a shift that moves some context is a monster (IsMonster), an operator on the context of utterance rather than on the circumstance of evaluation. A shift that is no monster leaves every access pattern stable (AccessPattern.stable_of_not_isMonster), and a monster is exactly a shift under which the innermost context itself is unstable (isMonster_iff_not_stable_innermost_id). The identity shift that Kaplan's thesis assigns to English attitude verbs is no monster (not_isMonster_one); the attitude shift of [Sch03a] and [anand- nevins-2004], which makes the holder the agent, is one whenever the holder is not the speaker (isMonster_attitudeShift).

References

• [Kap89]
• [Sch11b]
• [Sch03a]
• [AN04b]

A priori and necessary truth

def Reference.Character.HoldsAt {C : Type u_1} {W : Type u_3} (world : C → W) (χ : Character C W Prop) (c : C) : Prop

A character holds at a context when its content is true at the world of that context: the evaluation of a root sentence.

Equations

• Reference.Character.HoldsAt world χ c = χ c (world c)

def Reference.Character.IsAPriori {C : Type u_1} {W : Type u_3} (world : C → W) (χ : Character C W Prop) : Prop

A character is a priori when it holds at every context.

Equations

• Reference.Character.IsAPriori world χ = ∀ (c : C), Reference.Character.HoldsAt world χ c

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

A character is necessary when its content is true at every world of every context.

Equations

• χ.IsNecessary = ∀ (c : C) (w : W), χ c w

theorem Reference.Character.IsNecessary.isAPriori {C : Type u_1} {W : Type u_3} (world : C → W) {χ : Character C W Prop} (h : χ.IsNecessary) : IsAPriori world χ

def Reference.Kaplan.existsAgent {C : Type u_1} {W : Type u_3} {E : Type u_4} (agent : C → E) (exists_ : E → W → Prop) : Character C W Prop

The character of I exist: the agent of the context exists at the world of evaluation.

Equations

• Reference.Kaplan.existsAgent agent exists_ c w = exists_ (agent c) w

def Reference.Kaplan.locatedAgent {C : Type u_1} {W : Type u_3} {E : Type u_4} {P : Type u_5} {T : Type u_6} (agent : C → E) (position : C → P) (time : C → T) (located : E → P → T → W → Prop) : Character C W Prop

The character of I am here now: the agent of the context is at its position at its time in the world of evaluation.

Equations

• Reference.Kaplan.locatedAgent agent position time located c w = located (agent c) (position c) (time c) w

theorem Reference.Kaplan.isAPriori_existsAgent {C : Type u_1} {W : Type u_3} {E : Type u_4} (agent : C → E) (world : C → W) (exists_ : E → W → Prop) (h : ∀ (c : C), exists_ (agent c) (world c)) : Character.IsAPriori world (existsAgent agent exists_)

I exist is a priori when every context is proper, its agent existing at its world: Kaplan's coherence constraint on contexts.

theorem Reference.Kaplan.not_isNecessary_existsAgent {C : Type u_1} {W : Type u_3} {E : Type u_4} (agent : C → E) (exists_ : E → W → Prop) {c : C} {w : W} (h : ¬exists_ (agent c) w) : ¬(existsAgent agent exists_).IsNecessary

I exist is not necessary once some agent fails to exist at some world.

theorem Reference.Kaplan.isAPriori_locatedAgent {C : Type u_1} {W : Type u_3} {E : Type u_4} {P : Type u_5} {T : Type u_6} (agent : C → E) (world : C → W) (position : C → P) (time : C → T) (located : E → P → T → W → Prop) (h : ∀ (c : C), located (agent c) (position c) (time c) (world c)) : Character.IsAPriori world (locatedAgent agent position time located)

I am here now is a priori when every context is located.

theorem Reference.Kaplan.isAPriori_existsAgent_of_proper {W : Type u_3} {E : Type u_4} {P : Type u_5} {T : Type u_6} (exists_ : E → W → Prop) (h : ∀ (c : Context W E P T), c.Proper exists_) : Character.IsAPriori Context.world (existsAgent Context.agent exists_)

On the canonical tuple, properness of every context is Context.Proper.

Monsters

def Reference.IsMonster {C : Type u_1} (σ : Function.End C) : Prop

A context shift is a monster when it is not the identity: it moves some context.

Equations

• Reference.IsMonster σ = (σ ≠ 1)

theorem Reference.isMonster_iff {C : Type u_1} (σ : Function.End C) : IsMonster σ ↔ ∃ (c : C), σ • c ≠ c

theorem Reference.not_isMonster_one {C : Type u_1} : ¬IsMonster 1

theorem Reference.isMonster_attitudeShift {W : Type u_3} {E : Type u_4} {P : Type u_5} {T : Type u_6} (holder : E) (w' : W) (c : Context W E P T) (h : c.agent ≠ holder) : IsMonster (attitudeShift holder w')

An attitude shift to a holder other than some context's agent moves that context.

theorem Reference.AccessPattern.stable_of_not_isMonster {C : Type u_1} {R : Type u_2} (ap : AccessPattern C R) {σ : Function.End C} (h : ¬IsMonster σ) : ap.Stable σ

A shift that is no monster leaves every access pattern stable.

def Reference.AccessPattern.toCharacter {C : Type u_1} {R : Type u_2} {W : Type u_3} (ap : AccessPattern C R) : Character (ContextTower C) W R

An access pattern as a character over towers: at each tower, the rigid content at its value.

Equations

• ap.toCharacter = Reference.Character.dthat ap.resolve

@[simp]

theorem Reference.AccessPattern.toCharacter_apply {C : Type u_1} {R : Type u_2} {W : Type u_3} (ap : AccessPattern C R) (t : ContextTower C) (w : W) : ap.toCharacter t w = ap.resolve t

theorem Reference.AccessPattern.toCharacter_isDirectlyReferential {C : Type u_1} {R : Type u_2} {W : Type u_3} (ap : AccessPattern C R) : ap.toCharacter.IsDirectlyReferential

theorem Reference.AccessPattern.origin_toCharacter_root {C : Type u_1} {R : Type u_2} {W : Type u_3} (f : C → R) (c : C) : (origin f).toCharacter (ContextTower.root c) = Character.dthat f c

At a root tower an origin pattern is Kaplan's rigidifier of its coordinate.

def Reference.AccessPattern.IsKaplanCompliant {C : Type u_1} {R : Type u_2} (ap : AccessPattern C R) : Prop

An access pattern is Kaplan-compliant when it is stable under every shift.

Equations

• ap.IsKaplanCompliant = ∀ (σ : Function.End C), ap.Stable σ

theorem Reference.AccessPattern.isKaplanCompliant_origin {C : Type u_1} {R : Type u_2} (f : C → R) : (origin f).IsKaplanCompliant

theorem Reference.isMonster_iff_not_stable_innermost_id {C : Type u_1} (σ : Function.End C) : IsMonster σ ↔ ¬(AccessPattern.innermost id).Stable σ

A shift is a monster iff the innermost context is unstable under it.

The English pure indexicals

def Reference.Kaplan.I {W : Type u_3} {E : Type u_4} {P : Type u_5} {T : Type u_6} : AccessPattern (Context W E P T) E

I: the agent of the speech-act context.

Equations

• Reference.Kaplan.I = Reference.AccessPattern.origin Reference.Context.agent

def Reference.Kaplan.you {W : Type u_3} {E : Type u_4} {P : Type u_5} {T : Type u_6} : AccessPattern (Context W E P T) E

you: the addressee of the speech-act context.

Equations

• Reference.Kaplan.you = Reference.AccessPattern.origin Reference.Context.addressee

def Reference.Kaplan.now {W : Type u_3} {E : Type u_4} {P : Type u_5} {T : Type u_6} : AccessPattern (Context W E P T) T

now: the time of the speech-act context.

Equations

• Reference.Kaplan.now = Reference.AccessPattern.origin Reference.Context.time

def Reference.Kaplan.here {W : Type u_3} {E : Type u_4} {P : Type u_5} {T : Type u_6} : AccessPattern (Context W E P T) P

here: the position of the speech-act context.

Equations

• Reference.Kaplan.here = Reference.AccessPattern.origin Reference.Context.position

def Reference.Kaplan.actually {W : Type u_3} {E : Type u_4} {P : Type u_5} {T : Type u_6} : AccessPattern (Context W E P T) W

actually: the world of the speech-act context.

Equations

• Reference.Kaplan.actually = Reference.AccessPattern.origin Reference.Context.world