Context Quantification

@cite{schlenker-2003} @cite{hintikka-1962}

Bridges world quantification (Doxastic.lean) and context shifting (Shifts.lean).

@cite{schlenker-2003}'s key insight: attitude verbs quantify over contexts, not just worlds. Standard Hintikka semantics (∀w'. R(x,w,w') → p(w')) is a special case where only the world coordinate of the accessible context matters. In languages with shifted indexicals (Amharic, Zazaki), the agent coordinate of the accessible context carries semantic content that pure world quantification cannot capture.

Key Definitions

• sayMBool: monstrous say operator (Bool version of sayMTower in Monsters.lean)
• ctxFromShift: the accessible context generated by an attitude shift
• ctxBox: direct context quantification — Schlenker's primitive

Key Results

• sayM_reduces_to_box: tower quantification with world-only meaning = boxAt
• ctxBox_world_only: context quantification with world-only meaning = boxAt
• ctxBox_agent_sensitive: context quantification provides agent information that world quantification cannot capture
• doxastic_is_ctxBox_world_only: DoxasticPredicate.holdsAt is veridicality + ctxBox

def Semantics.Attitudes.ContextQuantification.sayMBool {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (R : Doxastic.AccessRel W E) (holder : E) (φ : Core.Context.ContextTower (Core.Context.KContext W E P T) → W → Bool) (t : Core.Context.ContextTower (Core.Context.KContext W E P T)) (w : W) (worlds : List W) : Bool

Monstrous attitude verb semantics via tower push (Bool version).

For each world w' accessible via R, push an attitude shift onto the tower (making the holder the agent, w' the world) and evaluate φ.

This is the computable counterpart of sayMTower in Monsters.lean: same quantificational structure, but Bool-valued and over a finite world list, making it compatible with boxAt.

Equations

• Semantics.Attitudes.ContextQuantification.sayMBool R holder φ t w worlds = worlds.all fun (w' : W) => !R holder w w' || φ (t.push (Core.Context.attitudeShift holder w')) w'

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

The context produced by an attitude shift: push the shift onto the tower and read the innermost context. This is the "accessible context" that the embedded clause evaluates against.

By push_innermost, this equals (attitudeShift holder w').apply t.innermost, i.e., { t.innermost with agent := holder, world := w' }.

Equations

• Semantics.Attitudes.ContextQuantification.ctxFromShift t holder w' = (t.push (Core.Context.attitudeShift holder w')).innermost

@[simp]

theorem Semantics.Attitudes.ContextQuantification.shift_world {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (t : Core.Context.ContextTower (Core.Context.KContext W E P T)) (holder : E) (w' : W) : (ctxFromShift t holder w').world = w'

@[simp]

theorem Semantics.Attitudes.ContextQuantification.shift_agent {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (t : Core.Context.ContextTower (Core.Context.KContext W E P T)) (holder : E) (w' : W) : (ctxFromShift t holder w').agent = holder

@[simp]

theorem Semantics.Attitudes.ContextQuantification.shift_time {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (t : Core.Context.ContextTower (Core.Context.KContext W E P T)) (holder : E) (w' : W) : (ctxFromShift t holder w').time = t.innermost.time

@[simp]

theorem Semantics.Attitudes.ContextQuantification.shift_position {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (t : Core.Context.ContextTower (Core.Context.KContext W E P T)) (holder : E) (w' : W) : (ctxFromShift t holder w').position = t.innermost.position

@[simp]

theorem Semantics.Attitudes.ContextQuantification.shift_addressee {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (t : Core.Context.ContextTower (Core.Context.KContext W E P T)) (holder : E) (w' : W) : (ctxFromShift t holder w').addressee = t.innermost.addressee

theorem Semantics.Attitudes.ContextQuantification.sayM_reduces_to_box {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (R : Doxastic.AccessRel W E) (holder : E) (p : W → Bool) (t : Core.Context.ContextTower (Core.Context.KContext W E P T)) (w : W) (worlds : List W) : sayMBool R holder (fun (x : Core.Context.ContextTower (Core.Context.KContext W E P T)) (w' : W) => p w') t w worlds = Doxastic.boxAt R holder w worlds p

When the embedded meaning ignores the context tower and depends only on the world, monstrous tower quantification reduces to standard Hintikka world quantification.

The proof is rfl: with φ = fun _ w' => p w', sayMBool and boxAt unfold to the same term. The ONLY difference between them is whether the meaning function can see the tower.

def Semantics.Attitudes.ContextQuantification.ctxBox {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (R : Doxastic.AccessRel W E) (holder : E) (φ : Core.Context.KContext W E P T → Bool) (t : Core.Context.ContextTower (Core.Context.KContext W E P T)) (w : W) (worlds : List W) : Bool

Direct context quantification: quantify over accessible worlds and evaluate φ on the shift-generated context at each world.

⟦x V φ⟧(t, w) = ∀w' ∈ worlds. R(x,w,w') → φ(ctxFromShift t x w')

This is @cite{schlenker-2003}'s primitive: attitude verbs quantify over contexts ⟨holder, w', t, p⟩, not just worlds w'.

Equations

• Semantics.Attitudes.ContextQuantification.ctxBox R holder φ t w worlds = worlds.all fun (w' : W) => !R holder w w' || φ (Semantics.Attitudes.ContextQuantification.ctxFromShift t holder w')

theorem Semantics.Attitudes.ContextQuantification.ctxBox_world_only {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (R : Doxastic.AccessRel W E) (holder : E) (p : W → Bool) (t : Core.Context.ContextTower (Core.Context.KContext W E P T)) (w : W) (worlds : List W) : ctxBox R holder (fun (c : Core.Context.KContext W E P T) => p c.world) t w worlds = Doxastic.boxAt R holder w worlds p

When φ depends only on the world coordinate, context quantification reduces to standard Hintikka world quantification (boxAt).

This is the formal content of @cite{schlenker-2003}'s observation: Hintikka semantics is a SPECIAL CASE of context quantification — the case where the embedded clause has no shifted indexicals, no perspective-dependent expressions, nothing that reads from the context beyond the world.

theorem Semantics.Attitudes.ContextQuantification.ctxBox_agent_sensitive {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (t : Core.Context.ContextTower (Core.Context.KContext W E P T)) (holder : E) (w' : W) (hDiff : t.innermost.agent ≠ holder) : (ctxFromShift t holder w').agent = holder ∧ (ctxFromShift t holder w').agent ≠ t.innermost.agent

Context quantification provides information that world quantification cannot capture: the identity of the attitude holder as agent.

In shift languages (Amharic, Zazaki), the embedded first person pronoun reads .agent from the accessible context. Under ctxBox, this yields the attitude holder. Under boxAt, there is no agent to read — the meaning is W → Bool, not KContext → Bool.

This is why monsters matter: ctxBox with agent-sensitive φ is strictly more expressive than boxAt.

theorem Semantics.Attitudes.ContextQuantification.doxastic_is_ctxBox_world_only {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 → Bool) (w : W) (worlds : List W) (t : Core.Context.ContextTower (Core.Context.KContext W E P T)) : V.holdsAt agent p w worlds = (Doxastic.veridicalityHolds V.veridicality p w && ctxBox V.access agent (fun (c : Core.Context.KContext W E P T) => p c.world) t w worlds)

DoxasticPredicate.holdsAt is a veridicality check plus ctxBox with world-projected meaning.

This connects the modular DoxasticPredicate API (Doxastic.lean) to context quantification: every doxastic predicate IS context quantification over world-only propositions, with an additional veridicality constraint at the evaluation world.

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

The Fixity Thesis (@cite{schlenker-2003}, Appendix): a tower-parameterized meaning satisfies Fixity iff its truth value is the same regardless of the tower configuration.

In @cite{schlenker-2003}'s formulation: ⟦φ⟧^{c,i} is independent of c. In the tower analysis: the meaning function ignores the tower parameter entirely.

The thesis holds in standard (non-monstrous) formal semantics where sentences have world-dependent but context-independent denotations. It fails in @cite{schlenker-2003}'s MEL (Monstrous Egli Language), where attitude operators bind context variables that shift indexical reference.

Equations

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

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

World-only meanings satisfy the Fixity Thesis. These are the non-monstrous meanings: their truth value depends only on the evaluation world, not on who uttered the sentence or how deeply embedded it is.

This captures the "easy direction" of Claim 2: in a language without monsters, every meaning is world-only, so Fixity holds.

theorem Semantics.Attitudes.ContextQuantification.ctxBox_fixity {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (R : Doxastic.AccessRel W E) (holder : E) (p : W → Bool) (t₁ t₂ : Core.Context.ContextTower (Core.Context.KContext W E P T)) (w : W) (worlds : List W) : ctxBox R holder (fun (c : Core.Context.KContext W E P T) => p c.world) t₁ w worlds = ctxBox R holder (fun (c : Core.Context.KContext W E P T) => p c.world) t₂ w worlds

Context quantification preserves Fixity: if the embedded meaning depends only on the world coordinate, ctxBox produces the same result regardless of which tower it is evaluated against.

This is because ctxBox with world-only meaning reduces to boxAt (by ctxBox_world_only), which is tower-independent.

theorem Semantics.Attitudes.ContextQuantification.ctxFromShift_agent_eq_amharic_I {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (t : Core.Context.ContextTower (Core.Context.KContext W E P T)) (holder : E) (w' : W) : (ctxFromShift t holder w').agent = Reference.ShiftedIndexicals.amharic_pronI.resolve (t.push (Core.Context.attitudeShift holder w'))

The agent of the accessible context equals what Amharic "I" (amharic_pronI) reads from the shifted tower.

This connects context quantification (ctxFromShift) to the shifted indexical framework: both pick out the attitude holder as the referent of the embedded first person.

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

English "I" (pronI_access) is invariant under the attitude shift used by ctxBox — it always returns the origin agent (actual speaker), not the attitude holder.