Schlenker (2003): A Plea for Monsters

@cite{schlenker-2003}

End-to-end verification of @cite{schlenker-2003}'s core argument:

1. Kaplan's thesis (no monsters) holds for English: "I" always refers to the actual speaker, even under attitude verbs
2. Amharic violates the thesis: "I" shifts to the attitude holder
3. Context quantification (ctxBox) captures both patterns:
   • With world-only meaning → reduces to standard boxAt (Fixity holds)
   • With agent-reading meaning → strictly more expressive (Fixity fails)
4. Person features as presuppositions derive logophoric pronouns

Derivation Chain

Core.Context.Tower (ContextTower, push, origin, innermost)
    ↓
Core.Context.Shifts (attitudeShift)
    ↓
Theories.Semantics.Reference.Kaplan (pronI_access, origin-reading)
    ↓
Theories.Semantics.Reference.ShiftedIndexicals (amharic_pronI, local-reading)
    ↓
Theories.Semantics.Attitudes.ContextQuantification (ctxBox, Fixity)
    ↓
Theories.Semantics.Reference.PersonFeatures (logophoric pronouns)
    ↓
This file: concrete end-to-end verification

inductive Schlenker2003.Person : Type

• alice : Person
• bob : Person

@[implicit_reducible]

instance Schlenker2003.instDecidableEqPerson : DecidableEq Person

Equations

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

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✝

@[implicit_reducible]

instance Schlenker2003.instReprPerson : Repr Person

Equations

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

inductive Schlenker2003.World : Type

• w0 : World
• w1 : World

@[implicit_reducible]

instance Schlenker2003.instDecidableEqWorld : DecidableEq World

Equations

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

@[implicit_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 = Core.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 : Core.Context.ContextTower Ctx

Equations

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

def Schlenker2003.bobBel : Semantics.Attitudes.Doxastic.AccessRel World Person

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)

@[implicit_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 : Core.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 (Core.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

@[implicit_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 : Semantics.Attitudes.ContextQuantification.ctxBox bobBel Person.bob (fun (c : Core.Context.KContext World Person Unit Unit) => isHappy Person.alice c.world) rootT World.w0 [World.w0, World.w1] = Semantics.Attitudes.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 : ¬Semantics.Attitudes.ContextQuantification.ctxBox bobBel Person.bob (fun (c : Core.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 : Semantics.Attitudes.ContextQuantification.ctxBox bobBel Person.bob (fun (c : Core.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 ctxBox does NOT reduce to boxAt.

theorem Schlenker2003.english_amharic_differ : ¬Semantics.Attitudes.ContextQuantification.ctxBox bobBel Person.bob (fun (c : Core.Context.KContext World Person Unit Unit) => isHappy Person.alice c.world) rootT World.w0 [World.w0, World.w1] ∧ Semantics.Attitudes.ContextQuantification.ctxBox bobBel Person.bob (fun (c : Core.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 @cite{schlenker-2003}'s argument that context quantification is strictly more expressive than world quantification.

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

World-only meanings satisfy Fixity (Claim 2): the truth value of "Alice is happy" is tower-independent.

theorem Schlenker2003.bridge_ctxFromShift_amharic : (Semantics.Attitudes.ContextQuantification.ctxFromShift rootT Person.bob World.w1).agent = Semantics.Reference.ShiftedIndexicals.amharic_pronI.resolve shiftedT

The agent of the accessible context (from ctxFromShift) 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 Core.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 Core.Context.DepthSpec.local = false

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