Decision-Theoretic Semantics: Scalar Implicature (@cite{merin-1999} §3)

@cite{merin-1999}

Merin's DTS account of scalar implicature via protentive speaker meaning and relevance-ordered alternatives. The key insight: scalar implicature arises because conjunction is more relevant than disjunction (Theorem 6a), so a speaker who says "A or B" implicates ¬(A ∧ B).

Key Definitions

• PSM — Protentive Speaker Meaning (Def. 7): the hypothesis supported by an utterance's relevance sign
• upwardCone / downwardCone — alternatives ordered by Bayes factor
• Hypothesis1 — claim/counterclaim structure for scalar alternatives

Main Results

• Prediction 1: A disjunct does not always dominate its disjunction
• Prediction 2: Under CIP, conjunction dominates both conjuncts and disjunction

inductive Theories.DTS.ScalarImplicature.RelevanceSign : Type

Sign of relevance: positive, negative, or neutral.

• pos : RelevanceSign
• neg : RelevanceSign
• neutral : RelevanceSign

instance Theories.DTS.ScalarImplicature.instDecidableEqRelevanceSign : DecidableEq RelevanceSign

Equations

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

instance Theories.DTS.ScalarImplicature.instReprRelevanceSign : Repr RelevanceSign

Equations

• Theories.DTS.ScalarImplicature.instReprRelevanceSign = { reprPrec := Theories.DTS.ScalarImplicature.instReprRelevanceSign.repr }

def Theories.DTS.ScalarImplicature.instReprRelevanceSign.repr : RelevanceSign → ℕ → Std.Format

Equations

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

def Theories.DTS.ScalarImplicature.sgnRelevance {W : Type u_1} [Fintype W] (ctx : DTSContext W) (e : BProp W) : RelevanceSign

Protentive Speaker Meaning (Def. 7): the hypothesis supported by an utterance's relevance sign.

If E is positively relevant, PSM = H. If E is negatively relevant, PSM = ¬H. Otherwise neutral.

Equations

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

def Theories.DTS.ScalarImplicature.upwardCone {W : Type u_1} [Fintype W] (ctx : DTSContext W) (alts : List (BProp W)) (σ : BProp W) : List (BProp W)

Upward cone: alternatives at least as relevant as σ.

Given a list of alternatives ordered by Bayes factor, the upward cone of σ contains all alternatives with BF ≥ BF(σ).

Equations

• Theories.DTS.ScalarImplicature.upwardCone ctx alts σ = List.filter (fun (a : BProp W) => decide (Theories.DTS.bayesFactor ctx a ≥ Theories.DTS.bayesFactor ctx σ)) alts

def Theories.DTS.ScalarImplicature.downwardCone {W : Type u_1} [Fintype W] (ctx : DTSContext W) (alts : List (BProp W)) (σ : BProp W) : List (BProp W)

Downward cone: alternatives at most as relevant as σ.

Equations

• Theories.DTS.ScalarImplicature.downwardCone ctx alts σ = List.filter (fun (a : BProp W) => decide (Theories.DTS.bayesFactor ctx a ≤ Theories.DTS.bayesFactor ctx σ)) alts

structure Theories.DTS.ScalarImplicature.ScalarInterpretation (W : Type u_1) : Type u_1

Hypothesis 1: Claim/counterclaim structure for scalar alternatives.

The claim is the disjunction of upward-cone members (what the speaker means to convey). The counterclaim is the disjunction of downward-cone members (what the speaker implicates is false).

• uttered : BProp W

  The scalar alternative uttered.

• claim : BProp W

  The claim: disjunction of upward cone members.

• counterclaim : BProp W

  The counterclaim: disjunction of downward cone members.

theorem Theories.DTS.ScalarImplicature.not_if_not_indeed_disjunct : ¬∀ (ctx : DTSContext Core.Proposition.World4) (a b : BProp Core.Proposition.World4), posRelevant ctx a → posRelevant ctx b → bayesFactor ctx a > bayesFactor ctx (Core.Proposition.Decidable.por Core.Proposition.World4 a b)

Prediction 1: It is NOT the case that a disjunct always dominates its disjunction in Bayes factor.

This follows from Theorem 6b direction: XOR (and hence plain disjunction) need not track the relevance of individual disjuncts.

theorem Theories.DTS.ScalarImplicature.if_not_indeed_conjunction {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) > bayesFactor ctx a ∧ bayesFactor ctx (Core.Proposition.Decidable.pand W a b) > bayesFactor ctx (Core.Proposition.Decidable.por W a b)

Prediction 2: Under CIP with both A,B positively relevant, conjunction dominates both conjuncts and disjunction.

This is the core of Merin's scalar implicature account: "A and B" is strictly more relevant than "A or B", explaining why "or" implicates ¬∧.