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).

The other half of @cite{heim-1992} — comparative-belief desire semantics for want/wish/hope — is at Phenomena/Modality/Studies/Heim1992.lean. Both halves of the paper are formalized; the substrate splits along the natural Phenomena boundary (presupposition vs modality).

World Model

inductive 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

@[implicit_reducible]

instance Heim1992.instDecidableEqAttWorld : DecidableEq AttWorld

Equations

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

def Heim1992.instReprAttWorld.repr : AttWorld → ℕ → Std.Format

Equations

• Heim1992.instReprAttWorld.repr Heim1992.AttWorld.actual prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Heim1992.AttWorld.actual")).group prec✝
• Heim1992.instReprAttWorld.repr Heim1992.AttWorld.believed prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Heim1992.AttWorld.believed")).group prec✝

@[implicit_reducible]

instance Heim1992.instReprAttWorld : Repr AttWorld

Equations

• Heim1992.instReprAttWorld = { reprPrec := Heim1992.instReprAttWorld.repr }

inductive Heim1992.Holder : Type

Single agent: John.

• john : Holder

@[implicit_reducible]

instance Heim1992.instDecidableEqHolder : DecidableEq Holder

Equations

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

Frame Construction

def Heim1992.knowsR : AttWorld → AttWorld → Prop

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

Equations

• Heim1992.knowsR x✝¹ x✝ = True

def Heim1992.believesR : AttWorld → AttWorld → Prop

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

Equations

• Heim1992.believesR x✝ Heim1992.AttWorld.believed = True
• Heim1992.believesR x✝ Heim1992.AttWorld.actual = False

def Heim1992.believesRBool : AttWorld → AttWorld → Bool

Bool-valued mirror of believesR for downstream code that needs decidable accessibility (e.g., MaybeMonad.believe).

Equations

• Heim1992.believesRBool x✝ Heim1992.AttWorld.believed = true
• Heim1992.believesRBool x✝ Heim1992.AttWorld.actual = false

theorem Heim1992.knowsR_refl : Core.Logic.Intensional.IsReflexive knowsR

Knowledge relation is reflexive.

theorem Heim1992.believesR_serial : Core.Logic.Intensional.IsSerial believesR

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

theorem Heim1992.believesR_not_refl : ¬Core.Logic.Intensional.IsReflexive believesR

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

theorem Heim1992.believesR_trans : Core.Logic.Intensional.IsTransitive believesR

Belief relation is transitive.

theorem Heim1992.believesR_eucl : Core.Logic.Intensional.IsEuclidean believesR

Belief relation is Euclidean.

theorem Heim1992.believes_sub_knows (w v : AttWorld) : believesR w v → knowsR w v

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

def Heim1992.agentKnowsR : Holder → AttWorld → AttWorld → Prop

The agent-indexed knowledge relation.

Equations

• Heim1992.agentKnowsR Heim1992.Holder.john = Heim1992.knowsR

def Heim1992.agentBelievesR : Holder → AttWorld → AttWorld → Prop

The agent-indexed belief relation.

Equations

• Heim1992.agentBelievesR Heim1992.Holder.john = Heim1992.believesR

def Heim1992.frame : Semantics.Modality.EpistemicLogic.KnowledgeBeliefFrame AttWorld Holder

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

Equations

• Heim1992.frame = { knowsRel := Heim1992.agentKnowsR, believesRel := Heim1992.agentBelievesR, believes_sub_knows := Heim1992.frame._proof_1 }

Presupposition

def 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 Heim1992.globalCtx : Core.CommonGround.ContextSet AttWorld

Global context: both worlds are in the context set.

Equations

• Heim1992.globalCtx x✝ = True

Local Contexts

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

Knowledge local context constructed via the bridge.

Equations

• Heim1992.knowledgeLocal = Semantics.Presupposition.BeliefEmbedding.knowledgeLocalCtxOfFrame Heim1992.frame Heim1992.globalCtx Heim1992.Holder.john

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

Belief local context constructed via the bridge.

Equations

• Heim1992.beliefLocal = Semantics.Presupposition.BeliefEmbedding.beliefLocalCtxOfFrame Heim1992.frame Heim1992.globalCtx Heim1992.Holder.john

@cite{heim-1992} Asymmetry Theorems

theorem Heim1992.reflexivity_forces_actual_truth (h : knowledgeLocal.atWorld AttWorld.actual ⊧ presup.presup) : presup.presup AttWorld.actual

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 Heim1992.non_reflexivity_permits_false_presup : (beliefLocal.atWorld AttWorld.actual ⊧ presup.presup) ∧ ¬presup.presup AttWorld.actual

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 is false. This is because the only belief-accessible world from actual is believed, where the presupposition holds.

theorem 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.