Documentation

Linglib.Phenomena.Questions.Studies.VanRooy2003

Van Rooy (2003): Questioning to Resolve Decision Problems #

@cite{van-rooy-2003}

Robert van Rooy. Questioning to Resolve Decision Problems. Linguistics and Philosophy 26(6): 727–763.

Key Contributions #

Van Rooy proposes that question interpretation is driven by the questioner's decision problem: the question is asked to help the questioner decide what to do. This yields:

Op(P)(w): The relevance-maximal groups of P-satisfiers in world w
⟦?xPx⟧^R: An underspecified question denotation that unifies mention-all and mention-some readings
>_Q ordering on answers: Relevance-based answer preference
Q > Q' ordering on questions: When one question is better than another
Domain selection: The wh-domain contains exactly decision-relevant individuals
Scalar questions: Preference-based orderings not reducible to entailment

Connection to G&S #

Van Rooy's theory extends Groenendijk & Stokhof's partition semantics. G&S's exhaustive partition is the limiting case when the questioner's decision problem requires complete information. Van Rooy shows that when partial information suffices, the question denotation naturally produces mention-some readings.

Connection to Existing Infrastructure #

Core.Agent.DecisionTheory: Decision problems, EUV, VSI, question utility
Theories.Semantics.Questions.Partition: G&S partition semantics
Theories.Semantics.Questions.MentionSome: G&S mention-some (§5)
Theories.Semantics.Questions.GSVanRooyBridge: Blackwell's theorem

Examples #

Italian Newspaper Example #

@cite{van-rooy-2003}, p. 739, 753–754: "Where can I buy an Italian newspaper?"

The questioner wants to buy an Italian newspaper. Any shop that sells one suffices. Op(P)(w) = {{s} : sells-Italian(s)(w)}, making each shop a separate answer. The question gets a mention-some reading.

inductive Phenomena.Questions.Studies.VanRooy2003.NewspaperWorld :

Worlds for the Italian newspaper scenario: which shops sell Italian papers.

shopA_only : NewspaperWorld
shopB_only : NewspaperWorld
both : NewspaperWorld

Instances For

instance Phenomena.Questions.Studies.VanRooy2003.instDecidableEqNewspaperWorld :

DecidableEq NewspaperWorld

Equations

Phenomena.Questions.Studies.VanRooy2003.instDecidableEqNewspaperWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Questions.Studies.VanRooy2003.instBEqNewspaperWorld :

BEq NewspaperWorld

Equations

Phenomena.Questions.Studies.VanRooy2003.instBEqNewspaperWorld = { beq := Phenomena.Questions.Studies.VanRooy2003.instBEqNewspaperWorld.beq }

def Phenomena.Questions.Studies.VanRooy2003.instBEqNewspaperWorld.beq :

NewspaperWorld → NewspaperWorld → Bool

Equations

Phenomena.Questions.Studies.VanRooy2003.instBEqNewspaperWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Phenomena.Questions.Studies.VanRooy2003.instReprNewspaperWorld :

Repr NewspaperWorld

Equations

Phenomena.Questions.Studies.VanRooy2003.instReprNewspaperWorld = { reprPrec := Phenomena.Questions.Studies.VanRooy2003.instReprNewspaperWorld.repr }

def Phenomena.Questions.Studies.VanRooy2003.instReprNewspaperWorld.repr :

NewspaperWorld → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Questions.Studies.VanRooy2003.instLawfulBEqNewspaperWorld :

LawfulBEq NewspaperWorld

instance Phenomena.Questions.Studies.VanRooy2003.instFintypeNewspaperWorld :

Fintype NewspaperWorld

Equations

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

inductive Phenomena.Questions.Studies.VanRooy2003.Shop :

Shops in the domain.

A : Shop
B : Shop

Instances For

instance Phenomena.Questions.Studies.VanRooy2003.instDecidableEqShop :

DecidableEq Shop

Equations

Phenomena.Questions.Studies.VanRooy2003.instDecidableEqShop x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Questions.Studies.VanRooy2003.instBEqShop.beq :

Shop → Shop → Bool

Equations

Phenomena.Questions.Studies.VanRooy2003.instBEqShop.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Phenomena.Questions.Studies.VanRooy2003.instBEqShop :

Equations

Phenomena.Questions.Studies.VanRooy2003.instBEqShop = { beq := Phenomena.Questions.Studies.VanRooy2003.instBEqShop.beq }

def Phenomena.Questions.Studies.VanRooy2003.instReprShop.repr :

Shop → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Questions.Studies.VanRooy2003.instReprShop :

Equations

Phenomena.Questions.Studies.VanRooy2003.instReprShop = { reprPrec := Phenomena.Questions.Studies.VanRooy2003.instReprShop.repr }

def Phenomena.Questions.Studies.VanRooy2003.sellsItalian :

NewspaperWorld → Shop → Bool

"x sells Italian newspapers" in world w.

Equations

Instances For

def Phenomena.Questions.Studies.VanRooy2003.newspaperRelevance :

Theories.Semantics.Questions.Relevance.RelevanceFunction NewspaperWorld Shop

Mention-some relevance for the newspaper scenario.

Equations

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

Instances For

def Phenomena.Questions.Studies.VanRooy2003.newspaperQuestion :

Core.DecisionTheory.Question NewspaperWorld

The underspecified denotation produces mention-some answers: "Shop A sells Italian papers" and "Shop B sells Italian papers." In the both-world, both answers are true.

Equations

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

Instances For

theorem Phenomena.Questions.Studies.VanRooy2003.newspaper_has_two_cells :

List.length newspaperQuestion = 2

The newspaper question has exactly 2 cells (one per shop).

theorem Phenomena.Questions.Studies.VanRooy2003.newspaper_shopA_only_resolved :

(List.filter (fun (x : NewspaperWorld → Bool) => x NewspaperWorld.shopA_only) newspaperQuestion).length = 1

In the shopA_only world, only the "Shop A" answer is true.

theorem Phenomena.Questions.Studies.VanRooy2003.newspaper_both_world_two_true :

(List.filter (fun (x : NewspaperWorld → Bool) => x NewspaperWorld.both) newspaperQuestion).length = 2

In the both world, both answers are true — either suffices.

def Phenomena.Questions.Studies.VanRooy2003.newspaperDP :

Core.DecisionTheory.DecisionProblem NewspaperWorld Shop

The newspaper scenario decision problem: go to shop A or shop B. Utility 1 if you go to a shop that sells Italian papers, 0 otherwise.

Equations

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

Instances For

The newspaper DP has mention-some structure: both cells resolve it.

"Where do you live?" Example #

@cite{van-rooy-2003}, p. 754–755: "Where do you live?"

The granularity of the answer depends on the decision problem:

Taxi driver: needs exact address
Census worker: needs city/state
Casual conversation: city suffices

This is modeled by different decision problems inducing different optimal partitions.

inductive Phenomena.Questions.Studies.VanRooy2003.Granularity :

Granularity levels for the "where do you live" example.

city : Granularity
district : Granularity
address : Granularity

Instances For

instance Phenomena.Questions.Studies.VanRooy2003.instDecidableEqGranularity :

DecidableEq Granularity

Equations

Phenomena.Questions.Studies.VanRooy2003.instDecidableEqGranularity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Questions.Studies.VanRooy2003.instBEqGranularity :

BEq Granularity

Equations

Phenomena.Questions.Studies.VanRooy2003.instBEqGranularity = { beq := Phenomena.Questions.Studies.VanRooy2003.instBEqGranularity.beq }

def Phenomena.Questions.Studies.VanRooy2003.instBEqGranularity.beq :

Granularity → Granularity → Bool

Equations

Phenomena.Questions.Studies.VanRooy2003.instBEqGranularity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Phenomena.Questions.Studies.VanRooy2003.instReprGranularity :

Repr Granularity

Equations

Phenomena.Questions.Studies.VanRooy2003.instReprGranularity = { reprPrec := Phenomena.Questions.Studies.VanRooy2003.instReprGranularity.repr }

def Phenomena.Questions.Studies.VanRooy2003.instReprGranularity.repr :

Granularity → ℕ → Std.Format

Equations

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

Instances For

structure Phenomena.Questions.Studies.VanRooy2003.GranularityDatum :

Different decision problems require different granularity. The required granularity determines the question interpretation.

asker : String
Who is asking?
decisionProblem : String
What decision problem do they face?
requiredGranularity : Granularity
What granularity is needed?
question : String
Natural language form of the question

Instances For

def Phenomena.Questions.Studies.VanRooy2003.instReprGranularityDatum.repr :

GranularityDatum → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Questions.Studies.VanRooy2003.instReprGranularityDatum :

Repr GranularityDatum

Equations

Phenomena.Questions.Studies.VanRooy2003.instReprGranularityDatum = { reprPrec := Phenomena.Questions.Studies.VanRooy2003.instReprGranularityDatum.repr }

def Phenomena.Questions.Studies.VanRooy2003.taxiDriver :

GranularityDatum

Equations

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

Instances For

def Phenomena.Questions.Studies.VanRooy2003.censusWorker :

GranularityDatum

Equations

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

Instances For

def Phenomena.Questions.Studies.VanRooy2003.casualConversation :

GranularityDatum

Equations

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

Instances For

def Phenomena.Questions.Studies.VanRooy2003.granularityExamples :

List GranularityDatum

Equations

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

Instances For

theorem Phenomena.Questions.Studies.VanRooy2003.granularity_varies :

(taxiDriver.requiredGranularity != censusWorker.requiredGranularity) = true ∧ (censusWorker.requiredGranularity != casualConversation.requiredGranularity) = true

Different askers need different granularity.

The Beatle Hierarchy: Scalar Questions #

@cite{van-rooy-2003}, p. 759–760: "Which Beatle records do you have?"

Consider a collector who values Beatles records differently: John > Paul > George > Ringo

The questioner (a record shop owner) wants to sell records. The ordering on answers is preference-based, not entailment-based: knowing the collector has John records is more useful than knowing they have Ringo records (because John records are more valuable to sell).

This shows that Van Rooy's relevance ordering goes beyond standard partition refinement: it can produce scale-like orderings that don't reduce to set-containment/entailment.

inductive Phenomena.Questions.Studies.VanRooy2003.Beatle :

Beatles for the collector example.

john : Beatle
paul : Beatle
george : Beatle
ringo : Beatle

Instances For

instance Phenomena.Questions.Studies.VanRooy2003.instDecidableEqBeatle :

DecidableEq Beatle

Equations

Phenomena.Questions.Studies.VanRooy2003.instDecidableEqBeatle x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Questions.Studies.VanRooy2003.instBEqBeatle :

Equations

Phenomena.Questions.Studies.VanRooy2003.instBEqBeatle = { beq := Phenomena.Questions.Studies.VanRooy2003.instBEqBeatle.beq }

def Phenomena.Questions.Studies.VanRooy2003.instBEqBeatle.beq :

Beatle → Beatle → Bool

Equations

Phenomena.Questions.Studies.VanRooy2003.instBEqBeatle.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

def Phenomena.Questions.Studies.VanRooy2003.instReprBeatle.repr :

Beatle → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Questions.Studies.VanRooy2003.instReprBeatle :

Equations

Phenomena.Questions.Studies.VanRooy2003.instReprBeatle = { reprPrec := Phenomena.Questions.Studies.VanRooy2003.instReprBeatle.repr }

def Phenomena.Questions.Studies.VanRooy2003.beatleValue :

Preference ranking over Beatles records (higher = more valuable).

Equations

Instances For

inductive Phenomena.Questions.Studies.VanRooy2003.BeatleWorld :

Worlds: which Beatle's records the collector has. Simplified to single-record worlds.

hasJohn : BeatleWorld
hasPaul : BeatleWorld
hasGeorge : BeatleWorld
hasRingo : BeatleWorld

Instances For

instance Phenomena.Questions.Studies.VanRooy2003.instDecidableEqBeatleWorld :

DecidableEq BeatleWorld

Equations

Phenomena.Questions.Studies.VanRooy2003.instDecidableEqBeatleWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Questions.Studies.VanRooy2003.instBEqBeatleWorld.beq :

BeatleWorld → BeatleWorld → Bool

Equations

Phenomena.Questions.Studies.VanRooy2003.instBEqBeatleWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Phenomena.Questions.Studies.VanRooy2003.instBEqBeatleWorld :

BEq BeatleWorld

Equations

Phenomena.Questions.Studies.VanRooy2003.instBEqBeatleWorld = { beq := Phenomena.Questions.Studies.VanRooy2003.instBEqBeatleWorld.beq }

def Phenomena.Questions.Studies.VanRooy2003.instReprBeatleWorld.repr :

BeatleWorld → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Questions.Studies.VanRooy2003.instReprBeatleWorld :

Repr BeatleWorld

Equations

Phenomena.Questions.Studies.VanRooy2003.instReprBeatleWorld = { reprPrec := Phenomena.Questions.Studies.VanRooy2003.instReprBeatleWorld.repr }

instance Phenomena.Questions.Studies.VanRooy2003.instFintypeBeatleWorld :

Fintype BeatleWorld

Equations

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

def Phenomena.Questions.Studies.VanRooy2003.collectorHas :

BeatleWorld → Beatle

Which Beatle the collector has in each world.

Equations

Instances For

def Phenomena.Questions.Studies.VanRooy2003.recordShopDP :

Core.DecisionTheory.DecisionProblem BeatleWorld Beatle

The record shop DP: utility of selling Beatle b's records to the collector. Utility equals the value of the Beatle if the collector actually has that Beatle's records (and thus would want related merchandise).

Equations

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

Instances For

Learning "has John" is more useful than "has Ringo" for the record shop.

This is the scalar ordering: UV({hasJohn}) > UV({hasRingo}).

theorem Phenomena.Questions.Studies.VanRooy2003.beatle_utility_ordering :

have uv := fun (w : BeatleWorld) => Core.DecisionTheory.utilityValue recordShopDP {Beatle.john , Beatle.paul , Beatle.george , Beatle.ringo } {x : BeatleWorld | (x == w) = true}; uv BeatleWorld.hasJohn > uv BeatleWorld.hasPaul ∧ uv BeatleWorld.hasPaul > uv BeatleWorld.hasGeorge ∧ uv BeatleWorld.hasGeorge > uv BeatleWorld.hasRingo

The full scalar ordering: John > Paul > George > Ringo in utility value.

Domain Selection #

@cite{van-rooy-2003}, §4.2 (p. 745–746): The wh-domain of a question contains exactly those individuals that are decision-relevant. An individual d is decision-relevant if knowing whether P(d) holds has positive expected utility value.

This explains why "Where can I buy an Italian newspaper?" doesn't range over non-shops (e.g., hospitals, parks): those locations have zero utility value for the buy-newspaper decision problem.

In the newspaper example, both shops are decision-relevant.

Summary Theorems #

Structural properties connecting the examples back to the core theory.

theorem Phenomena.Questions.Studies.VanRooy2003.mentionSome_from_goal_dp :

have worlds := {NewspaperWorld.shopA_only , NewspaperWorld.shopB_only , NewspaperWorld.both }; have q := [fun (w : NewspaperWorld) => sellsItalian w Shop.A, fun (w : NewspaperWorld) => sellsItalian w Shop.B]; Core.DecisionTheory.isMentionSome newspaperDP worlds {Shop.A , Shop.B } q = true

Mention-some reading arises when the decision problem is goal-directed: any satisfier achieves the goal. This connects Van Rooy's Op(P) analysis to the isMentionSome predicate from Core.Agent.DecisionTheory.

We use the newspaper DP directly (not mentionSomeDP which takes a unary predicate). The newspaper DP has utility 1 for going to a shop that sells Italian papers, so each shop-cell resolves it.

theorem Phenomena.Questions.Studies.VanRooy2003.mentionAll_from_complete_dp :

have dp := Core.DecisionTheory.completeInformationDP; have worlds := {NewspaperWorld.shopA_only , NewspaperWorld.shopB_only , NewspaperWorld.both }; have q := [fun (w : NewspaperWorld) => sellsItalian w Shop.A, fun (w : NewspaperWorld) => sellsItalian w Shop.B]; Core.DecisionTheory.isMentionAll dp worlds {NewspaperWorld.shopA_only , NewspaperWorld.shopB_only , NewspaperWorld.both } q = true

Mention-all reading arises when the decision problem requires complete information (e.g., the complete information DP).

theorem Phenomena.Questions.Studies.VanRooy2003.newspaper_question_has_value :

Core.DecisionTheory.questionUtility newspaperDP {Shop.A , Shop.B } (Core.DecisionTheory.questionToFinset [fun (w : NewspaperWorld) => sellsItalian w Shop.A, fun (w : NewspaperWorld) => sellsItalian w Shop.B]) > 0

The newspaper question utility is positive: asking is worthwhile.

Resolution–Value Saturation #

The deepest mathematical connection between @cite{van-rooy-2003} and @cite{groenendijk-stokhof-1984}: resolution of a question by a decision problem implies value saturation — the question extracts all decision-relevant information, and coarsening from the G&S partition to Van Rooy's underspecified denotation is decision-theoretically free.

The algebraic heart #

Blackwell's theorem (proved in Core.Partition) uses sub-additivity of max:

max_a [Σ_w f(w,a)] ≤ Σ_w [max_a f(w,a)]

This gives: finer partitions have higher partitionValue. But the inequality can be tight: if cell C has a dominant action a_dom (∀b, ∀w∈C: U(w,a_dom) ≥ U(w,b)), then a_dom achieves the pointwise maximum at every world, so max-of-sums = sum-of-maxes:

max_a [Σ_{w∈C} π(w)·U(w,a)]
  ≥ Σ_{w∈C} π(w)·U(w,a_dom)          — choosing a = a_dom
  = Σ_{w∈C} π(w)·max_b U(w,b)         — a_dom achieves max at each w
  = Σ_{w∈C} [max_a π(w)·U(w,a)]       — when π ≥ 0
  ≥ max_a [Σ_{w∈C} π(w)·U(w,a)]       — sub-additivity (Blackwell)

The squeeze gives equality. Summing over cells:

partitionValue(Q) = partitionValue(Q_exact)

Resolution is exactly when Blackwell's sub-additivity inequality is tight at every cell. This characterizes the "plateau" in the Blackwell ordering: all resolving partitions achieve the same maximal value.

Connection to Van Rooy's underspecified denotation #

Van Rooy's ⟦?xPx⟧^R with mention-some relevance produces cells that each resolve the questioner's DP. So the coarsening from G&S's three-cell partition (only-A, only-B, both) to Van Rooy's two-cell denotation (A-sells, B-sells) is decision-theoretically free: no information of value to the questioner is lost.

This is the formal sense in which "Where can I buy an Italian newspaper?" need only mention one shop.

The G&S partition for the newspaper scenario #

def Phenomena.Questions.Studies.VanRooy2003.newspaperGS :

QUD NewspaperWorld

The G&S partition for "where can I buy an Italian newspaper?": two worlds are equivalent iff they have the same extension for "sells Italian newspapers." This gives three cells: {shopA_only}, {shopB_only}, {both}.

Equations

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

Instances For

def Phenomena.Questions.Studies.VanRooy2003.newspaperMS_A :

QUD NewspaperWorld

The mention-some partition: two worlds are equivalent iff they give the same answer to "does SOME shop sell Italian newspapers?" This gives two cells: {shopA_only, shopB_only, both} vs ∅ (but all our worlds have a satisfier, so there's just one cell — trivial partition).

For a non-trivial mention-some partition, we use a coarser grouping: worlds are equivalent iff they agree on whether shop A sells. This gives two cells: {shopA_only, both} and {shopB_only}.

Equations

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

Instances For

def Phenomena.Questions.Studies.VanRooy2003.newspaperMS_B :

QUD NewspaperWorld

The mention-some partition based on shop B.

Equations

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

Instances For

Value saturation: concrete verification #

The G&S partition (3 cells) and the mention-some-A partition (2 cells) achieve the same partitionValue for the newspaper DP.

This is the concrete instance of value saturation: coarsening from the exhaustive partition to the mention-some partition loses nothing, because both resolve the DP.

Same for the shop-B mention-some partition.

Both mention-some partitions achieve the same value as the exact (identity) partition. This is the full value saturation: even the coarsest resolving partition extracts all decision-relevant information.

Verification: the G&S partition also equals the exact partition's value. (Follows from the previous two, but verified independently.)

Value saturation FAILS for the complete-information DP #

For the complete-information DP (where knowing the exact world matters), the mention-some partition achieves STRICTLY LESS value than the G&S partition. Coarsening is no longer free — information is lost.

The underspecified denotation achieves value saturation #

def Phenomena.Questions.Studies.VanRooy2003.newspaperUnderspecCells :

Core.DecisionTheory.Question NewspaperWorld

The cells of the underspecified denotation for the newspaper scenario.

Equations

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

Instances For

theorem Phenomena.Questions.Studies.VanRooy2003.underspecified_all_cells_resolve :

List.all newspaperUnderspecCells (Core.DecisionTheory.resolves newspaperDP {NewspaperWorld.shopA_only , NewspaperWorld.shopB_only , NewspaperWorld.both } {Shop.A , Shop.B }) = true

Every cell of the underspecified denotation (mention-some relevance) resolves the newspaper DP: after learning any answer, the questioner can act optimally.

This is the bridge from Van Rooy's Op(P) construction to value saturation: Op(P) produces cells → cells resolve → value is saturated.

The General Theorem #

The concrete verifications above are instances of a general principle. We state it here; the proof combines Blackwell (one direction) with the resolution lower bound (the other direction).

theorem Phenomena.Questions.Studies.VanRooy2003.resolution_value_saturation {W : Type u_1} [Fintype W] [DecidableEq W] {A : Type u_2} [DecidableEq A] (dp : Core.DecisionTheory.DecisionProblem W A) (q : QUD W) (actions : Finset A) (hResolves : ∀ cell ∈ q.toCellsFinset Finset.univ, ∃ a ∈ actions, ∀ b ∈ actions, ∀ w ∈ cell, dp.utility w a ≥ dp.utility w b) (hPrior : ∀ (w : W), dp.prior w ≥ 0) :

QUD.partitionValue dp q Finset.univ actions = QUD.partitionValue dp QUD.exact Finset.univ actions

Resolution–Value Saturation Theorem (general form).

For a decision problem D with non-negative priors and utilities, and a partition Q where every cell resolves D:

partitionValue(Q, D) = partitionValue(Q_exact, D)

Resolution marks the plateau in the Blackwell ordering: all resolving partitions achieve the maximal value, regardless of their granularity.

Proof sketch (both directions):

(≤) Blackwell: Q_exact refines Q, so partitionValue(Q_exact) ≥ partitionValue(Q).

(≥) For each cell C of Q with dominant action a_dom:

max_a [Σ_{w∈C} π(w)·U(w,a)] ≥ Σ_{w∈C} π(w)·U(w,a_dom) (choosing a_dom)
= Σ_{w∈C} π(w)·max_b U(w,b) (a_dom achieves max at every w)
= Σ_{w∈C} max_a [π(w)·U(w,a)] (when π ≥ 0, U ≥ 0)
Summing over cells: partitionValue(Q) ≥ partitionValue(Q_exact)

Combined: equality.

Delegates to QUD.resolution_value_eq_exact (proved in Core.Partition).

Corollary: For a mention-some DP, the underspecified denotation (coarsened to a partition) achieves the same value as the full G&S partition. The mention-some question is decision-theoretically equivalent to the mention-all question.

This is the mathematical core of Van Rooy's theory: the partition structure of a question should match the decision problem's resolution structure, and coarser-than-necessary partitions that still resolve lose nothing.