The Identity Decision Problem

The identity DP is the decision problem where:

• Actions = Worlds (choosing which world you "guess" is true)
• Utility = 1 if your guess matches the actual world, 0 otherwise

This encodes pure epistemic accuracy: the agent wants to know the truth.

Under the identity DP, decision-theoretic utility equals epistemic utility (log-likelihood). RSA is "decision-theoretic" even though it maximizes informativity.

def Comparisons.Relevance.identityDP {W : Type u_1} [DecidableEq W] (_worlds : List W) (prior : W → ℚ := fun (x : W) => 1) : Core.DecisionTheory.DecisionProblem W W

The identity decision problem: actions = worlds, utility = accuracy.

This is the "canonical epistemic DP" where the agent's goal is pure accuracy. Choosing action w is equivalent to guessing "the true world is w".

D_identity = ⟨W, W, U, π⟩ where U(w, a) = 1 if a = w, else 0

Equations

• Comparisons.Relevance.identityDP _worlds prior = { utility := fun (w a : W) => if (a == w) = true then 1 else 0, prior := prior }

theorem Comparisons.Relevance.identityDP_value_is_max_posterior {W : Type u_1} [Fintype W] [DecidableEq W] (worlds : List W) (posterior : W → ℚ) (hNonneg : ∀ w ∈ worlds, posterior w ≥ 0) : Core.DecisionTheory.dpValue (identityDP worlds posterior) worlds.toFinset ≥ 0

Under the identity DP, the DP value is non-negative for non-negative priors.

dpValue = posterior(optimal action) ≥ 0 since the optimal action is chosen from worlds and all posteriors in worlds are non-negative.

theorem Comparisons.Relevance.identityDP_questionUtility_nonneg {W : Type u_1} [Fintype W] [DecidableEq W] (q : QUD W) (hsum : ∑ x : W, 1 = 1) : Core.DecisionTheory.questionUtility (identityDP Finset.univ.val.toList) Finset.univ (q.toCellsFinset Finset.univ) ≥ 0

Per-cell utility value can be negative: utilityValue for a single cell is max_a E[U|C] − max_a E[U], and the conditional optimum can be worse than the unconditional optimum.

The correct non-negativity result is at the partition level: expected UV across all cells of a partition is ≥ 0. This is questionUtility_nonneg_from_blackwell in GSVanRooyBridge.lean, which follows from Blackwell's theorem (every partition refines the trivial partition).

Theorem 1: Epistemic as Decision-Theoretic

Sumers et al. Theorem 1: There exists a decision problem D₀ such that decision-theoretic utility equals epistemic utility (log-likelihood).

Under the identity DP with appropriate parameterization, maximizing decision-theoretic utility is equivalent to maximizing informativity in the RSA sense. RSA's "epistemic" speaker is a decision-theoretic speaker with the identity decision problem. Accuracy is itself a decision problem.

theorem Comparisons.Relevance.epistemic_is_decision_theoretic {W : Type u_1} [DecidableEq W] (worlds : List W) (_hNe : worlds.length > 0) : ∃ (dp : Core.DecisionTheory.DecisionProblem W W), ∀ (posterior : W → ℚ), ∀ w ∈ worlds, posterior w > 0 → dp.utility w w = 1

Theorem 1: Epistemic utility is decision-theoretic utility.

RSA's speaker utility (log P_L(w|u)) can be recovered from decision-theoretic utility under the identity DP. This unifies RSA with game-theoretic/ decision-theoretic pragmatics.

theorem Comparisons.Relevance.rsa_speaker_is_dt_optimal {W : Type u_1} [DecidableEq W] (worlds : List W) : have dp := identityDP worlds; ∀ (w : W), dp.utility w w = 1

Corollary: RSA speaker IS a decision-theoretic agent.

The RSA speaker maximizes expected utility under the identity DP. RSA is optimal communication for accuracy goals.

Truthfulness as Limit

The identity QUD (pure truthfulness) emerges as the limit when we marginalize over all possible decision problems with a uniform prior over DPs.

• Specific DPs care about specific distinctions (e.g., "is it raining?")
• When we do not know the DP, we must communicate information useful for any DP
• The only universally useful information is accurate information about the world
• Thus: E_DP[U_DT(u|w, DP)] = U_truthfulness(u|w) as DP→uniform

Epistemic utility is the decision-theoretic utility that is robust across all possible goals.

theorem Comparisons.Relevance.truthfulness_from_marginalization {W : Type u_1} [DecidableEq W] (worlds : List W) : have dp := identityDP worlds; ∀ w ∈ worlds, dp.utility w w = 1 ∧ ∀ w' ∈ worlds, w' ≠ w → dp.utility w w' = 0

When marginalizing over all DPs with uniform prior, we recover truthfulness.

Formally: The identity DP is the "Bayesian aggregation" of all possible DPs.

theorem Comparisons.Relevance.identity_qud_is_finest {W : Type u_1} [DecidableEq W] (q : Semantics.Questions.GSQuestion W) : QUD.refines Semantics.Questions.GSQuestion.exact q

Blackwell's theorem explains why this works.

Since Q ⊑ Q' iff ∀DP: EUV_DP(Q) ≥ EUV_DP(Q'), the finest partition (identity QUD) dominates all others for the identity DP.

The identity QUD = finest partition = maximum informativity.

Theorem 2: Every QUD is a Decision Problem

Sumers et al. Theorem 2: Any partition-based QUD can be recovered from some decision problem via an "identity DP over cells".

Given a QUD Q that partitions W into cells {C₁,..., Cₙ}:

• Create actions A = {a₁,..., aₙ} (one per cell)
• Utility U(w, aᵢ) = 1 if w ∈ Cᵢ, else 0

Under this DP, the optimal speaker behavior matches QUD-based communication: communicate which cell contains the true world.

def Comparisons.Relevance.qudToDP {W : Type u_1} (q : Semantics.Questions.GSQuestion W) (worlds : List W) (prior : W → ℚ := fun (x : W) => 1) : Core.DecisionTheory.DecisionProblem W ℕ

Convert a G&S question (partition) to a decision problem.

The DP has actions = partition cells, utility = cell membership. This encodes "the goal is to identify which cell the world is in".

Equations

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

theorem Comparisons.Relevance.qud_as_decision_problem {W : Type u_1} [DecidableEq W] (q : Semantics.Questions.GSQuestion W) (worlds : List W) : ∃ (dp : Core.DecisionTheory.DecisionProblem W ℕ), ∀ (w v : W), q.sameAnswer w v = true → ∀ (i : ℕ), dp.utility w i = dp.utility v i

Theorem 2: Any QUD can be recovered from some DP.

The induced DP respects the partition structure: worlds in the same cell have identical utility profiles. Combined with QUD.eu_eq_partitionEU (EU decomposes over any partition), this means the QUD's information structure IS the DP's information structure — they encode the same decision-relevant distinctions.

def Comparisons.Relevance.dpToQUD {W : Type u_1} {A : Type u_2} [DecidableEq A] (dp : Core.DecisionTheory.DecisionProblem W A) (actions : Finset A) : Semantics.Questions.GSQuestion W

The converse: a DP with cell-structured utility induces a QUD.

If U(w, a) depends only on which cell w is, the DP is QUD-equivalent.

Equations

• Comparisons.Relevance.dpToQUD dp actions = { sameAnswer := fun (w v : W) => decide (∀ a ∈ actions, dp.utility w a = dp.utility v a), refl := ⋯, symm := ⋯, trans := ⋯ }

Theorem 3: Decision-Theoretic Relevance is Strictly More Expressive

Sumers et al. Theorem 3: Not all decision problems can be expressed as QUD partitions.

Counterexample: Continuous utility gradations.

• QUDs partition worlds into equivalence classes (discrete cells)
• DPs can assign continuous utility values to worlds
• A DP with U(w, a) = w · a (for numeric worlds) has infinitely fine gradations

This shows decision-theoretic semantics is strictly more expressive than partition semantics.

def Comparisons.Relevance.continuousUtilityDP : Core.DecisionTheory.DecisionProblem ℚ ℚ

Counterexample: Continuous utility DP.

Consider W = ℚ (rational worlds), A = ℚ (rational actions). U(w, a) = -|w - a| (closer guesses are better)

This DP has infinitely many "levels" of utility - no finite partition captures it.

Equations

• Comparisons.Relevance.continuousUtilityDP = { utility := fun (w a : ℚ) => -|w - a|, prior := fun (x : ℚ) => 1 }

theorem Comparisons.Relevance.decision_theoretic_strictly_more_expressive : ∃ (dp : Core.DecisionTheory.DecisionProblem ℚ ℚ), ∀ (w v : ℚ), w ≠ v → ∃ (a : ℚ), dp.utility w a ≠ dp.utility v a

Theorem 3: DT is strictly more expressive than QUD.

There exists a DP where every pair of distinct worlds has a different utility profile under some action. The induced QUD (dpToQUD) is the exact partition, but the DP's graded utility values carry more information than the partition's same/different distinction. Partitions are all-or-nothing; DPs can encode degrees.

theorem Comparisons.Relevance.continuous_dp_not_partition (w v : ℚ) : w ≠ v → ∃ (a : ℚ), continuousUtilityDP.utility w a ≠ continuousUtilityDP.utility v a

The continuous DP cannot be captured by any finite partition.

Any partition groups some distinct worlds together, but the DP distinguishes all worlds (different optimal actions for each world).

Theorem 6: RSA IS Decision-Theoretic

Standard RSA speaker utility is log P_L(w|u). By Theorem 1, this equals decision-theoretic utility under the identity DP.

RSA is not "merely epistemic" -- it is decision-theoretic communication with an accuracy-oriented DP. This unifies RSA with game-theoretic pragmatics (Benz, Parikh, Van Rooij). The apparent distinction between "epistemic" and "decision-theoretic" models dissolves: epistemic is decision-theoretic under the identity DP.

theorem Comparisons.Relevance.rsa_is_decision_theoretic {W : Type u_1} [DecidableEq W] (worlds : List W) (prior : W → ℚ) : have dp := identityDP worlds prior; ∀ (w : W), dp.utility w w = 1

Theorem 6: RSA is decision-theoretic communication.

RSA's epistemic utility function is decision-theoretic utility under the identity decision problem.

theorem Comparisons.Relevance.rsa_game_theoretic_unity {W : Type u_1} [Fintype W] [DecidableEq W] (dp : Core.DecisionTheory.DecisionProblem W W) (q : Semantics.Questions.GSQuestion W) (a : W) (hprior : ∀ (w : W), dp.prior w ≥ 0) : Core.DecisionTheory.expectedUtility dp a = QUD.partitionEU dp q a

Corollary: RSA and game-theoretic pragmatics are unified via partition EU.

For any partition Q and any action a, unconditional EU equals partition-relative EU (QUD.eu_eq_partitionEU). RSA's informativity- maximizing speaker computes partition EU for the identity QUD; game-theoretic pragmatics computes partition EU for a goal-specific QUD. Same decomposition, different partitions.

Theorem 7: Pragmatic Answerhood ≡ Positive Utility Value

G&S's J-relative pragmatic answerhood corresponds to "learning the answer has positive utility value" under the appropriate DP.

This bridges discourse-level concepts (answering questions) to decision-level concepts (helping achieve goals).

theorem Comparisons.Relevance.pragmatic_answerhood_partition_UV {W : Type u_1} [Fintype W] [DecidableEq W] (dp : Core.DecisionTheory.DecisionProblem W W) (q : QUD W) (actions : Finset W) (hprior : ∀ (w : W), dp.prior w ≥ 0) (hsum : Finset.univ.sum dp.prior = 1) : Core.DecisionTheory.questionUtility dp actions (q.toCellsFinset Finset.univ) ≥ 0

Pragmatic answerhood corresponds to positive question utility at the partition level: learning the answer to a QUD-derived question always has non-negative expected UV. (Per-cell UV can be negative — the correct non-negativity is the weighted average across cells.)

This is questionUtility_nonneg_from_blackwell in GSVanRooyBridge.lean.

theorem Comparisons.Relevance.identity_dp_links_answerhood_uv {W : Type u_1} [DecidableEq W] (worlds : List W) (w : W) : (identityDP worlds).utility w w = 1

Corollary: The identity DP links pragmatic answerhood to UV.

Under the identity DP, the optimal action for a world w is w itself (guessing the truth), and its utility is 1. This grounds the connection between G&S pragmatic answerhood and Van Rooy's UV.

Theorem: Blackwell Bridges Both Theories

Blackwell's theorem holds for both QUD and DT formulations. This is why the two theories often agree in practice.

For partition-based questions:

• QUD ordering: Q ⊑ Q' iff Q refines Q' (finer partition)
• DT ordering: Q ≥_DT Q' iff ∀DP: EUV_DP(Q) ≥ EUV_DP(Q')

Blackwell: These orderings coincide!

The empirical success of both theories follows from agreement on the fundamental ordering of question informativity.

theorem Comparisons.Relevance.blackwell_unifies_relevance {W : Type u_1} [Fintype W] [DecidableEq W] (q q' : Semantics.Questions.GSQuestion W) : QUD.refines q q' ↔ ∀ (A : Type) [inst : DecidableEq A] (dp : Core.DecisionTheory.DecisionProblem W A) (actions : Finset A), (∀ (w : W), dp.prior w ≥ 0) → Core.DecisionTheory.questionUtility dp actions (QUD.toCellsFinset q Finset.univ) ≥ Core.DecisionTheory.questionUtility dp actions (QUD.toCellsFinset q' Finset.univ)

Blackwell's theorem holds for both QUD and DT formulations.

Refinement ↔ universal dominance, quantifying over ALL action types.

Partition-Level Foundations

The Blackwell bridge above connects G&S refinement to question utility. @cite{merin-1999} @cite{sumers-etal-2023} establishes the deeper partition-theoretic foundations in Core.Partition:

1. EU compositionality (QUD.eu_eq_partitionEU): Expected utility equals partition-relative EU for any partition, because cells are exhaustive and mutually exclusive. This means the partition faithfully decomposes EU.

2. Coarsening preserves EU (QUD.coarsening_preserves_eu): Coarsening (merging cells) cannot change the total EU for a fixed action.

3. Blackwell = refinement (QUD.blackwell_characterizes_refinement): Q refines Q' iff Q is at least as valuable as Q' for every DP.

Together these show that the QUD framework and the decision-theoretic framework are not independent approaches to relevance but the SAME theory expressed in different mathematical languages. The partition lattice IS the Blackwell lattice.

This grounds Sumers et al.'s Theorem 2 (any QUD is some DP): the QUD partition structure decomposes EU additively, so the partition literally encodes the decision-relevant information structure.

theorem Comparisons.Relevance.partition_blackwell_refinement {W : Type u_1} {A : Type u_2} [DecidableEq W] (dp : Core.DecisionTheory.DecisionProblem W A) (q q' : Semantics.Questions.GSQuestion W) (worlds : Finset W) (actions : Finset A) (hRefines : QUD.refines q q') (hprior : ∀ (w : W), dp.prior w ≥ 0) : QUD.partitionValue dp q worlds actions ≥ QUD.partitionValue dp q' worlds actions

Partition-level Blackwell: refinement implies greater partition value.

This is QUD.blackwell_refinement_value from Core.Partition, restated at the question-semantics level. Since GSQuestion = QUD, the theorem applies directly.

theorem Comparisons.Relevance.partitionValue_implies_questionUtility {W : Type u_1} {A : Type u_2} [Fintype W] [DecidableEq W] [DecidableEq A] (dp : Core.DecisionTheory.DecisionProblem W A) (q q' : Semantics.Questions.GSQuestion W) (actions : Finset A) (hRefines : QUD.refines q q') (hprior : ∀ (w : W), dp.prior w ≥ 0) : Core.DecisionTheory.questionUtility dp actions (QUD.toCellsFinset q Finset.univ) ≥ Core.DecisionTheory.questionUtility dp actions (QUD.toCellsFinset q' Finset.univ)

The partition value ordering implies the question utility ordering.

Since questionUtility = partitionValue - dpValue × totalPrior and dpValue is partition-independent, the orderings coincide. This is why Blackwell works for both Merin's partition value and Van Rooy's question utility.

Proved via QUD.questionUtility_refinement_ge from Core.Partition, which establishes the algebraic decomposition directly.

theorem Comparisons.Relevance.eu_compositional_grounding {W : Type u_1} [Fintype W] [DecidableEq W] (dp : Core.DecisionTheory.DecisionProblem W W) (q : Semantics.Questions.GSQuestion W) (a : W) (hprior : ∀ (w : W), dp.prior w ≥ 0) : Core.DecisionTheory.expectedUtility dp a = QUD.partitionEU dp q a

EU compositionality grounds the QUD→DP direction (Sumers Theorem 2).

QUD.eu_eq_partitionEU shows that computing EU through any partition gives the same answer as unconditional EU. The partition structure doesn't distort expected utility — it decomposes it faithfully. The QUD literally encodes the decision-relevant information structure of a DP.

This is Merin's central theorem: EU is compositional under partitioning.

theorem Comparisons.Relevance.coarsening_preserves_eu_bridge {W : Type u_1} {A : Type u_2} [Fintype W] [DecidableEq W] (dp : Core.DecisionTheory.DecisionProblem W A) (q q' : Semantics.Questions.GSQuestion W) (a : A) (hCoarse : QUD.coarsens q q') (hprior : ∀ (w : W), dp.prior w ≥ 0) : QUD.partitionEU dp q a = QUD.partitionEU dp q' a

Coarsening preserves EU: merging partition cells cannot change total EU.

This is the formal content of Merin's claim that partitions are decision-theoretically privileged. For a FIXED action, computing EU via a coarser partition gives the same answer. Only the VALUE of information (optimal action per cell) depends on partition fineness — the EU decomposition itself is invariant.

Combined Model (Sumers et al.)

The combined model interpolates between truthfulness and relevance:

U_combined(u|w,A) = λ·U_relevance + (1-λ)·U_truthfulness + C(u)

• λ = 0: Pure truthfulness (standard RSA)
• λ = 1: Pure decision-theoretic relevance
• 0 < λ < 1: Weighted combination

theorem Comparisons.Relevance.combined_model_endpoints_relevance (truthfulness relevance : ℚ) : RSA.CombinedUtility.combined 0 truthfulness relevance = truthfulness ∧ RSA.CombinedUtility.combined 1 truthfulness relevance = relevance

Theorem 5: Combined model endpoints (uses combined from RSA.CombinedUtility).

The combined model reduces to pure truthfulness when lam=0 and pure relevance when lam=1.

This theorem is proven in RSA.CombinedUtility as combined_endpoints. We re-export the reference here for the unified view.

Theorem 12: Information-Theoretic Characterization

QUD-based relevance maximizes mutual information I(W;A) where A is the answer variable. Decision-theoretic relevance maximizes expected utility.

These coincide under log-loss (identity DP).

This connects:

• Information theory: mutual information, entropy reduction
• Decision theory: expected utility maximization
• Semantics: partition refinement

All three perspectives align for the identity DP.

def Comparisons.Relevance.approxMutualInformation {W : Type u_1} [DecidableEq W] (prior : W → ℚ) (_q : Semantics.Questions.GSQuestion W) (worlds : List W) : ℚ

Mutual information approximation for rational arithmetic.

Since we can't compute true MI (requires log) with rationals, we use utility value as a proxy that captures the same structure.

Note: This is a simplified approximation using expected utility under the identity DP as a proxy for mutual information.

Equations

• Comparisons.Relevance.approxMutualInformation prior _q worlds = List.foldl (fun (acc : ℚ) (w : W) => acc + prior w * (Comparisons.Relevance.identityDP worlds prior).utility w w) 0 worlds

theorem Comparisons.Relevance.qud_maximizes_mutual_information {W : Type u_1} {A : Type u_2} [DecidableEq W] [BEq W] [LawfulBEq W] (dp : Core.DecisionTheory.DecisionProblem W A) (q : Semantics.Questions.GSQuestion W) (worlds : Finset W) (actions : Finset A) (hprior : ∀ (w : W), dp.prior w ≥ 0) : QUD.partitionValue dp Semantics.Questions.GSQuestion.exact worlds actions ≥ QUD.partitionValue dp q worlds actions

Theorem 12: The exact QUD maximizes partition value for any DP.

Under any decision problem, the finest partition (identity QUD) has the highest partition value (Blackwell). For the identity DP, partition value tracks mutual information: finer partitions allow more precise action selection, yielding higher expected accuracy.

This is a direct corollary of QUD.blackwell_refinement_value: the exact partition refines all others (QUD.exact_refines_all), so its partition value dominates.

Summary: The Unified View

Concept	QUD Formulation	DT Formulation
Relevance	Partition refinement	Utility value
Truthfulness	Identity QUD	Identity DP
Answerhood	Cell membership	Positive UV
Ordering	⊑ (refines)	≥_DT (dominates)

These are not competing theories but the same theory expressed in different mathematical languages. Blackwell's theorem translates between them.

theorem Comparisons.Relevance.unified_view {W : Type u_1} [DecidableEq W] (q q' : Semantics.Questions.GSQuestion W) : QUD.refines q q' ↔ ∀ (worlds : Finset W) (A : Type) [DecidableEq A] (dp : Core.DecisionTheory.DecisionProblem W A) (actions : Finset A), (∀ (w : W), dp.prior w ≥ 0) → QUD.partitionValue dp q worlds actions ≥ QUD.partitionValue dp q' worlds actions

The unified view: QUD refinement = Blackwell ordering = universal dominance.

For any two partitions Q, Q':

• Q ⊑ Q' (semantic refinement)
• iff ∀ worlds, ∀DP: partitionValue(Q) ≥ partitionValue(Q') (Blackwell)

Merin's partition lattice, Blackwell's experiment ordering, and Van Rooy's question utility agree on the ordering of information structures. This is why QUD semantics and decision-theoretic semantics are the same theory.

Note: The Blackwell direction must quantify over all world lists, not just a fixed one, because the characterization proof constructs a specific 2-element world list [w, v] as witness.