Questions/GSVanRooyBridge.lean #
@cite{blackwell-1953} @cite{groenendijk-stokhof-1984} @cite{van-rooy-2003}
Bridging Theorems between @cite{groenendijk-stokhof-1984} and @cite{van-rooy-2003}.
Overview #
G&S and Van Rooy approach question semantics from different angles:
- G&S: Partition semantics (equivalence relations on worlds)
- Van Rooy: Decision-theoretic semantics (questions resolve decision problems)
This file establishes the formal connections between these approaches.
Results #
- Blackwell's Theorem: Semantic refinement = pragmatic dominance
- Mention-Some Characterization: Decision-theoretic <-> goal-based licensing
- Pragmatic Answerhood <-> Utility: G&S's J-relative answerhood = positive UV
- Exhaustivity Characterization: When complete information is required
- Polar Question Optimality: PPQ/NPQ/Alt choice maximizes utility
Blackwell's Theorem #
The fundamental bridge: G&S's semantic refinement ordering on questions is exactly the universal pragmatic dominance ordering.
Q ⊑ Q' ⟺ ∀DP: EUV_DP(Q) ≥ EUV_DP(Q')
This is remarkable: the partition structure isn't arbitrary—it's the unique structure that respects decision-theoretic usefulness across ALL possible goals.
Proof sketch (→): If Q refines Q', its cells are subsets. More information can only help (or not hurt) any decision. By convexity of max.
Proof sketch (←): Contrapositive. If Q doesn't refine Q', find w,v that are Q-equivalent but Q'-inequivalent. Construct a DP where distinguishing w from v matters. Then Q' beats Q on this DP.
Blackwell's Theorem: Refinement implies dominance for expected utility.
If Q refines Q', then Q is at least as useful as Q' for ANY decision problem with non-negative priors. This is the "easy direction" of Blackwell.
Proved via QUD.questionUtility_refinement_ge from Core.Partition.
Blackwell's Theorem: Dominance implies refinement.
If Q dominates Q' for ALL decision problems (varying action type, action set, and utility function, with non-negative priors), then Q refines Q'.
The hypothesis must quantify over all action types A, not a fixed one:
with a fixed A of cardinality < 2, the hypothesis is vacuously true
(questionUtility with one action is partition-independent) but the
conclusion may be false.
Proved via three bridges: partitionValue_ge_of_questionUtility_ge converts
questionUtility ordering to partitionValue on Finset.univ;
partitionValue_restrict_support restricts to arbitrary worlds;
partitionValue_congr_on_worlds transfers between the zeroed-out DP
and the original.
Blackwell's Theorem (full characterization).
Semantic refinement ↔ universal pragmatic dominance (for non-negative priors). The RHS quantifies over ALL action types and action sets.
Blackwell forward direction for maximin: refinement implies maximin dominance.
The biconditional is FALSE with fixed action type A: if |A| < 2,
questionMaximin is partition-independent so dominance holds vacuously
but refinement may fail. Only the forward direction is correct for fixed A.
TODO: Each fine cell c' ⊆ c (coarse). The maximin over c' considers fewer worst cases → min over subset ≥ min over superset.
Mention-Some: G&S <-> Van Rooy #
G&S (Section 5): Mention-some is licensed by "human concerns"—practical goals where partial information suffices.
Van Rooy: Mention-some arises when multiple cells of the partition resolve the decision problem (i.e., make one action dominant).
Conjecture: These characterizations are equivalent.
The G&S "human concern" licensing corresponds exactly to the existence of a decision problem with the mention-some structure.
A decision problem has mention-some structure if multiple cells resolve it.
Van Rooy's characterization: mention-some <-> |resolving cells| > 1
Equations
- Semantics.Questions.Bridge.hasMentionSomeStructure dp worlds actions q = decide ((Core.DecisionTheory.resolvingAnswers dp worlds actions q).length > 1)
Instances For
Van Rooy's mention-some structure implies G&S mention-some is appropriate.
If a DP has multiple resolving cells, then mention-some answers are pragmatically appropriate (complete information is not required).
The canonical mention-some DP: "any satisfier achieves the goal".
This is the decision-theoretic encoding of G&S's "Where can I buy coffee?" The action is "go/don't go", utility is 1 iff you go to a coffee place.
Equations
- Semantics.Questions.Bridge.canonicalMentionSomeDP satisfies = Core.DecisionTheory.mentionSomeDP satisfies
Instances For
The canonical mention-some DP has mention-some structure.
For "Where can I buy coffee?", each coffee shop is a resolving cell.
Any mention-some interrogative with multiple satisfiers has mention-some structure.
This is the substantive bridge: when multiple entities satisfy the wh-restriction,
the canonical mention-some DP (go/don't-go with utility for reaching any satisfier)
has mention-some structure. This replaces the vacuous humanConcern_implies_mentionSomeDP
whose hypothesis (rfl) carried no content.
The key insight is that G&S's "human concern" licensing boils down to the existence of a satisfier-based DP with mention-some structure.
Question Utility Non-negativity from Blackwell #
Any QUD-derived question has non-negative questionUtility. This follows
from Blackwell: every QUD refines QUD.trivial (which has utility 0),
so by questionUtility_refinement_ge, the utility is ≥ 0.
This is the correct replacement for the false pragmatic answerhood ↔ utility
theorems that were here previously. Those theorems claimed an equivalence between
G&S's givesPragmaticAnswer and utilityValue for consistent DPs, but
utilityValue on an arbitrary Finset.filter doesn't connect to
givesPragmaticAnswer (which tests partition cell containment, not utility).
Question utility is non-negative for QUD-derived questions with proper priors.
Corollary of QUD.questionUtility_qud_nonneg proved in Core.Partition.
When is Exhaustive Information Required? #
G&S: Mention-all (exhaustive) reading is the default; mention-some requires special licensing.
Van Rooy: Exhaustive information is required when NO proper subset of cells resolves ALL relevant decision problems.
Conjecture: A question requires exhaustive answers iff the questioner's goal requires complete information to optimize.
A question requires exhaustive answers for a DP if only the complete partition resolves it (no single cell suffices).
Equations
- Semantics.Questions.Bridge.requiresExhaustive dp worlds actions q = List.all q fun (cell : W → Bool) => !Core.DecisionTheory.resolves dp worlds actions cell
Instances For
Mention-some DPs don't require exhaustive answers.
When any satisfier achieves the goal, partial answers work.
Polar Question Choice is Utility-Maximizing #
Van Rooy & Šafářová (2003): The choice between PPQ, NPQ, and Alt-Q depends on the relative utility of positive vs negative answers.
- PPQ (?p): Choose when UV(p) > UV(¬p)
- NPQ (?¬p): Choose when UV(¬p) > UV(p)
- Alt (?p∨¬p): Choose when UV(p) ≈ UV(¬p)
Conjecture: This choice rule is optimal—it maximizes expected communicative success given the speaker's goals.
Utility of positive answer exceeds negative.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Utility of negative answer exceeds positive.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Utilities are approximately equal.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Optimal question type given utility structure.
Equations
- One or more equations did not get rendered due to their size.
Instances For
PPQ is optimal when positive answer is more useful.
Van Rooy & Šafářová: Use PPQ (?p) when UV(p) > UV(¬p).
NPQ is optimal when negative answer is more useful.
Van Rooy & Šafářová: Use NPQ (?¬p) when UV(¬p) > UV(p).
Alt-Q is optimal when utilities are balanced.
Van Rooy & Šafářová: Use Alt (?p∨¬p) when UV(p) ≈ UV(¬p).
Refinement and Resolution #
A key property: if a coarser question resolves a decision problem, then any finer question also resolves it.
This follows from Blackwell but is useful to state directly.
A question resolves a DP if learning its answer determines optimal action.
Equations
- Semantics.Questions.Bridge.questionResolves dp worlds actions q = List.all q fun (cell : W → Bool) => Core.DecisionTheory.resolves dp worlds actions cell
Instances For
Helper: If some action dominates in a superset, it dominates in any subset.
Key lemma for refinement_preserves_resolution: if C resolves DP (some action dominates on C) and C' ⊆ C, then C' also resolves DP (same witness).
Refinement preserves resolution.
If Q resolves DP and Q' refines Q, then Q' also resolves DP. (More information never hurts.)
Exhaustivity is anti-monotone in refinement.
If Q' refines Q and Q' requires exhaustive answers (no fine cell resolves), then Q also requires exhaustive answers (no coarse cell resolves).
Proof idea: For each coarse cell c of Q, pick any fine cell c' ⊆ c (exists
by refinement). c' doesn't resolve (by hypothesis). By contrapositive of
resolves_subset (smaller doesn't resolve → bigger doesn't resolve), c
doesn't resolve either.
The converse is FALSE. Counterexample: W = {w1, w2}, actions = {a, b}, U(w1,a)=1, U(w1,b)=0, U(w2,a)=0, U(w2,b)=1. Coarse cell {w1,w2} doesn't resolve (neither dominates), but fine cells {w1}, {w2} each resolve.
Equations
- Semantics.Questions.Bridge.instDecidableEqExhW x✝ y✝ = if h : Semantics.Questions.Bridge.ExhW.ctorIdx✝ x✝ = Semantics.Questions.Bridge.ExhW.ctorIdx✝¹ y✝ then isTrue ⋯ else isFalse ⋯
Equations
- One or more equations did not get rendered due to their size.
Instances For
The trivial question resolves only trivial DPs.
If the trivial question (one cell = all worlds) resolves DP, the DP is trivial: some action dominates all others on all worlds.
The exact question resolves all DPs (with world-indexed actions).
The maximally fine partition always determines optimal action: in each singleton cell {wᵢ}, action wᵢ dominates all others (utility 1 vs 0).
Now correct after fixing resolves to existential.
The trivial question doesn't resolve the complete information DP.
When the goal is to know the exact world state, a single cell covering all worlds cannot resolve the DP: for any candidate action a, there exists w ≠ a with U(w, a) = 0 < 1 = U(w, w). Requires ≥2 distinct worlds.