Schlenker (2003): A Plea for Monsters

Schlenker treats attitude verbs as quantifiers over contexts. Kaplan's Fixity Thesis holds that an indexical's value is fixed by the context of the actual speech act, so that no operator shifts contexts (SatisfiesFixity); Amharic, where the first person under say denotes the reported speaker, is the counterexample. An attitude verb therefore quantifies over contexts of the reported speech act or thought (ContextBox), with the holder as agent and the accessible world as world (reportedContext), and Hintikka's quantification over worlds is the case where the embedded meaning reads only the world (contextBox_world_only, doxastic_holdsAt_iff_contextBox). English I resolves to the origin agent under any shift and Amharic I to the innermost agent (english_I_invariant, amharicI_ne_I), so Bob said that I am happy is false read as English and true read as Amharic in a two-person model (english_amharic_differ). A logophoric pronoun is the author of an embedded context who is not the actual speaker (Logophoric).

Implementation notes

The paper's context variables and its syntactic filtering of shiftable from non-shiftable indexicals are not modelled; shiftability is the choice between the origin and the innermost access pattern of Semantics/Reference/Context/Tower. Quantification over the accessible worlds is the relational box of Logic/Modal/Defs, decidable over finitely many worlds. A monstrous operator whose embedded meaning consumes the whole shifted tower, needed for mixed origin and local readings, is not defined.

References

• [Sch03a]
• [Kap89]
• [Hin62]

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 : Reference.ContextTower (Reference.Context W E P T)) (holder : E) (w' : W) : Reference.Context W E P T

The context of the reported speech act ([Sch03a] (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 (Reference.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 : Reference.ContextTower (Reference.Context 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 : Reference.ContextTower (Reference.Context 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 : Reference.ContextTower (Reference.Context 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 : Reference.ContextTower (Reference.Context 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 : Reference.ContextTower (Reference.Context 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 → SetRel W W) (holder : E) (φ : Reference.Context W E P T → Prop) (t : Reference.ContextTower (Reference.Context W E P T)) : W → Prop

ContextBox R holder φ t w iff at every world R holder-accessible from w the embedded meaning φ holds of the context of the reported speech act: [Sch03a]'s attitude verb quantifying over contexts, the box over the reported contexts.

Equations

• Schlenker2003.ContextBox R holder φ t = ModalLogic.Box (R holder) fun (w' : W) => φ (Schlenker2003.reportedContext t holder w')

@[instance_reducible]

instance Schlenker2003.instDecidableContextBoxOfFintypeOfDecidablePredContextOfMemProdSetRelMk {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [Fintype W] (R : E → SetRel W W) (holder : E) (φ : Reference.Context W E P T → Prop) [DecidablePred φ] (t : Reference.ContextTower (Reference.Context W E P T)) (w : W) [(v : W) → Decidable ((w, v) ∈ R holder)] : Decidable (ContextBox R holder φ t w)

Equations

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

theorem Schlenker2003.contextBox_world_only {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (R : E → SetRel W W) (holder : E) (p : W → Prop) (t : Reference.ContextTower (Reference.Context W E P T)) : ContextBox R holder (fun (c : Reference.Context W E P T) => p c.world) t = ModalLogic.Box (R holder) p

With a world-only meaning, context quantification is Hintikka world quantification, the sense in which [Hin62]'s semantics is a special case of [Sch03a]'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) (t : Reference.ContextTower (Reference.Context W E P T)) : V.HoldsAt agent p w ↔ (∀ x ∈ V.factivity, p w) ∧ Doxastic.VeridicalityHolds V.veridicality p w ∧ ContextBox V.access agent (fun (c : Reference.Context W E P T) => p c.world) t w

DoxasticPredicate.HoldsAt is a factivity and a veridicality requirement plus context quantification over a world-only meaning, so every doxastic predicate of Doxastic.lean is a special case of [Sch03a]'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} (φ : Reference.ContextTower (Reference.Context W E P T) → W → Prop) : Prop

The Fixity Thesis, [Sch03a] (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₂ : Reference.ContextTower (Reference.Context 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 : Reference.ContextTower (Reference.Context 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 : Reference.ContextTower (Reference.Context W E P T)) (holder : E) (w' : W) : Reference.Kaplan.I.resolve (t.push (Reference.attitudeShift holder w')) = Reference.Kaplan.I.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.

def Schlenker2003.amharicI {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} : Reference.AccessPattern (Reference.Context W E P T) E

Amharic I ([Sch03a] §3): the agent of the innermost context, so under an attitude shift the attitude holder.

Equations

• Schlenker2003.amharicI = Reference.AccessPattern.innermost Reference.Context.agent

theorem Schlenker2003.amharicI_ne_I {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : Reference.Context W E P T) (holder : E) (w' : W) (h : c.agent ≠ holder) : amharicI.resolve ((Reference.ContextTower.root c).push (Reference.attitudeShift holder w')) ≠ Reference.Kaplan.I.resolve ((Reference.ContextTower.root c).push (Reference.attitudeShift holder w'))

The paper's counterexample to Kaplan's thesis is that under an attitude shift to a holder other than the speaker, Amharic I and English I resolve differently.

Person features as presuppositions

def Schlenker2003.AuthorAt {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (d : Reference.DepthSpec) (x : E) (t : Reference.ContextTower (Reference.Context W E P T)) : Prop

The paper's +author(x, cᵢ) says that x is the agent of the context at depth d, and +author*(x) is the case d = .origin.

Equations

• Schlenker2003.AuthorAt d x t = (x = { depth := d, project := Reference.Context.agent }.resolve t)

def Schlenker2003.Logophoric {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (d : Reference.DepthSpec) (x : E) (t : Reference.ContextTower (Reference.Context W E P T)) : Prop

A logophoric pronoun (§6) is +author(x, cᵢ) ∧ −author*(x), the agent of the embedded context who is not the actual speaker.

Equations

• Schlenker2003.Logophoric d x t = (Schlenker2003.AuthorAt d x t ∧ ¬Schlenker2003.AuthorAt Reference.DepthSpec.origin x t)

@[instance_reducible]

instance Schlenker2003.instDecidableAuthorAtOfDecidableEq {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [DecidableEq E] (d : Reference.DepthSpec) (x : E) (t : Reference.ContextTower (Reference.Context W E P T)) : Decidable (AuthorAt d x t)

Equations

• Schlenker2003.instDecidableAuthorAtOfDecidableEq d x t = id inferInstance

@[instance_reducible]

instance Schlenker2003.instDecidableLogophoricOfDecidableEq {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [DecidableEq E] (d : Reference.DepthSpec) (x : E) (t : Reference.ContextTower (Reference.Context W E P T)) : Decidable (Logophoric d x t)

Equations

• Schlenker2003.instDecidableLogophoricOfDecidableEq d x t = id inferInstance

theorem Schlenker2003.logophoric_local_of_ne {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (t : Reference.ContextTower (Reference.Context W E P T)) (holder : E) (w' : W) (h : holder ≠ t.origin.agent) : Logophoric Reference.DepthSpec.local holder (t.push (Reference.attitudeShift holder w'))

Under an attitude shift, a holder other than the speaker is logophoric at the local depth.

theorem Schlenker2003.not_logophoric_origin_agent {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (t : Reference.ContextTower (Reference.Context W E P T)) (d : Reference.DepthSpec) : ¬Logophoric d t.origin.agent t

The actual speaker is never logophoric.

A two-person, two-world model

inductive Schlenker2003.Person : Type

The speaker Alice and the attitude holder Bob.

• 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 ⋯

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✝

@[instance_reducible]

instance Schlenker2003.instReprPerson : Repr Person

Equations

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

inductive Schlenker2003.World : Type

The actual world and one alternative.

• 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.instFintypeWorld : Fintype World

Equations

• Schlenker2003.instFintypeWorld = { elems := { val := ↑Schlenker2003.World.enumList, nodup := Schlenker2003.World.enumList_nodup }, complete := Schlenker2003.instFintypeWorld._proof_1 }

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✝

@[instance_reducible]

instance Schlenker2003.instReprWorld : Repr World

Equations

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

@[reducible, inline]

abbrev Schlenker2003.Ctx : Type

Equations

• Schlenker2003.Ctx = Reference.Context Schlenker2003.World Schlenker2003.Person Unit Unit

def Schlenker2003.speechCtx : Ctx

The context of the actual speech act: Alice speaking to Bob at the actual world.

Equations

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

def Schlenker2003.bobBel : Person → SetRel World World

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

Equations

• Schlenker2003.bobBel Schlenker2003.Person.bob = Set.univ
• Schlenker2003.bobBel Schlenker2003.Person.alice = {p : Schlenker2003.World × Schlenker2003.World | p.2 = Schlenker2003.World.w0}

@[instance_reducible]

instance Schlenker2003.instDecidableMemProdWorldSetRelBobBelMk (a : Person) (w w' : World) : Decidable ((w, w') ∈ bobBel a)

Equations

• Schlenker2003.instDecidableMemProdWorldSetRelBobBelMk Schlenker2003.Person.bob x✝¹ x✝ = { decide := true, reflects_decide := ⋯ }
• Schlenker2003.instDecidableMemProdWorldSetRelBobBelMk Schlenker2003.Person.alice x✝¹ x✝ = Schlenker2003.instDecidableMemProdWorldSetRelBobBelMk._aux_2 x✝¹ x✝

def Schlenker2003.isHappy : Person → World → Prop

Alice is happy only in the actual world; 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_amharic_differ : ¬ContextBox bobBel Person.bob (fun (c : Reference.Context World Person Unit Unit) => isHappy Person.alice c.world) (Reference.ContextTower.root speechCtx) World.w0 ∧ ContextBox bobBel Person.bob (fun (c : Reference.Context World Person Unit Unit) => isHappy c.agent c.world) (Reference.ContextTower.root speechCtx) World.w0

Bob said that I am happy is false read as English, where I is Alice and the meaning is world-only, and true read as Amharic, where I is the agent of the reported context: context quantification is strictly more expressive than world quantification.