Heim (1992): presupposition projection in attitude reports

[Hei92] derives Karttunen's generalization — if the complement of an attitude report presupposes p, the report presupposes that the attitude holder believes p ([Kar74a]) — from context change potentials for the attitude predicates. The belief rule (18) makes c + a believes φ defined iff Dox_a(w) + φ is defined for every w ∈ c, and then keeps the worlds whose doxastic state φ maps to itself; believes is that rule as a CCP.Partial combinator, with the doxastic accessibility assignment Dox : E → W → Set W of (11)–(12). On atomic complements its definedness condition is Karttunen's rule (3) taken on the union of the doxastic states (admits_believes_iff_iUnion) and the local-context condition of [Sch09a] (admits_believes_iff_presupAttributedToHolder). The paper's derivations follow: the too-discourse (20) presupposes nothing (believes_too_admits), while its doubt variant (25) is admitted only by contexts its first conjunct reduces to the absurd context (doubt_too_admits_iff). The factive rule for know from footnote 47 (knows) demands c + φ = c outright, so a know report projects its complement's presupposition transparently (transparentProjection_of_admits_knows); a belief report does so only when Dox is veridical (transparentProjection_of_admits_believes), and believes_admits_not_knows is the two-world witness on Patrick's cello (2).

The desire half (§4) replaces the Hintikka-style rule (27) with the comparative-belief semantics (31): a wants φ holds iff each doxastic alternative's closest φ-worlds are more desirable than its closest ¬φ-worlds, on [Sta68] / [Lew73b] similarity. The substrate is Semantics/Attitudes/Desire/Conditional.lean (Frame, Want, Defined). The four-world model below shows the naive rule failing on the shape of [Ash87]'s Concorde case (32) and the (40) amendment blocking simultaneous want p ∧ want ¬p. Stalnaker's get-well / have-been-sick contrast ([Sta84], Heim's three-world model on p. 195) needs a non-trivial similarity ordering and is not formalized.

Belief reports

def Heim1992.believes {W : Type u_1} {E : Type u_2} (Dox : E → W → Set W) (a : E) (φ : DynamicSemantics.CCP.Partial W) : DynamicSemantics.CCP.Partial W

Rule (18): c + a believes φ is defined iff Dox_a(w) + φ is defined for every w ∈ c, and then equals {w ∈ c | Dox_a(w) + φ = Dox_a(w)}.

Equations

• Heim1992.believes Dox a φ c = { Dom := ∀ w ∈ c, φ.admits (Dox a w), get := fun (x : ∀ w ∈ c, φ.admits (Dox a w)) => {w : W | w ∈ c ∧ Dox a w ∈ φ (Dox a w)} }

theorem Heim1992.admits_believes {W : Type u_1} {E : Type u_2} (Dox : E → W → Set W) (a : E) (φ : DynamicSemantics.CCP.Partial W) (c : Set W) : (believes Dox a φ).admits c ↔ ∀ w ∈ c, φ.admits (Dox a w)

@[simp]

theorem Heim1992.believes_get {W : Type u_1} {E : Type u_2} (Dox : E → W → Set W) (a : E) (φ : DynamicSemantics.CCP.Partial W) (c : Set W) (h : (believes Dox a φ).admits c) : (believes Dox a φ c).get h = {w : W | w ∈ c ∧ Dox a w ∈ φ (Dox a w)}

theorem Heim1992.admits_believes_ofPartialProp {W : Type u_1} {E : Type u_2} (Dox : E → W → Set W) (a : E) (p : Semantics.Presupposition.PartialProp W) (c : Set W) : (believes Dox a (DynamicSemantics.CCP.Partial.ofPartialProp p)).admits c ↔ ∀ w ∈ c, ModalLogic.Epistemic.believes Dox a p.presup w

Karttunen's generalization: if φ presupposes p, then a believes φ presupposes that a believes p.

theorem Heim1992.admits_believes_iff_iUnion {W : Type u_1} {E : Type u_2} (Dox : E → W → Set W) (a : E) (p : Semantics.Presupposition.PartialProp W) (c : Set W) : (believes Dox a (DynamicSemantics.CCP.Partial.ofPartialProp p)).admits c ↔ (DynamicSemantics.CCP.Partial.ofPartialProp p).admits (⋃ w ∈ c, Dox a w)

Karttunen's rule (3) on atomic complements: definedness on each Dox_a(w) is definedness on their union, the beliefs attributed to a in c.

theorem Heim1992.admits_believes_iff_presupAttributedToHolder {W : Type u_1} {E : Type u_2} (Dox : E → W → Set W) (a : E) (p : Semantics.Presupposition.PartialProp W) (c : Set W) : (believes Dox a (DynamicSemantics.CCP.Partial.ofPartialProp p)).admits c ↔ Semantics.Presupposition.BeliefEmbedding.presupAttributedToHolder { globalCtx := c, dox := Dox, agent := a } p

The definedness condition of (18) is the local-context condition of [Sch09a].

theorem Heim1992.believes_too_admits {W : Type u_1} {E : Type u_2} (Dox : E → W → Set W) (a : E) (c m s : Set W) : ((believes Dox a (DynamicSemantics.CCP.Partial.ofPartialProp (Semantics.Presupposition.PartialProp.ofProp m))).seq (believes Dox a (DynamicSemantics.CCP.Partial.ofPartialProp { presup := m, assertion := s }))).admits c

(20) presupposes nothing: every context admits John believes that Mary_i is here, and he believes that Susan_F is here too_i, where by (22) the too-clause presupposes that Mary is here.

theorem Heim1992.doubt_too_admits_iff {W : Type u_1} {E : Type u_2} (Dox : E → W → Set W) (a : E) (c m s : Set W) : ((believes Dox a (DynamicSemantics.CCP.Partial.ofPartialProp (Semantics.Presupposition.PartialProp.ofProp m))).neg.seq (believes Dox a (DynamicSemantics.CCP.Partial.ofPartialProp { presup := m, assertion := s }))).admits c ↔ ∀ w ∈ c, Dox a w ⊆ m

(25) John doubts that Mary_i is here and believes that Susan_F is here too_i is admitted only by contexts in which John already believes Mary is here — which its first conjunct then reduces to the absurd context.

def Heim1992.knows {W : Type u_1} {E : Type u_2} (Dox : E → W → Set W) (a : E) (φ : DynamicSemantics.CCP.Partial W) : DynamicSemantics.CCP.Partial W

The factive rule of footnote 47: c + a knows φ is undefined unless c + φ = c, and is otherwise c + a believes φ.

Equations

• Heim1992.knows Dox a φ c = Part.assert (c ∈ φ c) fun (x : c ∈ φ c) => Heim1992.believes Dox a φ c

theorem Heim1992.admits_knows {W : Type u_1} {E : Type u_2} (Dox : E → W → Set W) (a : E) (φ : DynamicSemantics.CCP.Partial W) (c : Set W) : (knows Dox a φ).admits c ↔ c ∈ φ c ∧ (believes Dox a φ).admits c

theorem Heim1992.transparentProjection_of_admits_knows {W : Type u_1} {E : Type u_2} (Dox : E → W → Set W) (a : E) (p : Semantics.Presupposition.PartialProp W) (c : Set W) (h : (knows Dox a (DynamicSemantics.CCP.Partial.ofPartialProp p)).admits c) : Semantics.Presupposition.BeliefEmbedding.transparentProjection c p

A know report projects its complement's presupposition transparently.

theorem Heim1992.transparentProjection_of_admits_believes {W : Type u_1} {E : Type u_2} (Dox : E → W → Set W) (a : E) (p : Semantics.Presupposition.PartialProp W) (c : Set W) (hrefl : ∀ w ∈ c, w ∈ Dox a w) (h : (believes Dox a (DynamicSemantics.CCP.Partial.ofPartialProp p)).admits c) : Semantics.Presupposition.BeliefEmbedding.transparentProjection c p

With veridical Dox on c, rule (18) already projects the complement's presupposition transparently — the factivity that knows imposes outright.

The know/believe contrast on Patrick's cello

inductive Heim1992.CelloWorld : Type

Whether Patrick owns a cello.

• owns : CelloWorld
• lacks : CelloWorld

@[instance_reducible]

instance Heim1992.instDecidableEqCelloWorld : DecidableEq CelloWorld

Equations

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

def Heim1992.celloDox : Unit → CelloWorld → Set CelloWorld

Patrick's misconception (2): whatever the facts, he believes he owns a cello.

Equations

• Heim1992.celloDox x✝¹ x✝ = {Heim1992.CelloWorld.owns}

def Heim1992.sellsCello : Semantics.Presupposition.PartialProp CelloWorld

Patrick sells his cello (1): presupposes that he owns one.

Equations

• Heim1992.sellsCello = { presup := fun (x : Heim1992.CelloWorld) => x = Heim1992.CelloWorld.owns, assertion := fun (x : Heim1992.CelloWorld) => True }

theorem Heim1992.believes_admits_not_knows : (believes celloDox () (DynamicSemantics.CCP.Partial.ofPartialProp sellsCello)).admits {CelloWorld.lacks} ∧ ¬(knows celloDox () (DynamicSemantics.CCP.Partial.ofPartialProp sellsCello)).admits {CelloWorld.lacks}

Where Patrick lacks a cello but believes he owns one, Patrick believes he is selling his cello is admitted and Patrick knows he is selling his cello is not: celloDox is not veridical at lacks.

Desire reports: the four-world model

inductive Heim1992.HealthWorld : Type

Worlds classified by two binary dimensions, recovered (r) and sick (s): w0 = r ∧ s, w1 = r ∧ ¬s, w2 = ¬r ∧ s, w3 = ¬r ∧ ¬s.

• w0 : HealthWorld
• w1 : HealthWorld
• w2 : HealthWorld
• w3 : HealthWorld

@[instance_reducible]

instance Heim1992.instDecidableEqHealthWorld : DecidableEq HealthWorld

Equations

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

@[instance_reducible]

instance Heim1992.instFintypeHealthWorld : Fintype HealthWorld

Equations

• Heim1992.instFintypeHealthWorld = { elems := { val := ↑Heim1992.HealthWorld.enumList, nodup := Heim1992.HealthWorld.enumList_nodup }, complete := Heim1992.instFintypeHealthWorld._proof_1 }

def Heim1992.recovered : Set HealthWorld

Equations

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

def Heim1992.sick : Set HealthWorld

Equations

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

@[instance_reducible]

instance Heim1992.instDecidablePredHealthWorldMemSetRecovered : DecidablePred fun (x : HealthWorld) => x ∈ recovered

Equations

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

theorem Heim1992.not_sick_subset_recovered : ¬sick ⊆ recovered

The naive Hintikka rule (27) — a wants φ iff every doxastic alternative is a φ-world, bel ⊆ φ — which Heim rejects on [Ash87]'s Concorde case (32), predicts wants recovered false under the belief state sick, since w2 is believed and not recovered.

def Heim1992.trivialSim : Semantics.Conditionals.SimilarityOrdering HealthWorld

Every world is equally similar to every other.

Equations

• Heim1992.trivialSim = Semantics.Conditionals.SimilarityOrdering.ofBool (fun (x x_1 x_2 : Heim1992.HealthWorld) => true) ⋯ ⋯

def Heim1992.prefRecovered : HealthWorld → HealthWorld → HealthWorld → Prop

Recovered worlds are preferred to non-recovered ones, at every evaluation world.

Equations

• Heim1992.prefRecovered x✝ x y = (x ∈ Heim1992.recovered ∧ y ∉ Heim1992.recovered)

@[instance_reducible]

instance Heim1992.instDecidableRelHealthWorldPrefRecovered (w : HealthWorld) : DecidableRel (prefRecovered w)

Equations

• Heim1992.instDecidableRelHealthWorldPrefRecovered w x y = Heim1992.instDecidableRelHealthWorldPrefRecovered._aux_1 w x y

instance Heim1992.instAntisymmHealthWorldPrefRecovered (w : HealthWorld) : Std.Antisymm (prefRecovered w)

@[reducible, inline]

abbrev Heim1992.heimFrame : Desire.Conditional.Frame HealthWorld

Equations

• Heim1992.heimFrame = { sim := Heim1992.trivialSim, pref := Heim1992.prefRecovered }

theorem Heim1992.defined_recovered : Desire.Conditional.Defined Set.univ recovered

The (40) amendment: want recovered is defined when both recovered and non-recovered worlds are believed possible.

theorem Heim1992.not_want_recovered_compl (h : Desire.Conditional.Want heimFrame Set.univ HealthWorld.w0 recovered) : ¬Desire.Conditional.Want heimFrame Set.univ HealthWorld.w0 recoveredᶜ

Under (40) and an asymmetric preference, want recovered and want ¬recovered cannot both hold. (Heim's own worry about (40)'s restrictiveness, at (41)–(42), concerns wanting what one is convinced of; her remedy (43) replaces Dox_a by a superset F_a.)