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 DTS.ScalarImplicature.RelevanceSign : Type

Sign of relevance: positive, negative, or neutral.

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

@[implicit_reducible]

instance DTS.ScalarImplicature.instDecidableEqRelevanceSign : DecidableEq RelevanceSign

Equations

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

@[implicit_reducible]

instance DTS.ScalarImplicature.instReprRelevanceSign : Repr RelevanceSign

Equations

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

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

Equations

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

def DTS.ScalarImplicature.sgnRelevance {W : Type u_1} [Fintype W] (ctx : DTSContext W) (e : Set W) [DecidablePred fun (x : W) => x ∈ e] : 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 DTS.ScalarImplicature.upwardCone {W : Type u_1} [Fintype W] (ctx : DTSContext W) (alts : List ((p : Set W) × DecidablePred fun (x : W) => x ∈ p)) (σ : Set W) [DecidablePred fun (x : W) => x ∈ σ] : List ((p : Set W) × DecidablePred fun (x : W) => x ∈ p)

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(σ).

Each alternative is bundled with its decidability instance so that bayesFactor (which requires [DecidablePred]) can be evaluated.

Equations

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

def DTS.ScalarImplicature.downwardCone {W : Type u_1} [Fintype W] (ctx : DTSContext W) (alts : List ((p : Set W) × DecidablePred fun (x : W) => x ∈ p)) (σ : Set W) [DecidablePred fun (x : W) => x ∈ σ] : List ((p : Set W) × DecidablePred fun (x : W) => x ∈ p)

Downward cone: alternatives at most as relevant as σ.

Equations

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

structure 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 : Set W

  The scalar alternative uttered.

• claim : Set W

  The claim: disjunction of upward cone members.

• counterclaim : Set W

  The counterclaim: disjunction of downward cone members.

theorem DTS.ScalarImplicature.not_if_not_indeed_disjunct : ¬∀ (ctx : DTSContext World4) (a b : Set World4) [inst : DecidablePred fun (x : World4) => x ∈ a] [inst_1 : DecidablePred fun (x : World4) => x ∈ b], posRelevant ctx a → posRelevant ctx b → bayesFactor ctx a > bayesFactor ctx (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.

TODO: Construct a concrete counterexample over World4 with appropriate prior, decidable predicates, and the witnesses showing bayesFactor ctx a = bayesFactor ctx (a ∪ b) (so the strict > inequality fails). The original Bool proof relied on native_decide over a 4-world enumeration; a Prop-level counterexample needs explicit decidability for the chosen predicates.

theorem DTS.ScalarImplicature.if_not_indeed_conjunction {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] (hcip : CIP ctx a b) (hPosA : posRelevant ctx a) (hPosB : posRelevant ctx b) (hNonzero : condProb ctx.prior a ctx.topicᶜ ≠ 0) (hNonzero' : condProb ctx.prior b ctx.topicᶜ ≠ 0) (hABNonzero : condProb ctx.prior (a ∩ b) ctx.topicᶜ ≠ 0) (hPrior : ∀ (w : W), ctx.prior w ≥ 0) : bayesFactor ctx (a ∩ b) > bayesFactor ctx a ∧ bayesFactor ctx (a ∩ b) > bayesFactor ctx (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 ¬∧.