The value of a question

Relative to a decision problem, a prior over worlds and a utility for each action in each world, an answer is worth the gain in decision value from learning it, and a question, a partition of the worlds, is worth the expected gain from learning its answer. That expectation is the value of information of the experiment revealing the answer, it is never negative, it vanishes exactly when no answer changes the best action, and it reaches the value of perfect information when the answer settles the utilities. One question refines another exactly when it is at least as useful in every decision problem. A wh-question over a domain partitions the worlds by the predicate's extension within the domain, so widening the domain cannot lower the question's value, and once the domain holds every individual the utilities depend on, widening it further only makes the question worse.

Main statements

• Question.utility_eq_valueOfInformation: a question's value is the value of information of revealing its answer.
• Question.utility_eq_zero_iff: a question is worthless exactly when the best action stays best whatever the answer.
• Question.le_iff_forall_utility_le: one question refines another exactly when it is at least as useful in every decision problem.
• Question.better_wh_of_factorsThrough: a wh-domain should contain only the individuals the decision depends on.

References

• [vR03b]
• [Bla53]
• [RS61]

The value of answers

noncomputable def Question.utilityValue {W : Type u} {A : Type u_1} [MeasurableSpace W] (U : W → A → ℝ) (μ : MeasureTheory.Measure W) (C : Set W) : ℝ

The utility value of learning C is the decision value of the prior conditioned on C, less the decision value of the prior.

Equations

• Question.utilityValue U μ C = ProbabilityTheory.decisionValue U μ[|C] - ProbabilityTheory.decisionValue U μ

def Question.BetterAnswer {W : Type u} {A : Type u_1} [MeasurableSpace W] (U : W → A → ℝ) (μ : MeasureTheory.Measure W) (C D : Set W) : Prop

An answer is better than another when it has a higher utility value, or the same value and is strictly less informative.

Equations

• Question.BetterAnswer U μ C D = (toLex (Question.utilityValue U μ D, D) < toLex (Question.utilityValue U μ C, C))

theorem Question.betterAnswer_iff {W : Type u} {A : Type u_1} [MeasurableSpace W] {U : W → A → ℝ} {μ : MeasureTheory.Measure W} {C D : Set W} : BetterAnswer U μ C D ↔ utilityValue U μ D < utilityValue U μ C ∨ utilityValue U μ C = utilityValue U μ D ∧ D ⊂ C

noncomputable def Question.valueSampleInfo {W : Type u} {A : Type u_1} [MeasurableSpace W] (U : W → A → ℝ) (μ : MeasureTheory.Measure W) (a : A) (C : Set W) : ℝ

The value of sample information of learning C compares the best action after learning C with the action a taken now.

Equations

• Question.valueSampleInfo U μ a C = ProbabilityTheory.decisionValue U μ[|C] - ∫ (w : W), U w a ∂μ[|C]

theorem Question.valueSampleInfo_nonneg {W : Type u} {A : Type u_1} [MeasurableSpace W] [Finite A] (U : W → A → ℝ) (μ : MeasureTheory.Measure W) (a : A) (C : Set W) : 0 ≤ valueSampleInfo U μ a C

The utility of questions

noncomputable def Question.utility {W : Type u} {A : Type u_1} [MeasurableSpace W] [Fintype W] [DecidableEq W] (U : W → A → ℝ) (μ : MeasureTheory.Measure W) (Q : Finpartition Finset.univ) : ℝ

The expected utility value of a question weights the utility value of each answer by its probability.

Equations

• Question.utility U μ Q = ∑ c ∈ Q.parts, μ.real ↑c * Question.utilityValue U μ ↑c

def Question.Better {W : Type u} {A : Type u_1} [MeasurableSpace W] [Fintype W] [DecidableEq W] (U : W → A → ℝ) (μ : MeasureTheory.Measure W) (Q Q' : Finpartition Finset.univ) : Prop

Relative to a decision problem, a question is better than another when it is more useful, or as useful and strictly coarser, since one should not ask for irrelevant information.

Equations

• Question.Better U μ Q Q' = (toLex (Question.utility U μ Q', Q') < toLex (Question.utility U μ Q, Q))

theorem Question.better_iff {W : Type u} {A : Type u_1} [MeasurableSpace W] [Fintype W] [DecidableEq W] {U : W → A → ℝ} {μ : MeasureTheory.Measure W} {Q Q' : Finpartition Finset.univ} : Better U μ Q Q' ↔ utility U μ Q' < utility U μ Q ∨ utility U μ Q = utility U μ Q' ∧ Q' < Q

theorem Question.utility_eq_valueOfInformation {W : Type u} {A : Type u_1} [MeasurableSpace W] [Fintype W] [DecidableEq W] [DiscreteMeasurableSpace W] (U : W → A → ℝ) (μ : MeasureTheory.Measure W) [MeasureTheory.IsProbabilityMeasure μ] [Nonempty W] [MeasurableSpace (Finset W)] [MeasurableSingletonClass (Finset W)] (Q : Finpartition Finset.univ) : utility U μ Q = ProbabilityTheory.valueOfInformation (ProbabilityTheory.decisionValue U) (ProbabilityTheory.Kernel.deterministic Q.part ⋯) μ

The expected utility value of a question is the value of information of the experiment that reveals its answer.

theorem Question.utility_eq_valueOfInformation_id {W : Type u} {A : Type u_1} [MeasurableSpace W] [Fintype W] [DecidableEq W] [DiscreteMeasurableSpace W] (U : W → A → ℝ) (μ : MeasureTheory.Measure W) [MeasureTheory.IsProbabilityMeasure μ] [Nonempty W] (Q : Finpartition Finset.univ) (hQ : Function.FactorsThrough U Q.part) : utility U μ Q = ProbabilityTheory.valueOfInformation (ProbabilityTheory.decisionValue U) ProbabilityTheory.Kernel.id μ

A question whose answer settles the utility of every action is worth as much as perfect information.

theorem Question.utility_bot {W : Type u} {A : Type u_1} [MeasurableSpace W] [Fintype W] [DecidableEq W] [DiscreteMeasurableSpace W] (U : W → A → ℝ) (μ : MeasureTheory.Measure W) [MeasureTheory.IsProbabilityMeasure μ] [Nonempty W] : utility U μ ⊥ = ProbabilityTheory.valueOfInformation (ProbabilityTheory.decisionValue U) ProbabilityTheory.Kernel.id μ

The finest question, what the world is like, is worth the expected value of perfect information of [RS61].

theorem Question.utility_nonneg {W : Type u} {A : Type u_1} [MeasurableSpace W] [Fintype W] [DecidableEq W] [DiscreteMeasurableSpace W] (U : W → A → ℝ) (μ : MeasureTheory.Measure W) [MeasureTheory.IsProbabilityMeasure μ] [Finite A] [Nonempty W] (Q : Finpartition Finset.univ) : 0 ≤ utility U μ Q

A question is never worth less than nothing.

theorem Question.utility_anti {W : Type u} {A : Type u_1} [MeasurableSpace W] [Fintype W] [DecidableEq W] [DiscreteMeasurableSpace W] (U : W → A → ℝ) (μ : MeasureTheory.Measure W) [MeasureTheory.IsProbabilityMeasure μ] [Finite A] [Nonempty W] {P Q : Finpartition Finset.univ} (h : P ≤ Q) : utility U μ Q ≤ utility U μ P

A finer question is worth at least as much as a coarser one, since revealing the coarser answer garbles the finer.

theorem Question.utility_le_bot {W : Type u} {A : Type u_1} [MeasurableSpace W] [Fintype W] [DecidableEq W] [DiscreteMeasurableSpace W] (U : W → A → ℝ) (μ : MeasureTheory.Measure W) [MeasureTheory.IsProbabilityMeasure μ] [Finite A] [Nonempty W] (Q : Finpartition Finset.univ) : utility U μ Q ≤ utility U μ ⊥

No question is worth more than the finest one, what the world is like.

theorem Question.utility_eq_sum_valueSampleInfo {W : Type u} {A : Type u_1} [MeasurableSpace W] [Fintype W] [DecidableEq W] [DiscreteMeasurableSpace W] (U : W → A → ℝ) (μ : MeasureTheory.Measure W) [MeasureTheory.IsProbabilityMeasure μ] [Nonempty W] (Q : Finpartition Finset.univ) {a : A} (ha : ∫ (w : W), U w a ∂μ = ProbabilityTheory.decisionValue U μ) : utility U μ Q = ∑ c ∈ Q.parts, μ.real ↑c * valueSampleInfo U μ a ↑c

When a is the best action now, the expected utility value of a question is its expected value of sample information.

theorem Question.utility_eq_zero_iff {W : Type u} {A : Type u_1} [MeasurableSpace W] [Fintype W] [DecidableEq W] [DiscreteMeasurableSpace W] (U : W → A → ℝ) (μ : MeasureTheory.Measure W) [MeasureTheory.IsProbabilityMeasure μ] [Finite A] [Nonempty W] (Q : Finpartition Finset.univ) {a : A} (ha : ∫ (w : W), U w a ∂μ = ProbabilityTheory.decisionValue U μ) : utility U μ Q = 0 ↔ ∀ c ∈ Q.parts, μ ↑c ≠ 0 → ∫ (w : W), U w a ∂μ[|↑c] = ProbabilityTheory.decisionValue U μ[|↑c]

A question is worthless exactly when the action that is best now stays best whatever the answer.

theorem Question.le_iff_forall_utility_le {W : Type u} [MeasurableSpace W] [Fintype W] [DecidableEq W] [DiscreteMeasurableSpace W] [Nonempty W] (P Q : Finpartition Finset.univ) : P ≤ Q ↔ ∀ {B : Type u} [Fintype B] (U : W → B → ℝ) (μ : MeasureTheory.Measure W) [MeasureTheory.IsProbabilityMeasure μ], utility U μ Q ≤ utility U μ P

One question refines another exactly when it is at least as useful in every decision problem with a probability prior, the special case of [Bla53] stated in section 4.1.

The domain of a wh-phrase

def Question.wh {W : Type u} [Fintype W] [DecidableEq W] {D : Type u_2} [DecidableEq D] (P : W → Finset D) (dom : Finset D) : Finpartition Finset.univ

The partition a wh-question induces over a domain puts two worlds together when the predicate's extension agrees on the domain.

Equations

• Question.wh P dom = Finpartition.ofFun fun (w : W) => dom ∩ P w

theorem Question.wh_anti {W : Type u} [Fintype W] [DecidableEq W] {D : Type u_2} [DecidableEq D] (P : W → Finset D) {dom dom' : Finset D} (h : dom ⊆ dom') : wh P dom' ≤ wh P dom

Enlarging the domain refines the question, since more individuals give more specific answers.

theorem Question.better_wh {W : Type u} {A : Type u_1} [Fintype W] [DecidableEq W] {D : Type u_2} [DecidableEq D] [MeasurableSpace W] (U : W → A → ℝ) (μ : MeasureTheory.Measure W) (P : W → Finset D) {dom dom' : Finset D} (h : dom ⊆ dom') (heq : utility U μ (wh P dom) = utility U μ (wh P dom')) (hne : wh P dom' ≠ wh P dom) : Better U μ (wh P dom) (wh P dom')

Of two domains yielding equally useful but different questions, the smaller gives the better question, so the domain relevance selects contains only individuals that could affect the decision.

theorem Question.utility_wh_mono {W : Type u} {A : Type u_1} [Fintype W] [DecidableEq W] {D : Type u_2} [DecidableEq D] [MeasurableSpace W] (U : W → A → ℝ) (μ : MeasureTheory.Measure W) [DiscreteMeasurableSpace W] [MeasureTheory.IsProbabilityMeasure μ] [Finite A] [Nonempty W] (P : W → Finset D) {dom dom' : Finset D} (h : dom ⊆ dom') : utility U μ (wh P dom) ≤ utility U μ (wh P dom')

Enlarging the domain cannot lower the value of the question, so the domain should contain every individual that could matter.

theorem Question.better_wh_of_factorsThrough {W : Type u} {A : Type u_1} [Fintype W] [DecidableEq W] {D : Type u_2} [DecidableEq D] [MeasurableSpace W] (U : W → A → ℝ) (μ : MeasureTheory.Measure W) [DiscreteMeasurableSpace W] [MeasureTheory.IsProbabilityMeasure μ] [Nonempty W] (P : W → Finset D) {dom dom' : Finset D} (h : dom ⊆ dom') (hU : Function.FactorsThrough U (wh P dom).part) (hne : wh P dom' ≠ wh P dom) : Better U μ (wh P dom) (wh P dom')

When the utilities depend only on which individuals of dom satisfy P, every larger domain yielding a different question gives a worse one.