Expected-value desire semantics

a wants p iff the conditional expected value of p given a's beliefs exceeds a contextual threshold — [Las17a]'s scalar semantics for evaluative predicates, applied to want ([Las11]). expectedValue is the conditional expected utility of the one-action decision problem whose utility is the value function; it is intermediate on disjoint propositions (expectedValue_intermediate), from which Weakening follows (Want.union). The bare threshold admits simultaneous want p and want ¬p (exists_want_and_want_compl); Sloman's Principle — the wanted proposition strictly dominates every alternative ([Las17a]) — excludes it (WantWithSloman.not_compl).

def Desire.ExpectedValue.toDecisionProblem {W : Type u_1} (pr V : W → ℚ) : Core.DecisionTheory.DecisionProblem ℚ W Unit

The one-action decision problem whose utility is the value function V.

Equations

• Desire.ExpectedValue.toDecisionProblem pr V = { utility := fun (w : W) (x : Unit) => V w, prior := pr }

def Desire.ExpectedValue.cell {W : Type u_1} [Fintype W] (bel p : Set W) [DecidablePred fun (x : W) => x ∈ bel] [DecidablePred fun (x : W) => x ∈ p] : Finset W

The worlds of p compatible with the beliefs.

Equations

• Desire.ExpectedValue.cell bel p = {x : W | x ∈ bel ∩ p}

def Desire.ExpectedValue.expectedValue {W : Type u_1} [Fintype W] (pr V : W → ℚ) (bel p : Set W) [DecidablePred fun (x : W) => x ∈ bel] [DecidablePred fun (x : W) => x ∈ p] : ℚ

E_V(p): the conditional expected value of p given the belief state (0 on a zero-mass cell).

Equations

• Desire.ExpectedValue.expectedValue pr V bel p = (Desire.ExpectedValue.toDecisionProblem pr V).condExpectedUtility (Desire.ExpectedValue.cell bel p) ()

def Desire.ExpectedValue.HasPositiveBeliefMass {W : Type u_1} [Fintype W] (pr : W → ℚ) (bel p : Set W) [DecidablePred fun (x : W) => x ∈ bel] [DecidablePred fun (x : W) => x ∈ p] : Prop

p carries positive prior mass inside the belief state.

Equations

• Desire.ExpectedValue.HasPositiveBeliefMass pr bel p = (0 < ∑ w ∈ Desire.ExpectedValue.cell bel p, pr w)

def Desire.ExpectedValue.Want {W : Type u_1} [Fintype W] (pr V : W → ℚ) (θ : ℚ) (bel p : Set W) [DecidablePred fun (x : W) => x ∈ bel] [DecidablePred fun (x : W) => x ∈ p] : Prop

a wants p: the expected value of p exceeds the threshold.

Equations

• Desire.ExpectedValue.Want pr V θ bel p = (θ < Desire.ExpectedValue.expectedValue pr V bel p)

@[instance_reducible]

instance Desire.ExpectedValue.instDecidableWant {W : Type u_1} [Fintype W] (pr V : W → ℚ) (θ : ℚ) (bel p : Set W) [DecidablePred fun (x : W) => x ∈ bel] [DecidablePred fun (x : W) => x ∈ p] : Decidable (Want pr V θ bel p)

Equations

• Desire.ExpectedValue.instDecidableWant pr V θ bel p = Desire.ExpectedValue.instDecidableWant._aux_1 pr V θ bel p

def Desire.ExpectedValue.SlomanPrinciple {W : Type u_1} [Fintype W] (pr V : W → ℚ) (bel : Set W) [DecidablePred fun (x : W) => x ∈ bel] [DecidableEq W] (alts : List (Finset W)) (s : Finset W) : Prop

s strictly dominates every other alternative on the expected-value scale.

Equations

• Desire.ExpectedValue.SlomanPrinciple pr V bel alts s = ∀ t ∈ alts, t ≠ s → Desire.ExpectedValue.expectedValue pr V bel ↑t < Desire.ExpectedValue.expectedValue pr V bel ↑s

def Desire.ExpectedValue.WantWithSloman {W : Type u_1} [Fintype W] (pr V : W → ℚ) (θ : ℚ) (bel : Set W) [DecidablePred fun (x : W) => x ∈ bel] [DecidableEq W] (alts : List (Finset W)) (s : Finset W) : Prop

The threshold reading together with Sloman's Principle.

Equations

• Desire.ExpectedValue.WantWithSloman pr V θ bel alts s = (Desire.ExpectedValue.Want pr V θ bel ↑s ∧ Desire.ExpectedValue.SlomanPrinciple pr V bel alts s)

theorem Desire.ExpectedValue.expectedValue_eq {W : Type u_1} [Fintype W] {pr V : W → ℚ} {bel p : Set W} [DecidablePred fun (x : W) => x ∈ bel] [DecidablePred fun (x : W) => x ∈ p] (h : HasPositiveBeliefMass pr bel p) : expectedValue pr V bel p = (∑ w ∈ cell bel p, pr w * V w) / ∑ w ∈ cell bel p, pr w

theorem Desire.ExpectedValue.cell_union {W : Type u_1} [Fintype W] {bel p q : Set W} [DecidablePred fun (x : W) => x ∈ bel] [DecidablePred fun (x : W) => x ∈ p] [DecidablePred fun (x : W) => x ∈ q] [DecidableEq W] : cell bel (p ∪ q) = cell bel p ∪ cell bel q

theorem Desire.ExpectedValue.disjoint_cell {W : Type u_1} [Fintype W] {bel p q : Set W} [DecidablePred fun (x : W) => x ∈ bel] [DecidablePred fun (x : W) => x ∈ p] [DecidablePred fun (x : W) => x ∈ q] [DecidableEq W] (h : Disjoint p q) : Disjoint (cell bel p) (cell bel q)

theorem Desire.ExpectedValue.expectedValue_intermediate {W : Type u_1} [Fintype W] {pr V : W → ℚ} {bel p q : Set W} [DecidablePred fun (x : W) => x ∈ bel] [DecidablePred fun (x : W) => x ∈ p] [DecidablePred fun (x : W) => x ∈ q] [DecidableEq W] (hp : HasPositiveBeliefMass pr bel p) (hq : HasPositiveBeliefMass pr bel q) (hd : Disjoint p q) : min (expectedValue pr V bel p) (expectedValue pr V bel q) ≤ expectedValue pr V bel (p ∪ q) ∧ expectedValue pr V bel (p ∪ q) ≤ max (expectedValue pr V bel p) (expectedValue pr V bel q)

The expected value of a disjoint union lies between the expected values of the parts.

theorem Desire.ExpectedValue.Want.union {W : Type u_1} [Fintype W] {pr V : W → ℚ} {θ : ℚ} {bel p q : Set W} [DecidablePred fun (x : W) => x ∈ bel] [DecidablePred fun (x : W) => x ∈ p] [DecidablePred fun (x : W) => x ∈ q] [DecidableEq W] (hp' : HasPositiveBeliefMass pr bel p) (hq' : HasPositiveBeliefMass pr bel q) (hd : Disjoint p q) (hp : Want pr V θ bel p) (hq : Want pr V θ bel q) : Want pr V θ bel (p ∪ q)

Weakening: disjoint p and q both above threshold put their union above it.

theorem Desire.ExpectedValue.WantWithSloman.not_compl {W : Type u_1} [Fintype W] {pr V : W → ℚ} {θ : ℚ} {bel : Set W} [DecidablePred fun (x : W) => x ∈ bel] [DecidableEq W] {alts : List (Finset W)} {s : Finset W} (hs : s ∈ alts) (hsc : sᶜ ∈ alts) (hne : s ≠ sᶜ) (h : WantWithSloman pr V θ bel alts s) : ¬WantWithSloman pr V θ bel alts sᶜ

theorem Desire.ExpectedValue.exists_want_and_want_compl : ∃ (W : Type) (x : Fintype W) (pr : W → ℚ) (V : W → ℚ) (θ : ℚ) (bel : Set W) (p : Set W) (x_1 : DecidablePred fun (x : W) => x ∈ bel) (x_2 : DecidablePred fun (x : W) => x ∈ p), Want pr V θ bel p ∧ Want pr V θ bel pᶜ

The bare threshold admits simultaneous want p and want ¬p.