Decision-Theoretic Semantics: Core

@cite{merin-1999}

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}.

Predicates over worlds are Set W; arithmetic operations carry [DecidablePred] constraints at use sites following the mathlib idiom.

Key Definitions

• DTSContext — a dichotomic issue (topic : Set W) plus a prior probability distribution. Following mathlib's Filter.principal pattern, the polar interrogative is not given a separate wrapper type: the topic is stored directly, and the inquisitive view is recovered as DTSContext.toCoreIssue ctx = Core.Question.polar {w | ctx.topic w} at consumption sites that need the general inquisitive-content lattice.
• condProb — conditional probability P(E|H) over finite worlds
• bayesFactor — P(E|H) / P(E|¬H), exact rational arithmetic
• posRelevant / negRelevant / irrelevant — ordinal relevance predicates
• hContrary — A and B have opposite relevance signs
• CIP — Conditional Independence Presumption
• (pxor and margProb removed in 0.230.500: use mathlib symmDiff and probSum directly.)

Main Results

• Corollary 3 (sign_reversal): BF_H(E) · BF_{¬H}(E) = 1
• Fact 5 (bayes_factor_multiplicative_under_cip): Under CIP, BF(A∧B) = BF(A) · BF(B)
• Theorem 6b (xor_not_necessarily_positive): Counterexample showing XOR of two positively relevant propositions can be negatively relevant

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

@[implicit_reducible]

instance DTS.instDecidableEqWorld4 : DecidableEq World4

Equations

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

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✝

@[implicit_reducible]

instance DTS.instReprWorld4 : Repr World4

Equations

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

def DTS.instInhabitedWorld4.default : World4

Equations

• DTS.instInhabitedWorld4.default = DTS.World4.w0

@[implicit_reducible]

instance DTS.instInhabitedWorld4 : Inhabited World4

Equations

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

@[implicit_reducible]

instance DTS.instFintypeWorld4 : Fintype World4

Equations

• DTS.instFintypeWorld4 = { elems := { val := ↑DTS.World4.enumList, nodup := DTS.World4.enumList_nodup }, complete := DTS.instFintypeWorld4._proof_1 }

structure DTS.DTSContext (W : Type u_1) : Type u_1

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

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 DTSContext.toCoreIssue.

• topic : Set W

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

• topicDec : DecidablePred fun (x : W) => x ∈ self.topic

  Decidability of topic — required so that arithmetic over finite worlds (probSum, condProb) is well-defined without invoking Classical.propDecidable at every use site.

• prior : W → ℚ

  Prior probability distribution over worlds (rational-valued).

def DTS.swapIssue {W : Type u_1} (ctx : DTSContext W) : DTSContext W

Swap the issue: replace H with ¬H.

Equations

• DTS.swapIssue ctx = { topic := ctx.topicᶜ, topicDec := inferInstance, prior := ctx.prior }

def DTS.DTSContext.toCoreIssue {W : Type u_1} (ctx : DTSContext W) : Core.Question W

Forgetful projection from a DTS context to the general Core.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 = Core.Question.polar {w : W | ctx.topic w}

@[simp]

theorem DTS.DTSContext.toCoreIssue_info {W : Type u_1} (ctx : DTSContext 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 Core.Question.info_polar.

theorem DTS.DTSContext.toCoreIssue_isInquisitive_iff {W : Type u_1} (ctx : DTSContext 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 Core.Question.isInquisitive_polar_iff.

def DTS.probSum {W : Type u_1} [Fintype W] (prior : W → ℚ) (p : Set W) [DecidablePred fun (x : W) => x ∈ p] : ℚ

Sum of prior probabilities over worlds satisfying a predicate.

Equations

• DTS.probSum prior p = ∑ w : W, if w ∈ p then prior w else 0

def DTS.condProb {W : Type u_1} [Fintype W] (prior : W → ℚ) (e h : Set W) [DecidablePred fun (x : W) => x ∈ e] [DecidablePred fun (x : W) => x ∈ h] : ℚ

Conditional probability P(E|H) = P(E∧H) / P(H).

Returns 0 when P(H) = 0 (undefined conditioning).

Equations

• DTS.condProb prior e h = if DTS.probSum prior h = 0 then 0 else DTS.probSum prior (e ∩ h) / DTS.probSum prior h

def DTS.bayesFactor {W : Type u_1} [Fintype W] (ctx : DTSContext W) (e : Set W) [DecidablePred fun (x : W) => x ∈ e] : ℚ

Bayes factor: P(E|H) / P(E|¬H).

The pre-log ratio that determines relevance sign and magnitude. Division-by-zero convention follows ArgumentativeStrength.bayesFactor:

• P(E|¬H) = 0, P(E|H) > 0 → 1000 (effectively +∞)
• P(E|¬H) = 0, P(E|H) = 0 → 1 (neutral)

Equations

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

def DTS.posRelevant {W : Type u_1} [Fintype W] (ctx : DTSContext W) (e : Set W) [DecidablePred fun (x : W) => x ∈ e] : Prop

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

Equations

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

@[implicit_reducible]

instance DTS.instDecidablePosRelevant {W : Type u_1} [Fintype W] (ctx : DTSContext W) (e : Set W) [DecidablePred fun (x : W) => x ∈ e] : Decidable (posRelevant ctx e)

Equations

• DTS.instDecidablePosRelevant ctx e = DTS.instDecidablePosRelevant._aux_1 ctx e

def DTS.negRelevant {W : Type u_1} [Fintype W] (ctx : DTSContext W) (e : Set W) [DecidablePred fun (x : W) => x ∈ e] : Prop

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

Equations

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

@[implicit_reducible]

instance DTS.instDecidableNegRelevant {W : Type u_1} [Fintype W] (ctx : DTSContext W) (e : Set W) [DecidablePred fun (x : W) => x ∈ e] : Decidable (negRelevant ctx e)

Equations

• DTS.instDecidableNegRelevant ctx e = DTS.instDecidableNegRelevant._aux_1 ctx e

def DTS.irrelevant {W : Type u_1} [Fintype W] (ctx : DTSContext W) (e : Set W) [DecidablePred fun (x : W) => x ∈ e] : Prop

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

Equations

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

@[implicit_reducible]

instance DTS.instDecidableIrrelevant {W : Type u_1} [Fintype W] (ctx : DTSContext W) (e : Set W) [DecidablePred fun (x : W) => x ∈ e] : Decidable (irrelevant ctx e)

Equations

• DTS.instDecidableIrrelevant ctx e = DTS.instDecidableIrrelevant._aux_1 ctx e

def DTS.hContrary {W : Type u_1} [Fintype W] (ctx : DTSContext W) (a b : Set W) [DecidablePred fun (x : W) => x ∈ a] [DecidablePred fun (x : W) => x ∈ b] : 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)

def DTS.CIP {W : Type u_1} [Fintype W] (ctx : DTSContext W) (a b : Set W) [DecidablePred fun (x : W) => x ∈ a] [DecidablePred fun (x : W) => x ∈ b] : Prop

Conditional Independence Presumption (CIP, Merin's Def. 6): A and B are conditionally independent given both H and ¬H.

P(A∧B|H) = P(A|H)·P(B|H) and P(A∧B|¬H) = P(A|¬H)·P(B|¬H).

Equations

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

@[implicit_reducible]

instance DTS.Set.symmDiff.decidablePred {α : Type u_1} (a b : Set α) [DecidablePred fun (x : α) => x ∈ a] [DecidablePred fun (x : α) => x ∈ b] : DecidablePred fun (x : α) => x ∈ symmDiff a b

Decidability of membership in a symmetric difference, given decidability of membership in each component. Not in mathlib for Set α; added here so posRelevant ctx (a ∆ b) resolves.

Equations

• DTS.Set.symmDiff.decidablePred a b w = decidable_of_iff (w ∈ a ∧ w ∉ b ∨ w ∈ b ∧ w ∉ a) ⋯

theorem DTS.probSum_nonneg {W : Type u_1} [Fintype W] (prior : W → ℚ) (hP : ∀ (w : W), prior w ≥ 0) (p : Set W) [DecidablePred fun (x : W) => x ∈ p] : probSum prior p ≥ 0

probSum is non-negative when prior is non-negative.

theorem DTS.probSum_partition {W : Type u_1} [Fintype W] (prior : W → ℚ) (e h : Set W) [DecidablePred fun (x : W) => x ∈ e] [DecidablePred fun (x : W) => x ∈ h] : probSum prior e = probSum prior (e ∩ h) + probSum prior (e ∩ hᶜ)

Partition: P(e) = P(e ∩ h) + P(e ∩ hᶜ) for any decidable conditioning set h. The DTS-side mirror of PMF.probOfSet_partition.

theorem DTS.probSum_compl {W : Type u_1} [Fintype W] (prior : W → ℚ) (h : Set W) [DecidablePred fun (x : W) => x ∈ h] : probSum prior h + probSum prior hᶜ = probSum prior Set.univ

Total mass: P(h) + P(hᶜ) = P(univ). With normalization P(univ) = 1, yields P(hᶜ) = 1 − P(h). The DTS-side mirror of PMF.probOfSet_compl_add.

noncomputable def DTS.priorAsPMF {W : Type u_1} [Fintype W] (prior : W → ℚ) (hNonneg : ∀ (w : W), prior w ≥ 0) (hSum : ∑ w : W, prior w = 1) : PMF W

Lift a non-negative ℚ-valued prior summing to 1 over a finite type to a mathlib PMF. Per 0.230.500 audit, this is the bridge constructor for incremental DTS→PMF migration: any DTS theorem can opt into mathlib's PMF.probOfSet/PMF.condProbSet lemmas via priorAsPMF without forcing all sibling theorems to migrate.

Equations

• DTS.priorAsPMF prior hNonneg hSum = PMF.ofFintype (fun (w : W) => ENNReal.ofReal ↑(prior w)) ⋯

@[simp]

theorem DTS.priorAsPMF_apply {W : Type u_1} [Fintype W] (prior : W → ℚ) (hNonneg : ∀ (w : W), prior w ≥ 0) (hSum : ∑ w : W, prior w = 1) (w : W) : (priorAsPMF prior hNonneg hSum) w = ENNReal.ofReal ↑(prior w)

Bridge lemma: each individual mass under priorAsPMF is the ENNReal coercion of the original ℚ prior.

theorem DTS.probSum_toReal_eq_probOfSet {W : Type u_1} [Fintype W] (prior : W → ℚ) (hNonneg : ∀ (w : W), prior w ≥ 0) (hSum : ∑ w : W, prior w = 1) (s : Set W) [DecidablePred fun (x : W) => x ∈ s] : ↑(probSum prior s) = ((priorAsPMF prior hNonneg hSum).probOfSet s).toReal

Bridge lemma: probSum (ℚ) and PMF.probOfSet (ENNReal) agree after coercion through ℝ/ENNReal. The toReal direction is the practical one — most consumers want ℚ-valued probabilities.

theorem DTS.sign_reversal_qual {W : Type u_1} [Fintype W] (ctx : DTSContext W) (e : Set W) [DecidablePred fun (x : W) => x ∈ e] (hEH : condProb ctx.prior e ctx.topic > 0) (hENotH : condProb 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} [Fintype W] (ctx : DTSContext W) (e : Set W) [DecidablePred fun (x : W) => x ∈ e] (hENotH : condProb ctx.prior e ctx.topicᶜ ≠ 0) (hEH : condProb 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 conditional probabilities are nonzero.

theorem DTS.relevance_as_differential_inf : True

Fact 2: Relationship between relevance and conditional informativeness.

r_H(E) = inf(E, H) − inf(E, ¬H) where inf(E,X) = −log P(E|X). That is, relevance is the differential of conditional informativeness.

Not provable in ℚ (requires logarithm properties).

theorem DTS.bayes_factor_multiplicative_under_cip {W : Type u_1} [Fintype W] (ctx : DTSContext W) (a b : Set W) [DecidablePred fun (x : W) => x ∈ a] [DecidablePred fun (x : W) => x ∈ b] (hcip : CIP ctx a b) (hNotH : condProb ctx.prior a ctx.topicᶜ ≠ 0) (hNotH' : condProb ctx.prior b ctx.topicᶜ ≠ 0) (hABNotH : condProb ctx.prior (a ∩ b) ctx.topicᶜ ≠ 0) : bayesFactor ctx (a ∩ b) = bayesFactor ctx a * bayesFactor ctx b

Fact 5: Under CIP, Bayes factor is multiplicative over conjunction.

BF(A∧B) = BF(A) · BF(B) when A and B are conditionally independent given both H and ¬H.

theorem DTS.conjunction_dominates_conjuncts {W : Type u_1} [Fintype W] (ctx : DTSContext W) (a b : Set W) [DecidablePred fun (x : W) => x ∈ a] [DecidablePred fun (x : W) => x ∈ b] (hcip : CIP ctx a b) (hPosA : posRelevant ctx a) (hPosB : posRelevant ctx b) (hNonzero : condProb ctx.prior a ctx.topicᶜ ≠ 0) (hNonzero' : condProb ctx.prior b ctx.topicᶜ ≠ 0) (hABNonzero : condProb ctx.prior (a ∩ b) ctx.topicᶜ ≠ 0) : bayesFactor ctx (a ∩ b) > max (bayesFactor ctx a) (bayesFactor ctx b)

Theorem 6a (part 1): Under CIP with both A,B positively relevant, conjunction dominates both conjuncts: BF(A∧B) > max(BF(A), BF(B)).

theorem DTS.conjunction_dominates_disjunction {W : Type u_1} [Fintype W] (ctx : DTSContext W) (a b : Set W) [DecidablePred fun (x : W) => x ∈ a] [DecidablePred fun (x : W) => x ∈ b] (hcip : CIP ctx a b) (hPosA : posRelevant ctx a) (hPosB : posRelevant ctx b) (hNonzero : condProb ctx.prior a ctx.topicᶜ ≠ 0) (hNonzero' : condProb ctx.prior b ctx.topicᶜ ≠ 0) (hABNonzero : condProb ctx.prior (a ∩ b) ctx.topicᶜ ≠ 0) (hPrior : ∀ (w : W), ctx.prior w ≥ 0) : bayesFactor ctx (a ∩ b) > max (bayesFactor ctx a) (bayesFactor ctx b) ∧ max (bayesFactor ctx a) (bayesFactor ctx b) > bayesFactor ctx (a ∪ b) ∧ bayesFactor ctx (a ∪ b) > 1

Theorem 6a (full): Under CIP with both A,B positively relevant, BF(A∧B) > max(BF(A), BF(B)) > BF(A∨B) > 1.

The disjunction ordering requires inclusion-exclusion on conditional probabilities: P(A∨B|X) = P(A|X) + P(B|X) - P(A∧B|X).

theorem DTS.probSupports_implies_posRelevant_binary {W : Type u_1} [Fintype W] (prior : W → ℚ) (topic : Set W) [DecidablePred fun (x : W) => x ∈ topic] (evidence : Set W) [DecidablePred fun (x : W) => x ∈ evidence] (hH_pos : probSum prior topic > 0) (hNH_pos : probSum prior topicᶜ > 0) (_hS_pos : probSum prior evidence > 0) (hNonneg : ∀ (w : W), prior w ≥ 0) (hNorm : probSum prior Set.univ = 1) (hSupp : condProb prior evidence topic > probSum prior evidence) : posRelevant { topic := topic, topicDec := inferInstance, prior := prior } evidence

Probabilistic support implies DTS positive relevance for binary issues. The Bayes-theorem bridge: P(H|E) > P(E) ⟹ BF_H(E) > 1.

Discharged via the DTS-side partition law (probSum_partition) plus the normalization P(H) + P(¬H) = 1 (probSum_compl + hNorm). Edge case P(E ∩ ¬H) = 0 is handled separately: the if-branches in bayesFactor's definition return 1000 when P(E|¬H) = 0 and P(E|H) > 0, both established from the partition.

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.negRelevant_implies_not_probSupports {W : Type u_1} [Fintype W] (prior : W → ℚ) (topic : Set W) [DecidablePred fun (x : W) => x ∈ topic] (evidence : Set W) [DecidablePred fun (x : W) => x ∈ evidence] (hH_pos : probSum prior topic > 0) (hNH_pos : probSum prior topicᶜ > 0) (hS_pos : probSum prior evidence > 0) (hNonneg : ∀ (w : W), prior w ≥ 0) (hNorm : probSum prior Set.univ = 1) (hNeg : negRelevant { topic := topic, topicDec := inferInstance, prior := prior } evidence) : ¬condProb prior evidence topic > probSum prior evidence

Negative relevance (DTS) implies non-support (probabilistic).

Contrapositive of probSupports_implies_posRelevant_binary. Promoted from IKW2025 Part II in 0.230.502.

theorem DTS.xor_not_necessarily_positive : ∃ (ctx : DTSContext World4) (a : Set World4) (b : Set World4) (x : DecidablePred fun (x : World4) => x ∈ a) (x_1 : DecidablePred fun (x : World4) => x ∈ b), 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}, uniform prior. BF(A) = 3, BF(B) = 3, but A⊕B = {w1,w2} has BF = 0 (not pos relevant).

TODO: Reconstruct the concrete counterexample in the new Prop-based formulation. The mathematical content is unchanged from the Bool-era formulation: the World4 witnesses still work, but threading the DecidablePred instances through decide requires care.