[Hei92] — Comparative-Belief Desire Semantics

⟦α wants φ⟧^w is true iff for every doxastic alternative w' ∈ Dox_α(w), every closest φ-world to w' is more desirable to α than every closest ¬φ-world to w'. The semantics builds on [Lew73b] / [Sta68] similarity orderings, departs from a Kratzer [Kra81]-style ordering source, and treats desirability as a primitive comparative relation parameterized by agent and evaluation world.

This study file replicates the desire-semantics half of [Hei92] (the presupposition-projection half is at Studies/Heim1992.lean). Substrate is Semantics/Attitudes/Desire.lean (wantHeim, wantHeimDefined, HeimDesireParams, wantHeim_no_simultaneous_pq_and_negpq).

§-by-§ map

Paper	Study file
§3 naive Hintikka (informally rejected)	§2 (wantHeimNaive + Asher-style failure case)
(32) Asher Concorde example, p. 194	§2 (analog scenario; see §2 caveat)
§4.2.2 (37/39) CCP-rephrased	§3 / substrate wantHeim
§4.2.3 (40) amendment	substrate wantHeimDefined
§4.3 conflicting desires (implicit)	§4 (substrate no-go)
Stalnaker get-well/¬have-been-sick (p. 195)	§5 (deferred — needs richer model)

Cross-references

• Studies/Heim1992.lean formalizes the know/believe asymmetry — the other half of Heim 1992 (and the more durably cited half).
• The substrate's BeliefBasedDesireSemantics typology (in Desire.lean) packages vF and Heim under one parametric no-go; later study files (PhillipsBrown2025, etc.) instantiate or refute it. Per project chronological-dependency rules, comparisons with later papers live in those later study files, not here.

§1. World model

A simple 4-world model with two binary dimensions:

World	recovered (r)	sick (s)
w0	T	T
w1	T	F
w2	F	T
w3	F	F

Models the Stalnaker [Sta84]-style example "I want to get well [recovered] but I don't want to have been sick" — the agent prefers r ∧ ¬s worlds (recovered without ever being sick) but believes they were sick (so all believed worlds have s). The (40) amendment makes wantHeim ¬s undefined under those beliefs.

inductive Heim1992.W : Type

• w0 : W
• w1 : W
• w2 : W
• w3 : W

@[implicit_reducible]

instance Heim1992.instDecidableEqW : DecidableEq W

Equations

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

def Heim1992.instReprW.repr : W → ℕ → Std.Format

Equations

• Heim1992.instReprW.repr Heim1992.W.w0 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Heim1992.W.w0")).group prec✝
• Heim1992.instReprW.repr Heim1992.W.w1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Heim1992.W.w1")).group prec✝
• Heim1992.instReprW.repr Heim1992.W.w2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Heim1992.W.w2")).group prec✝
• Heim1992.instReprW.repr Heim1992.W.w3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Heim1992.W.w3")).group prec✝

@[implicit_reducible]

instance Heim1992.instReprW : Repr W

Equations

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

@[implicit_reducible]

instance Heim1992.instInhabitedW : Inhabited W

Equations

• Heim1992.instInhabitedW = { default := Heim1992.instInhabitedW.default }

@[implicit_reducible]

instance Heim1992.instFintypeW : Fintype W

Equations

• Heim1992.instFintypeW = { elems := {Heim1992.W.w0, Heim1992.W.w1, Heim1992.W.w2, Heim1992.W.w3}, complete := Heim1992.instFintypeW._proof_1 }

def Heim1992.recovered : Set W

Equations

• Heim1992.recovered Heim1992.W.w0 = True
• Heim1992.recovered Heim1992.W.w1 = True
• Heim1992.recovered x✝ = False

def Heim1992.sick : Set W

Equations

• Heim1992.sick Heim1992.W.w0 = True
• Heim1992.sick Heim1992.W.w2 = True
• Heim1992.sick x✝ = False

@[implicit_reducible]

instance Heim1992.instDecidablePredWRecovered : DecidablePred recovered

Equations

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

@[implicit_reducible]

instance Heim1992.instDecidablePredWSick : DecidablePred sick

Equations

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

§2. Naive Hintikka rule fails on Asher-style cases

The "naive Hintikka" rule for wants (α wants φ iff every doxastic alternative is a φ-world) is rejected informally by Heim (it is not her numbered (27); (27) is the CCP rule). Heim cites [Ash87]'s example at (32), p. 194 ("Nicholas wants a free trip on the Concorde"): the agent wants φ but does not believe φ, so the naive rule wrongly predicts the ascription false.

The analog below is structurally weaker than Asher's Concorde case (no inferential gradient between propositions; no probability weighting). It exhibits only the basic shape — want φ under beliefs that don't entail φ — sufficient to falsify the naive rule. A faithful Concorde-style witness (free-trip ⊨ trip + agent assigns high prob to "trip ∧ pay") requires a richer model and is part of the deferred Phase 2.

def Heim1992.belSick : Set W

Beliefs: agent believes they are sick. belS = {w0, w2}. Neither belief-world entails recovered.

Equations

• Heim1992.belSick = Heim1992.sick

@[implicit_reducible]

instance Heim1992.instDecidablePredWBelSick : DecidablePred belSick

Equations

• Heim1992.instDecidablePredWBelSick = Heim1992.instDecidablePredWBelSick._aux_1

theorem Heim1992.naive_predicts_false_for_wants_recover : ¬Semantics.Attitudes.Desire.wantHeimNaive belSick recovered

The naive Hintikka rule predicts wants recovered false here (because w2 ∈ belSick and ¬ recovered w2). Empirically the ascription can be true, so the naive rule is inadequate — this motivates the move to a comparative semantics.

§3. Truth-conditional comparative-belief (31)

Heim's canonical formulation: ⟦α wants φ⟧ at w iff for every doxastic alternative w', every closest φ-world to w' is more desirable than every closest ¬φ-world to w'.

def Heim1992.trivialSim : Core.Order.SimilarityOrdering W

Trivial similarity ordering: every world is equally close to every other world. The closer relation is the constant True predicate.

Equations

• Heim1992.trivialSim = Core.Order.SimilarityOrdering.ofBool (fun (x x_1 x_2 : Heim1992.W) => true) ⋯ ⋯

def Heim1992.prefRecovered : W → W → W → Prop

Desirability: prefer recovered worlds to non-recovered worlds. The evaluation-world argument is suppressed (constant preference).

Equations

• Heim1992.prefRecovered _w_eval x y = (Heim1992.recovered x ∧ ¬Heim1992.recovered y)

@[implicit_reducible]

instance Heim1992.instDecidablePrefRecovered (w x y : W) : Decidable (prefRecovered w x y)

Equations

• Heim1992.instDecidablePrefRecovered x✝ x y = id inferInstance

def Heim1992.heimParams : Semantics.Attitudes.Desire.HeimDesireParams W

Equations

• Heim1992.heimParams = { sim := Heim1992.trivialSim, pref := Heim1992.prefRecovered, prefDec := inferInstance }

@[implicit_reducible]

instance Heim1992.instDecidablePredWUniv : DecidablePred Set.univ

Equations

• Heim1992.instDecidablePredWUniv x✝ = isTrue trivial

theorem Heim1992.wantHeim_recovered_defined : Semantics.Attitudes.Desire.wantHeimDefined Set.univ recovered

The (40) amendment: wantHeim recovered is defined under Set.univ (both recovered and ¬recovered worlds are believed possible).

§4. Heim (40) does not validate simultaneous want p ∧ want ¬p

A side-effect of (40) — flagged by Heim herself in §4.3 (cf. (41)/(42), where she worries that (40) is in fact too restrictive and proposes shrinking Dox to a "favored" subset F_α) — is that under preference asymmetry, no (belS, w_eval) configuration validates both wantHeim p and wantHeim ¬p. The substrate theorem wantHeim_no_simultaneous_pq_and_negpq discharges this generically.

Whether this side-effect is a virtue (Heim's account correctly rejects co-wanting p and ¬p) or a defect (Heim's account cannot represent genuine ambivalence) is the locus of subsequent debate; Heim's own §4.3 already concedes "a genuine modification is called for." Comparative discussion of later proposals (vF 1999, Phillips-Brown 2025, etc.) belongs in those later study files under the chronological-dependency rule.

theorem Heim1992.prefRecovered_asymm (w_eval x y : W) : prefRecovered w_eval x y → prefRecovered w_eval y x → x = y

prefRecovered is asymmetric: if x is preferred to y, then y is not preferred to x — and the implication "both directions ⇒ equality" requires that no two distinct worlds are both recovered and not-recovered, which is vacuously true.

theorem Heim1992.heim_no_simultaneous_recovered : ¬(Semantics.Attitudes.Desire.wantHeim Set.univ heimParams W.w0 recovered ∧ Semantics.Attitudes.Desire.wantHeim Set.univ heimParams W.w0 fun (w : W) => ¬recovered w)

Witness on this concrete model: under Set.univ, no wantHeim recovered ∧ wantHeim ¬recovered configuration is consistent. Delegates to the substrate's general theorem.

§5. Stalnaker get-well / ¬have-been-sick — deferred

Heim's central worked example (p. 195) is Stalnaker's "I want to get well, but I don't want to have been sick": both want recover and ¬want have-been-sick come out true even though recover ⊨ have-been-sick. Handling it requires the comparative-similarity machinery to do real work — Heim's Sim_w selects a single closest sick-recover-world, and desirability is compared between selections, not over the full belief set.

The minimal witness model (per PDF p. 195) has three worlds with desirability w₁ (healthy throughout) > w₂ (sick then recovered) > w₃ (sick and stays sick) and Dox(w₀) = {w₂, w₃}. The trivial similarity ordering used in §3 collapses this case onto a static rule; a faithful instantiation needs Sim non-trivial. Phase 2 will land this scenario along with prefRecovered's evaluation-world parameter genuinely exercised.