Decision-Theoretic Semantics: "Also" (@cite{merin-1999} §5.2–5.4)

@cite{merin-1999}

Merin's DTS account of additive particles. Presupposition is modeled as i-irrelevance: a presupposed proposition is one that doesn't change any conditional probability. "Also" requires topic-anaphoric salience — the antecedent D must have been relevant before becoming presupposed.

Key Definitions

• presupposedIrrelevant (Def. 12): presupposition as informational inertness
• topicAnaphoricSalience (Def. 13): conditions for anaphoric antecedent
• alsoFelicitous (Hypothesis 8): felicity conditions for "and also"
• properlyAccommodable (partial Def. 14): accommodable propositions

Main Results

• Corollary 15 (also_nonidentity): "also" requires non-identity (a ≠ b)
• Fact 17 (presuppositional_independence_additivity): presupposition implies multiplicativity of Bayes factor without CIP

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

Definition 12: A proposition A is i-presupposed iff conditioning on A doesn't change any conditional probability.

This is stronger than P(A)=1: it means A is informationally inert. Formally: P(X|A) = P(X) for all X, which is equivalent to P(X|A) = P(X|⊤) for all X.

Equations

• DTS.Also.presupposedIrrelevant prior a = ∀ (x : Set W) [inst : DecidablePred fun (x_1 : W) => x_1 ∈ x], DTS.condProb prior x a = DTS.condProb prior x Set.univ

structure DTS.Also.TopicAnaphoricSalience {W : Type u_1} [Fintype W] (ctx : DTSContext W) (d e : Set W) [DecidablePred fun (x : W) => x ∈ d] [DecidablePred fun (x : W) => x ∈ e] : Type

Definition 13: Topic-anaphoric salience.

D is topic-anaphorically salient for E in context iff: (i) E is relevant to the current issue H, (ii) D is presupposed (informationally inert), (iii) D was recently relevant — before becoming presupposed, D bore on the issue.

This captures the discourse requirement of "also": the antecedent must have been relevant before being taken for granted.

• eRelevant : posRelevant ctx e ∨ negRelevant ctx e

  E is relevant to the current issue.

• dPresupposed : presupposedIrrelevant ctx.prior d

  D is currently presupposed (informationally inert).

• dWasRelevant : ScalarImplicature.RelevanceSign

  D was previously relevant (before becoming presupposed).

structure DTS.Also.AlsoFelicitous {W : Type u_1} [Fintype W] (ctx : DTSContext W) (qa qb : Set W) [DecidablePred fun (x : W) => x ∈ qa] [DecidablePred fun (x : W) => x ∈ qb] : Type

Hypothesis 8: Felicity conditions for "and also(b, B)".

For "Q(a) and also Q(b)": Q(a) and Q(b) have the same relevance sign (both support or both oppose H). This distinguishes "and also" from "but also" (opposite signs).

The previousSign field records the relevance sign of Q(a) before it was presupposed; currentSign is the relevance sign of Q(b) now.

• qaPresupposed : presupposedIrrelevant ctx.prior qa

  Q(a) is presupposed.

• qbRelevant : posRelevant ctx qb ∨ negRelevant ctx qb

  Q(b) is relevant.

• sameSign : ScalarImplicature.RelevanceSign

  Same relevance sign: Q(a) had the same sign as Q(b) before presupposition.

• signMatches : ScalarImplicature.sgnRelevance ctx qb = self.sameSign

  The sign matches Q(b)'s current relevance direction.

structure DTS.Also.ButAlsoFelicitous {W : Type u_1} [Fintype W] (ctx : DTSContext W) (qa qb : Set W) [DecidablePred fun (x : W) => x ∈ qa] [DecidablePred fun (x : W) => x ∈ qb] : Type

"But also" variant: opposite relevance signs.

"Q(a) but also Q(b)": Q(a) had the opposite relevance sign from Q(b). This combines adversativity ("but") with additivity ("also").

• qaPresupposed : presupposedIrrelevant ctx.prior qa

  Q(a) is presupposed.

• qbRelevant : posRelevant ctx qb ∨ negRelevant ctx qb

  Q(b) is relevant.

• previousSign : ScalarImplicature.RelevanceSign

  Previous sign of Q(a).

• currentSign : ScalarImplicature.RelevanceSign

  Current sign of Q(b).

• oppositeSigns : self.previousSign = ScalarImplicature.RelevanceSign.pos ∧ self.currentSign = ScalarImplicature.RelevanceSign.neg ∨ self.previousSign = ScalarImplicature.RelevanceSign.neg ∧ self.currentSign = ScalarImplicature.RelevanceSign.pos

  Signs are opposite.

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

Partial Definition 14: Properly accommodable propositions.

A proposition φ is properly accommodable iff: (i) 0 < P(φ) (non-trivially satisfiable), (ii) P(φ) < 1 (not already known), (iii) φ is irrelevant to the current issue.

Accommodable propositions are those that can be "taken for granted" without affecting the ongoing argumentation.

Equations

• DTS.Also.properlyAccommodable ctx φ = (0 < DTS.probSum ctx.prior φ ∧ DTS.probSum ctx.prior φ < 1 ∧ DTS.irrelevant ctx φ)

theorem DTS.Also.also_nonidentity {W : Type u_1} [Fintype W] {E : Type u_2} [DecidableEq E] (ctx : DTSContext W) (Q : E → Set W) [(e : E) → DecidablePred fun (x : W) => x ∈ Q e] (a b : E) (hAlso : AlsoFelicitous ctx (Q a) (Q b)) (_hInj : ∀ (x y : E), Q x = Q y → x = y) (hNonneg : ∀ (w : W), ctx.prior w ≥ 0) (hH : probSum ctx.prior ctx.topic > 0) (hNH : probSum ctx.prior ctx.topicᶜ > 0) : a ≠ b

Corollary 15: "Also" requires non-identity.

If Q(a) is presupposed (informationally inert) and "Q(a) and also Q(b)" is felicitous, then a ≠ b (assuming Q is injective on entities).

Proof: If a = b then Q(b) = Q(a) is presupposed, so BF(Q(b)) = 1 by presup_implies_bf_one. But AlsoFelicitous requires Q(b) to be relevant (BF > 1 or BF < 1) — contradiction.

Requires nonneg prior and non-degenerate issue (Merin assumes both).

theorem DTS.Also.presuppositional_independence_additivity {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] (hPresup : presupposedIrrelevant ctx.prior a) (hNonneg : ∀ (w : W), ctx.prior w ≥ 0) (hH : probSum ctx.prior ctx.topic > 0) (hNH : probSum ctx.prior ctx.topicᶜ > 0) (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 17: Presupposition implies multiplicativity without CIP.

If A is presupposed (P(X|A) = P(X) for all X), then BF(A∧B) = BF(A) · BF(B) holds without the CIP assumption.

Proof: Presupposition implies CIP (the joint factorizes trivially when one factor is informationally inert), and multiplicativity follows from CIP by bayes_factor_multiplicative_under_cip.

Prediction 4 (not formalized): "Also" removes causal implicature.

In "Kim fell and she also broke her arm", the additive particle "also" enforces presuppositional independence of the antecedent ("Kim fell"), removing the default causal reading that plain "and" would carry ("Kim fell and [as a result] broke her arm").

This connects to Core.Causal — the causal reading arises from non-independence of the conjuncts, and "also" explicitly marks the antecedent as presupposed (hence independent).

-- TODO: Formalize using Core.Causal.SEM (BoolSEM / develop).