Decision-Theoretic Semantics: "But" (@cite{merin-1999} §4)

@cite{merin-1999}

Merin's DTS account of adversative conjunction. The felicity of "A but B" requires that A and B have opposite relevance signs, and that the conjunction A∧B is negatively relevant (the "but"-clause wins). The default interpretation sets H = B, yielding unexpected-B-given-A.

Key Definitions

• butFelicitous (Hypothesis 4): felicity conditions for "A but B"
• NNIR (Def. 10): Non-Negative Instantial Relevance
• defaultButCtx: the default interpretation where H = B

Main Results

• Theorem 8: CIP + contrariness → unexpectedness (P(B|A) < P(B))
• Theorem 9: When H = B, CIP holds automatically
• Theorem 10: Properties of default-but interpretation
• Corollary 11 (Harris universal): NNIR prevents "Qa but Qb"

def DTS.But.butFelicitous {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

Hypothesis 4: Felicity conditions for "A but B".

"A but B" is felicitous iff: (i) A is positively relevant to H, (ii) B is negatively relevant to H, (iii) A∧B is negatively relevant to H (B "wins").

Equations

• DTS.But.butFelicitous ctx a b = (DTS.posRelevant ctx a ∧ DTS.negRelevant ctx b ∧ DTS.negRelevant ctx (a ∩ b))

def DTS.But.NNIR {W : Type u_1} [Fintype W] (E : Type u_2) (prior : W → ℚ) (Q : E → Set W) [(e : E) → DecidablePred fun (x : W) => x ∈ Q e] : Prop

Definition 10: Non-Negative Instantial Relevance (NNIR).

For a predicate Q over entities, observing Q(a) never makes Q(b) less probable: P(Q(b)|Q(a)) ≥ P(Q(b)) for all a, b.

This captures a cross-linguistic universal: properties are positively correlated across instances (knowing one dog is friendly makes it more likely another is).

Equations

• DTS.But.NNIR E prior Q = ∀ (a b : E), DTS.condProb prior (Q b) (Q a) ≥ DTS.probSum prior (Q b)

def DTS.But.defaultButCtx {W : Type u_1} (prior : W → ℚ) (b : Set W) [DecidablePred fun (x : W) => x ∈ b] : DTSContext W

Default "but" context: the issue is identified with the but-clause itself (H = B).

Merin argues this is the preferred interpretation when no explicit issue is provided.

Equations

• DTS.But.defaultButCtx prior b = { topic := b, topicDec := inferInstance, prior := prior }

theorem DTS.But.cip_contrariness_implies_unexpectedness {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] (hPrior : ∀ (w : W), ctx.prior w ≥ 0) (hNorm : probSum ctx.prior Set.univ = 1) (hcip : CIP ctx a b) (hcontr : hContrary ctx a b) (hA_pos : 0 < probSum ctx.prior a) (hH_pos : 0 < probSum ctx.prior ctx.topic) (hNH_pos : 0 < probSum ctx.prior ctx.topicᶜ) : condProb ctx.prior b a < probSum ctx.prior b

Theorem 8: CIP + contrariness implies unexpectedness.

If A and B are conditionally independent given H and ¬H, and have opposite relevance signs, then P(B|A) < P(B) — B is unexpected given A.

Proof sketch: CIP gives P(B|H,A) = P(B|H) and P(B|¬H,A) = P(B|¬H). By total probability: P(B|A) = P(B|H)·P(H|A) + P(B|¬H)·P(¬H|A). And P(B) = P(B|H)·P(H) + P(B|¬H)·P(¬H). So P(B|A) - P(B) = (P(B|H) - P(B|¬H))·(P(H|A) - P(H)). Contrariness makes the two factors have opposite signs, giving P(B|A) < P(B).

theorem DTS.But.topic_eq_b_satisfies_cip {W : Type u_1} [Fintype W] (prior : W → ℚ) (a b : Set W) [DecidablePred fun (x : W) => x ∈ a] [DecidablePred fun (x : W) => x ∈ b] : CIP (defaultButCtx prior b) a b

Theorem 9: When H = B, CIP holds automatically for any A.

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

theorem DTS.But.default_but_properties {W : Type u_1} [Fintype W] (prior : W → ℚ) (a b : Set W) [DecidablePred fun (x : W) => x ∈ a] [DecidablePred fun (x : W) => x ∈ b] (hPrior : ∀ (w : W), prior w ≥ 0) (hNorm : probSum prior Set.univ = 1) (hNegA : negRelevant (defaultButCtx prior b) a) (hB_pos : 0 < probSum prior b) (hNotB_pos : 0 < probSum prior bᶜ) (hAnB_pos : 0 < probSum prior (a ∩ bᶜ)) : condProb prior b a < probSum prior b

Theorem 10: Negative relevance implies unexpectedness in default-but.

When the issue is B itself and A is negatively relevant to H=B, then P(B|A) < P(B) — B is unexpected given A.

The proof uses Bayes' reciprocity: negative relevance gives P(A|B)/P(A|¬B) < 1, so P(A∧B)·P(¬B) < P(A∧¬B)·P(B). By total probability P(A) = P(A∧B) + P(A∧¬B) and normalization P(B) + P(¬B) = 1, this yields P(A∧B) < P(A)·P(B), hence P(B|A) = P(A∧B)/P(A) < P(B) = probSum prior B.

TODO: This proof currently times out during elaboration of the bayesFactor unfolding step due to defaultButCtx field projections not reducing through simp only. Restructure to expose the underlying prior/topic equations before invoking if_neg/div_lt_one.

theorem DTS.But.harris_universal {W : Type u_1} [Fintype W] {E : Type u_2} (prior : W → ℚ) (Q : E → Set W) [(e : E) → DecidablePred fun (x : W) => x ∈ Q e] (a b : E) (_hnnir : NNIR E prior Q) : ¬butFelicitous (defaultButCtx prior (Q b)) (Q a) (Q b)

Corollary 11 (Harris universal): NNIR prevents "Qa but Qb".

Under NNIR, "Q(a) but Q(b)" is never felicitous in the default-but interpretation. When H = Q(b), the Bayes factor BF_{Q(b)}(Q(b)) is P(Q(b)|Q(b))/P(Q(b)|¬Q(b)) = 1/0 ≥ 1, so Q(b) cannot be negatively relevant to itself, violating the butFelicitous requirement.

Theorem 13 (not formalized): Savage-Kemeny-Gaifman-Humburg theorem.

Symmetric probability on finite models extends to infinite models only if NNIR holds. This provides a foundational justification for NNIR as a rationality constraint. Not formalized here (requires measure theory and de Finetti-style exchangeability arguments).

Reference: Gaifman, H. & Snir, M. (1982). Probabilities over rich languages.