Expected-value desire semantics

On Lassiter's scalar semantics want is a gradable predicate: a wants p holds when the expected value of p given a's beliefs lies above a contextual threshold, the positive form on the expected-value scale. The expected value is the expectation of a value function under the prior conditioned on the worlds of p compatible with the beliefs. It is an interval scale and lies between the values of disjoint propositions, from which the threshold reading derives Weakening and, when want is exclusive on the complement, the Smith Principle. The bare threshold admits wanting p and wanting ¬p at once.

Main definitions

• Desire.ExpectedValue.expectedValue: the expected value of a proposition given a belief state.
• Desire.ExpectedValue.Want: the positive form of want on the expected-value scale.

Main statements

• Desire.ExpectedValue.expectedValue_affine: the expected value is an interval scale.
• Desire.ExpectedValue.expectedValue_intermediate: the expected value of a disjoint union lies between those of its parts.
• Desire.ExpectedValue.Want.union, Desire.ExpectedValue.Want.inter_of_union_eq_univ: Weakening and the Smith Principle.
• Desire.ExpectedValue.exists_want_and_want_compl: a proposition and its negation can both be wanted.

References

• [Las11]
• [Las17a]

noncomputable def Desire.ExpectedValue.expectedValue {W : Type u_1} [MeasurableSpace W] (μ : MeasureTheory.Measure W) (V : W → ℝ) (bel p : Set W) : ℝ

The expected value E_V(p) of p given the belief state is the expectation of the value function under the prior conditioned on the worlds of p compatible with the beliefs.

Equations

• Desire.ExpectedValue.expectedValue μ V bel p = ∫ (w : W), V w ∂μ[|bel ∩ p]

def Desire.ExpectedValue.HasPositiveBeliefMass {W : Type u_1} [MeasurableSpace W] (μ : MeasureTheory.Measure W) (bel p : Set W) : Prop

p has positive prior mass inside the belief state when its compatible worlds do.

Equations

• Desire.ExpectedValue.HasPositiveBeliefMass μ bel p = (μ (bel ∩ p) ≠ 0)

def Desire.ExpectedValue.Want {W : Type u_1} [MeasurableSpace W] (μ : MeasureTheory.Measure W) (V : W → ℝ) (θ : ℝ) (bel p : Set W) : Prop

a wants p when p lies above the threshold on the expected-value scale, the positive form of a gradable predicate.

Equations

• Desire.ExpectedValue.Want μ V θ bel p = (p ∈ Desire.ExpectedValue.expectedValue μ V bel ⁻¹' Set.Ioi θ)

theorem Desire.ExpectedValue.want_iff {W : Type u_1} [MeasurableSpace W] {μ : MeasureTheory.Measure W} {V : W → ℝ} {θ : ℝ} {bel p : Set W} : Want μ V θ bel p ↔ θ < expectedValue μ V bel p

theorem Desire.ExpectedValue.measureReal_mul_expectedValue {W : Type u_1} [MeasurableSpace W] {μ : MeasureTheory.Measure W} {V : W → ℝ} {bel p : Set W} [MeasureTheory.IsFiniteMeasure μ] : μ.real (bel ∩ p) * expectedValue μ V bel p = ∫ (w : W) in bel ∩ p, V w ∂μ

The mass of the compatible worlds of p times the expected value of p is the integral of the value function over those worlds.

theorem Desire.ExpectedValue.expectedValue_eq_sum {W : Type u_1} [MeasurableSpace W] {μ : MeasureTheory.Measure W} {V : W → ℝ} {bel p : Set W} [MeasureTheory.IsFiniteMeasure μ] [Finite W] [MeasurableSingletonClass W] [Fintype W] [DecidablePred fun (x : W) => x ∈ bel ∩ p] : expectedValue μ V bel p = (∑ w : W with w ∈ bel ∩ p, μ.real {w} * V w) / ∑ w : W with w ∈ bel ∩ p, μ.real {w}

Over finitely many worlds, the expected value of p is the prior-weighted average of the value function over the worlds of p compatible with the beliefs.

theorem Desire.ExpectedValue.expectedValue_affine {W : Type u_1} [MeasurableSpace W] {μ : MeasureTheory.Measure W} {V : W → ℝ} {bel p : Set W} [MeasureTheory.IsFiniteMeasure μ] [Finite W] [MeasurableSingletonClass W] (h : HasPositiveBeliefMass μ bel p) (a b : ℝ) : expectedValue μ (fun (w : W) => a * V w + b) bel p = a * expectedValue μ V bel p + b

Expected value is an interval scale, commuting with affine transformations of the value function.

theorem Desire.ExpectedValue.expectedValue_intermediate {W : Type u_1} [MeasurableSpace W] {μ : MeasureTheory.Measure W} {V : W → ℝ} {bel p q : Set W} [MeasureTheory.IsFiniteMeasure μ] [Finite W] [MeasurableSingletonClass W] (hp : HasPositiveBeliefMass μ bel p) (hq : HasPositiveBeliefMass μ bel q) (hd : Disjoint p q) : min (expectedValue μ V bel p) (expectedValue μ V bel q) ≤ expectedValue μ V bel (p ∪ q) ∧ expectedValue μ V bel (p ∪ q) ≤ max (expectedValue μ V bel p) (expectedValue μ 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} [MeasurableSpace W] {μ : MeasureTheory.Measure W} {V : W → ℝ} {θ : ℝ} {bel p q : Set W} [MeasureTheory.IsFiniteMeasure μ] [Finite W] [MeasurableSingletonClass W] (hp' : HasPositiveBeliefMass μ bel p) (hq' : HasPositiveBeliefMass μ bel q) (hd : Disjoint p q) (hp : Want μ V θ bel p) (hq : Want μ V θ bel q) : Want μ V θ bel (p ∪ q)

Weakening holds, since disjoint p and q both above threshold put their union above it.

theorem Desire.ExpectedValue.Want.resolve_left {W : Type u_1} [MeasurableSpace W] {μ : MeasureTheory.Measure W} {V : W → ℝ} {θ : ℝ} {bel p q : Set W} [MeasureTheory.IsFiniteMeasure μ] [Finite W] [MeasurableSingletonClass W] (hp' : HasPositiveBeliefMass μ bel p) (hq' : HasPositiveBeliefMass μ bel q) (hd : Disjoint p q) (h : Want μ V θ bel (p ∪ q)) (hp : ¬Want μ V θ bel p) : Want μ V θ bel q

A disjoint union above threshold with one part at or below it has the other part above it.

theorem Desire.ExpectedValue.Want.inter_of_union_eq_univ {W : Type u_1} [MeasurableSpace W] {μ : MeasureTheory.Measure W} {V : W → ℝ} {θ : ℝ} {bel p q : Set W} [MeasureTheory.IsFiniteMeasure μ] [Finite W] [MeasurableSingletonClass W] (hpq : HasPositiveBeliefMass μ bel (p ∩ q)) (hq' : HasPositiveBeliefMass μ bel qᶜ) (huniv : p ∪ q = Set.univ) (hp : Want μ V θ bel p) (hex : ¬Want μ V θ bel qᶜ) : Want μ V θ bel (p ∩ q)

By the Smith Principle, when p and q exhaust the worlds, wanting p without wanting ¬q is wanting p ∩ q.

theorem Desire.ExpectedValue.exists_want_and_want_compl : ∃ (W : Type) (x : MeasurableSpace W) (μ : MeasureTheory.Measure W) (V : W → ℝ) (θ : ℝ) (bel : Set W) (p : Set W), Want μ V θ bel p ∧ Want μ V θ bel pᶜ

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