Decision-Theoretic Semantics: Core

[Mer99a]

Core definitions for Merin's Decision-Theoretic Semantics (DTS). Meaning is explicated through signed relevance — the Bayes factor P(E∣H)/P(E∣¬H) — relative to a dichotomic issue {H, ¬H}.

A context is a binary statistical model in the sense of mathlib's statistical decision theory (Mathlib.Probability.Decision): each side of the issue generates data from the prior conditioned on it (Context.conditional), the pair packages as a kernel out of Bool (Context.hypothesisKernel, the shape of Degenne's twoHypKernel), and bayesFactor is ProbabilityTheory.likelihoodRatio of the two conditionals. The substance of the Bayes-factor algebra lives at the two-measure level in Core.Probability.LikelihoodRatio; this file adds the issue vocabulary and the facts that genuinely concern the joint prior.

Key Definitions

• Context — a dichotomic issue (topic : Set W, with its measurability witness) plus a prior measure; Context.Nondegenerate marks a live issue
• bayesFactor — the likelihood ratio of the induced testing problem
• posRelevant / negRelevant / irrelevant — ordinal relevance predicates
• hContrary — A and B have opposite relevance signs
• CondIndepIssue — Merin's Conditional Independence Presumption, as mathlib IndepSet under both conditionals

Main Results

• Corollary 3 (sign_reversal): BF_H(E) · BF_{¬H}(E) = 1
• Fact 2 (log_bayesFactor): relevance is the differential of conditional informativeness
• Fact 5 (CondIndepIssue.bayesFactor_inter): under issue-conditional independence, BF(A∧B) = BF(A) · BF(B); Theorem 6a splits into CondIndepIssue.max_bayesFactor_lt_inter, .bayesFactor_union_lt_max, and .one_lt_bayesFactor_union
• Theorem 6b (xor_not_necessarily_positive): XOR of two positively relevant propositions can be negatively relevant
• avgRisk_hypothesisKernel: the average risk of an estimator against the induced problem, in its finite two-point form

inductive DTS.World4 : Type

4-world example type. Used by xor_not_necessarily_positive and consumers in this directory.

• w0 : World4
• w1 : World4
• w2 : World4
• w3 : World4

@[instance_reducible]

instance DTS.instDecidableEqWorld4 : DecidableEq World4

Equations

• DTS.instDecidableEqWorld4 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DTS.instReprWorld4 : Repr World4

Equations

• DTS.instReprWorld4 = { reprPrec := DTS.instReprWorld4.repr }

def DTS.instReprWorld4.repr : World4 → ℕ → Std.Format

Equations

• DTS.instReprWorld4.repr DTS.World4.w0 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DTS.World4.w0")).group prec✝
• DTS.instReprWorld4.repr DTS.World4.w1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DTS.World4.w1")).group prec✝
• DTS.instReprWorld4.repr DTS.World4.w2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DTS.World4.w2")).group prec✝
• DTS.instReprWorld4.repr DTS.World4.w3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "DTS.World4.w3")).group prec✝

@[instance_reducible]

instance DTS.instInhabitedWorld4 : Inhabited World4

Equations

• DTS.instInhabitedWorld4 = { default := DTS.instInhabitedWorld4.default }

@[instance_reducible]

instance DTS.instFintypeWorld4 : Fintype World4

Equations

• DTS.instFintypeWorld4 = { elems := {DTS.World4.w0, DTS.World4.w1, DTS.World4.w2, DTS.World4.w3}, complete := DTS.instFintypeWorld4._proof_1 }

@[instance_reducible]

instance DTS.instMeasurableSpaceWorld4 : MeasurableSpace World4

Equations

• DTS.instMeasurableSpaceWorld4 = ⊤

instance DTS.instDiscreteMeasurableSpaceWorld4 : DiscreteMeasurableSpace World4

Core types

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

A DTS context: a dichotomic hypothesis topic (the proposition H, with ¬H implicit) plus a prior measure over worlds.

Following mathlib's Filter.principal pattern, the polar interrogative {H, ¬H} is not packaged as a separate wrapper type — the topic is stored directly, and the inquisitive view is recovered on demand via Context.toCoreIssue.

• topic : Set W

  The hypothesis H. The dichotomic issue {H, ¬H} is recovered as Question.polar topic.

• topicMeasurable : MeasurableSet self.topic

  Measurability of the topic, so that conditioning on H and ¬H is well-behaved. Free (.of_discrete) on the discrete study enums.

• 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

Swap the issue: replace H with ¬H.

Equations

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

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

Forgetful projection from a DTS context to the general Question lattice via the polar interrogative content of the topic proposition. The two representations agree on the underlying question semantics: a DTS dichotomy {H, ¬H} is exactly the polar interrogative of H, with two alternatives ⟦H⟧ and ⟦¬H⟧.

Equations

• ctx.toCoreIssue = Question.polar {w : W | ctx.topic w}

@[simp]

theorem DTS.Context.toCoreIssue_info {W : Type u_1} [MeasurableSpace W] (ctx : Context W) : ctx.toCoreIssue.info = Set.univ

Every DTS dichotomic issue is non-informative (info = univ): the question {H, ¬H} itself rules out no worlds; only an answer to it does. Inherited from Question.info_polar.

theorem DTS.Context.toCoreIssue_isInquisitive_iff {W : Type u_1} [MeasurableSpace W] (ctx : Context W) : ctx.toCoreIssue.isInquisitive ↔ {w : W | ctx.topic w} ≠ ∅ ∧ {w : W | ctx.topic w} ≠ Set.univ

A DTS dichotomy is genuinely inquisitive (raises an unsettled question over the universal info state) iff its topic is non-trivial: neither everything nor nothing satisfies H. Inherited from Question.isInquisitive_polar_iff.

The induced binary testing problem

A context is a binary statistical model: the parameter space is Bool, and each side of the issue generates data from the prior conditioned on it. Context.conditional is the model's family of data-generating distributions and Context.hypothesisKernel packages it as the kernel of the testing problem (the shape of Degenne's twoHypKernel μ ν).

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

The data-generating distribution of each side of the issue: 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ᶜ]

theorem DTS.Context.conditional_swapIssue {W : Type u_1} [MeasurableSpace W] (ctx : Context W) (θ : Bool) : (swapIssue ctx).conditional θ = ctx.conditional !θ

Swapping the issue reindexes the conditionals along negation.

noncomputable def DTS.Context.hypothesisKernel {W : Type u_1} [MeasurableSpace W] (ctx : Context W) : ProbabilityTheory.Kernel Bool W

The data-generating kernel of the induced binary testing problem.

Equations

• ctx.hypothesisKernel = ProbabilityTheory.Kernel.ofFunOfCountable ctx.conditional

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

The parameter prior of the induced binary testing problem: the issue splits the prior's total mass.

Equations

• ctx.hypothesisPrior = ctx.prior ctx.topic • MeasureTheory.Measure.dirac true + ctx.prior ctx.topicᶜ • MeasureTheory.Measure.dirac false

@[simp]

theorem DTS.Context.hypothesisKernel_apply {W : Type u_1} [MeasurableSpace W] (ctx : Context W) (θ : Bool) : ctx.hypothesisKernel θ = ctx.conditional θ

@[simp]

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

@[simp]

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

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

A live issue: 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

Bayes factor: P(E∣H) / P(E∣¬H), in ℝ≥0∞ — the likelihood ratio of the induced binary testing problem. 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 = ProbabilityTheory.likelihoodRatio (ctx.conditional true) (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.bayesFactor_eq_hypothesisKernel_div {W : Type u_1} [MeasurableSpace W] (ctx : Context W) (e : Set W) : bayesFactor ctx e = (ctx.hypothesisKernel true) e / (ctx.hypothesisKernel false) e

bayesFactor is the likelihood ratio of the induced testing problem.

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

E is positively relevant to H: BF > 1 (E confirms H).

Equations

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

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

E is negatively relevant to H: BF < 1 (E disconfirms H).

Equations

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

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

E is irrelevant to H: BF = 1 (E neither confirms nor disconfirms).

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 have opposite relevance signs w.r.t. H.

Merin's "contrariness": one supports H while the other supports ¬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.

Cross-product characterizations

The relevance signs in real-valued cross-product mass form — the ENNReal→ℝ transfer done once, edge cases included; the particle files consume these.

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 (ctx.topicᶜ ∩ e)).toReal * (ctx.prior ctx.topic).toReal < (ctx.prior (ctx.topic ∩ e)).toReal * (ctx.prior ctx.topicᶜ).toReal

Positive relevance as a cross-product 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 (ctx.topic ∩ e)).toReal * (ctx.prior ctx.topicᶜ).toReal < (ctx.prior (ctx.topicᶜ ∩ e)).toReal * (ctx.prior ctx.topic).toReal

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

Merin's Conditional Independence Presumption (Def. 6): A and B are independent under the prior conditioned on each side of the issue — mathlib's IndepSet at both conditionals.

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ᶜ]

The product-equation characterization of issue-conditional independence: P(A∧B∣H) = P(A∣H)·P(B∣H) and likewise given ¬H.

Sign reversal

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

Corollary 3 (qualitative sign reversal): E is positively relevant to H iff E is negatively relevant to ¬H.

The ordinal content of r_H(E) = −r_{¬H}(E).

theorem DTS.sign_reversal {W : Type u_1} [MeasurableSpace W] (ctx : Context W) [MeasureTheory.IsFiniteMeasure ctx.prior] (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

Corollary 3 (quantitative): BF_H(E) · BF_{¬H}(E) = 1.

Exact when both conditional probabilities are nonzero.

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

Fact 2: relevance is the differential of conditional informativeness — 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 DTS.CondIndepIssue.bayesFactor_inter {W : Type u_1} [MeasurableSpace W] {ctx : Context W} [MeasureTheory.IsFiniteMeasure ctx.prior] {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

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

theorem DTS.CondIndepIssue.max_bayesFactor_lt_inter {W : Type u_1} [MeasurableSpace W] {ctx : Context W} [MeasureTheory.IsFiniteMeasure ctx.prior] [ctx.Nondegenerate] {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)

Theorem 6a (conjunction): under issue-conditional independence with both A, B positively relevant, conjunction dominates both conjuncts.

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)

Theorem 6a (disjunction, upper): under issue-conditional independence with both A, B positively relevant, the disjunction is dominated by the stronger disjunct.

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)

Theorem 6a (disjunction, lower): under issue-conditional independence with both A, B positively relevant, the disjunction is still positively relevant.

The Bayesian bridge

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

Probabilistic support implies positive relevance over a live issue: the Bayes-theorem bridge P(E∣H) > P(E) ⟹ BF_H(E) > 1. The edge case P(E ∩ ¬H) = 0 needs no special treatment: the factor is then genuinely infinite.

Promoted from the IKW2025 Part II "Bayesian-to-DTS bridge" in 0.230.502 — pure DTS-internal content (no IKW dependency), belongs in DTS Core.

theorem DTS.not_lt_cond_of_negRelevant {W : Type u_1} [MeasurableSpace W] (ctx : Context W) [MeasureTheory.IsProbabilityMeasure ctx.prior] [ctx.Nondegenerate] (e : Set W) (hNeg : negRelevant ctx e) : ¬ctx.prior e < ctx.prior[e | ctx.topic]

Negative relevance implies non-support: the contrapositive of posRelevant_of_lt_cond. Promoted from IKW2025 Part II in 0.230.502.

Exclusive disjunction

theorem DTS.xor_not_necessarily_positive : ∃ (ctx : Context World4) (a : Set World4) (b : Set World4), posRelevant ctx a ∧ posRelevant ctx b ∧ ¬posRelevant ctx (symmDiff a b)

Theorem 6b: XOR of two positively relevant propositions is not necessarily positively relevant.

Counterexample on World4: H = {w0}, A = {w0, w1}, B = {w0, w2}, counting prior. BF(A) = BF(B) = 3, but A ∆ B = {w1, w2} misses H entirely, so its Bayes factor is 0.

Risk of the induced problem

theorem DTS.avgRisk_hypothesisKernel {W : Type u_1} [MeasurableSpace W] {𝓨 : Type u_2} [MeasurableSpace 𝓨] (ctx : Context W) (ℓ : Bool → 𝓨 → ENNReal) (κ : ProbabilityTheory.Kernel W 𝓨) : ProbabilityTheory.avgRisk ℓ ctx.hypothesisKernel κ ctx.hypothesisPrior = (∫⁻ (y : 𝓨), ℓ true y ∂(κ.comp ctx.hypothesisKernel) true) * ctx.prior ctx.topic + (∫⁻ (y : 𝓨), ℓ false y ∂(κ.comp ctx.hypothesisKernel) false) * ctx.prior ctx.topicᶜ

The average risk of an estimator against the induced testing problem, in its finite two-point form: the loss on each side of the issue weighted by that side's prior mass (the countable-space register of Mathlib.Probability.Decision.Risk.Countable).