Conditional desire semantics

a wants p holds at w iff for every belief-world w', every p-world maximally similar to w' is more desirable than every ¬p-world maximally similar to w' — [Hei92]'s (31), with the comparison restricted to the belief state as in her (39), on [Lew73b] / [Sta68] similarity. Defined is the (40) amendment: the ascription is undefined when p or ¬p is already believed. Under it an antisymmetric desirability relation cannot make both p and ¬p wanted (Want.not_compl).

Main declarations

• Frame: a similarity ordering together with comparative desirability at each evaluation world.
• Frame.closest: Sim_w'(Bel ∩ p), the p-worlds in the belief state maximally similar to w'.
• Want, Defined, Want.not_compl.

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

A similarity ordering on worlds with comparative desirability: pref w x y says that at evaluation world w, x is more desirable than y.

• sim : Semantics.Conditionals.SimilarityOrdering W

  The similarity ordering.

• 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

Sim_w'(Bel ∩ p): the belief-worlds satisfying p that are maximally similar to w'.

Equations

• F.closest bel p w' = F.sim.closest w' (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: 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

def Desire.Conditional.Defined {W : Type u_1} (bel p : Set W) : Prop

The (40) amendment: neither p nor ¬p is already believed.

Equations

• Desire.Conditional.Defined bel p = ((bel ∩ p).Nonempty ∧ (bel ∩ pᶜ).Nonempty)

@[instance_reducible]

instance Desire.Conditional.instDecidablePredMemSetClosestOfFintype {W : Type u_1} (F : Frame W) (bel p : Set W) [Fintype W] [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.instDecidablePredMemSetClosestOfFintype F bel p w' = Desire.Conditional.instDecidablePredMemSetClosestOfFintype._aux_1 F bel p w'

@[instance_reducible]

instance Desire.Conditional.instDecidableWantOfFintypeOfDecidablePredMemSetOfDecidableRelPref {W : Type u_1} (F : Frame W) (bel : Set W) (w : W) (p : Set W) [Fintype W] [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.

@[instance_reducible]

instance Desire.Conditional.instDecidableDefinedOfFintypeOfDecidablePredMemSet {W : Type u_1} (bel p : Set W) [Fintype W] [DecidablePred fun (x : W) => x ∈ bel] [DecidablePred fun (x : W) => x ∈ p] : Decidable (Defined bel p)

Equations

• Desire.Conditional.instDecidableDefinedOfFintypeOfDecidablePredMemSet bel p = Desire.Conditional.instDecidableDefinedOfFintypeOfDecidablePredMemSet._aux_1 bel p

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 : Defined 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.