Heim (1992): Presupposition Projection and the Semantics of Attitude Verbs

Heim gives the attitude predicates context change potentials and derives their projection behaviour. The belief rule (18) is believes, a CCP.Partial combinator over the doxastic accessibility of (11)–(12): the report is defined iff the complement is defined on each doxastic state, so a complement presupposing p yields a report presupposing that its holder believes p, Karttunen's generalization. The factive rule of footnote 47 makes know admit only contexts that admit its complement's presupposition, which a belief report need not. The desire half replaces the Hintikka-style rule (27) with the comparative semantics (31) on similarity, the library's Desire.Conditional.Want, with the amendment (40) blocking want p ∧ want ¬p.

Main statements

• admits_believes_iff, believes_ofTrivalent: on atomic complements the belief rule is Karttunen's admittance in the holder's beliefs, and the update with a trivalent proposition.
• believes_too_admits, doubt_too_admits_iff: the too-discourse presupposes nothing, and its doubt variant is admitted only by contexts its first conjunct reduces to the absurd one.
• admits_of_admits_knows, believes_admits_not_knows: know passes on its complement's presupposition and believe need not, as Patrick's cello shows.
• defined_recovered, not_want_recovered_compl: on a four-world model shaped like Asher's Concorde case, the amendment blocks wanting both p and ¬p.

Implementation notes

• The three-world model of Section 4.1 for Stalnaker's get-well and have-been-sick contrast needs a non-trivial similarity ordering and is not formalized; the four-world model here uses the trivial ordering.

References

• [Hei92]
• [Kar74a]
• [Ash87]
• [Sta84]
• [Sta68]
• [Lew73b]

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

By 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

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

theorem Heim1992.admits_believes_ofTrivalent {W : Type u_1} {E : Type u_2} (Dox : E → W → Set W) (a : E) (p : W → SignType) (c : Set W) : DynamicSemantics.PartialUpdate.Admits (believes Dox a (DynamicSemantics.CCP.Partial.ofTrivalent p)) c ↔ ∀ w ∈ c, ModalLogic.Box (SetRel.ofSuccessors (Dox a)) (fun (x : W) => x ∈ Function.support p) w

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

theorem Heim1992.admits_believes_iff {W : Type u_1} {E : Type u_2} (Dox : E → W → Set W) (a : E) (p : W → SignType) (c : Set W) : DynamicSemantics.PartialUpdate.Admits (believes Dox a (DynamicSemantics.CCP.Partial.ofTrivalent p)) c ↔ (SetRel.ofSuccessors (Dox a)).image c ⊆ Function.support p

On atomic complements, Karttunen's rule (3) makes definedness on each Dox_a(w) admittance in their union, the image of c under the doxastic accessibility, which is what a is taken to believe in c.

theorem Heim1992.believes_ofTrivalent {W : Type u_1} {E : Type u_2} (Dox : E → W → Set W) (a : E) (p : W → SignType) : believes Dox a (DynamicSemantics.CCP.Partial.ofTrivalent p) = DynamicSemantics.CCP.Partial.ofTrivalent ({w : W | ModalLogic.Box (SetRel.ofSuccessors (Dox a)) (fun (x : W) => x ∈ Function.support p) w}.indicator fun (w : W) => SignType.ofProp (ModalLogic.Box (SetRel.ofSuccessors (Dox a)) (fun (x : W) => p x = 1) w))

On atomic complements (18) is static, as in the calculation (24), since a believes φ is the update with the trivalent proposition that presupposes that a believes φ's presupposition and asserts that a believes φ.

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) [DecidablePred fun (x : W) => x ∈ m] [DecidablePred fun (x : W) => x ∈ s] : (DynamicSemantics.PartialUpdate.seq (believes Dox a (DynamicSemantics.CCP.Partial.ofTrivalent fun (w : W) => SignType.ofProp (w ∈ m))) (believes Dox a (DynamicSemantics.CCP.Partial.ofTrivalent (m.indicator fun (w : W) => SignType.ofProp (w ∈ s))))).Admits c

(20) presupposes nothing, since 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) [DecidablePred fun (x : W) => x ∈ m] [DecidablePred fun (x : W) => x ∈ s] : (DynamicSemantics.PartialUpdate.seq (believes Dox a (DynamicSemantics.CCP.Partial.ofTrivalent fun (w : W) => SignType.ofProp (w ∈ m))).neg (believes Dox a (DynamicSemantics.CCP.Partial.ofTrivalent (m.indicator fun (w : W) => SignType.ofProp (w ∈ 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

By 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) : DynamicSemantics.PartialUpdate.Admits (knows Dox a φ) c ↔ c ∈ φ c ∧ DynamicSemantics.PartialUpdate.Admits (believes Dox a φ) c

theorem Heim1992.admits_of_admits_knows {W : Type u_1} {E : Type u_2} (Dox : E → W → Set W) (a : E) (p : W → SignType) (c : Set W) (h : DynamicSemantics.PartialUpdate.Admits (knows Dox a (DynamicSemantics.CCP.Partial.ofTrivalent p)) c) : c ⊆ Function.support p

A context admitting a know report admits its complement's presupposition.

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

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

Equations

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

noncomputable def Heim1992.sellsCello : CelloWorld → SignType

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

Equations

• Heim1992.sellsCello = {Heim1992.CelloWorld.owns}.indicator 1

theorem Heim1992.believes_admits_not_knows : DynamicSemantics.PartialUpdate.Admits (believes celloDox () (DynamicSemantics.CCP.Partial.ofTrivalent sellsCello)) {CelloWorld.lacks} ∧ ¬DynamicSemantics.PartialUpdate.Admits (knows celloDox () (DynamicSemantics.CCP.Partial.ofTrivalent sellsCello)) {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, since celloDox is not veridical at lacks.

Desire reports: the four-world model

inductive Heim1992.HealthWorld : Type

Worlds are classified by two binary dimensions, recovered (r) and sick (s), with w0 = r ∧ s, w1 = r ∧ ¬s, w2 = ¬r ∧ s and 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.

@[reducible, inline]

abbrev Heim1992.trivialSim : HealthWorld → Preorder HealthWorld

Every world is equally similar to every other.

Equations

• Heim1992.trivialSim x✝ = ⊤

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 = { decide := decide (x ∈ Heim1992.recovered) && decide (y ∉ Heim1992.recovered), reflects_decide := ⋯ }

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.IsContingent Set.univ recovered

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