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

Key Definitions

• Issue — a dichotomic hypothesis {H, ¬H}
• DTSContext — issue + prior probability
• 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 — exclusive disjunction for BProp

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

structure Theories.DTS.Issue (W : Type u_1) : Type u_1

A dichotomic issue {H, ¬H}, the hypothesis under consideration.

• topic : BProp W

  The hypothesis H (as a decidable proposition).

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

A DTS context: a dichotomic issue plus a prior probability distribution.

• issue : Issue W

  The dichotomic issue {H, ¬H}.

• prior : W → ℚ

  Prior probability distribution over worlds (rational-valued).

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

Swap the issue: replace H with ¬H.

Equations

• Theories.DTS.swapIssue ctx = { issue := { topic := Core.Proposition.Decidable.pnot W ctx.issue.topic }, prior := ctx.prior }

def Theories.DTS.probSum {W : Type u_1} [Fintype W] (prior : W → ℚ) (p : BProp W) : ℚ

Sum of prior probabilities over worlds satisfying a predicate.

Equations

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

def Theories.DTS.condProb {W : Type u_1} [Fintype W] (prior : W → ℚ) (e h : BProp W) : ℚ

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

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

Equations

• Theories.DTS.condProb prior e h = if Theories.DTS.probSum prior h = 0 then 0 else Theories.DTS.probSum prior (Core.Proposition.Decidable.pand W e h) / Theories.DTS.probSum prior h

def Theories.DTS.margProb {W : Type u_1} [Fintype W] (prior : W → ℚ) (e : BProp W) : ℚ

Marginal (unconditional) probability P(E) = P(E|⊤).

Equations

• Theories.DTS.margProb prior e = Theories.DTS.probSum prior e

def Theories.DTS.bayesFactor {W : Type u_1} [Fintype W] (ctx : DTSContext W) (e : BProp W) : ℚ

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 Theories.DTS.posRelevant {W : Type u_1} [Fintype W] (ctx : DTSContext W) (e : BProp W) : Prop

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

Equations

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

instance Theories.DTS.instDecidablePosRelevant {W : Type u_1} [Fintype W] (ctx : DTSContext W) (e : BProp W) : Decidable (posRelevant ctx e)

Equations

• Theories.DTS.instDecidablePosRelevant ctx e = inferInstanceAs (Decidable (Theories.DTS.bayesFactor ctx e > 1))

def Theories.DTS.negRelevant {W : Type u_1} [Fintype W] (ctx : DTSContext W) (e : BProp W) : Prop

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

Equations

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

instance Theories.DTS.instDecidableNegRelevant {W : Type u_1} [Fintype W] (ctx : DTSContext W) (e : BProp W) : Decidable (negRelevant ctx e)

Equations

• Theories.DTS.instDecidableNegRelevant ctx e = inferInstanceAs (Decidable (Theories.DTS.bayesFactor ctx e < 1))

def Theories.DTS.irrelevant {W : Type u_1} [Fintype W] (ctx : DTSContext W) (e : BProp W) : Prop

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

Equations

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

instance Theories.DTS.instDecidableIrrelevant {W : Type u_1} [Fintype W] (ctx : DTSContext W) (e : BProp W) : Decidable (irrelevant ctx e)

Equations

• Theories.DTS.instDecidableIrrelevant ctx e = inferInstanceAs (Decidable (Theories.DTS.bayesFactor ctx e = 1))

def Theories.DTS.hContrary {W : Type u_1} [Fintype W] (ctx : DTSContext W) (a b : BProp 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

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

def Theories.DTS.CIP {W : Type u_1} [Fintype W] (ctx : DTSContext W) (a b : BProp W) : 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.

def Theories.DTS.pxor {W : Type u_1} (a b : BProp W) : BProp W

Exclusive disjunction (XOR) for decidable propositions.

Equations

• Theories.DTS.pxor a b w = (a w ^^ b w)

theorem Theories.DTS.sign_reversal_qual {W : Type u_1} [Fintype W] (ctx : DTSContext W) (e : BProp W) (hEH : condProb ctx.prior e ctx.issue.topic > 0) (hENotH : condProb ctx.prior e (Core.Proposition.Decidable.pnot W ctx.issue.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 Theories.DTS.sign_reversal {W : Type u_1} [Fintype W] (ctx : DTSContext W) (e : BProp W) (hENotH : condProb ctx.prior e (Core.Proposition.Decidable.pnot W ctx.issue.topic) ≠ 0) (hEH : condProb ctx.prior e ctx.issue.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 Theories.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 Theories.DTS.bayes_factor_multiplicative_under_cip {W : Type u_1} [Fintype W] (ctx : DTSContext W) (a b : BProp W) (hcip : CIP ctx a b) (hNotH : condProb ctx.prior a (Core.Proposition.Decidable.pnot W ctx.issue.topic) ≠ 0) (hNotH' : condProb ctx.prior b (Core.Proposition.Decidable.pnot W ctx.issue.topic) ≠ 0) (hABNotH : condProb ctx.prior (Core.Proposition.Decidable.pand W a b) (Core.Proposition.Decidable.pnot W ctx.issue.topic) ≠ 0) : bayesFactor ctx (Core.Proposition.Decidable.pand W 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 Theories.DTS.conjunction_dominates_conjuncts {W : Type u_1} [Fintype W] (ctx : DTSContext W) (a b : BProp W) (hcip : CIP ctx a b) (hPosA : posRelevant ctx a) (hPosB : posRelevant ctx b) (hNonzero : condProb ctx.prior a (Core.Proposition.Decidable.pnot W ctx.issue.topic) ≠ 0) (hNonzero' : condProb ctx.prior b (Core.Proposition.Decidable.pnot W ctx.issue.topic) ≠ 0) (hABNonzero : condProb ctx.prior (Core.Proposition.Decidable.pand W a b) (Core.Proposition.Decidable.pnot W ctx.issue.topic) ≠ 0) : bayesFactor ctx (Core.Proposition.Decidable.pand W 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 Theories.DTS.conjunction_dominates_disjunction {W : Type u_1} [Fintype W] (ctx : DTSContext W) (a b : BProp W) (hcip : CIP ctx a b) (hPosA : posRelevant ctx a) (hPosB : posRelevant ctx b) (hNonzero : condProb ctx.prior a (Core.Proposition.Decidable.pnot W ctx.issue.topic) ≠ 0) (hNonzero' : condProb ctx.prior b (Core.Proposition.Decidable.pnot W ctx.issue.topic) ≠ 0) (hABNonzero : condProb ctx.prior (Core.Proposition.Decidable.pand W a b) (Core.Proposition.Decidable.pnot W ctx.issue.topic) ≠ 0) (hPrior : ∀ (w : W), ctx.prior w ≥ 0) : bayesFactor ctx (Core.Proposition.Decidable.pand W a b) > max (bayesFactor ctx a) (bayesFactor ctx b) ∧ max (bayesFactor ctx a) (bayesFactor ctx b) > bayesFactor ctx (Core.Proposition.Decidable.por W a b) ∧ bayesFactor ctx (Core.Proposition.Decidable.por W 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).

instance Theories.DTS.instFintypeWorld4 : Fintype Core.Proposition.World4

Equations

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

theorem Theories.DTS.xor_not_necessarily_positive : ∃ (ctx : DTSContext Core.Proposition.World4) (a : BProp Core.Proposition.World4) (b : BProp Core.Proposition.World4), posRelevant ctx a ∧ posRelevant ctx b ∧ ¬posRelevant ctx (pxor 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).