[vR03a]: Questioning to Resolve Decision Problems

[GS84] [Kar77b] [ginzburg-1995] [Mer99] [Bla53]

Single-paper formalisation of [vR03a], "Questioning to Resolve Decision Problems", Linguistics and Philosophy 26.6: 727–763. The paper grounds question semantics in Bayesian decision theory: questions are evaluated by how their answers affect the optimal action in the questioner's decision problem.

Substrate identification

The decision-theoretic machinery — EU, UV, VSI, DecisionProblem — is already in Semantics/Questions/DecisionTheory.lean. Van Rooy's notation maps to the substrate as:

[vR03a]	substrate
EU(a) = ∑_w P(w) · U(a, w) (p. 733)	Core.DecisionTheory.expectedUtility
UV(Choose now) = max_a EU(a) (p. 734)	Core.DecisionTheory.dpValue
EU(a, C) = ∑_w P_C(w) · U(a, w) (p. 735)	Core.DecisionTheory.conditionalEU
UV(Learn C, choose later) = max_a EU(a, C)	Core.DecisionTheory.valueAfterLearning
UV(C) = UV(L C, c later) − UV(C now) (p. 735)	Core.DecisionTheory.utilityValue
UV*(C) = VSI(C) ≥ 0 (p. 735)	Core.DecisionTheory.valueSampleInfo
EUV(Q) = ∑_q P(q) · UV(q) (p. 742)	Core.DecisionTheory.questionUtility
Q ⊑ Q' (every Q-alt ⊆ some Q'-alt) (p. 741)	Question.questionEntails
C resolves DP (p. 736)	Core.DecisionTheory.IsResolved

What this file proves

• §3.1 Action-induced partition A* (p. 736-737): optimalityCell dp acts a and actionPartition.
• §3.1 C resolves DP (p. 736): the substrate's Core.DecisionTheory.IsResolved dp acts C — some action weakly dominates every other on every world in C.
• §3.1/§4.1 decision-relevance (IsDecisionRelevant): the qualitative, prior-free core of van Rooy's relevance — a question is completely irrelevant exactly when EUV(Q) = EVSI(Q) = 0, i.e. no answer changes the optimal action (p. 742). alts_resolve_distinct recasts a witness in the substrate's IsResolved vocabulary.
• §4.1 Blackwell Fact (p. 741, 743): "Q is more informative than Q'" is van Rooy's Q ⊑ Q'. Van Rooy's §4.1 theorem (p. 743, "a special case of [Bla53]") is the quantitative iff Q ⊑ Q' ↔ ∀ DP, EUV(Q) ≥ EUV(Q'), stated over partition cells as blackwell_euv_fact. Its ⟹ ("only if") direction — a finer partition weakly dominates a coarser one for every decision problem — is the data-processing inequality blackwell_euv_fact_forward (deriving the substrate refinement map from ⊑ and applying Core.DecisionTheory.questionUtility_mono_of_refines). The ⟸ direction is the [Bla53] converse, ProbabilityTheory.isGarblingOf_of_blackwellDominates (finite, kernel-level — now proved; the partition-cell bridge to questionUtility is the remaining Layer-2 work, so this direction is still sorry). decisionRelevance_preserved_under_cover is a separate, qualitative one-directional transfer (see its docstring).

What this file does NOT replicate

• The identification-question discussion (§2 (1)–(8)) requires named-individual / referential machinery beyond plain Set W; deferred.
• The underspecified meaning proposal (§5) requires a typed ambiguity-resolution layer beyond Question W; deferred.
• The Italian-newspaper mention-some example (§3.2 (12)) is the natural target for the next refinement; it is gs1984_mentionsome_italian_newspaper in Data.Examples.GroenendijkStokhof1984.

Provenance

The IsDecisionRelevant family and the decision-relevance preservation theorem were consolidated here from the former Semantics/Questions/DecisionTheoretic.lean (a single-paper formalisation that did not meet the theory-layer ≥2-Studies admission bar). The reusable substrate it relied on stays one layer down: Question.questionEntails/CoversAltsOf in Relevance.lean, the Core.DecisionTheory value vocabulary in DecisionTheory.lean.

§3.1 Action-induced partition A* (p. 736-737)

[vR03a] p. 736: "Notice that not only a question, but also the set of alternative actions, A, gives rise to a set of propositions. We can relate each action a ∈ A to the set of worlds in which there is no other action b in A that is strictly better. We will denote the proposition corresponding with a by a*".

def VanRooy2003.optimalityCell {W : Type u_1} {A : Type u_2} (dp : Core.DecisionTheory.DecisionProblem W A) (acts : Set A) (a : A) : Set W

The optimality cell of action a: the worlds where a strictly dominates every other action in acts.

[vR03a]'s a* (p. 736-737) is the weaker "no other action is strictly better" region; this strict version is van Rooy's partition condition (p. 737: "exactly one action a ∈ A such that ∀b ∈ A−{a}: U(a,w) > U(b,w)"), which is what makes actionPartition genuinely disjoint (optimalityCell_pairwise_disjoint).

Equations

• VanRooy2003.optimalityCell dp acts a = {w : W | ∀ b ∈ acts, b ≠ a → dp.utility w a > dp.utility w b}

def VanRooy2003.actionPartition {W : Type u_1} {A : Type u_2} (dp : Core.DecisionTheory.DecisionProblem W A) (acts : Set A) : Set (Set W)

The action-induced partition A*: the set of optimality cells. [vR03a] p. 736-737.

Equations

• VanRooy2003.actionPartition dp acts = VanRooy2003.optimalityCell dp acts '' acts

theorem VanRooy2003.optimalityCell_pairwise_disjoint {W : Type u_1} {A : Type u_2} (dp : Core.DecisionTheory.DecisionProblem W A) (acts : Set A) {a a' : A} (haa' : a ≠ a') (w : W) (hwa : w ∈ optimalityCell dp acts a) (hwa' : w ∈ optimalityCell dp acts a') (ha_acts : a ∈ acts) (ha'_acts : a' ∈ acts) : False

The optimality cells are pairwise disjoint: each world lies in at most one cell. (Page 737: "the set of propositions A* does in general not partition the state space, but it does when for each world w there is always exactly one action a ∈ A such that ∀b ∈ A−{a} : U(a,w) > U(b,w)".)

§3.1 C resolves DP (p. 736)

"We should say that information C resolves a decision problem if after learning C, one of the actions in A dominates all other actions, i.e., if in each resulting world no action has a higher utility than this one."

This is exactly Core.DecisionTheory.IsResolved dp acts C. We do not introduce a paper-vocabulary alias — consumers should use the substrate predicate directly.

§3.1/§4.1 Decision-relevance

A question is completely irrelevant exactly when EUV(Q) = EVSI(Q) = 0 — when no answer would change the agent's decision (p. 742). The qualitative core below exhibits a witness pair of answers that do change it.

def VanRooy2003.IsDecisionRelevant {W : Type u_1} {A : Type u_2} (Q : Question W) (dp : Core.DecisionTheory.DecisionProblem W A) (acts : Set A) : Prop

Q is decision-relevant to dp (relative to action set acts): there exist two nonempty alternatives p, p' ∈ alt Q and two actions a, a' such that a strictly dominates a' on every world of p while a' strictly dominates a on every world of p'. Learning which alternative obtains then shifts the optimal action.

This is the qualitative, prior-independent core of [vR03a]'s relevance: a question is completely irrelevant exactly when EUV(Q) = EVSI(Q) = 0, i.e. no answer changes the agent's decision (p. 742); IsDecisionRelevant exhibits a witness pair of answers that do change it. It is therefore a sufficient condition for EUV(Q) > 0 that holds for any prior assigning positive mass to both cells, and is strictly stronger than van Rooy's prior-weighted EUV(Q) > 0 / UV(C) > 0 relevance (pp. 735-736, 742).

The nonemptiness clauses rule out the degenerate Q = ⊥ case where the dominance conditions hold vacuously over empty witnesses.

Equations

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

theorem VanRooy2003.IsDecisionRelevant.alts_resolve_distinct {W : Type u_1} {A : Type u_2} {Q : Question W} {dp : Core.DecisionTheory.DecisionProblem W A} {acts : Set A} (h : IsDecisionRelevant Q dp acts) : ∃ p ∈ Q.alt, p.Nonempty ∧ ∃ p' ∈ Q.alt, p'.Nonempty ∧ ∃ a ∈ acts, ∃ a' ∈ acts, a ≠ a' ∧ Core.DecisionTheory.IsResolved dp {a, a'} p ∧ Core.DecisionTheory.IsResolved dp {a, a'} p'

A IsDecisionRelevant witness exhibits two Q-alts whose two-action restriction {a, a'} is IsResolved (p. 736) to distinct actions: on p, action a resolves (dp, {a, a'}); on p', a' does. So decision-relevance is precisely "two Q-alts resolve to distinct actions" in the substrate's IsResolved vocabulary.

theorem VanRooy2003.not_isDecisionRelevant_of_subsingleton_alt {W : Type u_1} {A : Type u_2} {Q : Question W} {dp : Core.DecisionTheory.DecisionProblem W A} {acts : Set A} (hSingle : ∀ (p p' : Set W), p ∈ Q.alt → p' ∈ Q.alt → p = p') : ¬IsDecisionRelevant Q dp acts

A question with at most one alternative is not decision-relevant: a single answer carries no decision value (EVSI = 0, p. 742).

§4.1 Question ordering (p. 741)

[vR03a] p. 741: "Q is a better question than Q' [...] In terms of [GS84] partition semantics this comes down to the natural requirement that for every element of Q there must be an element of Q' such that the former entails the latter, i.e., Q ⊑ Q':

Q ⊑ Q' iff ∀q ∈ Q : ∃q' ∈ Q' : q ⊆ q'."

This is exactly Question.questionEntails Q Q'. We do not introduce a paper-vocabulary alias — consumers should write questionEntails Q Q' (or use ≤ on Question W's lattice instance) directly. The relation is reflexive (questionEntails_refl) and transitive (questionEntails_trans).

§4.1 Decision-relevance preservation

theorem VanRooy2003.decisionRelevance_preserved_under_cover {W : Type u_1} {A : Type u_2} {Q Q' : Question W} (hCover : Q.CoversAltsOf Q') {dp : Core.DecisionTheory.DecisionProblem W A} {acts : Set A} (hQ' : IsDecisionRelevant Q' dp acts) : IsDecisionRelevant Q dp acts

Qualitative monotonicity of decision-relevance (substrate corollary in the spirit of [vR03a]'s §4.1 relevance ordering): when Q covers Q''s alternatives (CoversAltsOf), a decision-relevance witness for Q' lifts to one for Q.

This is not van Rooy's §4.1 Blackwell theorem itself. That theorem (p. 743, "a special case of [Bla53]") is the quantitative iff questionEntails Q Q' ↔ ∀ dp, EUV(Q) ≥ EUV(Q') over the expected utility value EUV (= substrate questionUtility, with EUV = EVSI available as euv_eq_evsi). The result here is a one-directional, prior-free Prop transfer over the dual condition CoversAltsOf: on a general inquisitive (non-partition) Question W, questionEntails (P-alts ⊆ Q-alts) does not transfer the qualitative witness, but its dual does. On partition questions the two coincide, recovering [vR03a]'s partition-based argument.

For the quantitative §4.1 Fact (p. 743), the EUV-monotonicity ("only if") direction is now Core.DecisionTheory.questionUtility_split_ge (a finer partition has EUV ≥ the coarser one, for every decision problem). The remaining gap to the full questionEntails-level iff is (i) a Question W → Finset (Finset W) partition-cell bridge via HasAltList, and (ii) the [Bla53] converse ProbabilityTheory.isGarblingOf_of_blackwellDominates.

§4.1 The Blackwell Fact (p. 743): partition-cell form

[vR03a] p. 743 states that Q ⊑ Q' ↔ ∀ DP, EUV(Q) ≥ EUV(Q') is "a special case of [Bla53]". We state it over [GS84] partition cells — the Finset (Finset W) that Core.DecisionTheory.questionUtility consumes. There, van Rooy's Q ⊑ Q' (p. 741: "∀ q ∈ Q : ∃ q' ∈ Q' : q ⊆ q'") is the cell-level refinement ∀ f ∈ fine, ∃ c ∈ coarse, f ⊆ c, and the value side ranges over every decision problem with a proper prior.

(The lift to the type-level Question.questionEntails/Question W is the remaining mechanical step: a HasAltList Q → Finset (Finset W) adapter via Set.Finite.toFinset, discharging questionEntails against this cell refinement.)

theorem VanRooy2003.blackwell_euv_fact_forward {W : Type u_1} {A : Type u_2} [Fintype W] [DecidableEq W] [DecidableEq A] {fine coarse : Finset (Finset W)} (hcoarse_disj : ∀ c₁ ∈ coarse, ∀ c₂ ∈ coarse, c₁ ≠ c₂ → Disjoint c₁ c₂) (hfine_disj : ∀ f₁ ∈ fine, ∀ f₂ ∈ fine, f₁ ≠ f₂ → Disjoint f₁ f₂) (hfine_cover : ∀ (w : W), ∃ f ∈ fine, w ∈ f) (href : ∀ f ∈ fine, ∃ c ∈ coarse, f ⊆ c) (dp : Core.DecisionTheory.DecisionProblem W A) (acts : Finset A) (hprior : ∀ (w : W), 0 ≤ dp.prior w) : Core.DecisionTheory.questionUtility dp acts coarse ≤ Core.DecisionTheory.questionUtility dp acts fine

[vR03a] §4.1 Fact, the ⟹ ("only if") direction (p. 743): a finer question is weakly better than a coarser one for every decision problem (the data-processing inequality). Van Rooy's refinement fine ⊑ coarse (each fine cell ⊆ some coarse cell, p. 741) plus the partition structure furnish the substrate refinement map — each fine cell's containing coarse cell — and Core.DecisionTheory.questionUtility_mono_of_refines concludes.

hfine_cover and the disjointness hypotheses encode that fine, coarse are genuine [GS84] partitions of the world set.

theorem VanRooy2003.blackwell_euv_fact {W : Type u_1} {A : Type u_2} [Fintype W] [DecidableEq W] [DecidableEq A] {fine coarse : Finset (Finset W)} (hfine_disj : ∀ f₁ ∈ fine, ∀ f₂ ∈ fine, f₁ ≠ f₂ → Disjoint f₁ f₂) (hcoarse_disj : ∀ c₁ ∈ coarse, ∀ c₂ ∈ coarse, c₁ ≠ c₂ → Disjoint c₁ c₂) (hfine_cover : ∀ (w : W), ∃ f ∈ fine, w ∈ f) : (∀ f ∈ fine, ∃ c ∈ coarse, f ⊆ c) ↔ ∀ (dp : Core.DecisionTheory.DecisionProblem W A) (acts : Finset A), (∀ (w : W), 0 ≤ dp.prior w) → Core.DecisionTheory.questionUtility dp acts coarse ≤ Core.DecisionTheory.questionUtility dp acts fine

[vR03a] §4.1 Fact (p. 743), partition-cell form. For two [GS84] partitions fine, coarse of the worlds, van Rooy's refinement order fine ⊑ coarse (every fine cell is contained in some coarse cell, p. 741) is equivalent to: the finer question has expected utility value ≥ the coarser one for every decision problem (with a proper, nonnegative prior). Van Rooy calls this "a special case of [Bla53]".

The ⟹ direction is blackwell_euv_fact_forward (the data-processing inequality). The ⟸ direction (EUV-dominance across all decision problems forces refinement) follows from the now-proved [Bla53] converse, ProbabilityTheory.isGarblingOf_of_blackwellDominates, once the partition-cell bridge is in place: the deterministic experiments of fine/coarse as Markov kernels, deterministic garbling ↔ refinement, and questionUtility ↔ bayesRisk. That bridge (Layer 2) is the remaining work; this direction stays sorry until it lands.