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 Phenomena.Reference.Studies.Schlenker2003.Person : Type

• alice : Person
• bob : Person

instance Phenomena.Reference.Studies.Schlenker2003.instDecidableEqPerson : DecidableEq Person

Equations

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

def Phenomena.Reference.Studies.Schlenker2003.instBEqPerson.beq : Person → Person → Bool

Equations

• Phenomena.Reference.Studies.Schlenker2003.instBEqPerson.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Reference.Studies.Schlenker2003.instBEqPerson : BEq Person

Equations

• Phenomena.Reference.Studies.Schlenker2003.instBEqPerson = { beq := Phenomena.Reference.Studies.Schlenker2003.instBEqPerson.beq }

instance Phenomena.Reference.Studies.Schlenker2003.instReprPerson : Repr Person

Equations

• Phenomena.Reference.Studies.Schlenker2003.instReprPerson = { reprPrec := Phenomena.Reference.Studies.Schlenker2003.instReprPerson.repr }

def Phenomena.Reference.Studies.Schlenker2003.instReprPerson.repr : Person → ℕ → Std.Format

Equations

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

inductive Phenomena.Reference.Studies.Schlenker2003.World : Type

• w0 : World
• w1 : World

instance Phenomena.Reference.Studies.Schlenker2003.instDecidableEqWorld : DecidableEq World

Equations

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

instance Phenomena.Reference.Studies.Schlenker2003.instBEqWorld : BEq World

Equations

• Phenomena.Reference.Studies.Schlenker2003.instBEqWorld = { beq := Phenomena.Reference.Studies.Schlenker2003.instBEqWorld.beq }

def Phenomena.Reference.Studies.Schlenker2003.instBEqWorld.beq : World → World → Bool

Equations

• Phenomena.Reference.Studies.Schlenker2003.instBEqWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Reference.Studies.Schlenker2003.instReprWorld : Repr World

Equations

• Phenomena.Reference.Studies.Schlenker2003.instReprWorld = { reprPrec := Phenomena.Reference.Studies.Schlenker2003.instReprWorld.repr }

def Phenomena.Reference.Studies.Schlenker2003.instReprWorld.repr : World → ℕ → Std.Format

Equations

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

@[reducible, inline]

abbrev Phenomena.Reference.Studies.Schlenker2003.Ctx : Type

Equations

• Phenomena.Reference.Studies.Schlenker2003.Ctx = Core.Context.KContext Phenomena.Reference.Studies.Schlenker2003.World Phenomena.Reference.Studies.Schlenker2003.Person Unit Unit

def Phenomena.Reference.Studies.Schlenker2003.speechCtx : Ctx

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

Equations

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

def Phenomena.Reference.Studies.Schlenker2003.rootT : Core.Context.ContextTower Ctx

Equations

• Phenomena.Reference.Studies.Schlenker2003.rootT = Core.Context.ContextTower.root Phenomena.Reference.Studies.Schlenker2003.speechCtx

def Phenomena.Reference.Studies.Schlenker2003.bobBel : Semantics.Attitudes.Doxastic.AccessRel World Person

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

Equations

• Phenomena.Reference.Studies.Schlenker2003.bobBel Phenomena.Reference.Studies.Schlenker2003.Person.bob x✝¹ x✝ = true
• Phenomena.Reference.Studies.Schlenker2003.bobBel Phenomena.Reference.Studies.Schlenker2003.Person.alice x✝¹ x✝ = (x✝ == Phenomena.Reference.Studies.Schlenker2003.World.w0)

def Phenomena.Reference.Studies.Schlenker2003.shiftedT : Core.Context.ContextTower Ctx

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

Equations

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

theorem Phenomena.Reference.Studies.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 Phenomena.Reference.Studies.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 Phenomena.Reference.Studies.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 Phenomena.Reference.Studies.Schlenker2003.isHappy : Person → World → Bool

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

Equations

• Phenomena.Reference.Studies.Schlenker2003.isHappy Phenomena.Reference.Studies.Schlenker2003.Person.alice Phenomena.Reference.Studies.Schlenker2003.World.w0 = true
• Phenomena.Reference.Studies.Schlenker2003.isHappy Phenomena.Reference.Studies.Schlenker2003.Person.alice Phenomena.Reference.Studies.Schlenker2003.World.w1 = false
• Phenomena.Reference.Studies.Schlenker2003.isHappy Phenomena.Reference.Studies.Schlenker2003.Person.bob x✝ = true

theorem Phenomena.Reference.Studies.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 Phenomena.Reference.Studies.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] = false

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

theorem Phenomena.Reference.Studies.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] = true

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 Phenomena.Reference.Studies.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 is false, Amharic is true. This is the formal content of @cite{schlenker-2003}'s argument that context quantification is strictly more expressive than world quantification.

theorem Phenomena.Reference.Studies.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 Phenomena.Reference.Studies.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 Phenomena.Reference.Studies.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 Phenomena.Reference.Studies.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 Phenomena.Reference.Studies.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.