[CF21]: Rational Interpretation of Numerical Quantity

[CF21] [Mer99a]

[CF21] applies [Mer99a]'s log-likelihood-ratio measure of argumentative strength to numerical quantity expressions: the strength of utterance u toward goal G is log (P(u∣G) / P(u∣¬G)) (eq. 17), and a pragmatic variant replaces truth with felicitous assertability (eq. 25). The §5 worked example: a conference succeeds iff more than 120 people register, registrations are uniform on [0, 200], and the speaker chooses between more than 100 and more than 110.

Main results

• bayesFactor_lt_of_goal_entails: §5.1's alignment of semantic and argumentative strength, in general form — between utterances entailed by the goal, the semantically stronger one is the argumentatively stronger one, since its extra content can only shed ¬G-worlds.
• cond_prod_byInterpretation: §5.2's computation pattern in general form — over the enriched/literal interpretation mixture, an interpretation-dependent event's conditional probability is the mixture of its branches' conditional probabilities.
• strength_reversal: the paper's central demonstration — semantically more than 110 is the stronger argument for success (semantic_ordering, Bayes factors 6 < 12), but under assertability with a 90%-enriching listener the ordering reverses (21/8 vs 6/5).

The §5.1–5.2 Bayes-factor values are computed against a counting prior over 20 bands of width 10 (every threshold in the example — 100, 110, 120, 150 — is a band boundary, so the paper's continuous uniform distribution on [0, 200] is represented exactly, and conditioning normalizes away the total mass). Concrete masses evaluate by count_apply_fintype and comparisons transfer to ℝ, following the countable-space register of Mathlib.Probability.Decision.Risk.Countable. The measure strength is Real.log (nats) of DTS.bayesFactor; the paper leaves the log base unspecified (its printed values are base 10) and uses it only ordinally.

Deviation: for more than 110 the paper prints log 11, computed from "the probability that more than 100 is true given that more than 110 is false equals 1/11" — the Bayes factor of more than 100 toward the goal more than 110 (bayesFactor_moreThan100_toward110). Toward the example's stated goal (more than 120) the factor is 12 (bayesFactor_moreThan110); the semantic ordering is the same either way.

Not formalized: the §5.4 rational-hearer conditions (eqs. 27–28), which compare an utterance's strength against the alternatives assertable in ¬G-worlds and are stated but not computed with in the paper; and the §6 corpus study of research-ranking reports.

Semantic strength and goal entailment (§5.1)

theorem CumminsFranke2021.bayesFactor_lt_of_goal_entails {W : Type u_1} [MeasurableSpace W] (ctx : DTS.Context W) [MeasureTheory.IsFiniteMeasure ctx.prior] {u₁ u₂ : Set W} (h₂m : MeasurableSet u₂) (hsub : u₂ ⊆ u₁) (hent : ctx.topic ⊆ u₂) (hG : ctx.prior ctx.topic ≠ 0) (hgap : ctx.prior ((ctx.topicᶜ ∩ u₁) \ u₂) ≠ 0) (hpos : ctx.prior (ctx.topicᶜ ∩ u₂) ≠ 0) : DTS.bayesFactor ctx u₁ < DTS.bayesFactor ctx u₂

§5.1's alignment of semantic and argumentative strength: between two utterances entailed by the goal, the semantically stronger (smaller) one is the argumentatively stronger one — both are certain given the goal, and the weaker utterance's extra extension can only add ¬G-mass to the denominator of the Bayes factor.

The §5 example

@[reducible, inline]

abbrev CumminsFranke2021.Band : Type

Registration totals in bands of width 10: band k covers (10k, 10(k+1)]. Every threshold in the §5 example (100, 110, 120, 150) is a band boundary, so the paper's continuous uniform distribution on [0, 200] is represented exactly by a counting prior over the 20 bands.

Equations

• CumminsFranke2021.Band = Fin 20

def CumminsFranke2021.moreThan (n : ℕ) : Set Band

The extension of more than n, for thresholds n that are multiples of 10: every total in band k exceeds n iff n ≤ 10k.

Equations

• CumminsFranke2021.moreThan n = {k : CumminsFranke2021.Band | n ≤ 10 * ↑k}

@[instance_reducible]

instance CumminsFranke2021.instDecidablePredBandMemSetMoreThan (n : ℕ) : DecidablePred fun (x : Band) => x ∈ moreThan n

Equations

• CumminsFranke2021.instDecidablePredBandMemSetMoreThan n k = CumminsFranke2021.instDecidablePredBandMemSetMoreThan._aux_1 n k

@[reducible, inline]

noncomputable abbrev CumminsFranke2021.successContext : DTS.Context Band

§5.1: the goal is S = more than 120 (conference success), with the counting prior (conditioning normalizes, so counting and uniform priors induce the same strengths).

Equations

• CumminsFranke2021.successContext = { topic := CumminsFranke2021.moreThan 120, topicMeasurable := CumminsFranke2021.successContext._proof_1, prior := MeasureTheory.Measure.count }

theorem CumminsFranke2021.bayesFactor_moreThan100 : DTS.bayesFactor successContext (moreThan 100) = 6

§5.1: the Bayes factor of more than 100 toward success is 1 / (1/6) = 6 (the paper's log 6 ≈ 0.78).

theorem CumminsFranke2021.bayesFactor_moreThan110 : DTS.bayesFactor successContext (moreThan 110) = 12

The Bayes factor of more than 110 toward success is 1 / (1/12) = 12. The paper instead prints log 11 (see bayesFactor_moreThan100_toward110); the ordering against bayesFactor_moreThan100 is the same.

theorem CumminsFranke2021.bayesFactor_moreThan100_toward110 : DTS.bayesFactor { topic := moreThan 110, topicMeasurable := ⋯, prior := MeasureTheory.Measure.count } (moreThan 100) = 11

The quantity behind the paper's printed log 11: the Bayes factor of more than 100 toward the goal more than 110 ("the probability that more than 100 is true given that more than 110 is false equals 1/11").

theorem CumminsFranke2021.semantic_ordering : DTS.bayesFactor successContext (moreThan 100) < DTS.bayesFactor successContext (moreThan 110)

§5.1 as an instance of bayesFactor_lt_of_goal_entails: both utterances are entailed by the goal and more than 110 is semantically stronger, so it is the stronger argument.

The assertability mixture (§5.2)

Assertability is stochastic: with probability 9/10 the listener enriches the utterance with its scalar implicature (more than 100 ⇝ not more than 150, more than 110 ⇝ not more than 120), so u is felicitously assertable only if the implicature is also true; with probability 1/10 the utterance is interpreted literally. The mixture lives on the product of worlds and interpretations, where interpretation-dependent events are unions of rectangles and conditional probabilities decompose branchwise.

inductive CumminsFranke2021.Interpretation : Type

How the listener resolves an utterance (§5.2): enriched with its scalar implicature, or literal.

• enriched : Interpretation
• literal : 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 = ⊤

instance CumminsFranke2021.instDiscreteMeasurableSpaceInterpretation : DiscreteMeasurableSpace Interpretation

def CumminsFranke2021.byInterpretation {W : Type u_1} (enr lit : Set W) : Set (W × Interpretation)

An interpretation-dependent event: enr under enrichment, lit under literal interpretation.

Equations

• CumminsFranke2021.byInterpretation enr lit = enr ×ˢ {CumminsFranke2021.Interpretation.enriched} ∪ lit ×ˢ {CumminsFranke2021.Interpretation.literal}

theorem CumminsFranke2021.prod_byInterpretation {W : Type u_1} [MeasurableSpace W] (μ : MeasureTheory.Measure W) (ν : MeasureTheory.Measure Interpretation) [MeasureTheory.SFinite ν] {enr lit : Set W} (hlit : MeasurableSet lit) : (μ.prod ν) (byInterpretation enr lit) = μ enr * ν {Interpretation.enriched} + μ lit * ν {Interpretation.literal}

Mass of an interpretation-dependent event under a product prior: the branches weigh their events by the interpretation probabilities.

theorem CumminsFranke2021.cond_prod_byInterpretation {W : Type u_1} [MeasurableSpace W] (μ : MeasureTheory.Measure W) (ν : MeasureTheory.Measure Interpretation) [MeasureTheory.IsProbabilityMeasure ν] {s enr lit : Set W} (hs : MeasurableSet s) (hlit : MeasurableSet lit) : (μ.prod ν)[byInterpretation enr lit | s ×ˢ Set.univ] = ν {Interpretation.enriched} * μ[enr | s] + ν {Interpretation.literal} * μ[lit | s]

§5.2's computation pattern: conditional on a lifted event, an interpretation-dependent event's probability is the mixture of its branches' conditional probabilities.

noncomputable def CumminsFranke2021.interpretationMeasure : MeasureTheory.Measure Interpretation

The §5.2 interpretation mixture: enriched with probability 9/10, literal otherwise.

Equations

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

instance CumminsFranke2021.instIsProbabilityMeasureInterpretationInterpretationMeasure : MeasureTheory.IsProbabilityMeasure interpretationMeasure

Assertability in the example (§5.2)

noncomputable def CumminsFranke2021.assertabilityContext : DTS.Context (Band × Interpretation)

§5.2: the assertability context — bands crossed with the listener's interpretation, goal lifted along the band.

Equations

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

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

Felicitous assertability of more than n whose enrichment is not more than cap: under enrichment both the content and the implicature must hold; under literal interpretation only the content.

Equations

• CumminsFranke2021.assertable n cap = CumminsFranke2021.byInterpretation (CumminsFranke2021.moreThan n \ CumminsFranke2021.moreThan cap) (CumminsFranke2021.moreThan n)

theorem CumminsFranke2021.assertable_bayesFactor_moreThan100 : DTS.bayesFactor assertabilityContext (assertable 100 150) = 21 / 8

§5.2's value for more than 100 (enriched to not more than 150): P(A(u)∣S) = (9/10)·(3/8) + (1/10)·1 = 35/80 against P(A(u)∣¬S) = 1/6, giving Bayes factor 21/8 (the paper's log (21/8) = 0.419).

theorem CumminsFranke2021.assertable_bayesFactor_moreThan110 : DTS.bayesFactor assertabilityContext (assertable 110 120) = 6 / 5

§5.2's value for more than 110 (enriched to not more than 120): the enriched reading is incompatible with success, so P(A(u)∣S) = (9/10)·0 + (1/10)·1 = 1/10 against P(A(u)∣¬S) = 1/12, giving Bayes factor 6/5 (the paper's log (6/5) = 0.079).

The reversal

noncomputable def CumminsFranke2021.strength {W : Type u_1} [MeasurableSpace W] (ctx : DTS.Context W) (u : Set W) : ℝ

Argumentative strength (eq. 17; eq. 25 on the assertability space): the log of the Bayes factor, positive iff the utterance supports the goal.

Equations

• CumminsFranke2021.strength ctx u = Real.log (DTS.bayesFactor ctx u).toReal

theorem CumminsFranke2021.strength_reversal : strength successContext (moreThan 100) < strength successContext (moreThan 110) ∧ strength assertabilityContext (assertable 110 120) < strength assertabilityContext (assertable 100 150)

The paper's central §5.2 demonstration: semantically more than 110 is the stronger argument for success, but under assertability the ordering reverses — precision that looks argumentatively optimal is penalized once the listener's enrichment is priced in.