Belief Embedding and Local Contexts

How presuppositions project under belief predicates, following [Sch09a] Section 3.1.2: for "agent believes φ" uttered in context C, the local context of φ at utterance world w* is C(w*) ∩ Dox_agent(w*), so a projecting presupposition must hold throughout the attitude holder's belief state. This derives Obligatory Local Effect ([TBRS13]: OLE=yes triggers are attributed to the attitude holder).

Main declarations

• BeliefLocalCtx, BeliefLocalCtx.atWorld — Schlenker's λw* λw(w* ∈ C ∧ w ∈ Dox(w*)) local context.
• presupAttributedToHolder — the OLE=yes condition.
• transparentProjection, opaque_implies_transparent_when_reflexive — the opaque/transparent projection modes of [DPBS24] §3.2.

structure Semantics.Presupposition.BeliefEmbedding.BeliefLocalCtx (W : Type u_3) (Agent : Type u_4) : Type (max u_3 u_4)

The local context of an embedded clause under a belief predicate.

For "agent believes φ" evaluated in context C at world w*: The local context at φ is the set of (w*, w) pairs where:

• w* is in the global context C
• w is compatible with what agent believes at w*

Following [Sch09a] Section 3.1.2, this is a function from "context of utterance" (w*) to context sets.

• globalCtx : CommonGround.ContextSet W

  The global context set

• dox : Agent → W → W → Prop

  The doxastic accessibility relation

• agent : Agent

  The attitude holder

def Semantics.Presupposition.BeliefEmbedding.BeliefLocalCtx.atWorld {W : Type u_1} {Agent : Type u_2} (blc : BeliefLocalCtx W Agent) (w_star : W) : CommonGround.ContextSet W

Get the local context at a specific world of utterance.

This is Schlenker's λw* λw(w* ∈ C and w ∈ DoxJ(w*))

Equations

• blc.atWorld w_star w = (blc.globalCtx w_star ∧ blc.dox blc.agent w_star w)

def Semantics.Presupposition.BeliefEmbedding.presupAttributedToHolder {W : Type u_1} {Agent : Type u_2} (blc : BeliefLocalCtx W Agent) (p : PartialProp W) : Prop

A presupposition is attributed to the attitude holder iff it's entailed by the local context at all global worlds.

This is the OLE=yes case: the presupposition becomes part of the attitude holder's beliefs.

Equations

• Semantics.Presupposition.BeliefEmbedding.presupAttributedToHolder blc p = ∀ (w_star : W), blc.globalCtx w_star → (blc.atWorld w_star).entails p.presup

Opaque vs Transparent Presupposition Projection

[DPBS24] §3.2 distinguish two projection modes for presuppositions under attitude predicates:

• Transparent: presupposition evaluated in the global context (speaker's knowledge state). Implemented by PartialProp.negFactive: the factive presupposes the complement holds in reality.

• Opaque: presupposition attributed to the attitude holder's belief state. This is presupAttributedToHolder: the presupposition holds at all doxastically accessible worlds.

Both modes yield free choice when applied to pex output, because both ensure homogeneity is satisfied (in different contexts) along with the prejacent.

def Semantics.Presupposition.BeliefEmbedding.transparentProjection {W : Type u_3} (globalCtx : CommonGround.ContextSet W) (p : PartialProp W) : Prop

Transparent projection: presupposition projects to the speaker's (global) context, evaluated independently of the attitude holder's beliefs. Captures negative factives ("is unaware that"): the factive presupposes the complement holds in the actual world.

[DPBS24] §3.2

Equations

• Semantics.Presupposition.BeliefEmbedding.transparentProjection globalCtx p = globalCtx.entails p.presup

theorem Semantics.Presupposition.BeliefEmbedding.negFactive_entails_transparent {W : Type u_3} (complement : PartialProp W) (believes : Set W → Set W) (globalCtx : CommonGround.ContextSet W) (h : globalCtx.entails (complement.negFactive believes).presup) : transparentProjection globalCtx complement

PartialProp.negFactive subsumes transparent projection: its presupposition (complement holds = presup ∧ assertion) entails transparent projection of the complement's presupposition.

This grounds the negFactive combinator in the projection theory. [Hei92], [DPBS24] §3.2

theorem Semantics.Presupposition.BeliefEmbedding.opaque_implies_transparent_when_reflexive {W : Type u_3} {Agent : Type u_4} (blc : BeliefLocalCtx W Agent) (p : PartialProp W) (hReflexive : ∀ (w : W), blc.globalCtx w → blc.dox blc.agent w w) (hOpaque : presupAttributedToHolder blc p) : transparentProjection blc.globalCtx p

Under S5 knowledge (reflexive accessibility), opaque projection implies transparent projection.

Reflexive dox means the evaluation world is among its own accessible worlds. What holds at all accessible worlds holds at the evaluation world. [Hin62]: S5 knowledge is reflexive.