Core Decision Theory

[vR03a] [Bla53]

Theory-neutral decision-theoretic infrastructure: decision problems, expected utility, maximin, and mention-some/mention-all classification.

Promoted from Semantics.Questions.DecisionTheory so that any module (RSA, causal decision theory, explanation models) can use decision problems without pulling in question-semantic types.

Design: Fintype + Finset

Functions that sum over the full universe use [Fintype W] with ∑ w : W. Functions that operate over action sets or world subsets use Finset. questionUtility and expectedVSI take Finset (Finset W) (cells as sets). Ordering-sensitive operations (questionMaximin, isMentionSome, resolvingAnswers, …) take a List (Finset W) of cells.

• [vR03a]. Questioning to Resolve Decision Problems. L&P 26.
• [Bla53]. Equivalent Comparisons of Experiments.

Decision Problems

structure Core.DecisionTheory.DecisionProblem (W : Type u_1) (A : Type u_2) : Type (max u_1 u_2)

A decision problem D = (W, A, U, π) with utility and prior.

• utility : W → A → ℚ

  Utility of action a in world w

• prior : W → ℚ

  Prior beliefs over worlds (should sum to 1 for proper probability)

def Core.DecisionTheory.DecisionProblem.uniformPrior {W : Type u_1} [Fintype W] [DecidableEq W] : W → ℚ

A uniform prior over a Fintype of worlds

Equations

• Core.DecisionTheory.DecisionProblem.uniformPrior = if Fintype.card W = 0 then fun (x : W) => 0 else fun (x : W) => 1 / ↑(Fintype.card W)

def Core.DecisionTheory.DecisionProblem.withUniformPrior {W : Type u_1} {A : Type u_2} [Fintype W] [DecidableEq W] (utility : W → A → ℚ) : DecisionProblem W A

Create a decision problem with uniform prior

Equations

• Core.DecisionTheory.DecisionProblem.withUniformPrior utility = { utility := utility, prior := Core.DecisionTheory.DecisionProblem.uniformPrior }

Expected Utility

def Core.DecisionTheory.expectedUtility {W : Type u_1} {A : Type u_2} [Fintype W] [DecidableEq W] (dp : DecisionProblem W A) (a : A) : ℚ

Expected utility of action a given beliefs.

Equations

• Core.DecisionTheory.expectedUtility dp a = ∑ w : W, dp.prior w * dp.utility w a

def Core.DecisionTheory.dpValue {W : Type u_1} {A : Type u_2} [Fintype W] [DecidableEq W] (dp : DecisionProblem W A) (actions : Finset A) : ℚ

Value of a decision problem: max EU over actions, or 0 if empty.

Equations

• Core.DecisionTheory.dpValue dp actions = if h : actions.Nonempty then actions.sup' h (Core.DecisionTheory.expectedUtility dp) else 0

def Core.DecisionTheory.conditionalEU {W : Type u_1} {A : Type u_2} [DecidableEq W] (dp : DecisionProblem W A) (cell : Finset W) (a : A) : ℚ

Conditional expected utility of action a given cell membership.

Equations

• Core.DecisionTheory.conditionalEU dp cell a = if cell.sum dp.prior = 0 then 0 else ∑ w ∈ cell, dp.prior w / cell.sum dp.prior * dp.utility w a

def Core.DecisionTheory.valueAfterLearning {W : Type u_1} {A : Type u_2} [DecidableEq W] (dp : DecisionProblem W A) (actions : Finset A) (cell : Finset W) : ℚ

Value of decision problem after learning cell (best EU among actions)

Equations

• Core.DecisionTheory.valueAfterLearning dp actions cell = if h : actions.Nonempty then actions.sup' h (Core.DecisionTheory.conditionalEU dp cell) else 0

def Core.DecisionTheory.utilityValue {W : Type u_1} {A : Type u_2} [Fintype W] [DecidableEq W] (dp : DecisionProblem W A) (actions : Finset A) (cell : Finset W) : ℚ

UV(C) = V(D|C) - V(D), the utility value of learning proposition C.

Equations

• Core.DecisionTheory.utilityValue dp actions cell = Core.DecisionTheory.valueAfterLearning dp actions cell - Core.DecisionTheory.dpValue dp actions

def Core.DecisionTheory.cellProbability {W : Type u_1} {A : Type u_2} [DecidableEq W] (dp : DecisionProblem W A) (cell : Finset W) : ℚ

Probability of a cell in the partition

Equations

• Core.DecisionTheory.cellProbability dp cell = cell.sum dp.prior

Maximin

def Core.DecisionTheory.securityLevel {W : Type u_1} {A : Type u_2} (dp : DecisionProblem W A) (worlds : Finset W) (a : A) : ℚ

S(a) = min_w U(w, a), security level of action a.

Equations

• Core.DecisionTheory.securityLevel dp worlds a = if h : worlds.Nonempty then worlds.inf' h fun (w : W) => dp.utility w a else 0

def Core.DecisionTheory.maximinValue {W : Type u_1} {A : Type u_2} (dp : DecisionProblem W A) (worlds : Finset W) (actions : Finset A) : ℚ

MV = max_a min_w U(w, a), maximin value.

Equations

• Core.DecisionTheory.maximinValue dp worlds actions = if h : actions.Nonempty then actions.sup' h fun (a : A) => Core.DecisionTheory.securityLevel dp worlds a else 0

def Core.DecisionTheory.conditionalSecurityLevel {W : Type u_1} {A : Type u_2} [DecidableEq W] (dp : DecisionProblem W A) (worlds : Finset W) (a : A) (c : Finset W) : ℚ

Conditional security level: worst case within cell C

Equations

• Core.DecisionTheory.conditionalSecurityLevel dp worlds a c = Core.DecisionTheory.securityLevel dp (worlds ∩ c) a

def Core.DecisionTheory.maximinAfterLearning {W : Type u_1} {A : Type u_2} [DecidableEq W] (dp : DecisionProblem W A) (worlds : Finset W) (actions : Finset A) (c : Finset W) : ℚ

Maximin value after learning C

Equations

• Core.DecisionTheory.maximinAfterLearning dp worlds actions c = Core.DecisionTheory.maximinValue dp (worlds ∩ c) actions

def Core.DecisionTheory.maximinUtilityValue {W : Type u_1} {A : Type u_2} [DecidableEq W] (dp : DecisionProblem W A) (worlds : Finset W) (actions : Finset A) (c : Finset W) : ℚ

Maximin utility value of learning C

Equations

• Core.DecisionTheory.maximinUtilityValue dp worlds actions c = Core.DecisionTheory.maximinAfterLearning dp worlds actions c - Core.DecisionTheory.maximinValue dp worlds actions

Resolution

[vR03a] p. 736 resolution definition: information c resolves decision problem (dp, acts) iff some action in acts weakly dominates every other action on every world in c.

def Core.DecisionTheory.IsResolved {W : Type u_1} {A : Type u_2} (dp : DecisionProblem W A) (acts : Set A) (c : Set W) : Prop

c resolves decision problem (dp, acts): some action in acts weakly dominates every other action on every world in c. [vR03a] p. 736.

Equations

• Core.DecisionTheory.IsResolved dp acts c = ∃ a ∈ acts, ∀ b ∈ acts, ∀ w ∈ c, dp.utility w a ≥ dp.utility w b

@[implicit_reducible]

instance Core.DecisionTheory.IsResolved.instDecidable {W : Type u_1} {A : Type u_2} (dp : DecisionProblem W A) (acts : Set A) (c : Set W) [Fintype A] [DecidablePred fun (x : A) => x ∈ acts] [Fintype W] [DecidablePred fun (x : W) => x ∈ c] : Decidable (IsResolved dp acts c)

Decidability of IsResolved under finite, decidable carriers. The consumer-side prerequisite for decide-based evaluation (e.g., List.filter over candidate cells in worked study examples).

Equations

• Core.DecisionTheory.IsResolved.instDecidable dp acts c = id inferInstance

Question Utility

def Core.DecisionTheory.questionUtility {W : Type u_1} {A : Type u_2} [Fintype W] [DecidableEq W] [DecidableEq A] (dp : DecisionProblem W A) (actions : Finset A) (cells : Finset (Finset W)) : ℚ

EUV(Q) = Sum_{q in Q} P(q) * UV(q), expected utility value of question Q.

Equations

• Core.DecisionTheory.questionUtility dp actions cells = ∑ cell ∈ cells, Core.DecisionTheory.cellProbability dp cell * Core.DecisionTheory.utilityValue dp actions cell

def Core.DecisionTheory.questionMaximin {W : Type u_1} {A : Type u_2} [DecidableEq W] (dp : DecisionProblem W A) (worlds : Finset W) (actions : Finset A) (q : List (Finset W)) : ℚ

MV(Q) = min_{q in Q} MV(q), maximin question value.

Equations

• One or more equations did not get rendered due to their size.
• Core.DecisionTheory.questionMaximin dp worlds actions [] = 0

Value of Sample Information

noncomputable def Core.DecisionTheory.optimalAction {W : Type u_1} {A : Type u_2} [Fintype W] [DecidableEq W] (dp : DecisionProblem W A) (actions : Finset A) : Option A

Optimal action: the one with highest expected utility.

Noncomputable because it extracts a witness from an existential (Finset.exists_max_image via Classical.choice).

Equations

• Core.DecisionTheory.optimalAction dp actions = if h : actions.Nonempty then some ⋯.choose else none

noncomputable def Core.DecisionTheory.valueSampleInfo {W : Type u_1} {A : Type u_2} [Fintype W] [DecidableEq W] (dp : DecisionProblem W A) (actions : Finset A) (cell : Finset W) : ℚ

VSI(C) = V(D|C) - EU(a⁰|C): the value of sample information from learning proposition C, where a⁰ is the current optimal action.

Unlike UV(C) = V(D|C) - V(D), VSI is always non-negative: learning C before choosing can never hurt relative to the current best action applied within C. [vR03a], p. 742.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Core.DecisionTheory.expectedVSI {W : Type u_1} {A : Type u_2} [Fintype W] [DecidableEq W] (dp : DecisionProblem W A) (actions : Finset A) (cells : Finset (Finset W)) : ℚ

EVSI(Q) = Σ P(C) · VSI(C): the expected value of sample information from asking question Q. [vR03a], p. 742.

Equations

• Core.DecisionTheory.expectedVSI dp actions cells = ∑ cell ∈ cells, Core.DecisionTheory.cellProbability dp cell * Core.DecisionTheory.valueSampleInfo dp actions cell

EUV = EVSI

theorem Core.DecisionTheory.euv_eq_evsi {W : Type u_1} {A : Type u_2} [Fintype W] [DecidableEq W] [DecidableEq A] (dp : DecisionProblem W A) (actions : Finset A) (cells : Finset (Finset W)) (hLTE : ∀ (a : A), ∑ cell ∈ cells, cellProbability dp cell * conditionalEU dp cell a = expectedUtility dp a) (hSum : ∑ cell ∈ cells, cellProbability dp cell = 1) : questionUtility dp actions cells = expectedVSI dp actions cells

EUV(Q) = EVSI(Q): the expected utility value of a question equals its expected value of sample information.

[vR03a], p. 742: "The expected utility value of a question is equal to its expected value of sample information."

The two hypotheses are the law of total expectation (Σ P(C)·EU(a|C) = EU(a) for all actions) and cell probability normalization (Σ P(C) = 1).

Refinement monotonicity (Blackwell forward direction / [vR03a] §4.1)

[vR03a] p. 743 states that Q ⊑ Q' ↔ ∀ DP, EUV(Q) ≥ EUV(Q') is "a special case of [Bla53]". The ⟹ ("only if") direction is the data-processing / Jensen inequality: a finer question can only raise question utility. We prove it directly at the questionUtility level.

The mathematical core is the unnormalized cell value maxₐ ∑_{w∈c} P(w)·U(w,a), which equals P(c)·V(D|c) (cellProb_mul_valueAfterLearning_eq_uValue) and is superadditive under splitting a cell into disjoint pieces (uValue_union_le): the max of a sum is at most the sum of the maxes. Summed over a partition, this gives questionUtility (finer) ≥ questionUtility (coarser).

theorem Core.DecisionTheory.cellProb_valueAfterLearning_split_ge {W : Type u_1} {A : Type u_2} [DecidableEq W] (dp : DecisionProblem W A) (acts : Finset A) {c₁ c₂ : Finset W} (hdisj : Disjoint c₁ c₂) (hprior : ∀ (w : W), 0 ≤ dp.prior w) : cellProbability dp (c₁ ∪ c₂) * valueAfterLearning dp acts (c₁ ∪ c₂) ≤ cellProbability dp c₁ * valueAfterLearning dp acts c₁ + cellProbability dp c₂ * valueAfterLearning dp acts c₂

Splitting a cell never decreases its decision value: for disjoint cells c₁, c₂ and a nonnegative prior, P(c₁)·V(D|c₁) + P(c₂)·V(D|c₂) ≥ P(c₁ ∪ c₂)·V(D|c₁ ∪ c₂). This is [Bla53]'s data-processing inequality for a single binary refinement, the building block of [vR03a]'s §4.1 question-utility monotonicity (p. 743).

theorem Core.DecisionTheory.questionUtility_split_ge {W : Type u_1} {A : Type u_2} [Fintype W] [DecidableEq W] [DecidableEq A] (dp : DecisionProblem W A) (acts : Finset A) {c₁ c₂ : Finset W} (rest : Finset (Finset W)) (hdisj : Disjoint c₁ c₂) (hprior : ∀ (w : W), 0 ≤ dp.prior w) (hc₁ : c₁ ∉ rest) (hc₂ : c₂ ∉ rest) (hne12 : c₁ ≠ c₂) (hcrest : c₁ ∪ c₂ ∉ rest) : questionUtility dp acts (insert (c₁ ∪ c₂) rest) ≤ questionUtility dp acts (insert c₁ (insert c₂ rest))

Question utility rises under refinement (binary split) — the ⟹ ("only if") direction of [vR03a]'s §4.1 Fact (p. 743), in its elementary case. Splitting one cell c₁ ∪ c₂ of a question into the two disjoint cells c₁, c₂ can only increase the expected utility value EUV. This is the finite-partition instance of [Bla53]'s data-processing inequality; any finite refinement of one partition by another is a composition of such binary splits, so iterating gives the full §4.1 monotonicity.

General partition refinement

The binary questionUtility_split_ge lifts to an arbitrary refinement of one partition by another, via general superadditivity of uValue and a fiberwise regrouping. The refinement is presented by a map assign sending each finer cell to the coarser cell containing it, with each coarser cell the union (Finset.sup) of its fiber.

theorem Core.DecisionTheory.questionUtility_mono_of_refines {W : Type u_1} {A : Type u_2} [Fintype W] [DecidableEq W] [DecidableEq A] (dp : DecisionProblem W A) (acts : Finset A) {fine coarse : Finset (Finset W)} (assign : Finset W → Finset W) (hmaps : ∀ f ∈ fine, assign f ∈ coarse) (hcover : ∀ c ∈ coarse, c = {f ∈ fine | assign f = c}.sup id) (hdisj : ∀ f₁ ∈ fine, ∀ f₂ ∈ fine, f₁ ≠ f₂ → Disjoint f₁ f₂) (hprior : ∀ (w : W), 0 ≤ dp.prior w) : questionUtility dp acts coarse ≤ questionUtility dp acts fine

Question utility is monotone under partition refinement — the ⟹ direction of [vR03a]'s §4.1 Fact (p. 743), in full generality. A finer partition fine (presented as a refinement of coarse via assign, with each coarse cell the disjoint union of its fiber) has EUV ≥ the coarser one. By [Bla53]: post-processing the finer experiment cannot raise the convex value. Generalizes questionUtility_split_ge.

Maximin Monotonicity

Security level and maximin value are anti-monotone in the world set: restricting to a subset can only improve worst-case guarantees. These lemmas support the Blackwell maximin forward theorem.

theorem Core.DecisionTheory.securityLevel_le_utility {W : Type u_1} {A : Type u_2} (dp : DecisionProblem W A) (worlds : Finset W) (a : A) {w : W} (hw : w ∈ worlds) : securityLevel dp worlds a ≤ dp.utility w a

Security level is ≤ the utility of any world in the finset.

theorem Core.DecisionTheory.securityLevel_subset_ge {W : Type u_1} {A : Type u_2} (dp : DecisionProblem W A) (S₁ S₂ : Finset W) (a : A) (hne : S₁.Nonempty) (hsub : S₁ ⊆ S₂) : securityLevel dp S₁ a ≥ securityLevel dp S₂ a

Security level on a subset ≥ security level on the superset.

min over fewer elements ≥ min over more elements.

theorem Core.DecisionTheory.maximinValue_subset_ge {W : Type u_1} {A : Type u_2} (dp : DecisionProblem W A) (S₁ S₂ : Finset W) (actions : Finset A) (hne : S₁.Nonempty) (hsub : S₁ ⊆ S₂) : maximinValue dp S₁ actions ≥ maximinValue dp S₂ actions

Maximin value on a subset ≥ maximin value on the superset.

Since securityLevel increases on subsets (fewer worst cases), maximinValue (max over actions of security levels) also increases.

theorem Core.DecisionTheory.maximinUtilityValue_monotone_cell {W : Type u_1} {A : Type u_2} [DecidableEq W] (dp : DecisionProblem W A) (worlds : Finset W) (actions : Finset A) (c1 c2 : Finset W) (hSub : c1 ⊆ c2) (hNe : (worlds ∩ c1).Nonempty) : maximinUtilityValue dp worlds actions c1 ≥ maximinUtilityValue dp worlds actions c2

Maximin utility value is monotone under cell containment: learning a more specific proposition (subset of worlds) gives higher MUV.

theorem Core.DecisionTheory.maximinUtilityValue_nonneg {W : Type u_1} {A : Type u_2} [DecidableEq W] (dp : DecisionProblem W A) (worlds : Finset W) (actions : Finset A) (c : Finset W) (hNonempty : (worlds ∩ c).Nonempty) : maximinUtilityValue dp worlds actions c ≥ 0

Maximin value of information is non-negative for nonempty cells.

When the cell is nonempty, worlds ∩ c ⊆ worlds, and the maximin over a subset considers fewer worst cases, so maximinAfterLearning ≥ maximinValue.

theorem Core.DecisionTheory.le_foldl_min {α : Type u_1} (f : α → ℚ) (xs : List α) (init b : ℚ) (hinit : b ≤ init) (hxs : ∀ x ∈ xs, b ≤ f x) : b ≤ List.foldl (fun (m : ℚ) (x : α) => min m (f x)) init xs

A lower bound of all values is ≤ foldl min.

theorem Core.DecisionTheory.questionMaximin_le_muv {W : Type u_1} {A : Type u_2} [DecidableEq W] (dp : DecisionProblem W A) (worlds : Finset W) (actions : Finset A) (q : List (Finset W)) (cell : Finset W) (hcell : cell ∈ q) : questionMaximin dp worlds actions q ≤ maximinUtilityValue dp worlds actions cell

The question maximin value is ≤ MUV of each cell in the question.

Special Decision Problems

def Core.DecisionTheory.epistemicDP {W : Type u_1} {A : Type u_2} [DecidableEq W] (target : W) : DecisionProblem W A

An epistemic DP where the agent wants to know the exact world state.

Equations

• Core.DecisionTheory.epistemicDP target = { utility := fun (w : W) (x : A) => if (w == target) = true then 1 else 0, prior := fun (x : W) => 1 }

def Core.DecisionTheory.completeInformationDP {W : Type u_1} [DecidableEq W] : DecisionProblem W W

A complete-information DP where only exact-state knowledge is useful.

Equations

• Core.DecisionTheory.completeInformationDP = { utility := fun (w a : W) => if (a == w) = true then 1 else 0, prior := fun (x : W) => 1 }

def Core.DecisionTheory.mentionSomeDP {W : Type u_1} (satisfies : W → Bool) : DecisionProblem W Bool

A mention-some DP: any satisfier resolves the problem.

Equations

• Core.DecisionTheory.mentionSomeDP satisfies = { utility := fun (w : W) (a : Bool) => if (a && satisfies w) = true then 1 else 0, prior := fun (x : W) => 1 }

Binary Question Value Decomposition

For a binary partition [P, ¬P], the probability-weighted sum of conditional DP values equals Van Rooy's question utility plus the baseline DP value. This is the structural identity connecting "the value of asking a yes/no question" to the decision-theoretic question framework of [vR03a].

theorem Core.DecisionTheory.binary_cellProb_sum {W : Type u_1} {A : Type u_2} [Fintype W] [DecidableEq W] (dp : DecisionProblem W A) (P : W → Bool) (hPrior : Finset.univ.sum dp.prior = 1) : cellProbability dp {w : W | P w = true} + cellProbability dp {w : W | (!P w) = true} = 1

Cell probabilities of a binary partition [P, ¬P] sum to 1 when the prior is a proper distribution.

theorem Core.DecisionTheory.binary_question_value_decomposition {W : Type u_1} {A : Type u_2} [Fintype W] [DecidableEq W] [DecidableEq A] (dp : DecisionProblem W A) (actions : Finset A) (P : W → Bool) (hPrior : Finset.univ.sum dp.prior = 1) : have yesCell := {w : W | P w = true}; have noCell := {w : W | (!P w) = true}; cellProbability dp yesCell * valueAfterLearning dp actions yesCell + cellProbability dp noCell * valueAfterLearning dp actions noCell = questionUtility dp actions {yesCell, noCell} + dpValue dp actions

Binary question value decomposition: for a binary partition {P, ¬P},

Σ P(cell) · V(D|cell) = EUV({P,¬P}, D) + V(D)

where the LHS is the probability-weighted sum of conditional DP values, EUV is questionUtility, and V(D) is dpValue.

Answer and Question Orderings

[vR03a]'s relevance-based orderings on answers and questions.

def Core.DecisionTheory.moreRelevantAnswer {W : Type u_1} {A : Type u_2} [Fintype W] [DecidableEq W] [DecidableEq A] (dp : DecisionProblem W A) (actions : Finset A) (c d : Finset W) : Bool

C >_Q D: answer C is strictly more relevant than D given question Q.

Equations

• Core.DecisionTheory.moreRelevantAnswer dp actions c d = decide (Core.DecisionTheory.utilityValue dp actions c > Core.DecisionTheory.utilityValue dp actions d)

def Core.DecisionTheory.betterQuestion {W : Type u_1} {A : Type u_2} [Fintype W] [DecidableEq W] [DecidableEq A] (dp : DecisionProblem W A) (actions : Finset A) (q q' : Finset (Finset W)) : Bool

Q > Q': question Q is strictly better than Q'.

Equations

• Core.DecisionTheory.betterQuestion dp actions q q' = decide (Core.DecisionTheory.questionUtility dp actions q > Core.DecisionTheory.questionUtility dp actions q')