@cite{cummins-franke-2021}: Argumentative Strength of Numerical Quantity

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

Formalizes the conference registration scenario (C&F pp. 7–8) demonstrating that semantic and pragmatic argumentative strength can reverse the ordering of "more than M" expressions. Also connects to Macuch @cite{macuch-silva-etal-2024}'s exam scenario on strategic quantifier choice.

Key Results

1. Semantic measure: "more than 110" > "more than 100" for goal "success" (because "more than 110" concentrates probability mass in goal-worlds)
2. Pragmatic reversal: with 90% enrichment to "approximately M", the ordering flips — "more than 100" becomes pragmatically stronger
3. Exam scenario: difficulty metric predicts quantifier weakening (all→most→some)

theorem RSA.Implementations.CumminsFranke2021.moreThan_from_lowerBound_zero (n : ℕ) : Semantics.Lexical.Numeral.moreThanMeaning 0 n = Semantics.Lexical.Numeral.LowerBound.meaning Semantics.Lexical.Numeral.BareNumeral.one n

"More than M" is equivalent to lower-bound meaning at M+1.

moreThan(M)(n) = true ↔ n > M ↔ n ≥ M+1 = lowerBound(M+1)(n)

Uses the canonical moreThanMeaning from Numeral.Semantics.

theorem RSA.Implementations.CumminsFranke2021.moreThan_from_lowerBound_one (n : ℕ) : Semantics.Lexical.Numeral.moreThanMeaning 1 n = Semantics.Lexical.Numeral.LowerBound.meaning Semantics.Lexical.Numeral.BareNumeral.two n

theorem RSA.Implementations.CumminsFranke2021.moreThan_from_lowerBound_two (n : ℕ) : Semantics.Lexical.Numeral.moreThanMeaning 2 n = Semantics.Lexical.Numeral.LowerBound.meaning Semantics.Lexical.Numeral.BareNumeral.three n

@[reducible, inline]

abbrev RSA.Implementations.CumminsFranke2021.numWorlds : ℕ

Number of worlds: cardinalities 0 through 200

Equations

• RSA.Implementations.CumminsFranke2021.numWorlds = 201

def RSA.Implementations.CumminsFranke2021.conferenceSuccess (w : Fin numWorlds) : Bool

Goal: conference is a success iff more than 120 attend

Equations

• RSA.Implementations.CumminsFranke2021.conferenceSuccess w = decide (↑w > 120)

def RSA.Implementations.CumminsFranke2021.conferenceGoal : ArgumentativeStrength.ArgumentativeGoal (Fin numWorlds)

Conference argumentative goal

Equations

• RSA.Implementations.CumminsFranke2021.conferenceGoal = { goalTrue := RSA.Implementations.CumminsFranke2021.conferenceSuccess }

def RSA.Implementations.CumminsFranke2021.numGoalWorlds : ℕ

Number of goal worlds: 121.200 = 80 worlds

Equations

• RSA.Implementations.CumminsFranke2021.numGoalWorlds = 80

def RSA.Implementations.CumminsFranke2021.numNonGoalWorlds : ℕ

Number of non-goal worlds: 0.120 = 121 worlds

Equations

• RSA.Implementations.CumminsFranke2021.numNonGoalWorlds = 121

def RSA.Implementations.CumminsFranke2021.moreThan100_trueWorlds : ℕ

Worlds where "more than 100" is true: 101.200 = 100 worlds

Equations

• RSA.Implementations.CumminsFranke2021.moreThan100_trueWorlds = 100

def RSA.Implementations.CumminsFranke2021.p_mt100_givenG : ℚ

P("more than 100" | G): among goal worlds (121.200), all 80 satisfy >100

Equations

• RSA.Implementations.CumminsFranke2021.p_mt100_givenG = 80 / 80

def RSA.Implementations.CumminsFranke2021.p_mt100_givenNotG : ℚ

P("more than 100" | ¬G): among non-goal worlds (0.120), those >100 are 101.120 = 20

Equations

• RSA.Implementations.CumminsFranke2021.p_mt100_givenNotG = 20 / 121

def RSA.Implementations.CumminsFranke2021.p_mt110_givenG : ℚ

P("more than 110" | G): among goal worlds (121.200), all 80 satisfy >110

Equations

• RSA.Implementations.CumminsFranke2021.p_mt110_givenG = 80 / 80

def RSA.Implementations.CumminsFranke2021.p_mt110_givenNotG : ℚ

P("more than 110" | ¬G): among non-goal worlds (0.120), those >110 are 111.120 = 10

Equations

• RSA.Implementations.CumminsFranke2021.p_mt110_givenNotG = 10 / 121

def RSA.Implementations.CumminsFranke2021.argStr_moreThan100 : ℚ

argStr("more than 100", success)

Equations

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

def RSA.Implementations.CumminsFranke2021.argStr_moreThan110 : ℚ

argStr("more than 110", success)

Equations

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

theorem RSA.Implementations.CumminsFranke2021.moreThan110_semantically_stronger : argStr_moreThan110 > argStr_moreThan100

"More than 110" is semantically stronger than "more than 100" for the conference goal.

This is C&F's key semantic result: the more precise (higher M) expression has higher argStr because it has lower P(u|¬G).

theorem RSA.Implementations.CumminsFranke2021.moreThan100_supports_goal : ArgumentativeStrength.hasPositiveArgStr p_mt100_givenG p_mt100_givenNotG

Both utterances have positive argumentative strength for the goal

theorem RSA.Implementations.CumminsFranke2021.moreThan110_supports_goal : ArgumentativeStrength.hasPositiveArgStr p_mt110_givenG p_mt110_givenNotG

theorem RSA.Implementations.CumminsFranke2021.moreThan110_higher_bayesFactor : ArgumentativeStrength.bayesFactor p_mt110_givenG p_mt110_givenNotG > ArgumentativeStrength.bayesFactor p_mt100_givenG p_mt100_givenNotG

def RSA.Implementations.CumminsFranke2021.p_mt100_assertable_givenG : ℚ

Assertability of "more than 100" given G: 60 out of 80 goal worlds (101.160 enriched range intersected with 121.200)

Equations

• RSA.Implementations.CumminsFranke2021.p_mt100_assertable_givenG = 60 / 80

def RSA.Implementations.CumminsFranke2021.p_mt100_assertable_givenNotG : ℚ

Assertability of "more than 100" given ¬G: 20 out of 121 non-goal worlds (enriched range 91.110 intersected with 0.120)

Equations

• RSA.Implementations.CumminsFranke2021.p_mt100_assertable_givenNotG = 20 / 121

def RSA.Implementations.CumminsFranke2021.p_mt110_assertable_givenG : ℚ

Assertability of "more than 110" given G: 60 out of 80 goal worlds (111.170 enriched range intersected with 121.200)

Equations

• RSA.Implementations.CumminsFranke2021.p_mt110_assertable_givenG = 60 / 80

def RSA.Implementations.CumminsFranke2021.p_mt110_assertable_givenNotG : ℚ

Assertability of "more than 110" given ¬G: 10 out of 121 non-goal worlds (enriched range 101.120 intersected with 0.120)

Equations

• RSA.Implementations.CumminsFranke2021.p_mt110_assertable_givenNotG = 10 / 121

def RSA.Implementations.CumminsFranke2021.pragArgStr_moreThan100 : ℚ

pragArgStr("more than 100", success)

Equations

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

def RSA.Implementations.CumminsFranke2021.pragArgStr_moreThan110 : ℚ

pragArgStr("more than 110", success)

Equations

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

theorem RSA.Implementations.CumminsFranke2021.wider_enrichment_weakens_argStr (pG pNotG_narrow pNotG_wide : ℚ) (hG : 0 < pG) (hNarrow : 0 < pNotG_narrow) (hWide : 0 < pNotG_wide) (hWider : pNotG_narrow < pNotG_wide) : ArgumentativeStrength.bayesFactor pG pNotG_wide < ArgumentativeStrength.bayesFactor pG pNotG_narrow

With same assertability in G, the one with lower assertability in ¬G is pragmatically stronger. In this simplified model both have identical assertability ratios — the reversal depends on the enrichment asymmetry.

C&F's actual reversal uses a specific enrichment model where "more than 100" gets a wider enriched range. We verify the structural property: when P_a(u|¬G) increases (through wider enrichment), argStr decreases.

structure RSA.Implementations.CumminsFranke2021.ExamStimulus : Type

An exam stimulus: student got nCorrect out of nTotal questions right

• nCorrect : ℕ
• nTotal : ℕ
• h_le : self.nCorrect ≤ self.nTotal

def RSA.Implementations.CumminsFranke2021.ExamStimulus.proportion (s : ExamStimulus) : ℚ

Proportion correct as a rational

Equations

• s.proportion = if s.nTotal = 0 then 0 else ↑s.nCorrect / ↑s.nTotal

def RSA.Implementations.CumminsFranke2021.examDifficulty (s : ExamStimulus) (positive : Bool) : ArgumentativeStrength.ArgumentativeDifficulty

Compute argumentative difficulty for an exam stimulus.

Difficulty for positive framing = 1 - proportion (higher proportion = easier to frame positively). Difficulty for negative framing = proportion (higher proportion = easier to frame negatively).

Equations

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

def RSA.Implementations.CumminsFranke2021.truthfulQuantifiers (s : ExamStimulus) : List Domains.Quantity.ExtUtterance

Which quantifiers from the extended set are truthful for a given proportion?

Uses the standard extended semantics from Domains.Quantities:

• "all": true iff count = n (proportion = 1)
• "most": true iff count > n/2 (proportion > 0.5)
• "some": true iff count ≥ 1 (proportion > 0)
• "none": true iff count = 0 (proportion = 0)

Equations

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

def RSA.Implementations.CumminsFranke2021.strongestTruthfulPositive (s : ExamStimulus) : Domains.Quantity.ExtUtterance

As difficulty increases (proportion moves away from extremes), the strongest truthful quantifier weakens: all → most → some.

For positive framing with decreasing proportion:

• proportion = 1.0: all is truthful
• proportion = 0.7: most is strongest truthful
• proportion = 0.3: some is strongest truthful

Equations

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

theorem RSA.Implementations.CumminsFranke2021.perfect_allows_all : strongestTruthfulPositive { nCorrect := 60, nTotal := 60, h_le := ⋯ } = Domains.Quantity.ExtUtterance.all

Perfect score: "all" is available

theorem RSA.Implementations.CumminsFranke2021.fortytwo_allows_most : strongestTruthfulPositive { nCorrect := 42, nTotal := 60, h_le := ⋯ } = Domains.Quantity.ExtUtterance.most

42/60: "most" is strongest

theorem RSA.Implementations.CumminsFranke2021.eighteen_allows_some : strongestTruthfulPositive { nCorrect := 18, nTotal := 60, h_le := ⋯ } = Domains.Quantity.ExtUtterance.some_

18/60: "some" is strongest

theorem RSA.Implementations.CumminsFranke2021.quantifier_ordering_matches_scale : Core.Scale.Quantifiers.entails Core.Scale.Quantifiers.QuantExpr.all Core.Scale.Quantifiers.QuantExpr.most = true ∧ Core.Scale.Quantifiers.entails Core.Scale.Quantifiers.QuantExpr.most Core.Scale.Quantifiers.QuantExpr.some_ = true ∧ Core.Scale.Quantifiers.entails Core.Scale.Quantifiers.QuantExpr.some_ Core.Scale.Quantifiers.QuantExpr.none_ = false

The quantifier ordering matches the Horn scale from Core.Scale: none < some < most < all