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

This file formalizes the semantics of necessity modals as expected value that Chung and Mascarenhas propose, together with its applications to the miners puzzle and to two reasoning fallacies, and the derivations the paper runs against the rival accounts.

Necessity modals share one semantics over a family R of relevant propositions: expectedValue is the conditional expectation of the number countTrue R of relevant propositions true at a world ((5) and (7)), equal to the sum of the likelihoods of the evidence (12), and must φ holds when φ's expected value alone clears a threshold θ (6). Read deontically the expectation is φ's expected utility, read epistemically its explanatory value; ought φ asks instead that φ be strictly best among the good-enough (17) and follows from must φ (ought_of_must); might is must's dual with the polar alternative (59); and the §5 plausibility patch mustPlausible adds a reasonably high prior for the prejacent. A prejacent entailing all its evidence has maximal explanatory value (expectedValue_eq_card_of_subset), the §7 question-begging P(φ ∣ φ) and the §5 problem of success, and the deontic reading is Lassiter's expected-value scale (toReal_expectedValue), the paper's "reproduction of Lassiter's analysis". The Korean conditional evaluative cip-ey iss-eya toy-n-ta composes the evaluative predicate, the conditional, Lassiter's threshold (46) and the -(e)ya exhaustifier into exactly (6) (§4, (48)).

In the miners puzzle of Kolodny and MacFarlane (§3.1), stated over any measure satisfying the paper's assumptions (equiprobable locations independent of the action, with uniformOn as witness) and the ideals (18) of Cariani, Kaufmann and Kaufmann, blocking neither shaft is the only good-enough option for a threshold between 5 and 9 (26a), the conditional must needs one between 9 and 10 (25b), and no single threshold serves both (must_thresholds_incompatible); kratzer_miners_unsatisfiable is the paper's proof sketch (16) that no ordering source lets the classical account verify all of (15a)–(15c), and expectedValue_inA_lt_inA_blockNeither is footnote 17's observation that blocking neither stays above the expected utility of indifference. The modal conjunction fallacy (34) and modal base-rate neglect (41) are theorems about must over every measure realizing the paper's printed conditional probabilities, each with a finite witness model; the Kratzer row of Table 2 is Modality.necessity_and_left, conjunction elimination, which the expected-value must escapes.

Implementation notes

• The paper world-indexes the probability function Pr_w (its fn 9); the formalization fixes a single measure, as no formalized claim varies the evaluation world.
• Alternative sets are explicit Set (Set W) arguments (the paper's fn 8 leaves their source to the question under discussion); might hard-codes the polar alternative, following §6.
• Printed probabilities enter as hypotheses on conditional measures, decimals as ENNReal.ofReal values and the miners' utilities as exact numerals; no parallel rational arithmetic.
• The alternative log-likelihood formulation ((13)–(14)) and its might variant are not formalized: the paper sets them aside after noting (6) suffices.

References

• W. Chung and S. Mascarenhas, Modality, expected utility, and hypothesis testing (2023)
• N. Kolodny and J. MacFarlane, Ifs and oughts (2010)
• F. Cariani, M. Kaufmann and S. Kaufmann, Deliberative modality under epistemic uncertainty (2013)
• A. Kratzer, Modality (1991)
• D. Lassiter, Measurement and Modality (2011)
• D. Lassiter, Graded Modality (2017)
• K. von Fintel and S. Iatridou, What to do if you want to go to Harlem (2005)
• A. Tversky and D. Kahneman, Extensional Versus Intuitive Reasoning: The Conjunction Fallacy in Probability Judgment (1983)
• D. Kahneman and A. Tversky, On the psychology of prediction (1973)

The measure function and expected value

noncomputable def ChungMascarenhas2023.countTrue {W : Type u_1} {ι : Type u_2} [Fintype ι] (R : ι → Set W) : W → ENNReal

The measure function μ_EVAL gives the number of relevant propositions R i true at a world, as the sum of their indicators (7). The relevant propositions are an indexed family and not a finite set of propositions, so that extensionally coincident rules keep their multiplicity.

Equations

• ChungMascarenhas2023.countTrue R = ∑ i : ι, (R i).indicator 1

@[simp]

theorem ChungMascarenhas2023.countTrue_apply {W : Type u_1} {ι : Type u_2} [Fintype ι] (R : ι → Set W) (a : W) [(i : ι) → Decidable (a ∈ R i)] : countTrue R a = ↑{x : ι | a ∈ R x}.card

μ_EVAL at a world is the cardinality of the set of relevant propositions true there.

noncomputable def ChungMascarenhas2023.expectedValue {W : Type u_1} [MeasurableSpace W] {ι : Type u_2} [Fintype ι] (p : MeasureTheory.Measure W) (R : ι → Set W) (φ : Set W) : ENNReal

The expected value of φ is the conditional expectation of μ_EVAL given φ (5), expected utility read deontically and explanatory value read epistemically.

Equations

• ChungMascarenhas2023.expectedValue p R φ = ∫⁻ (w : W), ChungMascarenhas2023.countTrue R w ∂p[|φ]

theorem ChungMascarenhas2023.expectedValue_eq_sum_cond {W : Type u_1} [MeasurableSpace W] [DiscreteMeasurableSpace W] {ι : Type u_2} [Fintype ι] (p : MeasureTheory.Measure W) (R : ι → Set W) (φ : Set W) : expectedValue p R φ = ∑ i : ι, p[R i | φ]

The expected value of a hypothesis is the sum Σ_i P(R i ∣ φ) of the likelihoods of the relevant propositions (12).

theorem ChungMascarenhas2023.expectedValue_le_card {W : Type u_1} [MeasurableSpace W] [DiscreteMeasurableSpace W] {ι : Type u_2} [Fintype ι] (p : MeasureTheory.Measure W) (R : ι → Set W) (φ : Set W) : expectedValue p R φ ≤ ↑(Fintype.card ι)

Expected value never exceeds the number of relevant propositions.

theorem ChungMascarenhas2023.expectedValue_eq_card_of_subset {W : Type u_1} [MeasurableSpace W] [DiscreteMeasurableSpace W] {ι : Type u_2} [Fintype ι] (p : MeasureTheory.Measure W) [MeasureTheory.IsFiniteMeasure p] (R : ι → Set W) (φ : Set W) (hφ : p φ ≠ 0) (h : ∀ (i : ι), φ ⊆ R i) : expectedValue p R φ = ↑(Fintype.card ι)

A prejacent entailing every piece of evidence has maximal explanatory value: each P(R i ∣ φ) is the question-begging P(φ ∣ φ), "as high as any probability can get" (§7).

theorem ChungMascarenhas2023.expectedValue_le_of_cond_eq_one {W : Type u_1} [MeasurableSpace W] [DiscreteMeasurableSpace W] {p : MeasureTheory.Measure W} {e φ : Set W} (ψ : Set W) (h : p[e | φ] = 1) : expectedValue p ![e] ψ ≤ expectedValue p ![e] φ

A hypothesis that fully predicts the evidence is weakly best, whatever its prior: the §5 problem of success behind (50)–(51), which the plausibility requirement answers.

theorem ChungMascarenhas2023.toReal_expectedValue {W : Type u_1} [MeasurableSpace W] [DiscreteMeasurableSpace W] {ι : Type u_2} [Fintype ι] (p : MeasureTheory.Measure W) (R : ι → Set W) (φ : Set W) : (expectedValue p R φ).toReal = Desire.ExpectedValue.expectedValue p (fun (w : W) => (countTrue R w).toReal) Set.univ φ

The deontic reading is Lassiter's expected-value scale with value function μ_EVAL: the paper's §3.1 is "more or less a reproduction of Lassiter's analysis".

theorem ChungMascarenhas2023.uniformOn_univ_cond_apply {W : Type u_1} [MeasurableSpace W] [DiscreteMeasurableSpace W] [Fintype W] (s t : Set W) [DecidablePred fun (x : W) => x ∈ t] [DecidablePred fun (x : W) => x ∈ t ∩ s] : (ProbabilityTheory.uniformOn Set.univ)[s | t] = ↑{x : W | x ∈ t ∩ s}.card / ↑{x : W | x ∈ t}.card

A conditional probability of the uniform prior is a counting ratio.

theorem ChungMascarenhas2023.expectedValue_uniformOn_univ {W : Type u_1} [MeasurableSpace W] [DiscreteMeasurableSpace W] {ι : Type u_2} [Fintype ι] [Fintype W] (R : ι → Set W) (φ : Set W) [DecidablePred fun (x : W) => x ∈ φ] [(i : ι) → DecidablePred fun (x : W) => x ∈ φ ∩ R i] : expectedValue (ProbabilityTheory.uniformOn Set.univ) R φ = ↑(∑ i : ι, {x : W | x ∈ φ ∩ R i}.card) / ↑{x : W | x ∈ φ}.card

Under a uniform prior, expected value is a sum of counting ratios.

theorem ChungMascarenhas2023.uniformOn_univ_cond_eq_ofReal {W : Type u_1} [MeasurableSpace W] [DiscreteMeasurableSpace W] [Fintype W] {s t : Set W} [DecidablePred fun (x : W) => x ∈ t] [DecidablePred fun (x : W) => x ∈ t ∩ s] {m n : ℕ} {q : ℝ} (hs : {x : W | x ∈ t ∩ s}.card = m) (ht : {x : W | x ∈ t}.card = n) (hn : n ≠ 0) (hq : q = ↑m / ↑n) : (ProbabilityTheory.uniformOn Set.univ)[s | t] = ENNReal.ofReal q

A conditional probability of the uniform prior equals a printed decimal, by counting.

The operators

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

must φ holds iff the expected value of φ exceeds the threshold θ and no alternative's does, φ being the only good-enough option or explanation (6).

Equations

• ChungMascarenhas2023.must p R φ alts θ = (θ < ChungMascarenhas2023.expectedValue p R φ ∧ ∀ ψ ∈ alts, ChungMascarenhas2023.expectedValue p R ψ ≤ θ)

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

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

Equations

• ChungMascarenhas2023.ought p R φ alts θ = (θ < ChungMascarenhas2023.expectedValue p R φ ∧ ∀ ψ ∈ alts, ChungMascarenhas2023.expectedValue p R ψ < ChungMascarenhas2023.expectedValue p R φ)

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

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

Equations

• ChungMascarenhas2023.mustPlausible p R φ alts θ θplaus = (ChungMascarenhas2023.must p R φ alts θ ∧ θplaus ≤ p φ)

def ChungMascarenhas2023.might {W : Type u_1} [MeasurableSpace W] {ι : Type u_2} [Fintype ι] (p : MeasureTheory.Measure W) (R : ι → Set W) (φ : Set W) (θ : ENNReal) : Prop

might φ is ¬ must ¬φ, with the alternative set fixed as the polar alternative (59).

Equations

• ChungMascarenhas2023.might p R φ θ = ¬ChungMascarenhas2023.must p R φᶜ {φ} θ

theorem ChungMascarenhas2023.ought_of_must {W : Type u_1} [MeasurableSpace W] {ι : Type u_2} [Fintype ι] {p : MeasureTheory.Measure W} {R : ι → Set W} {φ : Set W} {alts : Set (Set W)} {θ : ENNReal} (h : must p R φ alts θ) : ought p R φ alts θ

ought is the semantics for must minus the requirement that φ be the only good-enough alternative (§3.1), after the weak-necessity literature [vFI05].

theorem ChungMascarenhas2023.not_mustPlausible_of_lt {W : Type u_1} [MeasurableSpace W] {ι : Type u_2} [Fintype ι] {p : MeasureTheory.Measure W} {R : ι → Set W} {φ : Set W} {alts : Set (Set W)} {θ θplaus : ENNReal} (h : p φ < θplaus) : ¬mustPlausible p R φ alts θ θplaus

An implausible prejacent is never a must, whatever its explanatory value: §5's resolution of (49) and its 99-lawyers prediction.

theorem ChungMascarenhas2023.might_iff {W : Type u_1} [MeasurableSpace W] {ι : Type u_2} [Fintype ι] {p : MeasureTheory.Measure W} {R : ι → Set W} {φ : Set W} {θ : ENNReal} : might p R φ θ ↔ expectedValue p R φᶜ ≤ θ ∨ θ < expectedValue p R φ

The disjunctive truth conditions of might that the paper writes out under (59).

theorem ChungMascarenhas2023.not_must_and_might_compl {W : Type u_1} [MeasurableSpace W] {ι : Type u_2} [Fintype ι] {p : MeasureTheory.Measure W} {R : ι → Set W} {φ : Set W} {θ : ENNReal} : ¬(must p R φ {φᶜ} θ ∧ might p R φᶜ θ)

It must be raining, but of course it might not be is contradictory (§6).

Korean conditional evaluatives (§4)

def ChungMascarenhas2023.conditionalEval {W : Type u_1} [MeasurableSpace W] {ι : Type u_2} [Fintype ι] (p : MeasureTheory.Measure W) (R : ι → Set W) (φ : Set W) (θ : ENNReal) : Prop

Lassiter's threshold Θ (46) applied to the conditional if φ, then eval, whose denotation is the conditional expectation of μ_EVAL (45).

Equations

• ChungMascarenhas2023.conditionalEval p R φ θ = (θ < ∫⁻ (w : W), ChungMascarenhas2023.countTrue R w ∂p[|φ])

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

The left-hand side of (48), the composition of cip-ey iss-eya toy-n-ta: the -(e)ya exhaustifier negates each alternative's thresholded conditional.

Equations

• ChungMascarenhas2023.koreanConditionalEvaluative p R φ alts θ = (ChungMascarenhas2023.conditionalEval p R φ θ ∧ ∀ ψ ∈ alts, ¬ChungMascarenhas2023.conditionalEval p R ψ θ)

theorem ChungMascarenhas2023.koreanConditionalEvaluative_iff_must {W : Type u_1} [MeasurableSpace W] {ι : Type u_2} [Fintype ι] {p : MeasureTheory.Measure W} {R : ι → Set W} {φ : Set W} {alts : Set (Set W)} {θ : ENNReal} : koreanConditionalEvaluative p R φ alts θ ↔ must p R φ alts θ

The Korean composition is the must semantics (6): this is (48).

The miners puzzle (§3.1)

inductive ChungMascarenhas2023.Miners.Action : Type

The actions available in the miners scenario.

• blockA : Action
• blockB : Action
• blockNeither : Action

@[instance_reducible]

instance ChungMascarenhas2023.Miners.instDecidableEqAction : DecidableEq Action

Equations

• ChungMascarenhas2023.Miners.instDecidableEqAction x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ChungMascarenhas2023.Miners.instFintypeAction : Fintype Action

Equations

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

inductive ChungMascarenhas2023.Miners.Shaft : Type

The shaft the miners are in.

• A : Shaft
• B : Shaft

@[instance_reducible]

instance ChungMascarenhas2023.Miners.instDecidableEqShaft : DecidableEq Shaft

Equations

• ChungMascarenhas2023.Miners.instDecidableEqShaft x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ChungMascarenhas2023.Miners.instFintypeShaft : Fintype Shaft

Equations

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

@[reducible, inline]

abbrev ChungMascarenhas2023.Miners.World : Type

The six action-by-location worlds of Table 1.

Equations

• ChungMascarenhas2023.Miners.World = (ChungMascarenhas2023.Miners.Action × ChungMascarenhas2023.Miners.Shaft)

@[instance_reducible]

instance ChungMascarenhas2023.Miners.instMeasurableSpaceWorld : MeasurableSpace World

Equations

• ChungMascarenhas2023.Miners.instMeasurableSpaceWorld = ⊤

@[reducible, inline]

abbrev ChungMascarenhas2023.Miners.act (a : Action) : Set World

The proposition that action a is taken.

Equations

• ChungMascarenhas2023.Miners.act a = {w : ChungMascarenhas2023.Miners.World | w.1 = a}

@[reducible, inline]

abbrev ChungMascarenhas2023.Miners.inShaft (s : Shaft) : Set World

The proposition that the miners are in shaft s.

Equations

• ChungMascarenhas2023.Miners.inShaft s = {w : ChungMascarenhas2023.Miners.World | w.2 = s}

def ChungMascarenhas2023.Miners.saved : World → ℕ

The miners saved at each world (Table 1).

Equations

• ChungMascarenhas2023.Miners.saved (ChungMascarenhas2023.Miners.Action.blockA, ChungMascarenhas2023.Miners.Shaft.A) = 10
• ChungMascarenhas2023.Miners.saved (ChungMascarenhas2023.Miners.Action.blockA, ChungMascarenhas2023.Miners.Shaft.B) = 0
• ChungMascarenhas2023.Miners.saved (ChungMascarenhas2023.Miners.Action.blockB, ChungMascarenhas2023.Miners.Shaft.A) = 0
• ChungMascarenhas2023.Miners.saved (ChungMascarenhas2023.Miners.Action.blockB, ChungMascarenhas2023.Miners.Shaft.B) = 10
• ChungMascarenhas2023.Miners.saved (ChungMascarenhas2023.Miners.Action.blockNeither, snd) = 9

@[reducible, inline]

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

The ideals R_D of (18), after Cariani, Kaufmann and Kaufmann, are {one miner saved, …, ten miners saved}: ideal k holds where at least k + 1 miners are saved. An indexed family is essential, since ideals one through nine coincide in extension on the six worlds.

Equations

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

noncomputable def ChungMascarenhas2023.Miners.prior : MeasureTheory.Measure World

The uniform prior, the paper's background assumptions in their simplest realization.

Equations

• ChungMascarenhas2023.Miners.prior = ProbabilityTheory.uniformOn Set.univ

@[instance_reducible]

instance ChungMascarenhas2023.Miners.instInhabitedWorld : Inhabited World

Equations

• ChungMascarenhas2023.Miners.instInhabitedWorld = { default := (ChungMascarenhas2023.Miners.Action.blockNeither, ChungMascarenhas2023.Miners.Shaft.A) }

instance ChungMascarenhas2023.Miners.instIsProbabilityMeasureWorldPrior : MeasureTheory.IsProbabilityMeasure prior

theorem ChungMascarenhas2023.Miners.prior_ne_zero {A : Set World} (h : A.Nonempty) : prior A ≠ 0

Any proposition exemplified at some world has positive uniform prior.

theorem ChungMascarenhas2023.Miners.countTrue_idealsRD (w : World) : countTrue idealsRD w = ↑(saved w)

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

The expected utilities (19)–(21) and (23) under the paper's stated assumptions: the locations are equiprobable and independent of the action, and the conditioned propositions carry mass.

theorem ChungMascarenhas2023.Miners.expectedValue_blockA_of_cond (p : MeasureTheory.Measure World) [MeasureTheory.IsFiniteMeasure p] (h : p[inShaft Shaft.A | act Action.blockA] = 1 / 2) : expectedValue p idealsRD (act Action.blockA) = 5

Blocking shaft A has expected utility 5 (20).

theorem ChungMascarenhas2023.Miners.expectedValue_blockB_of_cond (p : MeasureTheory.Measure World) [MeasureTheory.IsFiniteMeasure p] (h : p[inShaft Shaft.B | act Action.blockB] = 1 / 2) : expectedValue p idealsRD (act Action.blockB) = 5

Blocking shaft B has expected utility 5 (21).

theorem ChungMascarenhas2023.Miners.expectedValue_blockNeither_of_ne (p : MeasureTheory.Measure World) [MeasureTheory.IsFiniteMeasure p] (h : p (act Action.blockNeither) ≠ 0) : expectedValue p idealsRD (act Action.blockNeither) = 9

Blocking neither shaft has expected utility 9 whatever the distribution (19): one miner drowns whatever their location.

theorem ChungMascarenhas2023.Miners.expectedValue_inA_blockNeither_of_ne (p : MeasureTheory.Measure World) [MeasureTheory.IsFiniteMeasure p] (h : p (inShaft Shaft.A ∩ act Action.blockNeither) ≠ 0) : expectedValue p idealsRD (inShaft Shaft.A ∩ act Action.blockNeither) = 9

Conditionalized on the miners being in A, blocking neither still has expected utility 9.

theorem ChungMascarenhas2023.Miners.expectedValue_inA_blockA_of_ne (p : MeasureTheory.Measure World) [MeasureTheory.IsFiniteMeasure p] (h : p (inShaft Shaft.A ∩ act Action.blockA) ≠ 0) : expectedValue p idealsRD (inShaft Shaft.A ∩ act Action.blockA) = 10

Conditionalized on the miners being in A, blocking A has expected utility 10 (23): the prejacent realizes every ideal.

theorem ChungMascarenhas2023.Miners.expectedValue_inA_blockB (p : MeasureTheory.Measure World) [MeasureTheory.IsFiniteMeasure p] : expectedValue p idealsRD (inShaft Shaft.A ∩ act Action.blockB) = 0

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

theorem ChungMascarenhas2023.Miners.ought_blockNeither {p : MeasureTheory.Measure World} [MeasureTheory.IsFiniteMeasure p] {θ : ENNReal} (hbn : p (act Action.blockNeither) ≠ 0) (hA : p[inShaft Shaft.A | act Action.blockA] = 1 / 2) (hB : p[inShaft Shaft.B | act Action.blockB] = 1 / 2) (hθ : θ < 9) : ought p idealsRD (act Action.blockNeither) {act Action.blockA, act Action.blockB} θ

We ought to block neither shaft holds for any θ < 9 (22).

theorem ChungMascarenhas2023.Miners.ought_if_inA_blockA {p : MeasureTheory.Measure World} [MeasureTheory.IsFiniteMeasure p] {θ : ENNReal} (hbA : p (inShaft Shaft.A ∩ act Action.blockA) ≠ 0) (hbn : p (inShaft Shaft.A ∩ act Action.blockNeither) ≠ 0) (hθ : θ < 10) : ought p idealsRD (inShaft Shaft.A ∩ act Action.blockA) {inShaft Shaft.A ∩ act Action.blockNeither, inShaft Shaft.A ∩ act Action.blockB} θ

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

theorem ChungMascarenhas2023.Miners.must_blockNeither {p : MeasureTheory.Measure World} [MeasureTheory.IsFiniteMeasure p] {θ : ENNReal} (hbn : p (act Action.blockNeither) ≠ 0) (hA : p[inShaft Shaft.A | act Action.blockA] = 1 / 2) (hB : p[inShaft Shaft.B | act Action.blockB] = 1 / 2) (h5 : 5 ≤ θ) (h9 : θ < 9) : must p idealsRD (act Action.blockNeither) {act Action.blockA, act Action.blockB} θ

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

theorem ChungMascarenhas2023.Miners.must_if_inA_blockA {p : MeasureTheory.Measure World} [MeasureTheory.IsFiniteMeasure p] {θ : ENNReal} (hbA : p (inShaft Shaft.A ∩ act Action.blockA) ≠ 0) (hbn : p (inShaft Shaft.A ∩ act Action.blockNeither) ≠ 0) (h9 : 9 ≤ θ) (h10 : θ < 10) : must p idealsRD (inShaft Shaft.A ∩ act Action.blockA) {inShaft Shaft.A ∩ act Action.blockNeither, inShaft Shaft.A ∩ act Action.blockB} θ

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

theorem ChungMascarenhas2023.Miners.must_thresholds_incompatible {p : MeasureTheory.Measure World} [MeasureTheory.IsFiniteMeasure p] (hbn : p (act Action.blockNeither) ≠ 0) (hAbn : p (inShaft Shaft.A ∩ act Action.blockNeither) ≠ 0) : ¬∃ (θ : ENNReal), must p idealsRD (act Action.blockNeither) {act Action.blockA, act Action.blockB} θ ∧ must p idealsRD (inShaft Shaft.A ∩ act Action.blockA) {inShaft Shaft.A ∩ act Action.blockNeither, inShaft Shaft.A ∩ act Action.blockB} θ

No single threshold verifies both must claims, since (26a) needs θ < 9 while (25b) needs 9 ≤ θ; positivity of the two block-neither propositions is all it takes.

Under the uniform prior the paper's assumptions hold, and footnote 17's indifference calculation goes through.

theorem ChungMascarenhas2023.Miners.prior_cond_inShaft (s : Shaft) (a : Action) : prior[inShaft s | act a] = 1 / 2

The uniform prior makes the locations equiprobable given any action.

theorem ChungMascarenhas2023.Miners.expectedValue_inA : expectedValue prior idealsRD (inShaft Shaft.A) = 19 / 3

Under the uniform prior, indifference given in-A — the union of the three actions, footnote 17's comparison point for Lassiter's must — has expected utility 19/3.

theorem ChungMascarenhas2023.Miners.expectedValue_inA_lt_inA_blockNeither : expectedValue prior idealsRD (inShaft Shaft.A) < expectedValue prior idealsRD (inShaft Shaft.A ∩ act Action.blockNeither)

Blocking neither stays above indifference given in-A, so a must that compares the alternatives to indifference, as footnote 17 reads Lassiter, cannot verify (25b).

The classical account, run on the same scenario.

theorem ChungMascarenhas2023.Miners.kratzer_miners_unsatisfiable {V : Type u_3} (f g : Modality.Background V) (w : V) (inA inB bA bB bN : V → Prop) (hbest : (Modality.bestWorlds f g w).Nonempty) (hcover : ∀ v ∈ f.accessibleWorlds w, inA v ∨ inB v) (hA : ∀ (v : V), bA v → ¬bN v) (hB : ∀ (v : V), bB v → ¬bN v) : ¬(Modality.necessity f g bN w ∧ Modality.necessity (f.restrict inA) g bA w ∧ Modality.necessity (f.restrict inB) g bB w)

Following the paper's proof sketch (16), over any modal base whose accessible worlds locate the miners in one of the two shafts and any ordering source with best worlds — the paper's limit assumption, its fn 1 — the three ought claims of (15) are jointly unsatisfiable on Kratzer's account [Kra91], the if-clauses restricting the modal base.

Modal Linda (§3.2)

theorem ChungMascarenhas2023.ModalLinda.modal_conjunction_fallacy {W : Type u_1} [MeasurableSpace W] [DiscreteMeasurableSpace W] (p : MeasureTheory.Measure W) (R : Fin 2 → Set W) (teller feministTeller : Set W) (hsub : feministTeller ⊆ teller) (h₁ : p[R 0 | teller] = ENNReal.ofReal 0.3) (h₂ : p[R 1 | teller] = ENNReal.ofReal 0.2) (h₃ : p[R 0 | feministTeller] = ENNReal.ofReal 0.8) (h₄ : p[R 1 | feministTeller] = ENNReal.ofReal 0.7) {θ : ENNReal} (hlo : ENNReal.ofReal 0.5 ≤ θ) (hhi : θ < ENNReal.ofReal 1.5) : must p R feministTeller {teller} θ ∧ ¬must p R teller {feministTeller} θ ∧ p feministTeller ≤ p teller

In the modal conjunction fallacy ((30)–(34)), for every measure realizing the printed conditional probabilities and any threshold in [0.5, 1.5), Linda must be a feminist bank teller is true and Linda must be a bank teller false, although the feminist tellers are a subset of the tellers and so no more probable. The expected values are (32) and (33); by Modality.necessity_and_left no Kratzer reading of must can pattern this way.

theorem ChungMascarenhas2023.ModalLinda.exists_model : ∃ (p : MeasureTheory.Measure (Fin 40)) (R : Fin 2 → Set (Fin 40)) (teller : Set (Fin 40)), ∃ feministTeller ⊆ teller, p[R 0 | teller] = ENNReal.ofReal 0.3 ∧ p[R 1 | teller] = ENNReal.ofReal 0.2 ∧ p[R 0 | feministTeller] = ENNReal.ofReal 0.8 ∧ p[R 1 | feministTeller] = ENNReal.ofReal 0.7

The printed probabilities (30)–(31) are consistent: forty equiprobable worlds, ten of them feminist tellers.

Modal Lawyers and Engineers (§3.3)

theorem ChungMascarenhas2023.ModalLawyers.base_rate_neglect {W : Type u_1} [MeasurableSpace W] [DiscreteMeasurableSpace W] (p : MeasureTheory.Measure W) (R : Fin 2 → Set W) (engineer lawyer : Set W) (h₁ : p[R 0 | engineer] = ENNReal.ofReal 0.78) (h₂ : p[R 1 | engineer] = ENNReal.ofReal 0.55) (h₃ : p[R 0 | lawyer] = ENNReal.ofReal 0.35) (h₄ : p[R 1 | lawyer] = ENNReal.ofReal 0.28) {θ : ENNReal} (hlo : ENNReal.ofReal 0.63 ≤ θ) (hhi : θ < ENNReal.ofReal 1.33) : must p R engineer {lawyer} θ ∧ ¬must p R lawyer {engineer} θ

Modal base-rate neglect ((37)–(41)): for every measure realizing the printed conditional probabilities and any threshold in [0.63, 1.33), Jack must be an engineer is true and Jack must be a lawyer false. No hypothesis mentions the prior on engineer: explanatory value conditions only on the hypotheses, which is the neglect.

theorem ChungMascarenhas2023.ModalLawyers.exists_model : ∃ (p : MeasureTheory.Measure (Fin 2 × Fin 100)) (R : Fin 2 → Set (Fin 2 × Fin 100)) (engineer : Set (Fin 2 × Fin 100)) (lawyer : Set (Fin 2 × Fin 100)), Disjoint engineer lawyer ∧ p[R 0 | engineer] = ENNReal.ofReal 0.78 ∧ p[R 1 | engineer] = ENNReal.ofReal 0.55 ∧ p[R 0 | lawyer] = ENNReal.ofReal 0.35 ∧ p[R 1 | lawyer] = ENNReal.ofReal 0.28

The printed probabilities (37)–(38) are consistent: two hypotheses of a hundred equiprobable evidence cells each.