Decision-Theoretic Semantics

This file sets up the core of Merin's Decision-Theoretic Semantics (DTS) [Mer99b]: meaning explicated through the signed relevance of a proposition E to one side H of a dichotomic issue {H, ¬H}, the log Bayes factor log (P(E∣H) / P(E∣¬H)).

Each side of the issue conditions the prior on itself (Context.conditional), and the Bayes factor of E is the ratio of the two conditional probabilities of E. The paper's applications to or, but, even, and also are in Studies/Merin1999a.lean.

Main definitions

• Context: a dichotomic issue (topic : Set W, with its measurability witness) plus a prior (Partial Definition 6); Context.Nondegenerate marks a live issue
• bayesFactor: the ratio P(E∣H) / P(E∣¬H)
• relevance: its logarithm, Merin's relevance of E to H (Definition 4)
• posRelevant, negRelevant, irrelevant: the relevance signs (Definition 5)
• hContrary: A and B have opposite relevance signs
• CondIndepIssue: independence of A and B conditionally on H and on ¬H (Definition 9), the content of the Conditional Independence Presumption (Hypothesis 2)

Main results

• posRelevant_iff_cond_lt: E confirms H iff H makes E more probable than ¬H does
• sign_reversal: BF_H(E) · BF_¬H(E) = 1 (Corollary 3)
• relevance_eq_neg_log_sub_neg_log: relevance is the differential of conditional informativeness (Fact 2)
• CondIndepIssue.bayesFactor_inter: under issue-conditional independence, BF(A∧B) = BF(A) · BF(B) (Fact 5); Theorem 6a's order of conjunction, disjuncts, and disjunction is CondIndepIssue.max_bayesFactor_lt_inter, .bayesFactor_union_lt_max, and .one_lt_bayesFactor_union

Implementation notes

The context stores H, with ¬H implicit. Relevance is carried by bayesFactor in ℝ≥0∞, where the boundary cases P(E∣¬H) = 0 and P(E∣H) = 0 take their true values ∞ and 0 (Merin's r = ±∞); relevance is the real logarithm, which sends both to 0, so sign and order facts are stated on bayesFactor.

References

• [Mer99b]

Contexts

structure DTS.Context (W : Type u_1) [MeasurableSpace W] : Type u_1

A DTS context (Partial Definition 6) consists of the proposition H at issue, with ¬H implicit, and a prior over worlds.

• topic : Set W

  The hypothesis H.

• topicMeasurable : MeasurableSet self.topic

  Measurability of the topic, so that conditioning on H and ¬H is well-behaved.

• prior : MeasureTheory.Measure W

  Prior measure over worlds. Conditioning normalizes, so an unnormalized prior (e.g. Measure.count) induces the same relevance facts as its normalization.

def DTS.swapIssue {W : Type u_1} [MeasurableSpace W] (ctx : Context W) : Context W

Swapping the issue replaces H with ¬H.

Equations

• DTS.swapIssue ctx = { topic := ctx.topicᶜ, topicMeasurable := ⋯, prior := ctx.prior }

noncomputable def DTS.Context.conditional {W : Type u_1} [MeasurableSpace W] (ctx : Context W) : Bool → MeasureTheory.Measure W

The prior conditioned on H (at true) or on ¬H (at false).

Equations

• ctx.conditional true = ctx.prior[|ctx.topic]
• ctx.conditional false = ctx.prior[|ctx.topicᶜ]

@[simp]

theorem DTS.Context.conditional_true {W : Type u_1} [MeasurableSpace W] (ctx : Context W) : ctx.conditional true = ctx.prior[|ctx.topic]

@[simp]

theorem DTS.Context.conditional_false {W : Type u_1} [MeasurableSpace W] (ctx : Context W) : ctx.conditional false = ctx.prior[|ctx.topicᶜ]

class DTS.Context.Nondegenerate {W : Type u_1} [MeasurableSpace W] (ctx : Context W) : Prop

An issue is live when both sides carry mass. Merin's dichotomic issue {H, ¬H} presupposes a genuine question, so the degenerate cases are excluded at the level of the object rather than per theorem.

• topic_ne_zero : ctx.prior ctx.topic ≠ 0
• compl_ne_zero : ctx.prior ctx.topicᶜ ≠ 0

instance DTS.instNondegenerateSwapIssue {W : Type u_1} [MeasurableSpace W] (ctx : Context W) [h : ctx.Nondegenerate] : (swapIssue ctx).Nondegenerate

theorem DTS.Context.isProbabilityMeasure_conditional {W : Type u_1} [MeasurableSpace W] (ctx : Context W) [MeasureTheory.IsFiniteMeasure ctx.prior] [ctx.Nondegenerate] (θ : Bool) : MeasureTheory.IsProbabilityMeasure (ctx.conditional θ)

Each side's conditional is a genuine probability measure over a live issue.

instance DTS.instIsZeroOrProbabilityMeasureConditional {W : Type u_1} [MeasurableSpace W] (ctx : Context W) (θ : Bool) : MeasureTheory.IsZeroOrProbabilityMeasure (ctx.conditional θ)

Bayes factor and relevance

noncomputable def DTS.bayesFactor {W : Type u_1} [MeasurableSpace W] (ctx : Context W) (e : Set W) : ENNReal

The Bayes factor P(E∣H) / P(E∣¬H), in ℝ≥0∞. Total division gives the boundary cases their true values: P(E∣¬H) = 0 with P(E∣H) > 0 is ∞ (infinitely strong evidence for H), and 0/0 = 0.

Equations

• DTS.bayesFactor ctx e = (ctx.conditional true) e / (ctx.conditional false) e

theorem DTS.bayesFactor_def {W : Type u_1} [MeasurableSpace W] (ctx : Context W) (e : Set W) : bayesFactor ctx e = ctx.prior[e | ctx.topic] / ctx.prior[e | ctx.topicᶜ]

theorem DTS.toReal_bayesFactor {W : Type u_1} [MeasurableSpace W] (ctx : Context W) (e : Set W) : (bayesFactor ctx e).toReal = ctx.prior[|ctx.topic].real e / ctx.prior[|ctx.topicᶜ].real e

noncomputable def DTS.relevance {W : Type u_1} [MeasurableSpace W] (ctx : Context W) (e : Set W) : ℝ

Merin's relevance of E to H (Definition 4) is the log Bayes factor, real-valued through ENNReal.toReal. The boundary cases 0 and ∞ both land at Real.log 0 = 0, so sign and order facts are read off bayesFactor itself (posRelevant_iff_one_lt_toReal, relevance_lt_relevance).

Equations

• DTS.relevance ctx e = Real.log (DTS.bayesFactor ctx e).toReal

theorem DTS.bayesFactor_ne_zero {W : Type u_1} [MeasurableSpace W] {ctx : Context W} {e : Set W} (h : ctx.prior[e | ctx.topic] ≠ 0) : bayesFactor ctx e ≠ 0

theorem DTS.bayesFactor_ne_top {W : Type u_1} [MeasurableSpace W] {ctx : Context W} {e : Set W} (h : ctx.prior[e | ctx.topicᶜ] ≠ 0) : bayesFactor ctx e ≠ ⊤

theorem DTS.relevance_lt_relevance {W : Type u_1} [MeasurableSpace W] {ctx : Context W} {e₁ e₂ : Set W} (h₁ : bayesFactor ctx e₁ ≠ 0) (h₂ : bayesFactor ctx e₂ ≠ ⊤) (h : bayesFactor ctx e₁ < bayesFactor ctx e₂) : relevance ctx e₁ < relevance ctx e₂

Relevance is strictly monotone in the Bayes factor away from the boundary cases.

def DTS.posRelevant {W : Type u_1} [MeasurableSpace W] (ctx : Context W) (e : Set W) : Prop

E is positively relevant to H, and so confirms it, when BF > 1 (Definition 5).

Equations

• DTS.posRelevant ctx e = (1 < DTS.bayesFactor ctx e)

theorem DTS.posRelevant_iff_one_lt_toReal {W : Type u_1} [MeasurableSpace W] {ctx : Context W} {e : Set W} (ht : bayesFactor ctx e ≠ ⊤) : posRelevant ctx e ↔ 1 < (bayesFactor ctx e).toReal

def DTS.negRelevant {W : Type u_1} [MeasurableSpace W] (ctx : Context W) (e : Set W) : Prop

E is negatively relevant to H, and so disconfirms it, when BF < 1 (Definition 5).

Equations

• DTS.negRelevant ctx e = (DTS.bayesFactor ctx e < 1)

theorem DTS.negRelevant_iff_toReal_lt_one {W : Type u_1} [MeasurableSpace W] {ctx : Context W} {e : Set W} (ht : bayesFactor ctx e ≠ ⊤) : negRelevant ctx e ↔ (bayesFactor ctx e).toReal < 1

def DTS.irrelevant {W : Type u_1} [MeasurableSpace W] (ctx : Context W) (e : Set W) : Prop

E is irrelevant to H, neither confirming nor disconfirming it, when BF = 1 (Definition 5).

Equations

• DTS.irrelevant ctx e = (DTS.bayesFactor ctx e = 1)

def DTS.hContrary {W : Type u_1} [MeasurableSpace W] (ctx : Context W) (a b : Set W) : Prop

A and B are H-contrary: they have opposite nonzero relevance signs, one supporting H and the other ¬H.

Equations

• DTS.hContrary ctx a b = (DTS.posRelevant ctx a ∧ DTS.negRelevant ctx b ∨ DTS.negRelevant ctx a ∧ DTS.posRelevant ctx b)

theorem DTS.bayesFactor_swapIssue {W : Type u_1} [MeasurableSpace W] (ctx : Context W) (e : Set W) : bayesFactor (swapIssue ctx) e = ctx.prior[e | ctx.topicᶜ] / ctx.prior[e | ctx.topic]

bayesFactor under the swapped issue, with the double complement reduced.

theorem DTS.posRelevant_iff_cond_lt {W : Type u_1} [MeasurableSpace W] {ctx : Context W} {e : Set W} : posRelevant ctx e ↔ ctx.prior[e | ctx.topicᶜ] < ctx.prior[e | ctx.topic]

E confirms H exactly when H makes E more probable than ¬H does.

theorem DTS.negRelevant_iff_cond_lt {W : Type u_1} [MeasurableSpace W] {ctx : Context W} {e : Set W} (h : ctx.prior[e | ctx.topicᶜ] ≠ 0) : negRelevant ctx e ↔ ctx.prior[e | ctx.topic] < ctx.prior[e | ctx.topicᶜ]

E disconfirms H exactly when ¬H makes E more probable than H does, once E is possible given ¬H.

Monotonicity

Shedding ¬H-worlds from an utterance can only strengthen it as an argument for H: the H-side conditional is unchanged and the ¬H-side conditional can only fall.

theorem DTS.bayesFactor_le_of_subset {W : Type u_1} [MeasurableSpace W] (ctx : Context W) {u₁ u₂ : Set W} (hsub : u₂ ⊆ u₁) (hent : ctx.topic ∩ u₁ ⊆ u₂) : bayesFactor ctx u₁ ≤ bayesFactor ctx u₂

If u₂ ⊆ u₁ and every H-world of u₁ lies in u₂, then u₂ is at least as relevant to H as u₁.

theorem DTS.bayesFactor_lt_of_subset {W : Type u_1} [MeasurableSpace W] (ctx : Context W) [MeasureTheory.IsFiniteMeasure ctx.prior] {u₁ u₂ : Set W} (hu₂ : MeasurableSet u₂) (hsub : u₂ ⊆ u₁) (hent : ctx.topic ∩ u₁ ⊆ u₂) (hpos : ctx.prior (ctx.topic ∩ u₂) ≠ 0) (hgap : ctx.prior (u₁ \ u₂) ≠ 0) : bayesFactor ctx u₁ < bayesFactor ctx u₂

Strictly so once the shed worlds carry mass and u₂ is possible under H.

Counting priors

Over a finite type with the counting prior, the Bayes factor is a ratio of proportions and relevance its logarithm. The real-valued forms need no side conditions: the junk values agree (0 / 0 = 0 in ℝ, Real.log 0 = 0).

theorem DTS.toReal_bayesFactor_count {W : Type u_1} [MeasurableSpace W] [Fintype W] [MeasurableSingletonClass W] (topic e : Set W) : (bayesFactor { topic := topic, topicMeasurable := ⋯, prior := MeasureTheory.Measure.count } e).toReal = ↑(topic ∩ e).ncard / ↑topic.ncard / (↑(topicᶜ ∩ e).ncard / ↑topicᶜ.ncard)

theorem DTS.relevance_count {W : Type u_1} [MeasurableSpace W] [Fintype W] [MeasurableSingletonClass W] (topic e : Set W) : relevance { topic := topic, topicMeasurable := ⋯, prior := MeasureTheory.Measure.count } e = Real.log (↑(topic ∩ e).ncard / ↑topic.ncard / (↑(topicᶜ ∩ e).ncard / ↑topicᶜ.ncard))

theorem DTS.bayesFactor_count_ne_zero {W : Type u_1} [MeasurableSpace W] [Fintype W] [MeasurableSingletonClass W] {topic e : Set W} (h : (topic ∩ e).Nonempty) : bayesFactor { topic := topic, topicMeasurable := ⋯, prior := MeasureTheory.Measure.count } e ≠ 0

theorem DTS.bayesFactor_count_ne_top {W : Type u_1} [MeasurableSpace W] [Fintype W] [MeasurableSingletonClass W] {topic e : Set W} (h : (topicᶜ ∩ e).Nonempty) : bayesFactor { topic := topic, topicMeasurable := ⋯, prior := MeasureTheory.Measure.count } e ≠ ⊤

Cross-product characterizations

The relevance signs as comparisons of cross-products of real masses.

theorem DTS.posRelevant_iff_real_cross {W : Type u_1} [MeasurableSpace W] (ctx : Context W) [MeasureTheory.IsFiniteMeasure ctx.prior] [ctx.Nondegenerate] {e : Set W} : posRelevant ctx e ↔ ctx.prior.real (ctx.topicᶜ ∩ e) * ctx.prior.real ctx.topic < ctx.prior.real (ctx.topic ∩ e) * ctx.prior.real ctx.topicᶜ

Positive relevance is a comparison of cross-products of real masses: E confirms H iff the H-side mass of E outweighs its ¬H-side mass after weighting each by the opposite cell of the issue.

theorem DTS.negRelevant_iff_real_cross {W : Type u_1} [MeasurableSpace W] (ctx : Context W) [MeasureTheory.IsFiniteMeasure ctx.prior] [ctx.Nondegenerate] {e : Set W} (he : ctx.prior e ≠ 0) : negRelevant ctx e ↔ ctx.prior.real (ctx.topic ∩ e) * ctx.prior.real ctx.topicᶜ < ctx.prior.real (ctx.topicᶜ ∩ e) * ctx.prior.real ctx.topic

Negative relevance as a cross-product of real masses, for a live proposition E (one of nonzero mass; a null E is vacuously negatively relevant but has a degenerate cross-product).

Issue-conditional independence

def DTS.CondIndepIssue {W : Type u_1} [MeasurableSpace W] (ctx : Context W) (a b : Set W) : Prop

A and B are independent conditionally on H and on ¬H (Definition 9) when mathlib's IndepSet holds at both conditionals. Merin's Conditional Independence Presumption (Hypothesis 2) is that interpretation assumes this of coordinated sisters unless something suggests otherwise.

Equations

• DTS.CondIndepIssue ctx a b = ∀ (θ : Bool), ProbabilityTheory.IndepSet a b (ctx.conditional θ)

theorem DTS.condIndepIssue_iff {W : Type u_1} [MeasurableSpace W] (ctx : Context W) {a b : Set W} (ham : MeasurableSet a) (hbm : MeasurableSet b) : CondIndepIssue ctx a b ↔ ctx.prior[a ∩ b | ctx.topic] = ctx.prior[a | ctx.topic] * ctx.prior[b | ctx.topic] ∧ ctx.prior[a ∩ b | ctx.topicᶜ] = ctx.prior[a | ctx.topicᶜ] * ctx.prior[b | ctx.topicᶜ]

Issue-conditional independence is the product equation P(A∧B∣H) = P(A∣H)·P(B∣H) together with its analogue given ¬H.

theorem DTS.condIndepIssue_count_iff {W : Type u_1} [MeasurableSpace W] [Fintype W] [MeasurableSingletonClass W] {topic a b : Set W} : CondIndepIssue { topic := topic, topicMeasurable := ⋯, prior := MeasureTheory.Measure.count } a b ↔ (topic ∩ (a ∩ b)).ncard * topic.ncard = (topic ∩ a).ncard * (topic ∩ b).ncard ∧ (topicᶜ ∩ (a ∩ b)).ncard * topicᶜ.ncard = (topicᶜ ∩ a).ncard * (topicᶜ ∩ b).ncard

Over a counting prior, issue-conditional independence is the product equation of cardinalities on each side of the issue.

Sign reversal

theorem DTS.sign_reversal_qual {W : Type u_1} [MeasurableSpace W] (ctx : Context W) (e : Set W) (hEH : ctx.prior[e | ctx.topic] ≠ 0) : posRelevant ctx e ↔ negRelevant (swapIssue ctx) e

E is positively relevant to H iff E is negatively relevant to ¬H. This is the qualitative sign reversal of Corollary 3, the ordinal content of r_H(E) = −r_{¬H}(E).

theorem DTS.sign_reversal {W : Type u_1} [MeasurableSpace W] (ctx : Context W) (e : Set W) (hEH : ctx.prior[e | ctx.topic] ≠ 0) (hENotH : ctx.prior[e | ctx.topicᶜ] ≠ 0) : bayesFactor ctx e * bayesFactor (swapIssue ctx) e = 1

The Bayes factors of E for H and for ¬H multiply to one, BF_H(E) · BF_{¬H}(E) = 1, the quantitative form of Corollary 3. The identity is exact when both conditional probabilities are nonzero.

theorem DTS.relevance_eq_neg_log_sub_neg_log {W : Type u_1} [MeasurableSpace W] (ctx : Context W) (e : Set W) (hEH : ctx.prior[e | ctx.topic] ≠ 0) (hENotH : ctx.prior[e | ctx.topicᶜ] ≠ 0) : relevance ctx e = -Real.log ctx.prior[e | ctx.topicᶜ].toReal - -Real.log ctx.prior[e | ctx.topic].toReal

Relevance is the differential of conditional informativeness (Fact 2): log BF_H(E) = inf(E, ¬H) − inf(E, H), where inf(E, X) = −log P(E∣X) is the conditional surprisal of E.

Consequences of issue-conditional independence

Theorem 6a holds for any two probability measures under which A and B are independent; the conditionals on the two sides of the issue are such a pair.

theorem DTS.CondIndepIssue.bayesFactor_inter {W : Type u_1} [MeasurableSpace W] {ctx : Context W} {a b : Set W} (h : CondIndepIssue ctx a b) (hNotH' : ctx.prior[b | ctx.topicᶜ] ≠ 0) : bayesFactor ctx (a ∩ b) = bayesFactor ctx a * bayesFactor ctx b

Under issue-conditional independence the Bayes factor is multiplicative over conjunction, BF(A∧B) = BF(A) · BF(B) (Fact 5).

theorem DTS.CondIndepIssue.max_bayesFactor_lt_inter {W : Type u_1} [MeasurableSpace W] {ctx : Context W} {a b : Set W} (h : CondIndepIssue ctx a b) (hPosA : posRelevant ctx a) (hPosB : posRelevant ctx b) (hNa : ctx.prior[a | ctx.topicᶜ] ≠ 0) (hNb : ctx.prior[b | ctx.topicᶜ] ≠ 0) : max (bayesFactor ctx a) (bayesFactor ctx b) < bayesFactor ctx (a ∩ b)

Under issue-conditional independence with A and B both positively relevant, their conjunction dominates both conjuncts, the conjunction case of Theorem 6a.

theorem DTS.CondIndepIssue.bayesFactor_union_lt_max {W : Type u_1} [MeasurableSpace W] {ctx : Context W} [MeasureTheory.IsFiniteMeasure ctx.prior] [ctx.Nondegenerate] {a b : Set W} (hbm : MeasurableSet b) (h : CondIndepIssue ctx a b) (hPosA : posRelevant ctx a) (hPosB : posRelevant ctx b) (hNa : ctx.prior[a | ctx.topicᶜ] ≠ 0) (hNb : ctx.prior[b | ctx.topicᶜ] ≠ 0) : bayesFactor ctx (a ∪ b) < max (bayesFactor ctx a) (bayesFactor ctx b)

Under issue-conditional independence with A and B both positively relevant, their disjunction is dominated by the stronger disjunct, the upper bound for disjunction in Theorem 6a.

theorem DTS.CondIndepIssue.one_lt_bayesFactor_union {W : Type u_1} [MeasurableSpace W] {ctx : Context W} [MeasureTheory.IsFiniteMeasure ctx.prior] [ctx.Nondegenerate] {a b : Set W} (hbm : MeasurableSet b) (h : CondIndepIssue ctx a b) (hPosA : posRelevant ctx a) (hPosB : posRelevant ctx b) (hNa : ctx.prior[a | ctx.topicᶜ] ≠ 0) (hNb : ctx.prior[b | ctx.topicᶜ] ≠ 0) : 1 < bayesFactor ctx (a ∪ b)

Under issue-conditional independence with A and B both positively relevant, their disjunction is still positively relevant, the lower bound for disjunction in Theorem 6a.

The Bayesian bridge

theorem DTS.posRelevant_iff_lt_cond {W : Type u_1} [MeasurableSpace W] (ctx : Context W) [MeasureTheory.IsProbabilityMeasure ctx.prior] [ctx.Nondegenerate] (e : Set W) : posRelevant ctx e ↔ ctx.prior e < ctx.prior[e | ctx.topic]

Over a live issue, E confirms H iff H makes E more probable than it is a priori, so Bayes' theorem links P(E∣H) > P(E) with BF_H(E) > 1.