Best-worlds desire semantics

a wants p iff every best belief-world is a p-world, where belief-worlds are ordered by the desires they satisfy — [vF99a]'s semantics, with [Kra81]'s ordering over the desire propositions. Some belief-world is always best on a finite frame (exists_undominated), so p and ¬p cannot both be wanted (Want.not_compl); the semantics is upward monotone in p (Want.mono), which is the doxastic-closure problem of [Vil08].

def Desire.BestWorlds.le {W : Type u_1} (G : List (Finset W)) (w z : W) : Prop

le G w z: every desire in G satisfied at z is satisfied at w.

Equations

• Desire.BestWorlds.le G w z = (w ≤[List.map (fun (s : Finset W) (w : W) => w ∈ s) G] z)

theorem Desire.BestWorlds.le_iff {W : Type u_1} (G : List (Finset W)) (w z : W) : le G w z ↔ ∀ s ∈ G, z ∈ s → w ∈ s

@[instance_reducible]

instance Desire.BestWorlds.instDecidableLeOfDecidableEq {W : Type u_1} (G : List (Finset W)) [DecidableEq W] (w z : W) : Decidable (le G w z)

Equations

• Desire.BestWorlds.instDecidableLeOfDecidableEq G w z = decidable_of_iff (∀ s ∈ G, z ∈ s → w ∈ s) ⋯

def Desire.BestWorlds.Undominated {W : Type u_1} (G : List (Finset W)) (bel : Set W) (w : W) : Prop

No belief-world is strictly better than w.

Equations

• Desire.BestWorlds.Undominated G bel w = ∀ z ∈ bel, Desire.BestWorlds.le G z w → Desire.BestWorlds.le G w z

def Desire.BestWorlds.Want {W : Type u_1} (G : List (Finset W)) (bel p : Set W) : Prop

a wants p: every best belief-world is a p-world.

Equations

• Desire.BestWorlds.Want G bel p = ∀ w ∈ bel, Desire.BestWorlds.Undominated G bel w → w ∈ p

@[instance_reducible]

instance Desire.BestWorlds.instDecidableUndominatedOfFintypeOfDecidableEqOfDecidablePredMemSet {W : Type u_1} (G : List (Finset W)) (bel : Set W) [Fintype W] [DecidableEq W] [DecidablePred fun (x : W) => x ∈ bel] (w : W) : Decidable (Undominated G bel w)

Equations

• Desire.BestWorlds.instDecidableUndominatedOfFintypeOfDecidableEqOfDecidablePredMemSet G bel w = Desire.BestWorlds.instDecidableUndominatedOfFintypeOfDecidableEqOfDecidablePredMemSet._aux_1 G bel w

@[instance_reducible]

instance Desire.BestWorlds.instDecidableWantOfFintypeOfDecidableEqOfDecidablePredMemSet {W : Type u_1} (G : List (Finset W)) (bel p : Set W) [Fintype W] [DecidableEq W] [DecidablePred fun (x : W) => x ∈ bel] [DecidablePred fun (x : W) => x ∈ p] : Decidable (Want G bel p)

Equations

• Desire.BestWorlds.instDecidableWantOfFintypeOfDecidableEqOfDecidablePredMemSet G bel p = Desire.BestWorlds.instDecidableWantOfFintypeOfDecidableEqOfDecidablePredMemSet._aux_1 G bel p

theorem Desire.BestWorlds.exists_undominated {W : Type u_1} (G : List (Finset W)) (bel : Set W) [Finite W] (h : bel.Nonempty) : ∃ w ∈ bel, Undominated G bel w

On a finite frame every nonempty belief state has a best world.

theorem Desire.BestWorlds.Want.not_compl {W : Type u_1} {G : List (Finset W)} {bel p : Set W} [Finite W] (h : bel.Nonempty) (hp : Want G bel p) : ¬Want G bel pᶜ

theorem Desire.BestWorlds.Want.mono {W : Type u_1} {G : List (Finset W)} {bel p q : Set W} (hpq : p ⊆ q) (h : Want G bel p) : Want G bel q