Cummins and Franke (2021): Rational Interpretation of Numerical Quantity in Argumentative Contexts

Cummins and Franke measure the argumentative strength of a numerical utterance toward a speaker's goal, after Merin, as a log Bayes factor: once on the utterance's truth conditions and once on its felicitous assertability, which accounts for the implicatures a hearer may draw. In their conference example the goal is that more than 120 people attend, attendees are those who registered, registrations are uniform on [0, 200], and the speaker chooses between more than 100 and more than 110. Semantically the stronger utterance is the stronger argument, but a hearer who reads more than 110 as implicating not more than 120 finds that reading incompatible with the goal, so pragmatically the utterance is only weak evidence and the order reverses.

We derive the semantic ordering from the general fact that shedding worlds where the goal fails only strengthens an argument. When an implicature holds wherever the goal fails, the pragmatic Bayes factor is the semantic one discounted by the enrichment rate times the probability, given success, that the implicature fails. The paper asks which stronger alternative more than 100 negates. On its granularity account the hearer negates every numeral above it at least as round on the scale evoked, which leaves not more than the next point of that scale. The order then reverses at no rate on the scale of tens, above sixteen in seventeen on the scale of 25s, above eight in eleven for the illustration's 150, and above one in two on the scale of hundreds, the coarsest decimal scale through 100. Cummins's constraint-based account selects the same alternatives for both numerals. The paper's high-framing examples, its rules for a sceptical hearer and its corpus study are not formalized.

Implementation notes

• Registrations are uniform on the counts from 1 to 200, each count standing for the unit interval below it, so at the example's whole-number thresholds every probability is the one the paper computes on [0, 200]; more than n denotes Set.Ioi n.
• For more than 110 the paper prints log 11, the Bayes factor of more than 100 toward the goal more than 110. Its own pragmatic calculation gives more than 110 probability 1/12 given failure, so toward the stated goal the factor is 12, which the rate-zero case recovers. The ordering is unaffected.
• Strengths are natural logarithms; the paper prints base-ten decimals, and a change of base preserves the sign, order and ratios of strengths.

References

• [CF21]
• [Mer99b]
• [CSS12]
• [Kri09a]
• [Cum15]

The conference

@[reducible, inline]

noncomputable abbrev CumminsFranke2021.prior : MeasureTheory.Measure ℕ

Registrations are uniform on the counts from 1 to 200.

Equations

• CumminsFranke2021.prior = ProbabilityTheory.uniformOn (Set.Icc 1 200)

@[reducible, inline]

noncomputable abbrev CumminsFranke2021.success : DTS.Context ℕ

The conference succeeds iff more than 120 people register, and so attend.

Equations

• CumminsFranke2021.success = { topic := Set.Ioi 120, topicMeasurable := CumminsFranke2021.success._proof_1, prior := CumminsFranke2021.prior }

theorem CumminsFranke2021.real_cond_Ioi {a c : ℕ} (hac : a ≤ c) (hc : c ≤ 200) : prior[|Set.Ioi a].real (Set.Ioi c) = (200 - ↑c) / (200 - ↑a)

Given more than a registrations, the total is uniform on the counts above a.

theorem CumminsFranke2021.real_cond_Ioi_of_le {a c : ℕ} (hca : c ≤ a) (ha : a < 200) : prior[|Set.Ioi a].real (Set.Ioi c) = 1

theorem CumminsFranke2021.real_cond_Iic {a c : ℕ} (hca : c ≤ a) (ha : a ≤ 200) : prior[|Set.Iic a].real (Set.Ioi c) = (↑a - ↑c) / ↑a

Given at most a registrations, the total is uniform on the counts up to a.

Truth conditions

theorem CumminsFranke2021.cond_moreThan100_le_moreThan110 : prior[Set.Ioi 120 | Set.Ioi 100] ≤ prior[Set.Ioi 120 | Set.Ioi 110]

Success is at least as probable given more than 110 as given more than 100, since the totals that more than 110 sheds are all failures.

theorem CumminsFranke2021.bayesFactor_moreThan100_lt_moreThan110 : DTS.bayesFactor success (Set.Ioi 100) < DTS.bayesFactor success (Set.Ioi 110)

Hence more than 110 is semantically the stronger argument for success.

theorem CumminsFranke2021.toReal_bayesFactor_moreThan100 : (DTS.bayesFactor success (Set.Ioi 100)).toReal = 6

theorem CumminsFranke2021.toReal_bayesFactor_moreThan110 : (DTS.bayesFactor success (Set.Ioi 110)).toReal = 12

theorem CumminsFranke2021.relevance_moreThan100 : DTS.relevance success (Set.Ioi 100) = Real.log 6

The paper's log 6 for more than 100.

theorem CumminsFranke2021.relevance_moreThan110 : DTS.relevance success (Set.Ioi 110) = Real.log 12

Toward the stated goal more than 110 has strength log 12, where the paper prints log 11.

theorem CumminsFranke2021.relevance_moreThan100_toward110 : DTS.relevance { topic := Set.Ioi 110, topicMeasurable := ⋯, prior := prior } (Set.Ioi 100) = Real.log 11

The paper's log 11 is the strength of more than 100 toward the goal more than 110.

Assertability

Assertability is stochastic: with probability ρ the hearer gives the utterance a pragmatic interpretation, enriching more than n with an implicature not more than c, and otherwise a semantic one, so the utterance is felicitously assertable iff it is true on the interpretation drawn. The joint of registrations and interpretations is the product of the prior with the hearer's coin.

inductive CumminsFranke2021.Interpretation : Type

How the hearer resolves the utterance.

• pragmatic : Interpretation
• semantic : Interpretation

@[instance_reducible]

instance CumminsFranke2021.instDecidableEqInterpretation : DecidableEq Interpretation

Equations

• CumminsFranke2021.instDecidableEqInterpretation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance CumminsFranke2021.instFintypeInterpretation : Fintype Interpretation

Equations

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

@[instance_reducible]

instance CumminsFranke2021.instMeasurableSpaceInterpretation : MeasurableSpace Interpretation

Equations

• CumminsFranke2021.instMeasurableSpaceInterpretation = ⊤

@[reducible, inline]

noncomputable abbrev CumminsFranke2021.hearer (ρ : ↑unitInterval) : MeasureTheory.Measure Interpretation

The hearer interprets pragmatically with probability ρ and semantically otherwise.

Equations

• CumminsFranke2021.hearer ρ = ProbabilityTheory.bernoulliMeasure CumminsFranke2021.Interpretation.pragmatic CumminsFranke2021.Interpretation.semantic ρ

def CumminsFranke2021.reading (n c : ℕ) : Interpretation → Set ℕ

The readings of more than n whose implicature is not more than c.

Equations

• CumminsFranke2021.reading n c CumminsFranke2021.Interpretation.pragmatic = Set.Ioc n c
• CumminsFranke2021.reading n c CumminsFranke2021.Interpretation.semantic = Set.Ioi n

@[reducible, inline]

noncomputable abbrev CumminsFranke2021.assertability (ρ : ↑unitInterval) : DTS.Context (ℕ × Interpretation)

The assertability model pairs registrations with the hearer's interpretation under the prior and the hearer's coin, and lifts the goal along the registration.

Equations

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

def CumminsFranke2021.assertable (n c : ℕ) : Set (ℕ × Interpretation)

more than n is felicitously assertable iff it is true on the interpretation drawn.

Equations

• CumminsFranke2021.assertable n c = {p : ℕ × CumminsFranke2021.Interpretation | p.1 ∈ CumminsFranke2021.reading n c p.2}

theorem CumminsFranke2021.real_cond_assertable (ρ : ↑unitInterval) (s : Set ℕ) (n c : ℕ) : (prior.prod (hearer ρ))[|Prod.fst ⁻¹' s].real (assertable n c) = prior[|s].real (Set.Ioc n c) * ↑ρ + prior[|s].real (Set.Ioi n) * (1 - ↑ρ)

Given the registration total, the probability that more than n is assertable is the paper's mixture of its readings' probabilities.

theorem CumminsFranke2021.real_assertable_of_failure (ρ : ↑unitInterval) (n : ℕ) {c : ℕ} (hc : 120 ≤ c) : (assertability ρ).prior[|(assertability ρ).topicᶜ].real (assertable n c) = prior[|Set.Iic 120].real (Set.Ioi n)

Given failure, more than n is as probable to be assertable as to be true, when its implicature holds wherever the conference fails.

theorem CumminsFranke2021.real_assertable_of_success (ρ : ↑unitInterval) {n c : ℕ} (hn : n ≤ 120) (hnc : n ≤ c) : (assertability ρ).prior[|(assertability ρ).topic].real (assertable n c) = 1 - ↑ρ * prior[|Set.Ioi 120].real (Set.Ioi c)

Given success, the probability that more than n is assertable, for n short of the goal, is the probability that the hearer does not draw an implicature not more than c that fails.

theorem CumminsFranke2021.toReal_bayesFactor_assertable (ρ : ↑unitInterval) {n c : ℕ} (hn : n ≤ 120) (hc : 120 ≤ c) : (DTS.bayesFactor (assertability ρ) (assertable n c)).toReal = (DTS.bayesFactor success (Set.Ioi n)).toReal * (1 - ↑ρ * prior[|Set.Ioi 120].real (Set.Ioi c))

The pragmatic Bayes factor of more than n, for n short of the goal, is the semantic one discounted by the enrichment rate times the probability, given success, that its implicature fails, when the implicature holds wherever the conference fails.

theorem CumminsFranke2021.bayesFactor_assertability_zero (n c : ℕ) : DTS.bayesFactor (assertability 0) (assertable n c) = DTS.bayesFactor success (Set.Ioi n)

At enrichment rate zero the pragmatic measure is the semantic one.

theorem CumminsFranke2021.toReal_bayesFactor_assertable_moreThan100 (ρ : ↑unitInterval) {c : ℕ} (hc : 120 ≤ c) (hc' : c ≤ 200) : (DTS.bayesFactor (assertability ρ) (assertable 100 c)).toReal = 6 * (1 - ↑ρ * ((200 - ↑c) / 80))

theorem CumminsFranke2021.toReal_bayesFactor_assertable_moreThan110 (ρ : ↑unitInterval) : (DTS.bayesFactor (assertability ρ) (assertable 110 120)).toReal = 12 * (1 - ↑ρ)

The implicature of more than 110, not more than 120, fails on every successful total, so its pragmatic strength is its semantic strength 12 times the probability of a semantic interpretation.

theorem CumminsFranke2021.relevance_assertable_moreThan100 (ρ : ↑unitInterval) : DTS.relevance (assertability ρ) (assertable 100 150) = Real.log (6 * (1 - 5 / 8 * ↑ρ))

theorem CumminsFranke2021.relevance_assertable_moreThan110 (ρ : ↑unitInterval) : DTS.relevance (assertability ρ) (assertable 110 120) = Real.log (12 * (1 - ↑ρ))

theorem CumminsFranke2021.posRelevant_assertable_moreThan100 (ρ : ↑unitInterval) : DTS.posRelevant (assertability ρ) (assertable 100 150)

Pragmatically, more than 100 with the implicature not more than 150 remains positive evidence for success at every enrichment rate.

theorem CumminsFranke2021.posRelevant_assertable_moreThan110_iff (ρ : ↑unitInterval) : DTS.posRelevant (assertability ρ) (assertable 110 120) ↔ ↑ρ < 11 / 12

Pragmatically, more than 110 remains positive evidence for success iff the hearer enriches less than eleven times in twelve.

The reversal

theorem CumminsFranke2021.bayesFactor_assertable_lt_iff_of_le (ρ : ↑unitInterval) {c : ℕ} (hc : 120 ≤ c) (hc' : c ≤ 200) : DTS.bayesFactor (assertability ρ) (assertable 110 120) < DTS.bayesFactor (assertability ρ) (assertable 100 c) ↔ 80 < ↑ρ * (↑c - 40)

When more than 100 implicates not more than c for a cap c at or above the goal, it is the stronger pragmatic argument iff the rate times c - 40 exceeds 80.

theorem CumminsFranke2021.bayesFactor_assertable_lt_iff (ρ : ↑unitInterval) : DTS.bayesFactor (assertability ρ) (assertable 110 120) < DTS.bayesFactor (assertability ρ) (assertable 100 150) ↔ 8 / 11 < ↑ρ

For the illustration's not more than 150 the order of the two arguments reverses iff the hearer enriches more than eight times in eleven. The paper fixes the rate at nine in ten and does not state the threshold.

theorem CumminsFranke2021.bayesFactor_assertable_moreThan100_tens_le (ρ : ↑unitInterval) : DTS.bayesFactor (assertability ρ) (assertable 100 110) ≤ DTS.bayesFactor (assertability ρ) (assertable 110 120)

On the scale of tens more than 100 implicates not more than 110, which fails on every successful total and on half the failures where the utterance is true, so more than 110 stays at least as strong at every rate.

theorem CumminsFranke2021.reversal_on_scales (ρ : ↑unitInterval) : ¬DTS.bayesFactor (assertability ρ) (assertable 110 120) < DTS.bayesFactor (assertability ρ) (assertable 100 110) ∧ (DTS.bayesFactor (assertability ρ) (assertable 110 120) < DTS.bayesFactor (assertability ρ) (assertable 100 125) ↔ 16 / 17 < ↑ρ) ∧ (DTS.bayesFactor (assertability ρ) (assertable 110 120) < DTS.bayesFactor (assertability ρ) (assertable 100 200) ↔ 1 / 2 < ↑ρ)

On the scales the paper names for more than 100, tens, 25s and hundreds, the implicatures not more than 110, 125 and 200 reverse the order at no rate, above sixteen in seventeen, and above one in two.

Granularity

def CumminsFranke2021.enrichment (W : Finset ℤ) (n : ℕ) : Set ℕ

The pragmatic reading of more than n on the scales W negates more than m for every numeral m above n at least as round as n on them.

Equations

• CumminsFranke2021.enrichment W n = Set.Ioi n \ ⋃ m ∈ {m : ℕ | n < m ∧ Numerals.Roundness.AtLeastAsRound (Numerals.Roundness.OnScale W) ↑n ↑m}, Set.Ioi m

theorem CumminsFranke2021.enrichment_eq {W : Finset ℤ} (hW : 0 ∉ W) {n w : ℕ} (hw : ↑w = Numerals.Roundness.scaleLcm W ↑n) : enrichment W n = Set.Ioc n (n + w)

On scales of multiples, the pragmatic reading of more than n is not more than n + w, the next point of the coarsest scale through n, where w is the lcm of the widths of the scales through n.

theorem CumminsFranke2021.enrichment_singleton {w n : ℕ} (hw : 0 < w) (h : w ∣ n) : enrichment {↑w} n = Set.Ioc n (n + w)

On a single scale of width w through n, more than n implicates not more than n + w: on the scale of fifties more than 100 implicates the illustration's not more than 150, and on the scale of tens more than 110 implicates not more than 120.

def CumminsFranke2021.decimal : Finset ℤ

The aligned decimal scales of units, tens, hundreds and thousands.

Equations

• CumminsFranke2021.decimal = {1000, 100, 10, 1}

theorem CumminsFranke2021.enrichment_decimal : enrichment decimal 110 = Set.Ioc 110 120 ∧ enrichment decimal 100 = Set.Ioc 100 200

On the decimal scales, where each numeral is read at the coarsest scale through it, more than 110 implicates the paper's not more than 120 and more than 100 the vacuous not more than 200.

theorem CumminsFranke2021.isLeast_strongerAlternative (ctx : Cummins2015.Context) : IsLeast {m : ℕ | Cummins2015.StrongerAlternative ctx 100 m} 200 ∧ (ctx.granularity ≠ none → IsLeast {m : ℕ | Cummins2015.StrongerAlternative ctx 110 m} 120)

In Cummins's constraint-based account the stronger alternatives to more than 100 begin at 200 in every context, since an alternative must be entirely round like 100 and no numeral in between is, and those to more than 110 begin at 120 in a context that sets a granularity level, the next points of the coarsest decimal scales.

The paper's rate

@[reducible, inline]

noncomputable abbrev CumminsFranke2021.nineTenths : ↑unitInterval

The paper's illustrative enrichment rate of nine in ten.

Equations

• CumminsFranke2021.nineTenths = ⟨9 / 10, CumminsFranke2021.nineTenths._proof_5⟩

theorem CumminsFranke2021.relevance_reversal : DTS.relevance success (Set.Ioi 100) < DTS.relevance success (Set.Ioi 110) ∧ DTS.relevance (assertability nineTenths) (assertable 110 120) < DTS.relevance (assertability nineTenths) (assertable 100 150)

Semantically more than 110 is the stronger argument for success, but pragmatically, at the paper's rate of nine in ten, the order reverses.

theorem CumminsFranke2021.relevance_assertable_moreThan100_nineTenths : DTS.relevance (assertability nineTenths) (assertable 100 150) = Real.log (21 / 8)

The paper's pragmatic log (21/8) for more than 100.

theorem CumminsFranke2021.relevance_assertable_moreThan110_nineTenths : DTS.relevance (assertability nineTenths) (assertable 110 120) = Real.log (6 / 5)

The paper's pragmatic log (6/5) for more than 110.