Argumentative Strength for Quantity Expressions

@cite{cummins-franke-2021} @cite{merin-1999} @cite{macuch-silva-etal-2024}

@cite{merin-1999}'s log-likelihood ratio measure of argumentative strength, as applied to numerical quantity expressions in @cite{cummins-franke-2021} and quantifier choice in Macuch @cite{macuch-silva-etal-2024}.

Core Idea

Rather than maximizing informativity (standard RSA), speakers choose quantity expressions to serve argumentative goals: making a conclusion G more or less credible. The argumentative strength of utterance u for goal G is:

argStr(u, G) = log₂(P(u|G) / P(u|¬G)) (C&F Eq. 17)

A pragmatic variant replaces literal truth with assertability:

pragArgStr(u, G) = log₂(P_a(u|G) / P_a(u|¬G)) (C&F Eq. 25)

Key Results

• Semantic and pragmatic measures can reverse the ordering of utterances
• The Bayes factor P(u|G)/P(u|¬G) admits ordinal comparison without log
• argStr is a pointwise KL divergence (bridge to InformationTheory)
• At λ=1 in CombinedUtility, utility reduces to pure argumentative strength

structure RSA.ArgumentativeStrength.ArgumentativeGoal (W : Type) : Type

An argumentative goal partitions worlds into G (goal-supporting) vs ¬G.

• goalTrue : W → Bool

  Returns true for worlds where the goal holds

def RSA.ArgumentativeStrength.bayesFactor (pGivenG pGivenNotG : ℚ) : ℚ

Bayes factor: P(u|G) / P(u|¬G), the pre-log ratio.

This is the key quantity for argumentative strength. It measures how much more likely utterance u is to be true (or assertable) given G vs ¬G. C&F Eq. 17 (before taking log).

Equations

• RSA.ArgumentativeStrength.bayesFactor pGivenG pGivenNotG = if pGivenNotG = 0 then if pGivenG > 0 then 1000 else 1 else pGivenG / pGivenNotG

def RSA.ArgumentativeStrength.argStr (pGivenG pGivenNotG : ℚ) : ℚ

Argumentative strength: log₂ of the Bayes factor.

argStr(u, G) = log₂(P(u|G) / P(u|¬G))

C&F Eq. 17. Positive values mean u supports G; negative means u supports ¬G.

Equations

• RSA.ArgumentativeStrength.argStr pGivenG pGivenNotG = Core.InformationTheory.log2Approx (RSA.ArgumentativeStrength.bayesFactor pGivenG pGivenNotG)

def RSA.ArgumentativeStrength.pragArgStr (pAssertableGivenG pAssertableGivenNotG : ℚ) : ℚ

Pragmatic argumentative strength using assertability probabilities.

pragArgStr(u, G) = log₂(P_a(u|G) / P_a(u|¬G))

C&F Eq. 25. Replaces literal truth with pragmatic assertability.

Equations

• RSA.ArgumentativeStrength.pragArgStr pAssertableGivenG pAssertableGivenNotG = Core.InformationTheory.log2Approx (RSA.ArgumentativeStrength.bayesFactor pAssertableGivenG pAssertableGivenNotG)

def RSA.ArgumentativeStrength.hasPositiveArgStr (pGivenG pGivenNotG : ℚ) : Prop

Utterance has positive argumentative strength iff P(u|G) > P(u|¬G).

Ordinal characterization — no log needed.

Equations

• RSA.ArgumentativeStrength.hasPositiveArgStr pGivenG pGivenNotG = (pGivenG > pGivenNotG)

instance RSA.ArgumentativeStrength.instDecidableHasPositiveArgStr (pGivenG pGivenNotG : ℚ) : Decidable (hasPositiveArgStr pGivenG pGivenNotG)

Equations

• RSA.ArgumentativeStrength.instDecidableHasPositiveArgStr pGivenG pGivenNotG = inferInstanceAs (Decidable (pGivenG > pGivenNotG))

def RSA.ArgumentativeStrength.argumentativelyStronger (pGivenG₁ pGivenNotG₁ pGivenG₂ pGivenNotG₂ : ℚ) : Prop

Utterance u₁ is argumentatively stronger than u₂ for goal G iff its Bayes factor is higher. Ordinal comparison — no log needed.

Equations

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

instance RSA.ArgumentativeStrength.instDecidableArgumentativelyStronger (a b c d : ℚ) : Decidable (argumentativelyStronger a b c d)

Equations

• RSA.ArgumentativeStrength.instDecidableArgumentativelyStronger a b c d = inferInstanceAs (Decidable (RSA.ArgumentativeStrength.bayesFactor a b > RSA.ArgumentativeStrength.bayesFactor c d))

structure RSA.ArgumentativeStrength.ArgumentativeDifficulty : Type

Argumentative difficulty: proportion of truthful states where the strongest available quantifier is weak. From Macuch @cite{macuch-silva-etal-2024}.

For a given direction (positive/negative), difficulty measures how hard it is to frame the state in that direction truthfully. High difficulty → speakers must use weaker quantifiers.

• proportion : ℚ

  Proportion of relevant items (e.g., correct answers out of total)

• isPositiveFrame : Bool

  Whether the speaker is framing positively or negatively

• difficulty : ℚ

  Difficulty value: 0 = easy (can use "all"), 1 = hard (must use "some")

def RSA.ArgumentativeStrength.rationalHearerSemantic (pGivenG pGivenNotG : ℚ) : Bool

Rational hearer (semantic): increase belief in G upon hearing u iff argStr(u, G) > 0 (C&F Eq. 27).

Equations

• RSA.ArgumentativeStrength.rationalHearerSemantic pGivenG pGivenNotG = decide (RSA.ArgumentativeStrength.hasPositiveArgStr pGivenG pGivenNotG)

def RSA.ArgumentativeStrength.rationalHearerPragmatic (pAssertableGivenG pAssertableGivenNotG : ℚ) : Bool

Rational hearer (pragmatic): increase belief in G upon hearing u iff pragArgStr(u, G) > 0 (C&F Eq. 28).

Equations

• RSA.ArgumentativeStrength.rationalHearerPragmatic pAssertableGivenG pAssertableGivenNotG = decide (RSA.ArgumentativeStrength.hasPositiveArgStr pAssertableGivenG pAssertableGivenNotG)

theorem RSA.ArgumentativeStrength.argStr_eq_pointwiseKL (pGivenG pGivenNotG : ℚ) (_hG : 0 < pGivenG) (hNotG : 0 < pGivenNotG) : argStr pGivenG pGivenNotG = InformationTheory.log2Approx (pGivenG / pGivenNotG)

argStr is a pointwise KL divergence term.

The KL divergence D_KL(P_G || P_¬G) = Σ_u P_G(u) · log(P_G(u)/P_¬G(u)). Each summand P_G(u) · log(P_G(u)/P_¬G(u)) contains the argStr as the log factor. That is, argStr(u, G) = log₂(P(u|G)/P(u|¬G)) is the pointwise divergence.

theorem RSA.ArgumentativeStrength.argStr_positive_iff (pGivenG pGivenNotG : ℚ) (_hG : 0 ≤ pGivenG) (hNotG : 0 < pGivenNotG) : hasPositiveArgStr pGivenG pGivenNotG ↔ bayesFactor pGivenG pGivenNotG > 1

Positive argStr iff Bayes factor > 1 (ordinal characterization).

theorem RSA.ArgumentativeStrength.argStr_from_combined_at_one (utilInformative utilArgumentative : ℚ) : CombinedUtility.combined 1 utilInformative utilArgumentative = utilArgumentative

When λ=1 in CombinedUtility.combined, utility reduces to pure U_B. If U_B is argumentative strength, this connects combined utility to argStr.

That is: combined 1 U_informative U_argumentative = U_argumentative

theorem RSA.ArgumentativeStrength.argStr_speaker_prefers_stronger (uEpi argStr₁ argStr₂ β : ℚ) (hβ : 0 < β) (hStr : argStr₁ > argStr₂) : CombinedUtility.goalOrientedUtility uEpi argStr₂ β < CombinedUtility.goalOrientedUtility uEpi argStr₁ β

A goal-oriented speaker (β > 0) strictly prefers utterances with higher argumentative strength, connecting Cummins & Franke's argStr ordering to Barnett et al.'s goal-oriented utility framework.

When U_goal = argStr(u, G), higher argStr → higher goalOrientedUtility.