Decision-Theoretic Question Semantics

@cite{van-rooy-2003} @cite{van-rooy-safarova-2003} @cite{blackwell-1953} @cite{chierchia-2013}

Topical home for question semantics extended with utility / cost structure. The "value of a question" is defined relative to a decision problem; relevance, polar profiles, and Blackwell dominance are all derived notions over the inquisitive substrate.

Layout

• Utility-based relevance (@cite{van-rooy-2003} Op(P)). IsDecisionRelevant Q σ dp holds when resolving Q from state σ strictly changes the optimal action in dp.
• Polar utility profiles (@cite{van-rooy-safarova-2003}). IsPPQ, IsNPQ, IsAltQ classify a polar question's utility-asymmetry pattern.
• Blackwell dominance (@cite{blackwell-1953}). The inquisitive setting splits the partition notion of "refinement" into two independent directions, both in Core.Question.Relevance:
  • questionEntails P Q — every P-alt ⊆ some Q-alt (P-alts are contained in Q-alts).
  • CoversAltsOf P Q — every nonempty Q-alt is covered by some nonempty P-alt (the dual). For partition questions the two coincide. Decision-relevance preservation requires the dual; the CoversAltsOf.preserves_decisionRelevant theorem (proven below) is the @cite{van-rooy-2003} bridge.
• Question entropy / NPI strength (@cite{chierchia-2013}). An NPI-licensing context is one whose alternatives carry high Shannon entropy. The information-theoretic NPI account is @cite{chierchia-2013} (and earlier @cite{israel-1996} for the scalar-strengthening variant); @cite{krifka-1995a} Linguistic Analysis is the foundational lexical-semantic NPI paper but does not invoke entropy directly.

Substrate split

Question denotations are inquisitive (Core.Question W) — Set-based alternatives. Decision problems live in Core.Agent.DecisionTheory with Finset-based action and cell sets. The bridge requires [Fintype W] plus per-alternative decidability; consumers that don't need finite computation work directly with the Set-shaped predicates here.

Decision-relevance (@cite{van-rooy-2003} Op(P))

A question is decision-relevant if learning its answer can change which action maximises expected utility. The notion specialises @cite{van-rooy-2003}'s Op(P) to the inquisitive substrate: rather than computing EU(after Q) − EU(before Q) numerically, we ask whether some alternative of Q would shift the optimal action.

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

Q is decision-relevant to dp: there exist two non-empty alternatives p, p' ∈ alt Q and two actions a, a' ∈ acts such that a strictly dominates a' on p while a' strictly dominates a on p'. Then learning which alternative obtains shifts the optimal choice — the operational content of @cite{van-rooy-2003} Op(P) > 0.

The non-emptiness clauses rule out the degenerate case where Q = ⊥ (only ∅ in alt): with empty witness propositions the dominance conditions hold vacuously without genuinely distinguishing any worlds. Mathlib-shape: a substantive decision-relevance claim requires substantive (nonempty) witnesses.

Equations

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

Bridge to Core.DecisionTheory.IsResolved

theorem Semantics.Questions.DecisionTheoretic.IsDecisionRelevant.alts_resolve_distinct {W : Type u_1} {A : Type u_2} {Q : Core.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'

@cite{van-rooy-2003} §3.1 connection: a IsDecisionRelevant witness (p, p', a, a') exhibits two Q-alts whose two-action restriction is IsResolved to different witnesses. On p, action a resolves the restricted DP (dp, {a, a'}); on p', action a' does. So IsDecisionRelevant is precisely "two Q-alts resolve to distinct actions" in the substrate's IsResolved vocabulary.

theorem Semantics.Questions.DecisionTheoretic.IsDecisionRelevant.singleton_alt_false {W : Type u_1} {A : Type u_2} {Q : Core.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

The trivial question (single alternative) is not decision-relevant: one substantive alternative cannot witness the action-reversal.

Polar utility profiles (@cite{van-rooy-safarova-2003})

A polar question Q? = {p, ¬p} has a utility profile determined by the asymmetry of action-payoffs between the p-cell and the ¬p-cell.

• PPQ (positive polar): the p-alternative is utility-preferred. Speaker bias toward p (e.g., Did John leave? in a context where John leaving is good news).
• NPQ (negative polar): the ¬p-alternative is preferred. Speaker bias toward ¬p (Didn't John leave?).
• Alt (alternative question): both alternatives carry comparable utility — neither dominates.

def Semantics.Questions.DecisionTheoretic.IsPPQ {W : Type u_1} {A : Type u_2} (Q : Core.Question W) (dp : Core.DecisionTheory.DecisionProblem W A) (acts : Set A) (p : Set W) : Prop

Q is a PPQ for action set acts and polar split (p, ¬p): one specific alternative p ∈ alt Q strictly dominates every other alternative across every action. The "positive" cell is where the speaker's preferred outcome lies. @cite{van-rooy-safarova-2003}.

Equations

• Semantics.Questions.DecisionTheoretic.IsPPQ Q dp acts p = (p ∈ Q.alt ∧ ∃ a ∈ acts, ∀ p' ∈ Q.alt, p' ≠ p → ∀ w ∈ p, ∀ w' ∈ p', dp.utility w a > dp.utility w' a)

def Semantics.Questions.DecisionTheoretic.IsNPQ {W : Type u_1} {A : Type u_2} (Q : Core.Question W) (dp : Core.DecisionTheory.DecisionProblem W A) (acts : Set A) (p : Set W) : Prop

Q is an NPQ for action set acts and polar split (p, ¬p): a strictly non-p alternative is the utility-preferred one. @cite{van-rooy-safarova-2003}.

Equations

• Semantics.Questions.DecisionTheoretic.IsNPQ Q dp acts p = (p ∈ Q.alt ∧ ∃ p' ∈ Q.alt, p' ≠ p ∧ Semantics.Questions.DecisionTheoretic.IsPPQ Q dp acts p')

def Semantics.Questions.DecisionTheoretic.IsAltQ {W : Type u_1} {A : Type u_2} (Q : Core.Question W) (dp : Core.DecisionTheory.DecisionProblem W A) (acts : Set A) : Prop

Q is an alternative-utility question for action set acts: no single alternative strictly dominates. The utility-balanced case. @cite{van-rooy-safarova-2003}.

Equations

• Semantics.Questions.DecisionTheoretic.IsAltQ Q dp acts = ∀ p ∈ Q.alt, ¬Semantics.Questions.DecisionTheoretic.IsPPQ Q dp acts p

theorem Semantics.Questions.DecisionTheoretic.IsPPQ.not_isAltQ {W : Type u_1} {A : Type u_2} {Q : Core.Question W} {dp : Core.DecisionTheory.DecisionProblem W A} {acts : Set A} {p : Set W} (h : IsPPQ Q dp acts p) : ¬IsAltQ Q dp acts

A PPQ rules out the alt-utility classification.

Blackwell informativeness (@cite{blackwell-1953})

The Blackwell informativeness order on questions is Core.Question.Relevance.questionEntails P Q: every alternative of P is contained in some alternative of Q (P is finer than Q). The dual condition — every nonempty Q-alt is covered by a nonempty P-alt — is Core.Question.Relevance.CoversAltsOf P Q. On partition questions the two coincide; on general inquisitive Question W they are distinct. The decision-relevance preservation theorem requires the dual form.

The decision-relevance preservation theorem itself (CoversAltsOf.preserves_decisionRelevant) is declared at the bottom of this file, outside the topic namespace, under Core.Question.CoversAltsOf so dot notation works at consumer sites.

Question entropy and NPI strength (@cite{chierchia-2013})

@cite{chierchia-2013} relates NPI distribution to the informativeness of the alternative set raised by a sentence (the information-theoretic strand earlier traced through @cite{israel-1996} on lexical-semantic polarity sensitivity). A question whose alternatives are equiprobable under the prior carries maximal Shannon entropy; NPIs prefer such high-entropy contexts. The earlier @cite{krifka-1995a} Linguistic Analysis polarity-items paper is the foundational lexical-semantic NPI account but does not formulate licensing in entropy terms — the Chierchia/Israel synthesis is the right citation here.

The numeric API requires real-valued logarithms over the prior; deferred to a follow-up that lifts Core.Probability's PMF API to expose Shannon entropy. The Prop-level placeholder HasMultipleSubstantiveAlternatives captures the load-bearing condition that the question is informative — necessary for any NPI-licensing notion.

def Semantics.Questions.DecisionTheoretic.HasMultipleSubstantiveAlternatives {W : Type u_1} (Q : Core.Question W) : Prop

Q has multiple substantive alternatives: some pair of distinct alternatives are both nonempty. Necessary for any NPI-licensing formulation (a single-alt question carries no informational asymmetry). @cite{chierchia-2013} prerequisite.

Equations

• Semantics.Questions.DecisionTheoretic.HasMultipleSubstantiveAlternatives Q = ∃ p ∈ Q.alt, ∃ q ∈ Q.alt, p ≠ q ∧ p.Nonempty ∧ q.Nonempty

theorem Semantics.Questions.DecisionTheoretic.IsDecisionRelevant.imp_HasMultipleSubstantiveAlternatives {W : Type u_1} {A : Type u_2} {Q : Core.Question W} {dp : Core.DecisionTheory.DecisionProblem W A} {acts : Set A} (h : IsDecisionRelevant Q dp acts) : HasMultipleSubstantiveAlternatives Q

A decision-relevant question necessarily has multiple substantive (nonempty, distinct) alternatives. The substrate-level contrapositive of IsDecisionRelevant.singleton_alt_false: decision-relevance requires informational asymmetry, which is @cite{chierchia-2013}'s prerequisite for NPI licensing. So any decision-relevant question is a candidate NPI-licensing context.

CoversAltsOf API extensions

Theorem placed under Core.Question.CoversAltsOf namespace (not the file's Semantics.Questions.DecisionTheoretic topic namespace) so dot-notation hCover.preserves_decisionRelevant resolves at consumer sites. Mathlib pattern: declarations follow the type's namespace, not the file's topic namespace.

theorem Core.Question.CoversAltsOf.preserves_decisionRelevant {W : Type u_1} {A : Type u_2} {P Q : Question W} (hCover : P.CoversAltsOf Q) {dp : DecisionTheory.DecisionProblem W A} {acts : Set A} (hQ : Semantics.Questions.DecisionTheoretic.IsDecisionRelevant Q dp acts) : Semantics.Questions.DecisionTheoretic.IsDecisionRelevant P dp acts

@cite{blackwell-1953} ↔ @cite{van-rooy-2003}: when every nonempty alt of Q is covered by a nonempty alt of P, decision-relevance is preserved from Q to P.