Conditional desire semantics

On Heim's conditional semantics, a wants p holds at w when for every belief world w', every p-world maximally similar to w' is more desirable than every non-p-world maximally similar to w', with the comparison restricted to the belief state and similarity as in Stalnaker and Lewis. Her amendment, that the ascription is undefined when p or its negation is already believed, is Desire.IsContingent, which von Fintel's best-worlds want shares; under it an antisymmetric desirability relation cannot make both p and ¬p wanted.

Main definitions

• Desire.Conditional.Frame: similarity preorders with comparative desirability at each world.
• Desire.Conditional.Frame.closest: the p-worlds of the belief state maximally similar to a world.
• Desire.Conditional.Want, Desire.IsContingent: Heim's (31) and her (40) amendment.

Main results

• Desire.Conditional.Want.not_compl: under the amendment, p and ¬p are not both wanted.

References

• [Hei92]
• [Sta68]
• [Lew73b]
• [vF99a]

def Desire.IsContingent {W : Type u_1} (D p : Set W) : Prop

A domain D is contingent on p when it contains both p-worlds and non-p-worlds, Heim's (40) amendment, which von Fintel adopts as presuppositions of want.

Equations

• Desire.IsContingent D p = ((D ∩ p).Nonempty ∧ (D \ p).Nonempty)

@[instance_reducible]

instance Desire.instDecidableIsContingentOfFintypeOfDecidablePredMemSet {W : Type u_1} [Fintype W] {D p : Set W} [DecidablePred fun (x : W) => x ∈ D] [DecidablePred fun (x : W) => x ∈ p] : Decidable (IsContingent D p)

Equations

• Desire.instDecidableIsContingentOfFintypeOfDecidablePredMemSet = { decide := decide (∃ (x : W), x ∈ D ∩ p) && decide (∃ (x : W), x ∈ D \ p), reflects_decide := ⋯ }

structure Desire.Conditional.Frame (W : Type u_2) : Type u_2

A frame has similarity preorders on worlds and comparative desirability, pref w x y saying that at evaluation world w, x is more desirable than y.

• sim : W → Preorder W

  Similarity to each world.

• pref : W → W → W → Prop

  Comparative desirability at each evaluation world.

def Desire.Conditional.Frame.closest {W : Type u_1} (F : Frame W) (bel p : Set W) (w' : W) : Set W

F.closest bel p w', Heim's Sim_w'(Bel ∩ p), is the set of belief-worlds satisfying p that are maximally similar to w'.

Equations

• F.closest bel p w' = (F.sim w').minimals (bel ∩ p)

def Desire.Conditional.Want {W : Type u_1} (F : Frame W) (bel : Set W) (w : W) (p : Set W) : Prop

a wants p at w when for every belief-world w', every closest p-world to w' is more desirable than every closest ¬p-world to w'.

Equations

• Desire.Conditional.Want F bel w p = ∀ w' ∈ bel, ∀ x ∈ F.closest bel p w', ∀ y ∈ F.closest bel pᶜ w', F.pref w x y

@[instance_reducible]

instance Desire.Conditional.instDecidablePredMemSetClosestOfFintypeOfDecidableRelLe {W : Type u_1} (F : Frame W) (bel p : Set W) [Fintype W] [(w : W) → DecidableRel LE.le] [DecidablePred fun (x : W) => x ∈ bel] [DecidablePred fun (x : W) => x ∈ p] (w' : W) : DecidablePred fun (x : W) => x ∈ F.closest bel p w'

Equations

• Desire.Conditional.instDecidablePredMemSetClosestOfFintypeOfDecidableRelLe F bel p w' = Desire.Conditional.instDecidablePredMemSetClosestOfFintypeOfDecidableRelLe._aux_1 F bel p w'

@[instance_reducible]

instance Desire.Conditional.instDecidableWantOfFintypeOfLeOfDecidablePredMemSetOfDecidableRelPref {W : Type u_1} (F : Frame W) (bel : Set W) (w : W) (p : Set W) [Fintype W] [(w : W) → DecidableRel LE.le] [DecidablePred fun (x : W) => x ∈ bel] [DecidablePred fun (x : W) => x ∈ p] [(w : W) → DecidableRel (F.pref w)] : Decidable (Want F bel w p)

Equations

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

theorem Desire.Conditional.Want.not_compl {W : Type u_1} {F : Frame W} {bel : Set W} {w : W} {p : Set W} [Finite W] [Std.Antisymm (F.pref w)] (hd : IsContingent bel p) (hp : Want F bel w p) : ¬Want F bel w pᶜ

Under (40) and antisymmetric desirability, p and ¬p cannot both be wanted.