Best-worlds desire semantics

On the best-worlds semantics, a wants p when the best worlds of a domain, ranked by the subject's preferences as a Kratzer ordering source, are p-worlds (Want). Von Fintel takes the domain to be the worlds compatible with what the subject believes whatever she chooses to do, and gives want, glad and sorry one family of entries: want presupposes that its domain contains both p-worlds and non-p-worlds, glad adds that the subject believes p and that the domain contains her belief worlds, and sorry has the presupposition of glad and the assertion of wanting p false.

Main definitions

• Desire.BestWorlds.Want: the best worlds of a domain under an ordering source are p-worlds.
• Desire.BestWorlds.want, Desire.BestWorlds.glad, Desire.BestWorlds.regret: von Fintel's entries as trivalent propositions, with world-indexed belief worlds, domain and ordering source.

Main results

• Desire.BestWorlds.Want.not_compl: on a finite frame p and ¬p are not both wanted.
• Desire.BestWorlds.Want.mono: the semantics is upward monotone in p, the doxastic-closure problem Villalta raises.
• Desire.BestWorlds.want_inter_iff: wanting a conjunction is wanting each conjunct, which makes sorry anti-additive in its complement.
• Desire.BestWorlds.support_regret: sorry has the presupposition of glad.
• Desire.BestWorlds.ssubset_of_glad_ne_zero: the presupposition of glad makes the domain properly contain the belief worlds.

Implementation notes

The domain is a parameter. Von Fintel's is the set DOX* of worlds compatible with what the subject believes however she acts, a superset of her belief worlds; Phillips-Brown's rendering takes the belief worlds themselves. Von Fintel's condition that the domain of want be DOX* constrains the domain rather than the complement and is left to the caller, and his presupposition that p be contingent in the domain is Heim's (Desire.IsContingent). The subject is fixed, so the domain and the ordering source are indexed by worlds alone. glad is his best-worlds entry (50), which he replaces by a comparison of the belief worlds with the non-p worlds, (52), after the Honda Civic case; the replacement is VonFintel1999.gladBetter.

References

• [vF99a]
• [Hei92]
• [Kra81b]
• [Vil08]
• [PB25]

Wanting over a domain

def Desire.BestWorlds.Want {W : Type u_1} (A : Set (W → Prop)) (dom p : Set W) : Prop

Want A dom p holds when every best world of dom under the ordering source A is a p-world.

Equations

• Desire.BestWorlds.Want A dom p = ((Modality.premisePreorder A).minimals dom ⊆ p)

theorem Desire.BestWorlds.want_iff {W : Type u_1} {A : Set (W → Prop)} {dom p : Set W} : Want A dom p ↔ ∀ w ∈ dom, (∀ z ∈ dom, z ≤ w → w ≤ z) → w ∈ p

@[instance_reducible]

instance Desire.BestWorlds.instDecidableWantOfFintypeOfDecidableRelLeOfDecidablePredMemSet {W : Type u_1} {A : Set (W → Prop)} {dom p : Set W} [Fintype W] [DecidableRel LE.le] [DecidablePred fun (x : W) => x ∈ dom] [DecidablePred fun (x : W) => x ∈ p] : Decidable (Want A dom p)

Equations

• Desire.BestWorlds.instDecidableWantOfFintypeOfDecidableRelLeOfDecidablePredMemSet = decidable_of_iff (∀ w ∈ dom, (∀ z ∈ dom, z ≤ w → w ≤ z) → w ∈ p) ⋯

theorem Desire.BestWorlds.want_inter_iff {W : Type u_1} {A : Set (W → Prop)} {dom p q : Set W} : Want A dom (p ∩ q) ↔ Want A dom p ∧ Want A dom q

Wanting a conjunction is wanting each conjunct.

theorem Desire.BestWorlds.Want.mono_on {W : Type u_1} {A : Set (W → Prop)} {dom p q : Set W} (hpq : ∀ w ∈ dom, w ∈ p → w ∈ q) (h : Want A dom p) : Want A dom q

What is wanted is wanted under every consequence it has in the domain, the doxastic-closure problem of [Vil08].

theorem Desire.BestWorlds.Want.mono {W : Type u_1} {A : Set (W → Prop)} {dom p q : Set W} (hpq : p ⊆ q) (h : Want A dom p) : Want A dom q

theorem Desire.BestWorlds.Want.not_compl {W : Type u_1} {A : Set (W → Prop)} {dom p : Set W} [Finite W] (h : dom.Nonempty) (hp : Want A dom p) : ¬Want A dom pᶜ

Want, glad and sorry

noncomputable def Desire.BestWorlds.want {W : Type u_1} (base : W → Set W) (g : W → Set (W → Prop)) (p : Set W) : W → SignType

a wants p presupposes that the domain base contains both p-worlds and non-p-worlds and asserts that its best worlds under the ordering source g are p-worlds ([vF99a]'s (45)).

Equations

• Desire.BestWorlds.want base g p = {w : W | Desire.IsContingent (base w) p}.indicator fun (w : W) => SignType.ofProp (Desire.BestWorlds.Want (g w) (base w) p)

noncomputable def Desire.BestWorlds.glad {W : Type u_1} (dox base : W → Set W) (g : W → Set (W → Prop)) (p : Set W) : W → SignType

a is glad that p presupposes, besides the presupposition of want, that a believes p and that the domain contains her belief worlds, and asserts that a wants p ([vF99a]'s (50)).

Equations

• Desire.BestWorlds.glad dox base g p = {w : W | dox w ⊆ p ∧ dox w ⊆ base w}.indicator (Desire.BestWorlds.want base g p)

noncomputable def Desire.BestWorlds.regret {W : Type u_1} (dox base : W → Set W) (g : W → Set (W → Prop)) (p : Set W) : W → SignType

a regrets that p has the presupposition of glad and asserts that a wants p false ([vF99a]'s (53)), restricting want ¬p as glad restricts want p.

Equations

• Desire.BestWorlds.regret dox base g p = {w : W | dox w ⊆ p ∧ dox w ⊆ base w}.indicator (Desire.BestWorlds.want base g pᶜ)

@[simp]

theorem Desire.BestWorlds.want_eq_zero_iff {W : Type u_1} {base : W → Set W} {g : W → Set (W → Prop)} {p : Set W} {w : W} : want base g p w = 0 ↔ ¬IsContingent (base w) p

@[simp]

theorem Desire.BestWorlds.want_eq_one_iff {W : Type u_1} {base : W → Set W} {g : W → Set (W → Prop)} {p : Set W} {w : W} : want base g p w = 1 ↔ IsContingent (base w) p ∧ Want (g w) (base w) p

@[simp]

theorem Desire.BestWorlds.want_eq_neg_one_iff {W : Type u_1} {base : W → Set W} {g : W → Set (W → Prop)} {p : Set W} {w : W} : want base g p w = -1 ↔ IsContingent (base w) p ∧ ¬Want (g w) (base w) p

theorem Desire.BestWorlds.support_regret {W : Type u_1} (dox base : W → Set W) (g : W → Set (W → Prop)) (p : Set W) : Function.support (regret dox base g p) = Function.support (glad dox base g p)

Sorry has the presupposition of glad, since want presupposes as much of ¬p as of p.

theorem Desire.BestWorlds.ssubset_of_glad_ne_zero {W : Type u_1} {dox base : W → Set W} {g : W → Set (W → Prop)} {p : Set W} {w : W} (h : glad dox base g p w ≠ 0) : dox w ⊂ base w

The presupposition of glad makes the domain properly contain the belief worlds, since the belief worlds are p-worlds and the domain has a non-p-world ([vF99a], p. 123).