KD45 Projection: The [Hei92] Know/Believe Asymmetry

[Hei92]

[Hei92] 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 localCtxOf (from BeliefEmbedding.lean) to presupFiltered (from LocalContext.lean).

The other half of [Hei92] — comparative-belief desire semantics for want/wish/hope — is at Studies/Heim1992.lean. Both halves of the paper are formalized; the substrate splits along the natural empirical boundary (presupposition vs modality).

World Model

inductive Heim1992.AttWorld : Type

Two-world model for the [Hei92] 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 ⋯

@[implicit_reducible]

instance Heim1992.instReprAttWorld : Repr AttWorld

Equations

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

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✝

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., Grove2022.believe).

Equations

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

instance Heim1992.knowsR_isRefl : Std.Refl knowsR

Knowledge relation is reflexive.

instance Heim1992.knowsR_isEucl : Core.Logic.Modal.IsEuclidean knowsR

Knowledge relation is euclidean (trivially: knowsR is the universal relation, so any pair of successors satisfies the goal).

instance Heim1992.believesR_isSerial : Core.Logic.Modal.IsSerial believesR

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

theorem Heim1992.believesR_not_isRefl : ¬Std.Refl believesR

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

instance Heim1992.believesR_isTrans : IsTrans AttWorld believesR

Belief relation is transitive.

instance Heim1992.believesR_isEucl : Core.Logic.Modal.IsEuclidean believesR

Belief relation is Euclidean.

@[reducible]

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

The agent-indexed knowledge relation.

Equations

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

@[reducible]

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

The agent-indexed belief relation.

Equations

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

instance Heim1992.instIsS5FrameAttWorldAgentKnowsRJohn : Core.Logic.Modal.IsS5Frame (agentKnowsR Holder.john)

John's knowledge is S5.

instance Heim1992.instIsKD45FrameAttWorldAgentBelievesRJohn : Core.Logic.Modal.IsKD45Frame (agentBelievesR Holder.john)

John's belief is KD45.

instance Heim1992.instIsBeliefRefinementOfAttWorldAgentKnowsRJohnAgentBelievesR : Core.Logic.Modal.IsBeliefRefinementOf (agentKnowsR Holder.john) (agentBelievesR Holder.john)

Belief refines knowledge for John: R_B ⊆ R_K.

Presupposition

def Heim1992.presup : Semantics.Presupposition.PartialProp 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 : 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.

Equations

• Heim1992.knowledgeLocal = Semantics.Presupposition.BeliefEmbedding.localCtxOf Heim1992.agentKnowsR Heim1992.globalCtx Heim1992.Holder.john

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

Belief local context.

Equations

• Heim1992.beliefLocal = Semantics.Presupposition.BeliefEmbedding.localCtxOf Heim1992.agentBelievesR Heim1992.globalCtx Heim1992.Holder.john

[Hei92] Asymmetry Theorems

theorem Heim1992.reflexivity_forces_actual_truth (h : (knowledgeLocal.atWorld AttWorld.actual).entails 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).entails 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).entails presup.presup ∧ ¬(knowledgeLocal.atWorld AttWorld.actual).entails presup.presup

The [Hei92] 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.