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 Theories.DTS.Also.presupposedIrrelevant {W : Type u_1} [Fintype W] (prior : W → ℚ) (a : BProp W) : 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

• Theories.DTS.Also.presupposedIrrelevant prior a = ∀ (x : BProp W), Theories.DTS.condProb prior x a = Theories.DTS.condProb prior x (Core.Proposition.Decidable.top W)

structure Theories.DTS.Also.TopicAnaphoricSalience {W : Type u_1} [Fintype W] (ctx : DTSContext W) (d e : BProp W) : 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 Theories.DTS.Also.AlsoFelicitous {W : Type u_1} [Fintype W] (ctx : DTSContext W) (qa qb : BProp W) : 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 Theories.DTS.Also.ButAlsoFelicitous {W : Type u_1} [Fintype W] (ctx : DTSContext W) (qa qb : BProp W) : 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 Theories.DTS.Also.properlyAccommodable {W : Type u_1} [Fintype W] (ctx : DTSContext W) (φ : BProp W) : 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

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

theorem Theories.DTS.Also.also_nonidentity {W : Type u_1} [Fintype W] {E : Type u_2} [DecidableEq E] (ctx : DTSContext W) (Q : E → BProp W) (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.issue.topic > 0) (hNH : probSum ctx.prior (Core.Proposition.Decidable.pnot W ctx.issue.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 Theories.DTS.Also.presuppositional_independence_additivity {W : Type u_1} [Fintype W] (ctx : DTSContext W) (a b : BProp W) (hPresup : presupposedIrrelevant ctx.prior a) (hNonneg : ∀ (w : W), ctx.prior w ≥ 0) (hH : probSum ctx.prior ctx.issue.topic > 0) (hNH : probSum ctx.prior (Core.Proposition.Decidable.pnot W ctx.issue.topic) > 0) (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 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.StructuralEquationModel — the causal reading arises from non-independence of the conjuncts, and "also" explicitly marks the antecedent as presupposed (hence independent).

-- TODO: Formalize using CausalDynamics from Core.StructuralEquationModel