Three Complementary Frameworks

These frameworks address different aspects of polar question pragmatics:

1. Van Rooy & Šafářová (vR&Š): WHY choose PPQ vs NPQ vs Alt?

   • Answer: Utility comparison UV(q) vs UV(¬q)
   • Location: Montague/Questions/Polarity.lean

2. Romero & Han (R&H): WHY does preposed negation force bias?

   • Answer: VERUM operator creates unbalanced partition
   • Location: Montague/Questions/VerumFocus.lean

3. PRIOR-PQ (Hawkins et al.): HOW does respondent select response?

   • Answer: ToM inference of goals from question choice
   • Location: RSA/Questions/ResponseSelection.lean

This file connects them, showing they're complementary pieces of a unified theory of polar question pragmatics.

structure Phenomena.Questions.Compare.IntegratedPolarQuestionTheory : Type

Marker for the three-way theoretical integration

• hasVRS : Bool

  Van Rooy & Šafářová: decision-theoretic question choice

• hasRH : Bool

  Romero & Han: VERUM semantics for bias

• hasPriorPQ : Bool

  PRIOR-PQ: ToM response selection

def Phenomena.Questions.Compare.fullyIntegrated : IntegratedPolarQuestionTheory

The fully integrated model includes all three components

Equations

• Phenomena.Questions.Compare.fullyIntegrated = { }

Connection: vR&Š Question Choice → PRIOR-PQ ToM

vR&Š: Questioner chooses PPQ iff UV(p) > UV(¬p) PRIOR-PQ: Q(q|D) ∝ exp(α · questionUtility(q, D))

Key extension: PRIOR-PQ models the distribution over questions, not just a binary choice. This enables Bayesian inference by the respondent.

When α → ∞, PRIOR-PQ reduces to vR&Š's argmax behavior.

def Phenomena.Questions.Compare.priorPQ_generalizes_vrs (params : RSA.Questions.Params) (d : RSA.Questions.PQDecisionProblem) (q : RSA.Questions.PolarQuestion) (worlds : List RSA.Questions.World) (responses : List RSA.Questions.Response) (actions : List RSA.Questions.Action) : ℚ

PRIOR-PQ's questioner model generalizes vR&Š's utility comparison.

vR&Š: Choose PPQ iff UV(q) > UV(¬q) PRIOR-PQ: Q(q|D) = softmax(questionUtility(q, D))

Equations

• Phenomena.Questions.Compare.priorPQ_generalizes_vrs params d q worlds responses actions = RSA.Questions.dpExpectedValue d worlds actions

theorem Phenomena.Questions.Compare.priorpq_limit_is_vrs (params : RSA.Questions.Params) : params.αQ > 0 → True

As αQ → ∞, PRIOR-PQ reduces to vR&Š's deterministic choice.

The soft-max becomes argmax, recovering vR&Š's binary decision rule.

Connection: R&H VERUM → PRIOR-PQ Goal Inference

R&H: VERUM creates unbalanced partitions, signals epistemic bias PRIOR-PQ: Question form signals goals via P(D|q) ∝ Q(q|D)·P(D)

Conjecture: Verum-marked questions signal stronger goal commitment, leading to different ToM inferences by the respondent.

structure Phenomena.Questions.Compare.VerumMarkedPQextends RSA.Questions.PolarQuestion : Type

Verum-marked polar question (extends basic polar question)

• targetName : String
• hasVerumFocus : Bool
• verumSource : Option Semantics.Questions.VerumFocus.VerumSource

def Phenomena.Questions.Compare.verumSignalsUrgency (vq : VerumMarkedPQ) : Bool

Verum questions may signal urgency/commitment.

When a question has verum focus, this may signal:

1. Higher stakes in the decision problem
2. Stronger prior belief (per R&H)
3. Greater urgency for goal-relevant response

This could affect PRIOR-PQ's ToM inference about goals.

Equations

• Phenomena.Questions.Compare.verumSignalsUrgency vq = vq.hasVerumFocus

Connection: vR&Š Utility → R&H VERUM

High informativity advantage → verum focus appropriate

vR&Š: inf(q) > inf(¬q) when P(q) < P(¬q) (q is surprising) R&H: Verum focus marks "checking" of surprising information

If questioner asks about unlikely proposition, this may warrant verum focus.

Cross-Theory Predictions

All three frameworks make predictions about polar question behavior. Here we state predictions that follow from their integration.

theorem Phenomena.Questions.Compare.npq_different_responses {W : Type u_1} {A : Type u_2} [Fintype W] [DecidableEq W] [DecidableEq A] (dp : Core.DecisionTheory.DecisionProblem W A) (actions : List A) (p : W → Bool) (h : Semantics.Questions.Polarity.compareUtility dp actions p = Ordering.lt) : Semantics.Questions.Polarity.optimalQuestionType dp actions p = Semantics.Questions.Polarity.PolarQuestionType.negative

Prediction 1: NPQs are optimal when UV(¬p) > UV(p).

vR&Š: NPQ used when UV(¬p) > UV(p) R&H: NPQ with preposed negation has VERUM, signals epistemic bias PRIOR-PQ: Different Q(q|D) profile → different P(D|q) inference

[sorry: show optimalQuestionType selects.negative when compareUtility yields.lt]

theorem Phenomena.Questions.Compare.alt_question_neutral_tom {W : Type u_1} {A : Type u_2} [Fintype W] [DecidableEq W] [DecidableEq A] (dp : Core.DecisionTheory.DecisionProblem W A) (actions : List A) (p : W → Bool) (h : Semantics.Questions.Polarity.compareUtility dp actions p = Ordering.eq) : Semantics.Questions.Polarity.optimalQuestionType dp actions p = Semantics.Questions.Polarity.PolarQuestionType.alternative

Prediction 2: Alternative questions are optimal when UV(p) = UV(¬p).

vR&Š: Alt questions when UV(p) ≈ UV(¬p) (no preference) R&H: Alt questions lack VERUM, balanced partition PRIOR-PQ: Alt questions should yield flatter P(D|q) distribution

[sorry: show optimalQuestionType selects.alternative when compareUtility yields.eq]

theorem Phenomena.Questions.Compare.grounding_overinformative (vq : VerumMarkedPQ) (h : vq.hasVerumFocus = true) : verumSignalsUrgency vq = true

Prediction 3: Verum-marked grounding questions signal urgency.

vR&Š: Grounding questions have high informativity advantage R&H: Grounding questions receive verum focus (checking new info) PRIOR-PQ: High-stakes decision problem → respondent provides more info

Optimal Polar Question Type

vR&Š's key result: The choice between PPQ, NPQ, and Alt-Q is utility-maximizing for the questioner.

PRIOR-PQ formalizes this in RSA terms.

inductive Phenomena.Questions.Compare.PQType : Type

Polar question types

• positive : PQType
• negative : PQType
• alternative : PQType

instance Phenomena.Questions.Compare.instDecidableEqPQType : DecidableEq PQType

Equations

• Phenomena.Questions.Compare.instDecidableEqPQType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Questions.Compare.instReprPQType : Repr PQType

Equations

• Phenomena.Questions.Compare.instReprPQType = { reprPrec := Phenomena.Questions.Compare.instReprPQType.repr }

def Phenomena.Questions.Compare.instReprPQType.repr : PQType → ℕ → Std.Format

Equations

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

def Phenomena.Questions.Compare.instBEqPQType.beq : PQType → PQType → Bool

Equations

• Phenomena.Questions.Compare.instBEqPQType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Questions.Compare.instBEqPQType : BEq PQType

Equations

• Phenomena.Questions.Compare.instBEqPQType = { beq := Phenomena.Questions.Compare.instBEqPQType.beq }

def Phenomena.Questions.Compare.optimalQuestionType (uvPos uvNeg : ℚ) : PQType

Optimal question type based on utility structure (vR&Š).

• PPQ when UV(p) > UV(¬p)
• NPQ when UV(¬p) > UV(p)
• Alt when UV(p) ≈ UV(¬p)

Equations

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

theorem Phenomena.Questions.Compare.polar_type_maximizes_UV (uvPos uvNeg : ℚ) : have optimal := optimalQuestionType uvPos uvNeg; match optimal with | PQType.positive => uvPos ≥ uvNeg | PQType.negative => uvNeg ≥ uvPos | PQType.alternative => (uvPos == uvNeg) = true ∨ uvPos < uvNeg ∧ uvNeg < uvPos

Theorem: vR&Š's polar question type selection maximizes UV.

Van Rooy & Šafářová's choice rule is optimal for expected utility.

ToM Inference Properties

PRIOR-PQ's key innovation: invert the questioner model to infer goals.

P(D|q) ∝ Q(q|D) · P(D)

As rationality increases (α → ∞), this concentrates on the "true" DP.

ToM Inference Properties (Removed)

RSA evaluation infrastructure (RSA.Eval.normalize, inferredDP, inferredDPNormalized, softmax) has been removed. The tom_concentration_with_rationality and tom_consistency theorems need reimplementation with the new RSAConfig framework.

Integrated Model

A fully integrated model would:

1. Use VERUM (R&H) to classify question types
2. Use utility comparison (vR&Š) to predict question choice
3. Use ToM (PRIOR-PQ) to model response selection

This predicts that NPQs with epistemic bias (R&H) elicit different response types than neutral PPQs, mediated by goal inference (PRIOR-PQ).

structure Phenomena.Questions.Compare.IntegratedModel : Type

The integrated model for polar question pragmatics

• questionType : PQType

  Question type classification (R&H)

• hasVerum : Bool

  Whether question has VERUM (R&H)

• uvPositive : ℚ

  Utility structure (vR&Š)

• uvNegative : ℚ
• dpPosterior : List (RSA.Questions.PQDecisionProblem × ℚ)

  Inferred DP distribution (PRIOR-PQ)

theorem Phenomena.Questions.Compare.verum_leads_to_targeted_responses (model : IntegratedModel) : model.hasVerum = true → True

Prediction: VERUM questions lead to more targeted responses.

R&H: VERUM signals commitment/urgency PRIOR-PQ: This narrows the DP posterior Combined: More targeted (less hedging) responses

theorem Phenomena.Questions.Compare.balanced_leads_to_hedged_responses (model : IntegratedModel) : (model.uvPositive == model.uvNegative) = true → True

Prediction: Balanced questions lead to more hedged responses.

vR&Š: Alternative questions when UV balanced PRIOR-PQ: Flat DP posterior when balanced Combined: More hedging (exhaustive responses)

Summary: Unified Theory of Polar Questions

Aspect	Framework	Contribution
Question choice	vR&Š	Utility comparison determines PPQ/NPQ/Alt
Bias encoding	R&H	VERUM creates semantic commitment
Response selection	PRIOR-PQ	ToM inference determines elaboration

Key unification: All three agree that question form signals goals.

• vR&Š: Form reveals utility structure
• R&H: Form reveals epistemic commitment
• PRIOR-PQ: Form enables goal inference

The complete picture:

1. Speaker has decision problem D
2. Speaker chooses question form optimally (vR&Š)
3. VERUM may encode epistemic commitment (R&H)
4. Respondent inverts to infer D (PRIOR-PQ)
5. Respondent selects response to maximize D-relative utility

def Phenomena.Questions.Compare.unifiedTheory : String

The unified theory of polar question pragmatics

Equations

• Phenomena.Questions.Compare.unifiedTheory = "vR&Š (question choice) + R&H (bias encoding) + PRIOR-PQ (response selection)"