def Semantics.Presupposition.BeliefEmbedding.DoxasticAccessibility (W : Type u_3) (Agent : Type u_4) : Type (max u_3 u_4)

Doxastic accessibility relation: the worlds compatible with what an agent believes at a given world.

Dox agent w = the set of worlds compatible with what agent believes at w

This is the standard modal semantics for belief.

Equations

• Semantics.Presupposition.BeliefEmbedding.DoxasticAccessibility W Agent = (Agent → W → Core.CommonGround.ContextSet W)

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

An agent's belief state at a world: the characteristic function of the doxastically accessible worlds.

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 : DoxasticAccessibility W Agent) (agent : Agent) (p : BProp W) (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' = true

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 @cite{schlenker-2009} Section 3.1.2, this is a function from "context of utterance" (w*) to context sets.

• globalCtx : Core.CommonGround.ContextSet W

  The global context set

• dox : DoxasticAccessibility 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) : Core.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 : Core.Presupposition.PrProp 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 ⊧ p.presup

def Semantics.Presupposition.BeliefEmbedding.presupAttributedToHolder {W : Type u_1} {Agent : Type u_2} (blc : BeliefLocalCtx W Agent) (p : Core.Presupposition.PrProp 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 ⊧ 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

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

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 : DoxasticAccessibility 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 : Core.Presupposition.PrProp 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 : Core.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, position := 0 }

def Semantics.Presupposition.BeliefEmbedding.expressiveProjectsToSpeaker {W : Type u_1} (globalCtx : Core.CommonGround.ContextSet W) (expressiverContent : BProp W) : 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 ⊧ 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, position := 1, depth := 1 }

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

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

Bridging Bool-valued and Prop-valued Accessibility

@cite{hintikka-1962}

EpistemicLogic uses Bool-valued AgentAccessRel W E = E → W → W → Bool. BeliefEmbedding uses Prop-valued DoxasticAccessibility W E = E → W → ContextSet W where ContextSet W = W → Prop.

Both represent the same concept (agent-indexed world accessibility). The bridge converts R i w v = true (Bool) to Dox i w v (Prop).

def Semantics.Presupposition.BeliefEmbedding.doxOfAccessRel {W : Type u_3} {E : Type u_4} (Rs : Core.ModalLogic.AgentAccessRel W E) : DoxasticAccessibility W E

Convert a Bool-valued AgentAccessRel to a Prop-valued DoxasticAccessibility. R i w v = true becomes the Prop Dox i w v.

Equations

• Semantics.Presupposition.BeliefEmbedding.doxOfAccessRel Rs i w v = (Rs i w v = true)

def Semantics.Presupposition.BeliefEmbedding.beliefLocalCtxOfFrame {W : Type u_3} {E : Type u_4} (frame : Modality.EpistemicLogic.KnowledgeBeliefFrame W E) (ctx : Core.CommonGround.ContextSet W) (i : E) : BeliefLocalCtx W E

Construct a BeliefLocalCtx from a KnowledgeBeliefFrame using the belief relation. This connects the KD45 belief operator from CommonGround.lean to the local context machinery in this file.

Equations

• Semantics.Presupposition.BeliefEmbedding.beliefLocalCtxOfFrame frame ctx i = { globalCtx := ctx, dox := Semantics.Presupposition.BeliefEmbedding.doxOfAccessRel frame.believesRel, agent := i }

def Semantics.Presupposition.BeliefEmbedding.knowledgeLocalCtxOfFrame {W : Type u_3} {E : Type u_4} (frame : Modality.EpistemicLogic.KnowledgeBeliefFrame W E) (ctx : Core.CommonGround.ContextSet W) (i : E) : BeliefLocalCtx W E

Construct a BeliefLocalCtx from a KnowledgeBeliefFrame using the knowledge relation. S5 knowledge is reflexive, so the local context includes the evaluation world itself.

Equations

• Semantics.Presupposition.BeliefEmbedding.knowledgeLocalCtxOfFrame frame ctx i = { globalCtx := ctx, dox := Semantics.Presupposition.BeliefEmbedding.doxOfAccessRel frame.knowsRel, agent := i }

theorem Semantics.Presupposition.BeliefEmbedding.beliefLocal_sub_knowledgeLocal {W : Type u_3} {E : Type u_4} (frame : Modality.EpistemicLogic.KnowledgeBeliefFrame W E) (ctx : Core.CommonGround.ContextSet W) (i : E) (w_star w : W) : (beliefLocalCtxOfFrame frame ctx i).atWorld w_star w → (knowledgeLocalCtxOfFrame frame ctx i).atWorld w_star w

Belief-accessible worlds are a subset of knowledge-accessible worlds.

Since R_B ⊆ R_K (from KnowledgeBeliefFrame.believes_sub_knows), the belief local context at any world is contained in the knowledge local context.

theorem Semantics.Presupposition.BeliefEmbedding.knowledge_filtered_implies_belief_filtered {W : Type u_3} {E : Type u_4} (frame : Modality.EpistemicLogic.KnowledgeBeliefFrame W E) (ctx : Core.CommonGround.ContextSet W) (i : E) (p : Core.Presupposition.PrProp W) (w_star : W) : ((knowledgeLocalCtxOfFrame frame ctx i).atWorld w_star ⊧ p.presup) → (beliefLocalCtxOfFrame frame ctx i).atWorld w_star ⊧ p.presup

If a presupposition is filtered under knowledge embedding (S5), it is also filtered under belief embedding (KD45).

The belief local context is a subset of the knowledge local context (since R_B ⊆ R_K). If p holds at all knowledge-accessible worlds, it holds at all belief-accessible worlds a fortiori.