Chung and Mascarenhas 2023: Modality, expected utility, and hypothesis testing

Necessity modals share one semantics over a family R of relevant propositions: must φ holds when the expectation, given φ, of the number μ_R of propositions in R that are true exceeds a threshold θ while no alternative's does (6); read deontically the expectation is φ's expected utility, read epistemically its explanatory value, the sum of the likelihoods of the evidence (12), and ought φ asks instead that φ be strictly best among the good-enough (17). In [kolodny-macfarlane-2010]'s miners puzzle (§3.1) blocking neither shaft is the only good-enough option for a threshold between 5 and 9 (26), but once the miners are known to be in shaft A the conditional must needs one between 9 and 10 (25b), an incompatibility the paper notes; the modal conjunction fallacy ([tversky-kahneman-1983], §3.2) and modal base-rate neglect ([kahneman-tversky-1973], §3.3) come out true for thresholds between the hypotheses' explanatory values ((34), (41)); and the Korean conditional evaluative cip-ey iss-eya toy-n-ta composes the evaluative predicate, the conditional, Lassiter's threshold and the -(e)ya exhaustifier into exactly (6) (§4, (48)).

mustCM, oughtCM and mustCMWithPlausibility are (6), (17) and the §5 plausibility patch over the substrate's sumLikelihoods, and koreanConditionalEvaluative_iff_mustCM is (48) by the identity condExpect_countMeasure. The miners puzzle is built from Table 1 with the ideals (18) of [cariani-kaufmann-kaufmann-2013] as an indexed family, and its expected utilities, ought and must claims and threshold incompatibility are derived from the uniform prior; modal Linda and modal Lawyers keep the paper's stipulated conditional probabilities as rationals, the text fixing no joint distribution.

References

• [W. Chung and S. Mascarenhas, Modality, expected utility, and hypothesis testing (2023)][chung-mascarenhas-2023]
• [N. Kolodny and J. MacFarlane, Ifs and oughts (2010)][kolodny-macfarlane-2010]
• [F. Cariani, M. Kaufmann and S. Kaufmann, Deliberative modality under epistemic uncertainty (2013)][cariani-kaufmann-kaufmann-2013]
• [A. Tversky and D. Kahneman, Extensional Versus Intuitive Reasoning: The Conjunction Fallacy in Probability Judgment (1983)][tversky-kahneman-1983]
• [D. Kahneman and A. Tversky, On the psychology of prediction (1973)][kahneman-tversky-1973]

The operators

def ChungMascarenhas2023.mustCM {W : Type u_1} {ι : Type u_2} [Fintype ι] (p : PMF W) (R : ι → Set W) (φ : Set W) (alts : Set (Set W)) (θ : ENNReal) : Prop

(6): must φ iff the expected μ_R given φ exceeds the threshold θ and no alternative's does, φ being the only good-enough option or explanation.

Equations

• ChungMascarenhas2023.mustCM p R φ alts θ = (PMF.Confirmation.sumLikelihoods p R φ > θ ∧ ∀ ψ ∈ alts, PMF.Confirmation.sumLikelihoods p R ψ ≤ θ)

def ChungMascarenhas2023.oughtCM {W : Type u_1} {ι : Type u_2} [Fintype ι] (p : PMF W) (R : ι → Set W) (φ : Set W) (alts : Set (Set W)) (θ : ENNReal) : Prop

(17): ought φ iff φ is the best good-enough option, above θ and of strictly greater expected value than every alternative.

Equations

• ChungMascarenhas2023.oughtCM p R φ alts θ = (PMF.Confirmation.sumLikelihoods p R φ > θ ∧ ∀ ψ ∈ alts, PMF.Confirmation.sumLikelihoods p R ψ < PMF.Confirmation.sumLikelihoods p R φ)

def ChungMascarenhas2023.mustCMWithPlausibility {W : Type u_1} {ι : Type u_2} [Fintype ι] (p : PMF W) (R : ι → Set W) (φ : Set W) (alts : Set (Set W)) (θ θplaus : ENNReal) : Prop

§5: mustCM with the plausibility requirement of a reasonably high prior for the prejacent, kept separate as the paper presents it as an add-on.

Equations

• ChungMascarenhas2023.mustCMWithPlausibility p R φ alts θ θplaus = (ChungMascarenhas2023.mustCM p R φ alts θ ∧ θplaus ≤ p.probOfSet φ)

Korean conditional evaluatives (§4)

def ChungMascarenhas2023.koreanConditionalEvaluative {W : Type u_1} [Fintype W] {ι : Type u_2} [Fintype ι] (p : PMF W) (R : ι → Set W) (φ : Set W) (alts : Set (Set W)) (θ : ENNReal) : Prop

(48), left-hand side, the composition of cip-ey iss-eya toy-n-ta: Lassiter's threshold Θ (46) applied to the conditional if φ, then eval ((45), condIf over μ_R), with the -(e)ya exhaustifier negating each alternative's thresholded conditional.

Equations

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

theorem ChungMascarenhas2023.koreanConditionalEvaluative_iff_mustCM {W : Type u_1} [Fintype W] {ι : Type u_2} [Fintype ι] (p : PMF W) (R : ι → Set W) (φ : Set W) (alts : Set (Set W)) (θ : ENNReal) : koreanConditionalEvaluative p R φ alts θ ↔ mustCM p R φ alts θ

(48): the Korean composition is the must semantics (6), by the identity condExpect_countMeasure between the conditional's expected μ_R (45) and the sum of likelihoods (12).

The miners puzzle (§3.1)

@[reducible, inline]

abbrev ChungMascarenhas2023.Miners.World : Type

The six action-by-location worlds of Table 1: 0 block A with the miners in A, 1 block A with them in B, 2 block B with them in A, 3 block B with them in B, 4 and 5 block neither.

Equations

• ChungMascarenhas2023.Miners.World = Fin 6

def ChungMascarenhas2023.Miners.blockA : Set World

Block shaft A.

Equations

• ChungMascarenhas2023.Miners.blockA = {w : ChungMascarenhas2023.Miners.World | ↑w = 0 ∨ ↑w = 1}

def ChungMascarenhas2023.Miners.blockB : Set World

Block shaft B.

Equations

• ChungMascarenhas2023.Miners.blockB = {w : ChungMascarenhas2023.Miners.World | ↑w = 2 ∨ ↑w = 3}

def ChungMascarenhas2023.Miners.blockNeither : Set World

Block neither shaft.

Equations

• ChungMascarenhas2023.Miners.blockNeither = {w : ChungMascarenhas2023.Miners.World | ↑w = 4 ∨ ↑w = 5}

def ChungMascarenhas2023.Miners.minersInA : Set World

The miners are in shaft A.

Equations

• ChungMascarenhas2023.Miners.minersInA = {w : ChungMascarenhas2023.Miners.World | ↑w = 0 ∨ ↑w = 2 ∨ ↑w = 4}

def ChungMascarenhas2023.Miners.minersInB : Set World

The miners are in shaft B.

Equations

• ChungMascarenhas2023.Miners.minersInB = {w : ChungMascarenhas2023.Miners.World | ↑w = 1 ∨ ↑w = 3 ∨ ↑w = 5}

def ChungMascarenhas2023.Miners.minersSaved : World → ℕ

Miners saved at each world (Table 1): all ten at 0 and 3, none at 1 and 2, nine at 4 and 5.

Equations

• ChungMascarenhas2023.Miners.minersSaved w = match ↑w with | 0 => 10 | 1 => 0 | 2 => 0 | 3 => 10 | 4 => 9 | 5 => 9 | x => 0

noncomputable def ChungMascarenhas2023.Miners.prior : PMF World

The uniform prior: the locations equiprobable and independent of the action.

Equations

• ChungMascarenhas2023.Miners.prior = PMF.uniformOfFintype ChungMascarenhas2023.Miners.World

def ChungMascarenhas2023.Miners.idealsRD : Fin 10 → Set World

(18), from [cariani-kaufmann-kaufmann-2013]: R_D = {one miner saved, …, ten miners saved}, an indexed family since distinct ideals coincide in extension on six worlds.

Equations

• ChungMascarenhas2023.Miners.idealsRD k = {w : ChungMascarenhas2023.Miners.World | ↑k < ChungMascarenhas2023.Miners.minersSaved w}

@[instance_reducible]

instance ChungMascarenhas2023.Miners.instDecidablePredWorldMemSetBlockA : DecidablePred fun (x : World) => x ∈ blockA

Equations

• ChungMascarenhas2023.Miners.instDecidablePredWorldMemSetBlockA w = ChungMascarenhas2023.Miners.instDecidablePredWorldMemSetBlockA._aux_1 w

@[instance_reducible]

instance ChungMascarenhas2023.Miners.instDecidablePredWorldMemSetBlockB : DecidablePred fun (x : World) => x ∈ blockB

Equations

• ChungMascarenhas2023.Miners.instDecidablePredWorldMemSetBlockB w = ChungMascarenhas2023.Miners.instDecidablePredWorldMemSetBlockB._aux_1 w

@[instance_reducible]

instance ChungMascarenhas2023.Miners.instDecidablePredWorldMemSetBlockNeither : DecidablePred fun (x : World) => x ∈ blockNeither

Equations

• ChungMascarenhas2023.Miners.instDecidablePredWorldMemSetBlockNeither w = ChungMascarenhas2023.Miners.instDecidablePredWorldMemSetBlockNeither._aux_1 w

@[instance_reducible]

instance ChungMascarenhas2023.Miners.instDecidablePredWorldMemSetMinersInA : DecidablePred fun (x : World) => x ∈ minersInA

Equations

• ChungMascarenhas2023.Miners.instDecidablePredWorldMemSetMinersInA w = ChungMascarenhas2023.Miners.instDecidablePredWorldMemSetMinersInA._aux_1 w

@[instance_reducible]

instance ChungMascarenhas2023.Miners.instDecidablePredWorldMemSetMinersInB : DecidablePred fun (x : World) => x ∈ minersInB

Equations

• ChungMascarenhas2023.Miners.instDecidablePredWorldMemSetMinersInB w = ChungMascarenhas2023.Miners.instDecidablePredWorldMemSetMinersInB._aux_1 w

@[instance_reducible]

instance ChungMascarenhas2023.Miners.instDecidablePredWorldMemSetIdealsRD (k : Fin 10) : DecidablePred fun (x : World) => x ∈ idealsRD k

Equations

• ChungMascarenhas2023.Miners.instDecidablePredWorldMemSetIdealsRD k w = ChungMascarenhas2023.Miners.instDecidablePredWorldMemSetIdealsRD._aux_1 k w

theorem ChungMascarenhas2023.Miners.countMeasure_idealsRD (w : World) : PMF.Confirmation.countMeasure idealsRD w = ↑(minersSaved w)

μ_{R_D} counts miners saved: each world abides by exactly minersSaved w of the ten ideals.

theorem ChungMascarenhas2023.Miners.ev_blockNeither : PMF.Confirmation.sumLikelihoods prior idealsRD blockNeither = 9

(19): blocking neither shaft has expected utility 9.

theorem ChungMascarenhas2023.Miners.ev_blockA : PMF.Confirmation.sumLikelihoods prior idealsRD blockA = 5

(20): blocking shaft A has expected utility 5.

theorem ChungMascarenhas2023.Miners.ev_blockB : PMF.Confirmation.sumLikelihoods prior idealsRD blockB = 5

(21): blocking shaft B has expected utility 5.

theorem ChungMascarenhas2023.Miners.ev_inA_blockA : PMF.Confirmation.sumLikelihoods prior idealsRD (minersInA ∩ blockA) = 10

(23): conditionalized on the miners being in A, blocking A has expected utility 10.

theorem ChungMascarenhas2023.Miners.ev_inA_blockNeither : PMF.Confirmation.sumLikelihoods prior idealsRD (minersInA ∩ blockNeither) = 9

Conditionalized on the miners being in A, blocking neither still has expected utility 9: one miner drowns whatever their location.

theorem ChungMascarenhas2023.Miners.ev_inA_blockB : PMF.Confirmation.sumLikelihoods prior idealsRD (minersInA ∩ blockB) = 0

Conditionalized on the miners being in A, blocking B has expected utility 0.

theorem ChungMascarenhas2023.Miners.ought_blockNeither {θ : ENNReal} (hθ : θ < 9) : oughtCM prior idealsRD blockNeither {blockA, blockB} θ

(22): we ought to block neither shaft, for any θ < 9.

theorem ChungMascarenhas2023.Miners.ought_if_inA_blockA {θ : ENNReal} (hθ : θ < 10) : oughtCM prior idealsRD (minersInA ∩ blockA) {minersInA ∩ blockNeither, minersInA ∩ blockB} θ

(24): if the miners are in shaft A, we ought to block shaft A, the if-clause conditionalizing every expected utility on its antecedent (fn. 16, after Lassiter), for any θ < 10.

theorem ChungMascarenhas2023.Miners.must_blockNeither {θ : ENNReal} (h5 : 5 ≤ θ) (h9 : θ < 9) : mustCM prior idealsRD blockNeither {blockA, blockB} θ

(26): we must block neither shaft for 5 ≤ θ < 9, blocking neither being the only good-enough option.

theorem ChungMascarenhas2023.Miners.must_if_inA_blockA {θ : ENNReal} (h9 : 9 ≤ θ) (h10 : θ < 10) : mustCM prior idealsRD (minersInA ∩ blockA) {minersInA ∩ blockNeither, minersInA ∩ blockB} θ

(25b) as must: conditionalized on the miners being in A, blocking A is the only good-enough option for 9 ≤ θ < 10, blocking neither sitting at 9.

theorem ChungMascarenhas2023.Miners.must_thresholds_incompatible : ¬∃ (θ : ENNReal), mustCM prior idealsRD blockNeither {blockA, blockB} θ ∧ mustCM prior idealsRD (minersInA ∩ blockA) {minersInA ∩ blockNeither, minersInA ∩ blockB} θ

(26) needs θ < 9 while (25b) needs 9 ≤ θ: no single threshold verifies both must claims.

Modal Linda (§3.2)

def ChungMascarenhas2023.ModalLinda.prSocialJusticeGivenTeller : ℚ

(30): P(social justice ∣ teller) = 0.3.

Equations

• ChungMascarenhas2023.ModalLinda.prSocialJusticeGivenTeller = 3 / 10

def ChungMascarenhas2023.ModalLinda.prAntiNuclearGivenTeller : ℚ

(30): P(anti-nuclear protests ∣ teller) = 0.2.

Equations

• ChungMascarenhas2023.ModalLinda.prAntiNuclearGivenTeller = 2 / 10

def ChungMascarenhas2023.ModalLinda.prSocialJusticeGivenFeministTeller : ℚ

(31): P(social justice ∣ feminist teller) = 0.8.

Equations

• ChungMascarenhas2023.ModalLinda.prSocialJusticeGivenFeministTeller = 8 / 10

def ChungMascarenhas2023.ModalLinda.prAntiNuclearGivenFeministTeller : ℚ

(31): P(anti-nuclear protests ∣ feminist teller) = 0.7.

Equations

• ChungMascarenhas2023.ModalLinda.prAntiNuclearGivenFeministTeller = 7 / 10

def ChungMascarenhas2023.ModalLinda.explanatoryValueTeller : ℚ

(32): E[μ_R ∣ teller] = 0.5.

Equations

• ChungMascarenhas2023.ModalLinda.explanatoryValueTeller = ChungMascarenhas2023.ModalLinda.prSocialJusticeGivenTeller + ChungMascarenhas2023.ModalLinda.prAntiNuclearGivenTeller

def ChungMascarenhas2023.ModalLinda.explanatoryValueFeministTeller : ℚ

(33): E[μ_R ∣ feminist teller] = 1.5.

Equations

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

theorem ChungMascarenhas2023.ModalLinda.modal_conjunction_fallacy {θ : ℚ} (h₀ : 1 / 2 ≤ θ) (h₁ : θ < 3 / 2) : explanatoryValueFeministTeller > θ ∧ explanatoryValueTeller ≤ θ

(34), the modal conjunction fallacy: for any threshold in [1/2, 3/2), Linda must be a feminist bank teller is true and Linda must be a bank teller false.

Modal Lawyers and Engineers (§3.3)

def ChungMascarenhas2023.ModalLawyers.prNotPoliticalGivenEngineer : ℚ

(37): P(no interest in political and social issues ∣ engineer) = 0.78.

Equations

• ChungMascarenhas2023.ModalLawyers.prNotPoliticalGivenEngineer = 78 / 100

def ChungMascarenhas2023.ModalLawyers.prMathGivenEngineer : ℚ

(37): P(enjoys mathematical puzzles ∣ engineer) = 0.55.

Equations

• ChungMascarenhas2023.ModalLawyers.prMathGivenEngineer = 55 / 100

def ChungMascarenhas2023.ModalLawyers.prNotPoliticalGivenLawyer : ℚ

(38): P(no interest in political and social issues ∣ lawyer) = 0.35.

Equations

• ChungMascarenhas2023.ModalLawyers.prNotPoliticalGivenLawyer = 35 / 100

def ChungMascarenhas2023.ModalLawyers.prMathGivenLawyer : ℚ

(38): P(enjoys mathematical puzzles ∣ lawyer) = 0.28.

Equations

• ChungMascarenhas2023.ModalLawyers.prMathGivenLawyer = 28 / 100

def ChungMascarenhas2023.ModalLawyers.explanatoryValueEngineer : ℚ

(39): E[μ_R ∣ engineer] = 1.33.

Equations

• ChungMascarenhas2023.ModalLawyers.explanatoryValueEngineer = ChungMascarenhas2023.ModalLawyers.prNotPoliticalGivenEngineer + ChungMascarenhas2023.ModalLawyers.prMathGivenEngineer

def ChungMascarenhas2023.ModalLawyers.explanatoryValueLawyer : ℚ

(40): E[μ_R ∣ lawyer] = 0.63.

Equations

• ChungMascarenhas2023.ModalLawyers.explanatoryValueLawyer = ChungMascarenhas2023.ModalLawyers.prNotPoliticalGivenLawyer + ChungMascarenhas2023.ModalLawyers.prMathGivenLawyer

theorem ChungMascarenhas2023.ModalLawyers.base_rate_neglect {θ : ℚ} (h₀ : 63 / 100 ≤ θ) (h₁ : θ < 133 / 100) : explanatoryValueEngineer > θ ∧ explanatoryValueLawyer ≤ θ

(41), base-rate neglect: for any threshold in [0.63, 1.33), Jack must be an engineer is true whatever the prior split, explanatory value conditioning only on the hypotheses.