Schlenker 2003: attitude verbs as context quantifiers

[Sch03]'s attitude semantics: attitude verbs quantify over contexts of the reported speech act, not just worlds. Standard Hintikka semantics ([Hin62]) — ∀w'. R(x,w,w') → p(w') — is the special case where the embedded meaning reads only the world coordinate (contextBox_world_only); in languages with shifted indexicals (Amharic, Zazaki) the agent coordinate carries semantic content that world quantification cannot express, because the embedded first person reads the agent of the shifted context (reportedContext_agent) while English I is invariant under the shift (english_I_invariant).

ContextBox is the operator: at each accessible world the embedded meaning is evaluated against reportedContext, the context of the reported speech act — the innermost context after pushing the attitude shift, with the holder as agent, the accessible world as world, and the remaining coordinates inherited. doxastic_holdsAt_iff_contextBox grounds the DoxasticPredicate API of Doxastic.lean as veridicality plus context quantification over a world-only meaning.

SatisfiesFixity renders the paper's Fixity Thesis, his (1): a meaning whose truth value is independent of the context tower. World-only meanings satisfy it (fixity_world_only); the shift-reading meanings of his monster-friendly logics (Appendix B) are the failures. A tower-general monstrous operator — an embedded meaning consuming the whole shifted tower, needed for mixed origin/local readings — is the generalization to mint when a study requires it; ContextBox's meaning consults only the reported context.

The model sections verify the argument end to end on a two-person, two-world model: English I refers to the actual speaker even under attitudes (Kaplan's thesis), Amharic I shifts to the attitude holder, ContextBox captures both patterns — reducing to BoxAt on world-only meanings, where Fixity holds, and strictly exceeding it on agent-reading meanings — and person features as presuppositions derive logophoric pronouns.

The context of the reported speech act

def Schlenker2003.reportedContext {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (t : Semantics.Context.ContextTower (Semantics.Context.KContext W E P T)) (holder : E) (w' : W) : Semantics.Context.KContext W E P T

The context of the reported speech act ([Sch03] (4)): push the attitude shift onto the tower and read the innermost context — the holder becomes the agent, the accessible world the world, and the remaining coordinates are inherited.

Equations

• Schlenker2003.reportedContext t holder w' = (t.push (Semantics.Context.attitudeShift holder w')).innermost

@[simp]

theorem Schlenker2003.reportedContext_world {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (t : Semantics.Context.ContextTower (Semantics.Context.KContext W E P T)) (holder : E) (w' : W) : (reportedContext t holder w').world = w'

@[simp]

theorem Schlenker2003.reportedContext_agent {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (t : Semantics.Context.ContextTower (Semantics.Context.KContext W E P T)) (holder : E) (w' : W) : (reportedContext t holder w').agent = holder

@[simp]

theorem Schlenker2003.reportedContext_time {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (t : Semantics.Context.ContextTower (Semantics.Context.KContext W E P T)) (holder : E) (w' : W) : (reportedContext t holder w').time = t.innermost.time

@[simp]

theorem Schlenker2003.reportedContext_position {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (t : Semantics.Context.ContextTower (Semantics.Context.KContext W E P T)) (holder : E) (w' : W) : (reportedContext t holder w').position = t.innermost.position

@[simp]

theorem Schlenker2003.reportedContext_addressee {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (t : Semantics.Context.ContextTower (Semantics.Context.KContext W E P T)) (holder : E) (w' : W) : (reportedContext t holder w').addressee = t.innermost.addressee

Context quantification

def Schlenker2003.ContextBox {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (R : E → W → W → Prop) (holder : E) (φ : Semantics.Context.KContext W E P T → Prop) (t : Semantics.Context.ContextTower (Semantics.Context.KContext W E P T)) (w : W) (worlds : List W) : Prop

ContextBox R holder φ t w worlds iff at every accessible world w' the embedded meaning φ holds of the context of the reported speech act — [Sch03]'s attitude verb quantifying over contexts, with the finite worlds list as the decidable rendering of the quantification (cf. BoxAt).

Equations

• Schlenker2003.ContextBox R holder φ t w worlds = ∀ w' ∈ worlds, R holder w w' → φ (Schlenker2003.reportedContext t holder w')

@[instance_reducible]

instance Schlenker2003.instDecidableContextBoxOfDecidablePredKContext {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (R : E → W → W → Prop) [(a : E) → (w w' : W) → Decidable (R a w w')] (holder : E) (φ : Semantics.Context.KContext W E P T → Prop) [DecidablePred φ] (t : Semantics.Context.ContextTower (Semantics.Context.KContext W E P T)) (w : W) (worlds : List W) : Decidable (ContextBox R holder φ t w worlds)

Equations

• Schlenker2003.instDecidableContextBoxOfDecidablePredKContext R holder φ t w worlds = Schlenker2003.instDecidableContextBoxOfDecidablePredKContext._aux_1 R holder φ t w worlds

theorem Schlenker2003.contextBox_world_only {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (R : E → W → W → Prop) (holder : E) (p : W → Prop) (t : Semantics.Context.ContextTower (Semantics.Context.KContext W E P T)) (w : W) (worlds : List W) : ContextBox R holder (fun (c : Semantics.Context.KContext W E P T) => p c.world) t w worlds ↔ Doxastic.BoxAt R holder w worlds p

With a world-only meaning, context quantification is Hintikka world quantification — the sense in which [Hin62]'s semantics is a special case of [Sch03]'s.

theorem Schlenker2003.doxastic_holdsAt_iff_contextBox {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (V : Doxastic.DoxasticPredicate W E) (agent : E) (p : W → Prop) (w : W) (worlds : List W) (t : Semantics.Context.ContextTower (Semantics.Context.KContext W E P T)) : V.HoldsAt agent p w worlds ↔ Doxastic.VeridicalityHolds V.veridicality p w ∧ ContextBox V.access agent (fun (c : Semantics.Context.KContext W E P T) => p c.world) t w worlds

DoxasticPredicate.HoldsAt is a veridicality check plus context quantification over a world-only meaning — every doxastic predicate of Doxastic.lean is a special case of [Sch03]'s context quantification.

The Fixity Thesis

def Schlenker2003.SatisfiesFixity {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (φ : Semantics.Context.ContextTower (Semantics.Context.KContext W E P T) → W → Prop) : Prop

The Fixity Thesis, [Sch03] (1): "the semantic value of an indexical is fixed solely by the context of the actual speech act, and cannot be affected by any logical operators." Rendered on tower-parameterized meanings: the truth value is independent of the tower configuration. It holds of every meaning of a monster-free language and fails for the shift-reading meanings of the paper's monster-friendly logics (Appendix B).

Equations

• Schlenker2003.SatisfiesFixity φ = ∀ (t₁ t₂ : Semantics.Context.ContextTower (Semantics.Context.KContext W E P T)) (w : W), φ t₁ w ↔ φ t₂ w

theorem Schlenker2003.fixity_world_only {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (p : W → Prop) : SatisfiesFixity fun (x : Semantics.Context.ContextTower (Semantics.Context.KContext W E P T)) (w : W) => p w

World-only meanings satisfy the Fixity Thesis.

Shifted indexicals

theorem Schlenker2003.english_I_invariant {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (t : Semantics.Context.ContextTower (Semantics.Context.KContext W E P T)) (holder : E) (w' : W) : Semantics.Reference.Kaplan.pronI_access.resolve (t.push (Semantics.Context.attitudeShift holder w')) = Semantics.Reference.Kaplan.pronI_access.resolve t

English I is invariant under the attitude shift used by ContextBox — it resolves to the origin agent (the actual speaker), not the attitude holder.

inductive Schlenker2003.Person : Type

• alice : Person
• bob : Person

@[instance_reducible]

instance Schlenker2003.instDecidableEqPerson : DecidableEq Person

Equations

• Schlenker2003.instDecidableEqPerson x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Schlenker2003.instReprPerson : Repr Person

Equations

• Schlenker2003.instReprPerson = { reprPrec := Schlenker2003.instReprPerson.repr }

def Schlenker2003.instReprPerson.repr : Person → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Schlenker2003.instReprPerson.repr Schlenker2003.Person.bob prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Schlenker2003.Person.bob")).group prec✝

inductive Schlenker2003.World : Type

• w0 : World
• w1 : World

@[instance_reducible]

instance Schlenker2003.instDecidableEqWorld : DecidableEq World

Equations

• Schlenker2003.instDecidableEqWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Schlenker2003.instReprWorld : Repr World

Equations

• Schlenker2003.instReprWorld = { reprPrec := Schlenker2003.instReprWorld.repr }

def Schlenker2003.instReprWorld.repr : World → ℕ → Std.Format

Equations

• Schlenker2003.instReprWorld.repr Schlenker2003.World.w0 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Schlenker2003.World.w0")).group prec✝
• Schlenker2003.instReprWorld.repr Schlenker2003.World.w1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Schlenker2003.World.w1")).group prec✝

@[reducible, inline]

abbrev Schlenker2003.Ctx : Type

Equations

• Schlenker2003.Ctx = Semantics.Context.KContext Schlenker2003.World Schlenker2003.Person Unit Unit

def Schlenker2003.speechCtx : Ctx

Speech-act context: Alice speaking to Bob at world w0.

Equations

• Schlenker2003.speechCtx = { agent := Schlenker2003.Person.alice, addressee := Schlenker2003.Person.bob, world := Schlenker2003.World.w0, time := (), position := () }

def Schlenker2003.rootT : Semantics.Context.ContextTower Ctx

Equations

• Schlenker2003.rootT = Semantics.Context.ContextTower.root Schlenker2003.speechCtx

def Schlenker2003.bobBel : Person → World → World → Prop

Bob's doxastic accessibility: both worlds are compatible with what Bob believes.

Equations

• Schlenker2003.bobBel Schlenker2003.Person.bob x✝¹ x✝ = True
• Schlenker2003.bobBel Schlenker2003.Person.alice x✝¹ x✝ = (x✝ = Schlenker2003.World.w0)

@[instance_reducible]

instance Schlenker2003.instDecidableBobBel (a : Person) (w w' : World) : Decidable (bobBel a w w')

Equations

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

def Schlenker2003.shiftedT : Semantics.Context.ContextTower Ctx

Tower after attitude shift: "Bob said that ..." pushes Bob as agent and w1 as the attitude world.

Equations

• Schlenker2003.shiftedT = Schlenker2003.rootT.push (Semantics.Context.attitudeShift Schlenker2003.Person.bob Schlenker2003.World.w1)

theorem Schlenker2003.english_I_is_speaker : Semantics.Reference.Kaplan.pronI_access.resolve shiftedT = Person.alice

English "I" = Alice (actual speaker), even under Bob's attitude verb.

theorem Schlenker2003.amharic_I_is_holder : Semantics.Reference.ShiftedIndexicals.amharic_pronI.resolve shiftedT = Person.bob

Amharic "I" = Bob (attitude holder), shifted by the attitude verb.

theorem Schlenker2003.indexicals_diverge : Semantics.Reference.Kaplan.pronI_access.resolve shiftedT ≠ Semantics.Reference.ShiftedIndexicals.amharic_pronI.resolve shiftedT

English and Amharic "I" diverge under the same attitude shift.

def Schlenker2003.isHappy : Person → World → Prop

Happiness predicate: Alice is happy in w0 only; Bob is happy in both.

Equations

• Schlenker2003.isHappy Schlenker2003.Person.alice Schlenker2003.World.w0 = True
• Schlenker2003.isHappy Schlenker2003.Person.alice Schlenker2003.World.w1 = False
• Schlenker2003.isHappy Schlenker2003.Person.bob x✝ = True

@[instance_reducible]

instance Schlenker2003.instDecidableIsHappy (p : Person) (w : World) : Decidable (isHappy p w)

Equations

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

theorem Schlenker2003.english_reduces_to_BoxAt : ContextBox bobBel Person.bob (fun (c : Semantics.Context.KContext World Person Unit Unit) => isHappy Person.alice c.world) rootT World.w0 [World.w0, World.w1] ↔ Doxastic.BoxAt bobBel Person.bob World.w0 [World.w0, World.w1] (isHappy Person.alice)

English: "Bob said that I am happy" = "Bob said that Alice is happy." The meaning is world-only (Alice is fixed by origin-reading "I"), so context quantification reduces to standard world quantification.

theorem Schlenker2003.english_result : ¬ContextBox bobBel Person.bob (fun (c : Semantics.Context.KContext World Person Unit Unit) => isHappy Person.alice c.world) rootT World.w0 [World.w0, World.w1]

English version is false: Alice is NOT happy in all of Bob's belief worlds (she's unhappy in w1).

theorem Schlenker2003.amharic_result : ContextBox bobBel Person.bob (fun (c : Semantics.Context.KContext World Person Unit Unit) => isHappy c.agent c.world) rootT World.w0 [World.w0, World.w1]

Amharic: "Bob said that I am happy" = "Bob said that Bob is happy." The meaning reads the agent from the shifted context (Bob), so ContextBox does NOT reduce to BoxAt.

theorem Schlenker2003.english_amharic_differ : ¬ContextBox bobBel Person.bob (fun (c : Semantics.Context.KContext World Person Unit Unit) => isHappy Person.alice c.world) rootT World.w0 [World.w0, World.w1] ∧ ContextBox bobBel Person.bob (fun (c : Semantics.Context.KContext World Person Unit Unit) => isHappy c.agent c.world) rootT World.w0 [World.w0, World.w1]

The English and Amharic versions have different truth values: English fails, Amharic holds. This is the formal content of [Sch03]'s argument that context quantification is strictly more expressive than world quantification.

theorem Schlenker2003.fixity_english : SatisfiesFixity fun (x : Semantics.Context.ContextTower (Semantics.Context.KContext World Person Unit Unit)) (w : World) => isHappy Person.alice w

World-only meanings satisfy the Fixity Thesis: the truth value of "Alice is happy" is tower-independent.

theorem Schlenker2003.bridge_reportedContext_amharic : (reportedContext rootT Person.bob World.w1).agent = Semantics.Reference.ShiftedIndexicals.amharic_pronI.resolve shiftedT

The agent of the reported context is exactly what Amharic "I" (amharic_pronI) resolves to.

theorem Schlenker2003.bridge_english_invariant : Semantics.Reference.Kaplan.pronI_access.resolve shiftedT = Semantics.Reference.Kaplan.pronI_access.resolve rootT

English "I" gives the same result with or without the shift: both return Alice (the origin agent).

theorem Schlenker2003.bob_is_logophoric : Semantics.Reference.PersonFeatures.isLogophoric Person.bob shiftedT Semantics.Context.DepthSpec.local = true

Bob is logophoric under the attitude shift: he is +author(local) (agent of the embedded context) but −author* (not the actual speaker Alice).

theorem Schlenker2003.alice_not_logophoric : Semantics.Reference.PersonFeatures.isLogophoric Person.alice shiftedT Semantics.Context.DepthSpec.local = false

Alice (the speaker) is never logophoric: +author* blocks it.