Documentation

Linglib.Semantics.Reference.Monsters

Kaplan's Anti-Monster Thesis (Tower Formulation) #

[AN04b] [Kap89] [Sch03]

[Kap89]'s anti-monster thesis: the claim that natural language operators are content operators (shifting circumstances of evaluation) rather than context operators (shifting contexts of utterance).

Under the tower analysis, a monster is a shift that destabilizes some expression — it changes what an access pattern resolves to (IsTowerMonster, the ∃-projection of AccessPattern.Stable; equivalently a non-identity shift). Kaplan's thesis for English says attitude verbs push identity shifts — they embed without changing the context of utterance — so English indexicals, which read from the origin, are stable under embedding (IsKaplanCompliant, the dual ∀-projection of Stable in Reference/Kaplan.lean).

Cross-linguistic counterexamples are languages where attitude verbs push non-identity shifts (e.g., attitudeShift changes the agent to the attitude holder).

Key Definitions #

Schlenker's monstrous Say_m operator lives in Attitudes/ContextQuantification.lean as sayM (with ctxBox its context-meaning specialization); this file is about the monster predicate and Kaplan's thesis, not the operator.

source
def Semantics.Reference.Monsters.IsTowerMonster {C : Type u_1} (σ : Context.ContextShift C) :
Prop

A context shift is a tower monster when it destabilizes the innermost reader: pushing it changes what the canonical local access pattern (AccessPattern.innermostReader) resolves to. This is the ∃-over-expressions projection of AccessPattern.Stable — the innermost reader is its universal witness, since a push only ever changes the innermost context — dual to Kaplan-compliance's ∀-over-operators projection (IsKaplanCompliant). Equivalently (isTowerMonster_iff_exists) the shift moves some context: ∃ c, σ.apply c ≠ c.

Under the tower analysis, monsters are exactly the non-identity shifts. English attitude verbs push identity shifts (not monsters); Amharic attitude verbs push attitude shifts (monsters).

Equations
Instances For
    source
    theorem Semantics.Reference.Monsters.isTowerMonster_iff_exists {C : Type u_1} (σ : Context.ContextShift C) :
    IsTowerMonster σ ↔ ∃ (c : C), σ.apply c ≠ c

    A shift is a monster iff it moves some context: the pointwise characterization recovering the direct form ∃ c, σ.apply c ≠ c.

    source
    theorem Semantics.Reference.Monsters.isTowerMonster_congr {C : Type u_1} {σ τ : Context.ContextShift C} (h : σ.apply = τ.apply) :
    IsTowerMonster σ ↔ IsTowerMonster τ

    Monsterhood depends only on the shift's action apply, not its label: shifts with equal apply are monsters together.

    source
    theorem Semantics.Reference.Monsters.identityShift_not_monster {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} :
    ¬IsTowerMonster Context.identityShift

    The identity shift is not a monster.

    source
    theorem Semantics.Reference.Monsters.attitudeShift_is_monster {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (holder : E) (attWorld : W) (c : Context.KContext W E P T) (hAgent : c.agent ≠ holder) :
    IsTowerMonster (Context.attitudeShift holder attWorld)

    An attitude shift is a monster when the holder differs from some context's agent.

    source
    def Semantics.Reference.Monsters.KaplansThesisHolds {C : Type u_1} (embeddingShifts : List (Context.ContextShift C)) :
    Prop

    Kaplan's thesis as a tower property: embedding verbs in a language push shifts that are not monsters (i.e., identity shifts).

    For English, this means all attitude verbs push identityShift: "John said that I am happy" evaluates "I" at the original context, because the embedding verb didn't shift anything.

    The embeddingShifts parameter lists the shifts that the language's embedding verbs produce. The thesis holds iff none of them is a monster.

    Equations
    Instances For
      source
      theorem Semantics.Reference.Monsters.kaplansThesisAsTower {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} :
      KaplansThesisHolds [Context.identityShift]

      English embedding verbs push identity shifts. Kaplan's thesis holds.