Hawkins, Tsvilodub, Bergey, Goodman and Franke (2025): Relevant answers to polar questions

This file formalizes the PRIOR-PQ model of [HTB+25], a Rational Speech Act model of question answering grounded in the questioner's decision problem. The base-level respondent R0 answers with any true and safe response (2.1), where a response is safe for a question when a questioner who knew it would know the answer (Safe, with the belief-state characterization safe_iff_forall_settles). The questioner questioner soft-maximizes the expected value of the decision problem updated by the base respondent's answer less its cost (2.3), with the Bayesian update (2.4) as the posterior of the observation model R0Model and the policy value of (2.2) as value; questionScore_eq_eig identifies the score with [Lin56]'s expected information gain of the question as an experiment. The pragmatic respondent respondent infers the questioner's decision problem from the question (respondentPosterior, respondentPosterior_lt_iff: a question is a signal about the goal) and soft-maximizes a mixture of informativity and action relevance less cost (2.5); respondentScore_beta_one and respondentScore_beta_zero are its two pure ends. posterior_lt_iff_card is the size principle of §2b: a response is strengthened towards the worlds with fewer true and safe alternatives.

Case study 1 (§3a) instantiates the model on the credit cards: polar_exhaustive_safe and mention_safe_iff classify the responses, yes_value_eq_exhaustive is the reason the exhaustive list is dispreferred after a question about a card the questioner holds (3), and generalYes_posterior_pos the residual uncertainty after the general question (5).

Implementation notes

• Softmaxes are Core.RationalAction.fromSoftmax; beliefs are functions W → ℝ, as in ProbabilityTheory.ObservationModel, and the Kullback–Leibler term of (2.5) is the finite sum kl in the direction the paper writes it.
• Both the safe base respondent of (2.1) and its truth-only relaxation R0' of §2c are RationalActions; the observation model needs every world to admit a true and safe response, which polar_admissible supplies for polar questions.
• The case study fixes the parameters the paper leaves free only where a theorem needs a sign; the fitted values of the electronic supplementary material are not reproduced.

TODO

• Case studies 2 and 3 (the iced tea and blanket vignettes) with the elicited utilities.

References

• [HTB+25]
• [Lin56]

Safe answers (§2a)

def HawkinsEtAl2025.Settles {W : Type u_1} (s : Set W) (p : W → Prop) : Prop

A belief state settles a proposition when it entails it or its negation.

Equations

• HawkinsEtAl2025.Settles s p = (s ⊆ {w : W | p w} ∨ s ⊆ {w : W | ¬p w})

def HawkinsEtAl2025.Safe {W : Type u_1} (q r : W → Prop) : Prop

A response r is safe for the polar question q (§2a): a questioner who knew r would know the answer to q, so r entails one of the complete answers.

Equations

• HawkinsEtAl2025.Safe q r = ((∀ (w : W), r w → q w) ∨ ∀ (w : W), r w → ¬q w)

@[instance_reducible]

instance HawkinsEtAl2025.instDecidableSafeOfFintypeOfDecidablePred {W : Type u_1} [Fintype W] (q r : W → Prop) [DecidablePred q] [DecidablePred r] : Decidable (Safe q r)

Equations

• HawkinsEtAl2025.instDecidableSafeOfFintypeOfDecidablePred q r = HawkinsEtAl2025.instDecidableSafeOfFintypeOfDecidablePred._aux_1 q r

theorem HawkinsEtAl2025.safe_iff_forall_settles {W : Type u_1} (q r : W → Prop) : Safe q r ↔ ∀ s ⊆ {w : W | r w}, Settles s q

Safety in belief states: every state verifying r settles q.

theorem HawkinsEtAl2025.safe_self {W : Type u_1} (q : W → Prop) : Safe q q

theorem HawkinsEtAl2025.safe_not {W : Type u_1} (q : W → Prop) : Safe q fun (w : W) => ¬q w

The model

structure HawkinsEtAl2025.Model (W : Type u_6) (Q : Type u_7) (R : Type u_8) (A : Type u_9) (D : Type u_10) : Type (max (max (max (max u_10 u_6) u_7) u_8) u_9)

A PRIOR-PQ model: the propositions questions and responses denote, the questioner's decision problems, and the cost of responses.

• question : Q → W → Prop

  The proposition a polar question asks about.

• response : R → W → Prop

  The proposition a response asserts.

• utility : D → W → A → ℝ

  The utility function of a decision problem.

• prior : D → W → ℝ

  The questioner's prior over worlds under a decision problem.

• cost : R → ℝ

  The production cost of a response.

def HawkinsEtAl2025.Model.Admissible {W : Type u_1} {Q : Type u_2} {R : Type u_3} {A : Type u_4} {D : Type u_5} (m : Model W Q R A D) (w : W) (q : Q) (r : R) : Prop

A response is admissible at a world and question when it is true there and safe.

Equations

• m.Admissible w q r = (m.response r w ∧ HawkinsEtAl2025.Safe (m.question q) (m.response r))

@[instance_reducible]

instance HawkinsEtAl2025.instDecidableAdmissible {W : Type u_1} {Q : Type u_2} {R : Type u_3} {A : Type u_4} {D : Type u_5} (m : Model W Q R A D) [(q : Q) → DecidablePred (m.question q)] [(r : R) → DecidablePred (m.response r)] [Fintype W] (w : W) (q : Q) (r : R) : Decidable (m.Admissible w q r)

Equations

• HawkinsEtAl2025.instDecidableAdmissible m w q r = HawkinsEtAl2025.instDecidableAdmissible._aux_1 m w q r

noncomputable def HawkinsEtAl2025.Model.R0 {W : Type u_1} {Q : Type u_2} {R : Type u_3} {A : Type u_4} {D : Type u_5} (m : Model W Q R A D) [(q : Q) → DecidablePred (m.question q)] [(r : R) → DecidablePred (m.response r)] [Fintype R] [Fintype W] : Core.RationalAction (W × Q) R

(2.1): the base-level respondent, uniform over the true and safe responses.

Equations

• m.R0 = { score := fun (wq : W × Q) (r : R) => if m.Admissible wq.1 wq.2 r then 1 else 0, score_nonneg := ⋯ }

noncomputable def HawkinsEtAl2025.Model.R0' {W : Type u_1} {Q : Type u_2} {R : Type u_3} {A : Type u_4} {D : Type u_5} (m : Model W Q R A D) [(r : R) → DecidablePred (m.response r)] [Fintype R] : Core.RationalAction (W × Q) R

§2c: the truth-only relaxation of the base respondent, uniform over the true responses.

Equations

• m.R0' = { score := fun (wq : W × Q) (r : R) => if m.response r wq.1 then 1 else 0, score_nonneg := ⋯ }

def HawkinsEtAl2025.Model.admissibleCard {W : Type u_1} {Q : Type u_2} {R : Type u_3} {A : Type u_4} {D : Type u_5} (m : Model W Q R A D) [(q : Q) → DecidablePred (m.question q)] [(r : R) → DecidablePred (m.response r)] [Fintype R] [Fintype W] (w : W) (q : Q) : ℕ

The number of true and safe responses at a world and question.

Equations

• m.admissibleCard w q = (Finset.filter (m.Admissible w q) Finset.univ).card

theorem HawkinsEtAl2025.Model.R0_totalScore {W : Type u_1} {Q : Type u_2} {R : Type u_3} {A : Type u_4} {D : Type u_5} (m : Model W Q R A D) [(q : Q) → DecidablePred (m.question q)] [(r : R) → DecidablePred (m.response r)] [Fintype R] [Fintype W] (w : W) (q : Q) : m.R0.totalScore (w, q) = ↑(m.admissibleCard w q)

theorem HawkinsEtAl2025.Model.R0_policy_pos_iff {W : Type u_1} {Q : Type u_2} {R : Type u_3} {A : Type u_4} {D : Type u_5} (m : Model W Q R A D) [(q : Q) → DecidablePred (m.question q)] [(r : R) → DecidablePred (m.response r)] [Fintype R] [Fintype W] {w : W} {q : Q} {r : R} (h : 0 < m.admissibleCard w q) : 0 < m.R0.policy (w, q) r ↔ m.Admissible w q r

The base respondent gives a response positive probability iff it is true and safe.

noncomputable def HawkinsEtAl2025.Model.R0Model {W : Type u_1} {Q : Type u_2} {R : Type u_3} {A : Type u_4} {D : Type u_5} (m : Model W Q R A D) [(q : Q) → DecidablePred (m.question q)] [(r : R) → DecidablePred (m.response r)] [Fintype R] [Fintype W] (h : ∀ (w : W) (q : Q), 0 < m.admissibleCard w q) : ProbabilityTheory.ObservationModel W Q R

The base respondent as an observation model, with questions as experiments and responses as observations, given that every world admits a true and safe response.

Equations

• m.R0Model h = { likelihood := fun (w : W) (q : Q) (r : R) => m.R0.policy (w, q) r, likelihood_nonneg := ⋯, likelihood_sum := ⋯ }

noncomputable def HawkinsEtAl2025.Model.R0Model' {W : Type u_1} {Q : Type u_2} {R : Type u_3} {A : Type u_4} {D : Type u_5} (m : Model W Q R A D) [(r : R) → DecidablePred (m.response r)] [Fintype R] (h : ∀ (w : W), ∃ (r : R), m.response r w) : ProbabilityTheory.ObservationModel W Q R

The truth-only base respondent as an observation model, given that every world makes some response true.

Equations

• m.R0Model' h = { likelihood := fun (w : W) (q : Q) (r : R) => m.R0'.policy (w, q) r, likelihood_nonneg := ⋯, likelihood_sum := ⋯ }

theorem HawkinsEtAl2025.Model.R0Model_likelihood_pos_iff {W : Type u_1} {Q : Type u_2} {R : Type u_3} {A : Type u_4} {D : Type u_5} (m : Model W Q R A D) [(q : Q) → DecidablePred (m.question q)] [(r : R) → DecidablePred (m.response r)] [Fintype R] [Fintype W] (h : ∀ (w : W) (q : Q), 0 < m.admissibleCard w q) {w : W} {q : Q} {r : R} : 0 < (m.R0Model h).likelihood w q r ↔ m.Admissible w q r

theorem HawkinsEtAl2025.Model.R0Model_marginal_pos {W : Type u_1} {Q : Type u_2} {R : Type u_3} {A : Type u_4} {D : Type u_5} (m : Model W Q R A D) [(q : Q) → DecidablePred (m.question q)] [(r : R) → DecidablePred (m.response r)] [Fintype R] [Fintype W] (h : ∀ (w : W) (q : Q), 0 < m.admissibleCard w q) (d : D) (hπ : ∀ (w : W), 0 < m.prior d w) {q : Q} {r : R} {w : W} (hadm : m.Admissible w q r) : 0 < (m.R0Model h).marginal (m.prior d) q r

The marginal of a response is positive when some world of positive prior admits it.

theorem HawkinsEtAl2025.Model.R0Model_posterior_pos_iff {W : Type u_1} {Q : Type u_2} {R : Type u_3} {A : Type u_4} {D : Type u_5} (m : Model W Q R A D) [(q : Q) → DecidablePred (m.question q)] [(r : R) → DecidablePred (m.response r)] [Fintype R] [Fintype W] (h : ∀ (w : W) (q : Q), 0 < m.admissibleCard w q) (d : D) (hπ : ∀ (w : W), 0 < m.prior d w) {q : Q} {r : R} (hm : (m.R0Model h).marginal (m.prior d) q r ≠ 0) {w : W} : 0 < (m.R0Model h).posterior (m.prior d) q r w ↔ m.Admissible w q r

Under positive priors a world has positive posterior after a response iff the response is true and safe there.

theorem HawkinsEtAl2025.Model.posterior_lt_iff_card {W : Type u_1} {Q : Type u_2} {R : Type u_3} {A : Type u_4} {D : Type u_5} (m : Model W Q R A D) [(q : Q) → DecidablePred (m.question q)] [(r : R) → DecidablePred (m.response r)] [Fintype R] [Fintype W] (h : ∀ (w : W) (q : Q), 0 < m.admissibleCard w q) (d : D) (q : Q) (r : R) {w₁ w₂ : W} (hπ : ∀ (w : W), 0 ≤ m.prior d w) (hp : m.prior d w₁ = m.prior d w₂) (hpos : 0 < m.prior d w₁) (h₁ : m.Admissible w₁ q r) (h₂ : m.Admissible w₂ q r) (hm : (m.R0Model h).marginal (m.prior d) q r ≠ 0) : (m.R0Model h).posterior (m.prior d) q r w₁ < (m.R0Model h).posterior (m.prior d) q r w₂ ↔ m.admissibleCard w₂ q < m.admissibleCard w₁ q

The size principle (§2b): between two worlds of equal prior at which a response is true and safe, the posterior favours the world with fewer true and safe alternatives.

The questioner (§2b)

noncomputable def HawkinsEtAl2025.policy {W : Type u_1} {A : Type u_4} [Fintype W] [Fintype A] (U : W → A → ℝ) (αℵ : ℝ) (π : W → ℝ) : A → ℝ

(2.2): the policy of a decision problem under beliefs π, a softmax over expected utility with rationality αℵ.

Equations

• HawkinsEtAl2025.policy U αℵ π = Real.softmax fun (a : A) => αℵ * ∑ w : W, π w * U w a

noncomputable def HawkinsEtAl2025.value {W : Type u_1} {A : Type u_4} [Fintype W] [Fintype A] [Nonempty A] (U : W → A → ℝ) (αℵ : ℝ) (π : W → ℝ) : ℝ

The value V(D) of a decision problem: the expected utility of following its policy.

Equations

• HawkinsEtAl2025.value U αℵ π = ∑ a : A, HawkinsEtAl2025.policy U αℵ π a * ∑ w : W, π w * U w a

theorem HawkinsEtAl2025.expectedUtility_eq_of_support {W : Type u_1} {A : Type u_4} [Fintype W] {π : W → ℝ} {U : W → A → ℝ} {c : A → ℝ} (hsum : ∑ w : W, π w = 1) (hU : ∀ (w : W), π w ≠ 0 → ∀ (a : A), U w a = c a) (a : A) : ∑ w : W, π w * U w a = c a

Beliefs whose support sees a constant utility profile have that profile as expected utility.

theorem HawkinsEtAl2025.value_eq_of_support {W : Type u_1} {A : Type u_4} [Fintype W] [Fintype A] [Nonempty A] {π π' : W → ℝ} {U : W → A → ℝ} {c : A → ℝ} (αℵ : ℝ) (hsum : ∑ w : W, π w = 1) (hsum' : ∑ w : W, π' w = 1) (hU : ∀ (w : W), π w ≠ 0 → ∀ (a : A), U w a = c a) (hU' : ∀ (w : W), π' w ≠ 0 → ∀ (a : A), U w a = c a) : value U αℵ π = value U αℵ π'

Two beliefs seeing the same constant utility profile have the same value.

noncomputable def HawkinsEtAl2025.Model.questionScore {W : Type u_1} {Q : Type u_2} {R : Type u_3} {A : Type u_4} {D : Type u_5} (m : Model W Q R A D) [Fintype R] [Fintype W] [Fintype A] [Nonempty A] (om : ProbabilityTheory.ObservationModel W Q R) (αℵ wc : ℝ) (d : D) (q : Q) : ℝ

The expected value to the questioner of asking q (2.3): the expected value of the updated decision problem after the base respondent's answer, less the weighted cost.

Equations

• m.questionScore om αℵ wc d q = ∑ r : R, om.marginal (m.prior d) q r * (HawkinsEtAl2025.value (m.utility d) αℵ (om.posterior (m.prior d) q r) - wc * m.cost r)

theorem HawkinsEtAl2025.Model.questionScore_eq_eig {W : Type u_1} {Q : Type u_2} {R : Type u_3} {A : Type u_4} {D : Type u_5} (m : Model W Q R A D) [Fintype R] [Fintype W] [Fintype A] [Nonempty A] (om : ProbabilityTheory.ObservationModel W Q R) (αℵ wc : ℝ) (d : D) (q : Q) : m.questionScore om αℵ wc d q = om.eig (m.prior d) (value (m.utility d) αℵ) q + value (m.utility d) αℵ (m.prior d) - wc * ∑ r : R, om.marginal (m.prior d) q r * m.cost r

The question score is [Lin56]'s expected information gain of the question under the policy value, plus the value of the prior, less the expected cost.

noncomputable def HawkinsEtAl2025.Model.questioner {W : Type u_1} {Q : Type u_2} {R : Type u_3} {A : Type u_4} {D : Type u_5} (m : Model W Q R A D) [Fintype R] [Fintype W] [Fintype A] [Nonempty A] [Fintype Q] (om : ProbabilityTheory.ObservationModel W Q R) (αℵ wc αQ : ℝ) : Core.RationalAction D Q

(2.3): the questioner, a softmax over question scores with rationality αQ.

Equations

• m.questioner om αℵ wc αQ = Core.RationalAction.fromSoftmax (m.questionScore om αℵ wc) αQ

The pragmatic respondent (§2c)

noncomputable def HawkinsEtAl2025.Model.respondentPosterior {W : Type u_1} {Q : Type u_2} {R : Type u_3} {A : Type u_4} {D : Type u_5} (m : Model W Q R A D) [Fintype R] [Fintype W] [Fintype A] [Nonempty A] [Fintype Q] [Fintype D] (om : ProbabilityTheory.ObservationModel W Q R) (αℵ wc αQ : ℝ) (πD : D → ℝ) (q : Q) (d : D) : ℝ

The respondent's posterior over decision problems after hearing q: Bayesian theory of mind through the questioner, π(D ∣ q) ∝ Q(q ∣ D) π(D).

Equations

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

theorem HawkinsEtAl2025.Model.respondentPosterior_lt_iff {W : Type u_1} {Q : Type u_2} {R : Type u_3} {A : Type u_4} {D : Type u_5} (m : Model W Q R A D) [Fintype R] [Fintype W] [Fintype A] [Nonempty A] [Fintype Q] [Fintype D] (om : ProbabilityTheory.ObservationModel W Q R) (αℵ wc αQ : ℝ) (πD : D → ℝ) (hπ : ∀ (d : D), 0 ≤ πD d) (q : Q) {d₁ d₂ : D} (hp : πD d₁ = πD d₂) (hpos : 0 < πD d₁) (hz : ∑ d' : D, (m.questioner om αℵ wc αQ).policy d' q * πD d' ≠ 0) : m.respondentPosterior om αℵ wc αQ πD q d₁ < m.respondentPosterior om αℵ wc αQ πD q d₂ ↔ (m.questioner om αℵ wc αQ).policy d₁ q < (m.questioner om αℵ wc αQ).policy d₂ q

A question is a signal about the goal: with equal priors, the decision problem under which the question was the more probable is the more probable after it.

noncomputable def HawkinsEtAl2025.kl {W : Type u_1} [Fintype W] (p q : W → ℝ) : ℝ

The finite Kullback–Leibler divergence of beliefs, in the direction of (2.5).

Equations

• HawkinsEtAl2025.kl p q = ∑ w : W, p w * Real.log (p w / q w)

noncomputable def HawkinsEtAl2025.Model.singleScore {W : Type u_1} {Q : Type u_2} {R : Type u_3} {A : Type u_4} {D : Type u_5} (m : Model W Q R A D) [Fintype R] [Fintype W] [Fintype A] [Nonempty A] (om om' : ProbabilityTheory.ObservationModel W Q R) (αℵ wc β : ℝ) (πW : W → ℝ) (d : D) (q : Q) (r : R) : ℝ

The utility of a response under one decision problem (2.5): informativity weighted 1 − β, action relevance weighted β, less the weighted cost.

Equations

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

noncomputable def HawkinsEtAl2025.Model.respondentScore {W : Type u_1} {Q : Type u_2} {R : Type u_3} {A : Type u_4} {D : Type u_5} (m : Model W Q R A D) [Fintype R] [Fintype W] [Fintype A] [Nonempty A] [Fintype Q] [Fintype D] (om om' : ProbabilityTheory.ObservationModel W Q R) (αℵ wc αQ β : ℝ) (πD : D → ℝ) (πW : W → ℝ) (q : Q) (r : R) : ℝ

(2.5): the pragmatic respondent's score, the expected utility of a response over the inferred decision problem.

Equations

• m.respondentScore om om' αℵ wc αQ β πD πW q r = ∑ d : D, m.respondentPosterior om αℵ wc αQ πD q d * m.singleScore om om' αℵ wc β πW d q r

noncomputable def HawkinsEtAl2025.Model.respondent {W : Type u_1} {Q : Type u_2} {R : Type u_3} {A : Type u_4} {D : Type u_5} (m : Model W Q R A D) [Fintype R] [Fintype W] [Fintype A] [Nonempty A] [Fintype Q] [Fintype D] (om om' : ProbabilityTheory.ObservationModel W Q R) (αℵ wc αQ β αR : ℝ) (πD : D → ℝ) (πW : W → ℝ) : Core.RationalAction Q R

(2.5): the pragmatic respondent, a softmax over response scores with rationality αR.

Equations

• m.respondent om om' αℵ wc αQ β αR πD πW = Core.RationalAction.fromSoftmax (m.respondentScore om om' αℵ wc αQ β πD πW) αR

theorem HawkinsEtAl2025.Model.respondentScore_beta_one {W : Type u_1} {Q : Type u_2} {R : Type u_3} {A : Type u_4} {D : Type u_5} (m : Model W Q R A D) [Fintype R] [Fintype W] [Fintype A] [Nonempty A] [Fintype Q] [Fintype D] (om om' : ProbabilityTheory.ObservationModel W Q R) (αℵ wc αQ : ℝ) (πD : D → ℝ) (πW : W → ℝ) (q : Q) (r : R) : m.respondentScore om om' αℵ wc αQ 1 πD πW q r = ∑ d : D, m.respondentPosterior om αℵ wc αQ πD q d * (value (m.utility d) αℵ (om.posterior (m.prior d) q r) - wc * m.cost r)

At β = 1 the respondent weighs only action relevance and cost.

theorem HawkinsEtAl2025.Model.respondentScore_beta_zero {W : Type u_1} {Q : Type u_2} {R : Type u_3} {A : Type u_4} {D : Type u_5} (m : Model W Q R A D) [Fintype R] [Fintype W] [Fintype A] [Nonempty A] [Fintype Q] [Fintype D] (om om' : ProbabilityTheory.ObservationModel W Q R) (αℵ wc αQ : ℝ) (πD : D → ℝ) (πW : W → ℝ) (q : Q) (r : R) : m.respondentScore om om' αℵ wc αQ 0 πD πW q r = ∑ d : D, m.respondentPosterior om αℵ wc αQ πD q d * (-kl (om'.posterior (m.prior d) q r) πW - wc * m.cost r)

At β = 0 the respondent weighs only informativity and cost.

Case study 1: credit cards (§3a)

inductive HawkinsEtAl2025.Card : Type

The three cards.

• amex : Card
• mastercard : Card
• carteBlanche : Card

@[instance_reducible]

instance HawkinsEtAl2025.instDecidableEqCard : DecidableEq Card

Equations

• HawkinsEtAl2025.instDecidableEqCard x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance HawkinsEtAl2025.instFintypeCard : Fintype Card

Equations

• HawkinsEtAl2025.instFintypeCard = { elems := { val := ↑HawkinsEtAl2025.Card.enumList, nodup := HawkinsEtAl2025.Card.enumList_nodup }, complete := HawkinsEtAl2025.instFintypeCard._proof_1 }

def HawkinsEtAl2025.instReprCard.repr : Card → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• HawkinsEtAl2025.instReprCard.repr HawkinsEtAl2025.Card.amex prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HawkinsEtAl2025.Card.amex")).group prec✝

@[instance_reducible]

instance HawkinsEtAl2025.instReprCard : Repr Card

Equations

• HawkinsEtAl2025.instReprCard = { reprPrec := HawkinsEtAl2025.instReprCard.repr }

inductive HawkinsEtAl2025.Act : Type

The questioner's actions.

• stay : Act
• go : Act

@[instance_reducible]

instance HawkinsEtAl2025.instDecidableEqAct : DecidableEq Act

Equations

• HawkinsEtAl2025.instDecidableEqAct x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance HawkinsEtAl2025.instFintypeAct : Fintype Act

Equations

• HawkinsEtAl2025.instFintypeAct = { elems := { val := ↑HawkinsEtAl2025.Act.enumList, nodup := HawkinsEtAl2025.Act.enumList_nodup }, complete := HawkinsEtAl2025.instFintypeAct._proof_1 }

@[instance_reducible]

instance HawkinsEtAl2025.instReprAct : Repr Act

Equations

• HawkinsEtAl2025.instReprAct = { reprPrec := HawkinsEtAl2025.instReprAct.repr }

def HawkinsEtAl2025.instReprAct.repr : Act → ℕ → Std.Format

Equations

• HawkinsEtAl2025.instReprAct.repr HawkinsEtAl2025.Act.stay prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HawkinsEtAl2025.Act.stay")).group prec✝
• HawkinsEtAl2025.instReprAct.repr HawkinsEtAl2025.Act.go prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HawkinsEtAl2025.Act.go")).group prec✝

@[instance_reducible]

instance HawkinsEtAl2025.instInhabitedAct : Inhabited Act

Equations

• HawkinsEtAl2025.instInhabitedAct = { default := HawkinsEtAl2025.instInhabitedAct.default }

inductive HawkinsEtAl2025.Resp : Type

The responses: a polar answer to whether any card of S is accepted, the mention of some accepted cards, or the exhaustive list of the accepted cards.

• polar (S : Finset Card) (b : Bool) : Resp
• mention (T : Finset Card) : Resp
• exhaustive (T : Finset Card) : Resp

def HawkinsEtAl2025.instDecidableEqResp.decEq (x✝ x✝¹ : Resp) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• HawkinsEtAl2025.instDecidableEqResp.decEq (HawkinsEtAl2025.Resp.polar S b) (HawkinsEtAl2025.Resp.mention T) = isFalse ⋯
• HawkinsEtAl2025.instDecidableEqResp.decEq (HawkinsEtAl2025.Resp.polar S b) (HawkinsEtAl2025.Resp.exhaustive T) = isFalse ⋯
• HawkinsEtAl2025.instDecidableEqResp.decEq (HawkinsEtAl2025.Resp.mention T) (HawkinsEtAl2025.Resp.polar S b) = isFalse ⋯
• HawkinsEtAl2025.instDecidableEqResp.decEq (HawkinsEtAl2025.Resp.mention a) (HawkinsEtAl2025.Resp.mention b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• HawkinsEtAl2025.instDecidableEqResp.decEq (HawkinsEtAl2025.Resp.mention T) (HawkinsEtAl2025.Resp.exhaustive T_1) = isFalse ⋯
• HawkinsEtAl2025.instDecidableEqResp.decEq (HawkinsEtAl2025.Resp.exhaustive T) (HawkinsEtAl2025.Resp.polar S b) = isFalse ⋯
• HawkinsEtAl2025.instDecidableEqResp.decEq (HawkinsEtAl2025.Resp.exhaustive T) (HawkinsEtAl2025.Resp.mention T_1) = isFalse ⋯
• HawkinsEtAl2025.instDecidableEqResp.decEq (HawkinsEtAl2025.Resp.exhaustive a) (HawkinsEtAl2025.Resp.exhaustive b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance HawkinsEtAl2025.instDecidableEqResp : DecidableEq Resp

Equations

• HawkinsEtAl2025.instDecidableEqResp = HawkinsEtAl2025.instDecidableEqResp.decEq

@[instance_reducible]

instance HawkinsEtAl2025.instFintypeResp : Fintype Resp

Equations

• HawkinsEtAl2025.instFintypeResp = Fintype.ofEquiv ((_ : Finset HawkinsEtAl2025.Card) × Bool ⊕ Finset HawkinsEtAl2025.Card ⊕ Finset HawkinsEtAl2025.Card) HawkinsEtAl2025.Resp.proxyTypeEquiv

inductive HawkinsEtAl2025.Goal : Type

The decision problems: U1, whether any of the questioner's cards C is accepted, and U2, whether any card is accepted.

• ownCards (C : Finset Card) : Goal
• anyCard : Goal

def HawkinsEtAl2025.instDecidableEqGoal.decEq (x✝ x✝¹ : Goal) : Decidable (x✝ = x✝¹)

Equations

• HawkinsEtAl2025.instDecidableEqGoal.decEq (HawkinsEtAl2025.Goal.ownCards a) (HawkinsEtAl2025.Goal.ownCards b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• HawkinsEtAl2025.instDecidableEqGoal.decEq (HawkinsEtAl2025.Goal.ownCards C) HawkinsEtAl2025.Goal.anyCard = isFalse ⋯
• HawkinsEtAl2025.instDecidableEqGoal.decEq HawkinsEtAl2025.Goal.anyCard (HawkinsEtAl2025.Goal.ownCards C) = isFalse ⋯
• HawkinsEtAl2025.instDecidableEqGoal.decEq HawkinsEtAl2025.Goal.anyCard HawkinsEtAl2025.Goal.anyCard = isTrue ⋯

@[instance_reducible]

instance HawkinsEtAl2025.instDecidableEqGoal : DecidableEq Goal

Equations

• HawkinsEtAl2025.instDecidableEqGoal = HawkinsEtAl2025.instDecidableEqGoal.decEq

@[instance_reducible]

instance HawkinsEtAl2025.instFintypeGoal : Fintype Goal

Equations

• HawkinsEtAl2025.instFintypeGoal = Fintype.ofEquiv (Finset HawkinsEtAl2025.Card ⊕ Unit) HawkinsEtAl2025.Goal.proxyTypeEquiv

def HawkinsEtAl2025.cardUtility : Goal → Finset Card → Act → ℝ

The utility of §3a: 5 for going when a relevant card is accepted or staying when none is, 0 otherwise.

Equations

• HawkinsEtAl2025.cardUtility (HawkinsEtAl2025.Goal.ownCards C) x✝ HawkinsEtAl2025.Act.go = if (C ∩ x✝).Nonempty then 5 else 0
• HawkinsEtAl2025.cardUtility (HawkinsEtAl2025.Goal.ownCards C) x✝ HawkinsEtAl2025.Act.stay = if (C ∩ x✝).Nonempty then 0 else 5
• HawkinsEtAl2025.cardUtility HawkinsEtAl2025.Goal.anyCard x✝ HawkinsEtAl2025.Act.go = if x✝.Nonempty then 5 else 0
• HawkinsEtAl2025.cardUtility HawkinsEtAl2025.Goal.anyCard x✝ HawkinsEtAl2025.Act.stay = if x✝.Nonempty then 0 else 5

def HawkinsEtAl2025.respProp : Resp → Finset Card → Prop

The proposition a response asserts.

Equations

• HawkinsEtAl2025.respProp (HawkinsEtAl2025.Resp.polar S b) x✝ = ((S ∩ x✝).Nonempty ↔ b = true)
• HawkinsEtAl2025.respProp (HawkinsEtAl2025.Resp.mention T) x✝ = (T ⊆ x✝)
• HawkinsEtAl2025.respProp (HawkinsEtAl2025.Resp.exhaustive T) x✝ = (T = x✝)

@[instance_reducible]

instance HawkinsEtAl2025.instDecidablePredFinsetCardRespProp (r : Resp) : DecidablePred (respProp r)

Equations

• HawkinsEtAl2025.instDecidablePredFinsetCardRespProp (HawkinsEtAl2025.Resp.polar S b) x✝ = HawkinsEtAl2025.instDecidablePredFinsetCardRespProp._aux_1 S b x✝
• HawkinsEtAl2025.instDecidablePredFinsetCardRespProp (HawkinsEtAl2025.Resp.mention T) x✝ = HawkinsEtAl2025.instDecidablePredFinsetCardRespProp._aux_3 T x✝
• HawkinsEtAl2025.instDecidablePredFinsetCardRespProp (HawkinsEtAl2025.Resp.exhaustive T) x✝ = HawkinsEtAl2025.instDecidablePredFinsetCardRespProp._aux_5 T x✝

noncomputable def HawkinsEtAl2025.cards : Model (Finset Card) (Finset Card) Resp Act Goal

The credit-card model: a question asks whether any card of a set is accepted, worlds are the sets of accepted cards, priors are uniform over the eight worlds, and a response costs the cards it mentions.

Equations

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

@[instance_reducible]

instance HawkinsEtAl2025.instDecidablePredFinsetCardQuestionRespActGoalCards (S : Finset Card) : DecidablePred (cards.question S)

Equations

• HawkinsEtAl2025.instDecidablePredFinsetCardQuestionRespActGoalCards S w = HawkinsEtAl2025.instDecidablePredFinsetCardQuestionRespActGoalCards._aux_1 S w

@[instance_reducible]

instance HawkinsEtAl2025.instDecidablePredFinsetCardResponseRespActGoalCards (r : Resp) : DecidablePred (cards.response r)

Equations

• HawkinsEtAl2025.instDecidablePredFinsetCardResponseRespActGoalCards r = HawkinsEtAl2025.instDecidablePredFinsetCardResponseRespActGoalCards._aux_1 r

theorem HawkinsEtAl2025.polar_exhaustive_safe : (∀ (S : Finset Card) (b : Bool), Safe (cards.question S) (cards.response (Resp.polar S b))) ∧ ∀ (S T : Finset Card), Safe (cards.question S) (cards.response (Resp.exhaustive T))

Polar answers to the question asked are safe, as are exhaustive lists.

theorem HawkinsEtAl2025.mention_safe_iff (S T : Finset Card) (hS : S.Nonempty) : Safe (cards.question S) (cards.response (Resp.mention T)) ↔ (T ∩ S).Nonempty

Mentioning accepted cards is safe for a question exactly when one of them was asked about: in (2), naming a third card after a question about two others is not.

theorem HawkinsEtAl2025.polar_admissible (w q : Finset Card) : 0 < cards.admissibleCard w q

Every world admits a true and safe response to every question: the true polar answer.

noncomputable def HawkinsEtAl2025.cardsModel : ProbabilityTheory.ObservationModel (Finset Card) (Finset Card) Resp

The base respondent as an observation model for the credit cards.

Equations

• HawkinsEtAl2025.cardsModel = HawkinsEtAl2025.cards.R0Model HawkinsEtAl2025.polar_admissible

theorem HawkinsEtAl2025.yes_value_eq_exhaustive (C w : Finset Card) (hC : Card.amex ∈ C) (hw : Card.amex ∈ w) (αℵ : ℝ) : value (cards.utility (Goal.ownCards C)) αℵ (cardsModel.posterior (cards.prior (Goal.ownCards C)) {Card.amex} (Resp.polar {Card.amex} true)) = value (cards.utility (Goal.ownCards C)) αℵ (cardsModel.posterior (cards.prior (Goal.ownCards C)) {Card.amex} (Resp.exhaustive w))

(3): for a questioner holding the card asked about, after the answer "yes" the value of the decision problem already equals its value after the exhaustive list, since every world compatible with either answer accepts a card the questioner holds; only the cost separates the two answers.

theorem HawkinsEtAl2025.generalYes_posterior_pos : 0 < cardsModel.posterior (cards.prior (Goal.ownCards {Card.amex})) Finset.univ (Resp.polar Finset.univ true) {Card.mastercard} ∧ cardsModel.posterior (cards.prior (Goal.ownCards {Card.amex})) {Card.amex} (Resp.polar {Card.amex} true) {Card.mastercard} = 0

(5): after "yes" to the general question, a world accepting only MasterCard keeps positive posterior, so a questioner holding American Express remains uncertain; after "yes" to the question about American Express it does not.