KD45 Projection: The @cite{heim-1992} Know/Believe Asymmetry

@cite{heim-1992}

@cite{heim-1992} observed that presupposition projection differs under knowledge vs. belief predicates:

• "John knows Mary stopped smoking" → Mary actually smoked
• "John believes Mary stopped smoking" → Mary smoked in John's beliefs

The first projects the presupposition to the actual world; the second only attributes it to the attitude holder. This asymmetry follows from the modal frame conditions:

• Knowledge (S5): reflexive — the actual world is knowledge-accessible from itself, so presuppositions must hold there.
• Belief (KD45): serial but not reflexive — the actual world need not be belief-accessible, so presuppositions can hold only in the agent's belief worlds without being true.

This file constructs a concrete 2-world model demonstrating the asymmetry, connecting KnowledgeBeliefFrame (from EpistemicLogic.lean) through doxOfAccessRel (from BeliefEmbedding.lean) to presupFiltered (from LocalContext.lean).

World Model

inductive Phenomena.Presupposition.Studies.Heim1992.AttWorld : Type

Two-world model for the @cite{heim-1992} scenario.

• actual: Mary never smoked (presupposition false)
• believed: Mary used to smoke (presupposition true), accessible via John's beliefs

• actual : AttWorld
• believed : AttWorld

instance Phenomena.Presupposition.Studies.Heim1992.instDecidableEqAttWorld : DecidableEq AttWorld

Equations

• Phenomena.Presupposition.Studies.Heim1992.instDecidableEqAttWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Presupposition.Studies.Heim1992.instBEqAttWorld : BEq AttWorld

Equations

• Phenomena.Presupposition.Studies.Heim1992.instBEqAttWorld = { beq := Phenomena.Presupposition.Studies.Heim1992.instBEqAttWorld.beq }

def Phenomena.Presupposition.Studies.Heim1992.instBEqAttWorld.beq : AttWorld → AttWorld → Bool

Equations

• Phenomena.Presupposition.Studies.Heim1992.instBEqAttWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Presupposition.Studies.Heim1992.instReprAttWorld : Repr AttWorld

Equations

• Phenomena.Presupposition.Studies.Heim1992.instReprAttWorld = { reprPrec := Phenomena.Presupposition.Studies.Heim1992.instReprAttWorld.repr }

def Phenomena.Presupposition.Studies.Heim1992.instReprAttWorld.repr : AttWorld → ℕ → Std.Format

Equations

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

inductive Phenomena.Presupposition.Studies.Heim1992.Holder : Type

Single agent: John.

• john : Holder

instance Phenomena.Presupposition.Studies.Heim1992.instDecidableEqHolder : DecidableEq Holder

Equations

• Phenomena.Presupposition.Studies.Heim1992.instDecidableEqHolder x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Presupposition.Studies.Heim1992.instBEqHolder : BEq Holder

Equations

• Phenomena.Presupposition.Studies.Heim1992.instBEqHolder = { beq := Phenomena.Presupposition.Studies.Heim1992.instBEqHolder.beq }

def Phenomena.Presupposition.Studies.Heim1992.instBEqHolder.beq : Holder → Holder → Bool

Equations

• Phenomena.Presupposition.Studies.Heim1992.instBEqHolder.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Frame Construction

def Phenomena.Presupposition.Studies.Heim1992.knowsR : AttWorld → AttWorld → Bool

Knowledge accessibility (S5: reflexive). Both worlds access both worlds.

Equations

• Phenomena.Presupposition.Studies.Heim1992.knowsR x✝¹ x✝ = true

def Phenomena.Presupposition.Studies.Heim1992.believesR : AttWorld → AttWorld → Bool

Belief accessibility (KD45: serial, not reflexive). From actual, only believed is accessible. From believed, only believed is accessible.

Equations

• Phenomena.Presupposition.Studies.Heim1992.believesR x✝ Phenomena.Presupposition.Studies.Heim1992.AttWorld.believed = true
• Phenomena.Presupposition.Studies.Heim1992.believesR x✝ Phenomena.Presupposition.Studies.Heim1992.AttWorld.actual = false

theorem Phenomena.Presupposition.Studies.Heim1992.knowsR_refl : Core.ModalLogic.Refl knowsR

Knowledge relation is reflexive.

theorem Phenomena.Presupposition.Studies.Heim1992.believesR_serial : Core.ModalLogic.Serial believesR

Belief relation is serial (every world accesses some world).

theorem Phenomena.Presupposition.Studies.Heim1992.believesR_not_refl : ¬Core.ModalLogic.Refl believesR

Belief relation is NOT reflexive (actual does not access itself).

theorem Phenomena.Presupposition.Studies.Heim1992.believesR_trans : Core.ModalLogic.Trans believesR

Belief relation is transitive.

theorem Phenomena.Presupposition.Studies.Heim1992.believesR_eucl : Core.ModalLogic.Eucl believesR

Belief relation is Euclidean.

theorem Phenomena.Presupposition.Studies.Heim1992.believes_sub_knows (w v : AttWorld) : believesR w v = true → knowsR w v = true

R_B ⊆ R_K: belief-accessible worlds are knowledge-accessible.

def Phenomena.Presupposition.Studies.Heim1992.agentKnowsR : Holder → AttWorld → AttWorld → Bool

The agent-indexed knowledge relation.

Equations

• Phenomena.Presupposition.Studies.Heim1992.agentKnowsR Phenomena.Presupposition.Studies.Heim1992.Holder.john = Phenomena.Presupposition.Studies.Heim1992.knowsR

def Phenomena.Presupposition.Studies.Heim1992.agentBelievesR : Holder → AttWorld → AttWorld → Bool

The agent-indexed belief relation.

Equations

• Phenomena.Presupposition.Studies.Heim1992.agentBelievesR Phenomena.Presupposition.Studies.Heim1992.Holder.john = Phenomena.Presupposition.Studies.Heim1992.believesR

def Phenomena.Presupposition.Studies.Heim1992.frame : Semantics.Modality.EpistemicLogic.KnowledgeBeliefFrame AttWorld Holder

The knowledge-belief frame bundling S5 knowledge and KD45 belief.

Equations

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

Presupposition

def Phenomena.Presupposition.Studies.Heim1992.presup : Core.Presupposition.PrProp AttWorld

"Mary used to smoke" — the presupposition of "stop smoking". True at believed, false at actual.

Equations

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

def Phenomena.Presupposition.Studies.Heim1992.globalCtx : Core.CommonGround.ContextSet AttWorld

Global context: both worlds are in the context set.

Equations

• Phenomena.Presupposition.Studies.Heim1992.globalCtx x✝ = True

Local Contexts

def Phenomena.Presupposition.Studies.Heim1992.knowledgeLocal : Semantics.Presupposition.BeliefEmbedding.BeliefLocalCtx AttWorld Holder

Knowledge local context constructed via the bridge.

Equations

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

def Phenomena.Presupposition.Studies.Heim1992.beliefLocal : Semantics.Presupposition.BeliefEmbedding.BeliefLocalCtx AttWorld Holder

Belief local context constructed via the bridge.

Equations

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

@cite{heim-1992} Asymmetry Theorems

theorem Phenomena.Presupposition.Studies.Heim1992.reflexivity_forces_actual_truth (h : knowledgeLocal.atWorld AttWorld.actual ⊧ presup.presup) : presup.presup AttWorld.actual = true

S5 reflexivity forces presupposed content to be true at the actual world.

Under knowledge embedding, if the presupposition is filtered (entailed by the knowledge local context) at actual, then the presupposition must hold at actual — because S5 reflexivity makes actual one of the knowledge-accessible worlds from actual.

theorem Phenomena.Presupposition.Studies.Heim1992.non_reflexivity_permits_false_presup : (beliefLocal.atWorld AttWorld.actual ⊧ presup.presup) ∧ presup.presup AttWorld.actual = false

KD45 non-reflexivity permits false presuppositions under belief embedding.

The presupposition is filtered at actual (entailed by the belief local context) even though presup actual = false. This is because the only belief-accessible world from actual is believed, where the presupposition holds.

theorem Phenomena.Presupposition.Studies.Heim1992.heim_know_believe_asymmetry : (beliefLocal.atWorld AttWorld.actual ⊧ presup.presup) ∧ ¬knowledgeLocal.atWorld AttWorld.actual ⊧ presup.presup

The @cite{heim-1992} know/believe asymmetry.

Under our concrete model where the presupposition is false at the actual world:

1. The presupposition IS filtered under belief embedding (KD45) — John's belief worlds satisfy it.
2. The presupposition is NOT filtered under knowledge embedding (S5) — reflexivity forces it to hold at actual, where it is false.