def Semantics.Presupposition.BeliefEmbedding.beliefState {W : Type u_1} {Agent : Type u_2} (Dox : Core.Logic.Modal.AgentAccessRel W Agent) (agent : Agent) (w : W) : CommonGround.ContextSet W

An agent's belief state at a world: the doxastically accessible worlds, viewed as a context set. Doxastic accessibility is the agent-indexed accessibility relation Core.Logic.Modal.AgentAccessRel ([Hin62]): Dox agent w w' means w' is compatible with what agent believes at w.

Equations

• Semantics.Presupposition.BeliefEmbedding.beliefState Dox agent w = Dox agent w

def Semantics.Presupposition.BeliefEmbedding.believes {W : Type u_1} {Agent : Type u_2} (Dox : Core.Logic.Modal.AgentAccessRel W Agent) (agent : Agent) (p : W → Prop) (w : W) : Prop

An agent believes a proposition at a world iff the proposition holds at all doxastically accessible worlds.

Equations

• Semantics.Presupposition.BeliefEmbedding.believes Dox agent p w = ∀ (w' : W), Dox agent w w' → p w'

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 : Core.Logic.Modal.AgentAccessRel W Agent

  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.presupProjectsFromBelief {W : Type u_1} {Agent : Type u_2} (blc : BeliefLocalCtx W Agent) (p : PartialProp W) : Prop

A presupposition projects globally (to speaker) from under belief iff it's not entailed by the belief local context at any global world.

Equations

• Semantics.Presupposition.BeliefEmbedding.presupProjectsFromBelief blc p = ∃ (w_star : W), blc.globalCtx w_star ∧ ¬(blc.atWorld w_star).entails p.presup

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

inductive Semantics.Presupposition.BeliefEmbedding.SmokingWorld : Type

World type for the smoking example:

• Whether Mary used to smoke (in reality)
• Whether John believes Mary used to smoke
• Whether Mary currently smokes (in reality)

• maryUsedToSmoke_johnBelieves_maryQuit : SmokingWorld
• maryUsedToSmoke_johnBelieves_marySmokes : SmokingWorld
• maryNeverSmoked_johnBelieves_usedTo : SmokingWorld
• maryNeverSmoked_johnDoesntBelieve : SmokingWorld

@[implicit_reducible]

instance Semantics.Presupposition.BeliefEmbedding.instDecidableEqSmokingWorld : DecidableEq SmokingWorld

Equations

• Semantics.Presupposition.BeliefEmbedding.instDecidableEqSmokingWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Semantics.Presupposition.BeliefEmbedding.SmokingAgent : Type

Agent type for the example.

• john : SmokingAgent

@[implicit_reducible]

instance Semantics.Presupposition.BeliefEmbedding.instDecidableEqSmokingAgent : DecidableEq SmokingAgent

Equations

• Semantics.Presupposition.BeliefEmbedding.instDecidableEqSmokingAgent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Presupposition.BeliefEmbedding.smokingDox : Core.Logic.Modal.AgentAccessRel SmokingWorld SmokingAgent

John's belief state at each world.

Equations

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

def Semantics.Presupposition.BeliefEmbedding.maryStoppedSmoking : PartialProp SmokingWorld

"Mary stopped smoking" — presupposes Mary used to smoke.

Equations

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

theorem Semantics.Presupposition.BeliefEmbedding.stop_ole_attribution : have blc := { globalCtx := fun (w : SmokingWorld) => w = SmokingWorld.maryNeverSmoked_johnBelieves_usedTo, dox := smokingDox, agent := SmokingAgent.john }; presupAttributedToHolder blc maryStoppedSmoking

Under belief embedding, the presupposition "Mary used to smoke" is attributed to John (the attitude holder), not required of the global context.

At world maryNeverSmoked_johnBelieves_usedTo:

• Reality: Mary never smoked
• John's beliefs: Mary used to smoke
• Sentence "John believes Mary stopped smoking" is TRUE
• The presupposition holds in John's belief worlds, not in reality

This demonstrates OLE = yes for "stop" (Class C trigger).

def Semantics.Presupposition.BeliefEmbedding.speakerLocalCtx {W : Type u_1} (c : CommonGround.ContextSet W) : LocalContext.LocalCtx W

For OLE=no triggers (Class B and D), the projective content is not computed from the attitude holder's beliefs. Instead, it projects directly to the speaker's context.

This is modeled by having the local context be the global context, not the belief-restricted context.

Equations

• Semantics.Presupposition.BeliefEmbedding.speakerLocalCtx c = { worlds := c }

def Semantics.Presupposition.BeliefEmbedding.expressiveProjectsToSpeaker {W : Type u_1} (globalCtx : CommonGround.ContextSet W) (expressiverContent : W → Prop) : Prop

For Class B triggers (expressives, appositives), content projects to speaker.

"John believes that damn cat is outside" → SPEAKER is annoyed at the cat (not John)

The expressive content is evaluated in the speaker's context, ignoring the belief embedding.

Equations

• Semantics.Presupposition.BeliefEmbedding.expressiveProjectsToSpeaker globalCtx expressiverContent = globalCtx.entails expressiverContent

def Semantics.Presupposition.BeliefEmbedding.beliefToLocalCtx {W : Type u_1} {Agent : Type u_2} (blc : BeliefLocalCtx W Agent) (w_star : W) (_h : blc.globalCtx w_star) : LocalContext.LocalCtx W

Convert a belief local context to a standard local context.

This shows how the belief embedding fits into the general local context framework from LocalContext.lean.

Equations

• Semantics.Presupposition.BeliefEmbedding.beliefToLocalCtx blc w_star _h = { worlds := blc.atWorld w_star, depth := 1 }

theorem Semantics.Presupposition.BeliefEmbedding.belief_filtering_condition {W : Type u_1} {Agent : Type u_2} (blc : BeliefLocalCtx W Agent) (p : PartialProp W) (w_star : W) (_h : blc.globalCtx w_star) : LocalContext.presupFiltered (beliefToLocalCtx blc w_star _h) p ↔ (blc.atWorld w_star).entails p.presup

The presupposition filtering condition is the same: a presupposition is filtered iff it's entailed by the local context.

Refinement Between Knowledge and Belief Embeddings

[Hin62]

Doxastic accessibility is Core.Logic.Modal.AgentAccessRel directly, so belief local contexts compose with the epistemic-logic frame conditions: when belief pointwise refines knowledge (IsBeliefRefinementOf), filtering under knowledge embedding implies filtering under belief embedding.

def Semantics.Presupposition.BeliefEmbedding.localCtxOf {W : Type u_3} {E : Type u_4} (Rs : Core.Logic.Modal.AgentAccessRel W E) (ctx : CommonGround.ContextSet W) (i : E) : BeliefLocalCtx W E

Build a BeliefLocalCtx from an agent-indexed accessibility relation.

Equations

• Semantics.Presupposition.BeliefEmbedding.localCtxOf Rs ctx i = { globalCtx := ctx, dox := Rs, agent := i }

theorem Semantics.Presupposition.BeliefEmbedding.localCtx_sub_of_refinement {W : Type u_3} {E : Type u_4} (Rk Rb : Core.Logic.Modal.AgentAccessRel W E) (ctx : CommonGround.ContextSet W) (i : E) [hRef : Core.Logic.Modal.IsBeliefRefinementOf (Rk i) (Rb i)] (w_star w : W) : (localCtxOf Rb ctx i).atWorld w_star w → (localCtxOf Rk ctx i).atWorld w_star w

Belief-accessible worlds are a subset of knowledge-accessible worlds when belief refines knowledge pointwise.

theorem Semantics.Presupposition.BeliefEmbedding.knowledge_filtered_implies_belief_filtered {W : Type u_3} {E : Type u_4} (Rk Rb : Core.Logic.Modal.AgentAccessRel W E) (ctx : CommonGround.ContextSet W) (i : E) [Core.Logic.Modal.IsBeliefRefinementOf (Rk i) (Rb i)] (p : PartialProp W) (w_star : W) : ((localCtxOf Rk ctx i).atWorld w_star).entails p.presup → ((localCtxOf Rb ctx i).atWorld w_star).entails p.presup

If a presupposition is filtered under knowledge embedding, it is also filtered under any belief embedding that refines knowledge.

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.