[CM23] — Modality, expected utility, and hypothesis testing

A single lexical entry for must, parameterized by a set R of "relevant propositions". For deontics, R = R_D (rules/ideals); E[μ_R ∣ φ] is then the expected utility of φ. For epistemics, R = R_E (relevant known facts/evidence); E[μ_R ∣ φ] is what C&M call the explanatory value of φ, equal to the sum of likelihoods Σ_i P(e_i ∣ φ) (their eq. 12, which follows by definition once μ_R = Confirmation.countMeasure R).

Headline operator (C&M (6)):

⟦must φ⟧^w = (E_w[μ_R ∣ φ] > θ) ∧ ∀ψ ∈ Alt(φ). (E_w[μ_R ∣ ψ] ≤ θ)

What this file contains

• mustCM, oughtCM, mustCMWithPlausibility — the operator, the Sloman-style weak-necessity variant, and C&M §5's plausibility patch as a separate def (so the patch stays reviewable).
• Miners — the [KMF10] deontic scenario as a six-world PMF setup with idealsRD (paper notation R_D).
• ModalLinda — C&M's modal-conjunction-fallacy numerical claims as ℚ values with the headline inequality explanatoryValueTeller < explanatoryValueFeministTeller proven (= the modal conjunction fallacy at the operator's numerical level).
• ModalLawyers — same shape for C&M's base-rate-neglect prediction.
• ya_exhaustification_yields_mustCM — the Korean compositional derivation (C&M §4): the -(e)ya exhaustifier IS the second conjunct of mustCM.

The Linda and Lawyers files do not set up full PMFs (the joint distributions over hypothesis-and-evidence are not pinned down by C&M's text). The numerical-claim level is sufficient to document the operator's predicted direction without committing to modeling choices not in the paper.

Cross-references

• Studies/VonFintelIatridou2005.lean §6 — C&M's exhaustification realises [Slo70]'s "only candidate" / vF&I's have-to vs ought-to distinction.
• Studies/Lassiter2017.lean — Lassiter's want on the same EV substrate (PMF.condExpect); C&M's must differs by (i) the exhaustification clause, (ii) count-valued μ_R vs Lassiter's free-form value, (iii) likelihood-based epistemic reading vs Lassiter's posterior.

The operator

def ChungMascarenhas2024.mustCM {W : Type u_1} [Fintype W] (p : PMF W) (R : Finset (Set W)) (φ : Set W) (alts : Finset (Set W)) (θ : ENNReal) : Prop

[CM23] (6): must φ iff E_w[μ_R ∣ φ] exceeds the contextual threshold θ AND no alternative does.

Equations

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

def ChungMascarenhas2024.oughtCM {W : Type u_1} [Fintype W] (p : PMF W) (R : Finset (Set W)) (φ : Set W) (θ : ENNReal) : Prop

The [Slo70]-flavored ought: drop the exhaustification clause. [vFI05] §6 identifies this with the weak-necessity modal across teleological and deontic flavors.

Equations

• ChungMascarenhas2024.oughtCM p R φ θ = (PMF.Confirmation.sumLikelihoods p R φ > θ)

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

[CM23] §5: mustCM with the additional plausibility requirement P(φ) ≥ θplaus. Kept as a separate def rather than baked into mustCM, so the §5 patch (which C&M concede is not derived from the core) stays reviewable.

Equations

• ChungMascarenhas2024.mustCMWithPlausibility p R φ alts θ θplaus = (ChungMascarenhas2024.mustCM p R φ alts θ ∧ p.probOfSet φ ≥ θplaus)

Miners scenario [KMF10]

Six worlds = (block-action) × (miners-location):

• w0 = block-A, miners-in-A: 10 saved
• w1 = block-A, miners-in-B: 0 saved
• w2 = block-B, miners-in-A: 0 saved
• w3 = block-B, miners-in-B: 10 saved
• w4 = block-neither, miners-in-A: 9 saved
• w5 = block-neither, miners-in-B: 9 saved

Uniform prior over the 6 worlds — equivalent (under independence of action and location) to a uniform prior on miners-location with action a free choice. idealsRD (paper notation R_D) is {1 saved, 2 saved, ..., 10 saved}, following [CKK13].

@[reducible, inline]

abbrev ChungMascarenhas2024.Miners.World : Type

World type: six (action × miners-location) combinations.

Equations

• ChungMascarenhas2024.Miners.World = Fin 6

def ChungMascarenhas2024.Miners.blockA : Set World

Block-A.

Equations

• ChungMascarenhas2024.Miners.blockA w = (↑w = 0 ∨ ↑w = 1)

def ChungMascarenhas2024.Miners.blockB : Set World

Block-B.

Equations

• ChungMascarenhas2024.Miners.blockB w = (↑w = 2 ∨ ↑w = 3)

def ChungMascarenhas2024.Miners.blockNeither : Set World

Block-neither.

Equations

• ChungMascarenhas2024.Miners.blockNeither w = (↑w = 4 ∨ ↑w = 5)

def ChungMascarenhas2024.Miners.minersInA : Set World

Miners in shaft A.

Equations

• ChungMascarenhas2024.Miners.minersInA w = (↑w = 0 ∨ ↑w = 2 ∨ ↑w = 4)

def ChungMascarenhas2024.Miners.minersInB : Set World

Miners in shaft B.

Equations

• ChungMascarenhas2024.Miners.minersInB w = (↑w = 1 ∨ ↑w = 3 ∨ ↑w = 5)

def ChungMascarenhas2024.Miners.minersSaved : World → ℕ

Miners saved at each world (C&M Table 1).

Equations

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

noncomputable def ChungMascarenhas2024.Miners.prior : PMF World

Uniform PMF over the 6 worlds.

Equations

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

noncomputable def ChungMascarenhas2024.Miners.idealsRD : Finset (Set World)

The relevant-ideals set, paper notation R_D: the set of worlds where at least k miners are saved, for k = 1, ..., 10. μ_R(w) = minersSaved w by construction.

Equations

• ChungMascarenhas2024.Miners.idealsRD = Finset.image (fun (k : ℕ) => {w : ChungMascarenhas2024.Miners.World | ChungMascarenhas2024.Miners.minersSaved w ≥ k + 1}) (Finset.range 10)

Modal Linda [TK83]

C&M §3.2 + (30)/(31): the salient evidence from the Linda description projects to two propositions about Linda — concern with social justice (socialJustice) and anti-nuclear-protests participation (antiNuclearProtests). Conditional probabilities given each hypothesis:

• P(socialJustice ∣ teller) = 0.3, P(antiNuclear ∣ teller) = 0.2
• P(socialJustice ∣ feministTeller) = 0.8, P(antiNuclear ∣ feministTeller) = 0.7

C&M predict the modal conjunction fallacy: under any threshold θ with 0.5 < θ < 1.5, Linda must be a feminist bank teller is true while Linda must be a bank teller is false.

We do not set up the full joint PMF over hypothesis-and-evidence (those weights are not pinned down by C&M). The numerical-claim level is sufficient to document the prediction.

def ChungMascarenhas2024.ModalLinda.prSocialJusticeGivenTeller : ℚ

P(socialJustice ∣ teller) = 0.3 per C&M (30).

Equations

• ChungMascarenhas2024.ModalLinda.prSocialJusticeGivenTeller = 3 / 10

def ChungMascarenhas2024.ModalLinda.prAntiNuclearGivenTeller : ℚ

P(antiNuclearProtests ∣ teller) = 0.2 per C&M (30).

Equations

• ChungMascarenhas2024.ModalLinda.prAntiNuclearGivenTeller = 2 / 10

def ChungMascarenhas2024.ModalLinda.prSocialJusticeGivenFeministTeller : ℚ

P(socialJustice ∣ feministTeller) = 0.8 per C&M (31).

Equations

• ChungMascarenhas2024.ModalLinda.prSocialJusticeGivenFeministTeller = 8 / 10

def ChungMascarenhas2024.ModalLinda.prAntiNuclearGivenFeministTeller : ℚ

P(antiNuclearProtests ∣ feministTeller) = 0.7 per C&M (31).

Equations

• ChungMascarenhas2024.ModalLinda.prAntiNuclearGivenFeministTeller = 7 / 10

def ChungMascarenhas2024.ModalLinda.explanatoryValueTeller : ℚ

E[μ_R ∣ teller] = 0.5 per C&M (32).

Equations

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

def ChungMascarenhas2024.ModalLinda.explanatoryValueFeministTeller : ℚ

E[μ_R ∣ feministTeller] = 1.5 per C&M (33).

Equations

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

theorem ChungMascarenhas2024.ModalLinda.feministTeller_strictly_higher : explanatoryValueTeller < explanatoryValueFeministTeller

The modal conjunction fallacy as a numerical inequality: the conjunctive hypothesis has strictly higher explanatory value. Any threshold θ between the two predicts the must-conjunction true and the bare must-claim false.

Modal Lawyers and Engineers [KT73]

C&M §3.3 + (37)/(38): two evidence pieces from the Jack description — absence of interest in political/social issues (notPoliticalSocial) and enjoyment of mathematical puzzles (enjoysMath).

• P(notPoliticalSocial ∣ engineer) = 0.78, P(math ∣ engineer) = 0.55
• P(notPoliticalSocial ∣ lawyer) = 0.35, P(math ∣ lawyer) = 0.28

C&M predict base-rate neglect at the modal level: under any threshold θ with 0.63 < θ < 1.33, Jack must be an engineer is true irrespective of the prior split between lawyers and engineers.

Same caveat as ModalLinda.

def ChungMascarenhas2024.ModalLawyers.prNotPoliticalGivenEngineer : ℚ

P(notPoliticalSocial ∣ engineer) = 0.78 per C&M (37).

Equations

• ChungMascarenhas2024.ModalLawyers.prNotPoliticalGivenEngineer = 78 / 100

def ChungMascarenhas2024.ModalLawyers.prMathGivenEngineer : ℚ

P(enjoysMath ∣ engineer) = 0.55 per C&M (37).

Equations

• ChungMascarenhas2024.ModalLawyers.prMathGivenEngineer = 55 / 100

def ChungMascarenhas2024.ModalLawyers.prNotPoliticalGivenLawyer : ℚ

P(notPoliticalSocial ∣ lawyer) = 0.35 per C&M (38).

Equations

• ChungMascarenhas2024.ModalLawyers.prNotPoliticalGivenLawyer = 35 / 100

def ChungMascarenhas2024.ModalLawyers.prMathGivenLawyer : ℚ

P(enjoysMath ∣ lawyer) = 0.28 per C&M (38).

Equations

• ChungMascarenhas2024.ModalLawyers.prMathGivenLawyer = 28 / 100

def ChungMascarenhas2024.ModalLawyers.explanatoryValueEngineer : ℚ

E[μ_R ∣ engineer] = 1.33 per C&M (39).

Equations

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

def ChungMascarenhas2024.ModalLawyers.explanatoryValueLawyer : ℚ

E[μ_R ∣ lawyer] = 0.63 per C&M (40).

Equations

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

theorem ChungMascarenhas2024.ModalLawyers.engineer_strictly_higher : explanatoryValueLawyer < explanatoryValueEngineer

Base-rate neglect as a numerical inequality: the engineer hypothesis has strictly higher explanatory value than the lawyer hypothesis, irrespective of prior.

Compositional Korean derivation (C&M §4)

The Korean conditional evaluative cip-ey iss-eya toy-n-ta ('lit. only if at home, it suffices' ≈ 'must be home') is, per C&M, the transparent compositional form of English must:

1. the evaluative predicate toy 'EVAL' as the measure function μ_R
2. the conditional if φ, EVAL as E_w[μ_R ∣ φ] (their eq. 44, our Semantics.Conditionals.Probabilistic.condIf)
3. the exhaustifier -(e)ya 'only-if' adding the alternative negation: ∀ψ ∈ Alt(φ). E_w[μ_R ∣ ψ] ≤ θ

The composition (their (48)) yields mustCM exactly.

theorem ChungMascarenhas2024.ya_exhaustification_yields_mustCM {W : Type u_1} [Fintype W] (p : PMF W) (R : Finset (Set W)) (φ : Set W) (alts : Finset (Set W)) (θ : ENNReal) (hThresh : PMF.Confirmation.sumLikelihoods p R φ > θ) (hExhaust : ∀ ψ ∈ alts, PMF.Confirmation.sumLikelihoods p R ψ ≤ θ) : mustCM p R φ alts θ

[CM23] (48): adding the -(e)ya exhaustifier to Θ(⟦if φ, EVAL⟧^w) yields mustCM φ. Trivial by definition: the exhaustifier IS the second conjunct of mustCM. The named theorem documents the compositional claim for cross-references.