[BR21] — Rationalizing Evaluativity

[BR21] [LG17] [BLG16] [Ret15] [Bar02b]

Proceedings of Sinn und Bedeutung 25, pp. 187–204.

Key Claims

1. Evaluativity is gradient: Degree constructions differ in the strength of their evaluative inferences. The model produces a strict ranking: positive > equative > comparative.

2. Comparison-class uncertainty: Worlds are two-dimensional — subject height × comparison class center. The listener jointly infers height and CC statistics, extending [LG17]'s threshold RSA with [Bar02b]'s insight that CC uncertainty is informative.

3. Lexical uncertainty for markedness: Antonym-sensitive evaluativity (marked equatives like "as short as" are evaluative; unmarked "as tall as" are not) emerges from [BLG16]'s lexical uncertainty, where marked forms have higher production cost.

4. Evaluativity metric: E[ht − μ] — the expected deviation of the subject's height from the CC center — measures evaluativity strength.

Model Architecture (§2.1)

• L₀(w | u, L) ∝ P(w) · L(u, w)
• Sₙ(u | w, L) ∝ exp(α · (log Lₙ₋₁(w | u, L) − C(u)))
• L₁(w | u) ∝ P(w) · Σ_L P(L) · S₁(u | w, L)
• α = 4, C(marked) = 2, C(unmarked) = 1, C(∅) = 0

Discretization

The paper uses heights 1–17, CC centers 5–14, |ht − μ| ≤ 4 (SD = 2). We scale to heights 1–9, CC centers 3–7, |ht − μ| ≤ 2 (SD = 1), preserving the qualitative predictions with a 45-world grid (25 valid worlds after the Gaussian truncation).

Verified Predictions (Table 1)

1. Positive construction (Simulation 1): both antonyms evaluative
2. Exact equative (Simulation 2): marked antonym evaluative, unmarked weakly evaluative
3. ≥ Equative (Simulation 3): marked evaluative, unmarked barely evaluative
4. Comparative (Simulation 4): neither antonym evaluative — evaluative world does NOT win over non-evaluative world, unlike equatives
5. Antonym asymmetry: marked equative produces stronger evaluative inference
6. Cross-construction contrast: equative marked IS evaluative but comparative marked is NOT, confirming that partial antonymic competition (not just cost) drives evaluativity

Connection to [Ret15]

[Ret15] derives evaluativity categorically via Q/R-implicature (formalized in Pragmatics/Implicature/Evaluativity.lean). This RSA model derives the same predictions gradiently: evaluativity strength varies continuously across constructions. Both accounts agree on the antonym-sensitive pattern (equative marked > equative unmarked).

The RSA model adds two things the Neo-Gricean account lacks:

• Graded predictions (probability distributions over evaluativity strength)
• A unified mechanism (rational communication) rather than separate Q/R principles

@[reducible, inline]

abbrev BumfordRett2021.EvalWorld : Type

A world is a pair (height index, CC center index).

Height index i ∈ Fin 9 represents height i + 1 (range 1–9). CC center index j ∈ Fin 5 represents center j + 3 (range 3–7). Valid worlds satisfy |height − center| ≤ 2 (enforced via prior).

Equations

• BumfordRett2021.EvalWorld = (Fin 9 × Fin 5)

def BumfordRett2021.htVal (w : EvalWorld) : ℤ

Height value (1–9) from world indices.

Equations

• BumfordRett2021.htVal w = ↑↑w.1 + 1

def BumfordRett2021.muVal (w : EvalWorld) : ℤ

CC center value (3–7) from world indices.

Equations

• BumfordRett2021.muVal w = ↑↑w.2 + 3

def BumfordRett2021.deviation (w : EvalWorld) : ℤ

Deviation of height from CC center: ht − μ.

Equations

• BumfordRett2021.deviation w = BumfordRett2021.htVal w - BumfordRett2021.muVal w

def BumfordRett2021.worldPrior (w : EvalWorld) : ℚ

Gaussian-weighted prior over valid worlds.

CC center is uniform; height weight decreases with distance from center. Approximates N(μ, 1) truncated at |ht − μ| ≤ 2. Weights: d=0 → 10, d=1 → 6, d=2 → 1, d>2 → 0 (invalid world).

Equations

• BumfordRett2021.worldPrior w = match (BumfordRett2021.deviation w).natAbs with | 0 => 10 | 1 => 6 | 2 => 1 | x => 0

inductive BumfordRett2021.Utterance : Type

Utterance type: unmarked (positive-polar), marked (negative-polar), or null.

For the positive construction: unmarked = "tall", marked = "short". For the exact equative: unmarked = "as tall as K", marked = "as short as K". Cost asymmetry (marked = 2, unmarked = 1) drives antonym-sensitive evaluativity via [BLG16]'s lexical uncertainty.

• unmarked : Utterance
• marked : Utterance
• null : Utterance

def BumfordRett2021.instReprUtterance.repr : Utterance → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance BumfordRett2021.instReprUtterance : Repr Utterance

Equations

• BumfordRett2021.instReprUtterance = { reprPrec := BumfordRett2021.instReprUtterance.repr }

@[implicit_reducible]

instance BumfordRett2021.instDecidableEqUtterance : DecidableEq Utterance

Equations

• BumfordRett2021.instDecidableEqUtterance x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance BumfordRett2021.instFintypeUtterance : Fintype Utterance

Equations

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

def BumfordRett2021.cost : Utterance → ℚ

Utterance costs: marked = 2, unmarked = 1, null = 0.

Equations

• BumfordRett2021.cost BumfordRett2021.Utterance.unmarked = 1
• BumfordRett2021.cost BumfordRett2021.Utterance.marked = 2
• BumfordRett2021.cost BumfordRett2021.Utterance.null = 0

@[reducible, inline]

abbrev BumfordRett2021.Sigma : Type

Threshold offset σ ∈ {−2, −1, 0, 1, 2}.

Determines how far above the CC center a person must be to count as "tall." Index s ∈ Fin 5 represents σ = s − 2. Higher σ means a more exclusive threshold.

Equations

• BumfordRett2021.Sigma = Fin 5

def BumfordRett2021.sigmaVal (s : Sigma) : ℤ

Integer offset value: index s ↦ σ = s − 2.

Equations

• BumfordRett2021.sigmaVal s = ↑↑s - 2

noncomputable def BumfordRett2021.worldPriorR (w : EvalWorld) : ℝ

World prior as ℝ.

Equations

• BumfordRett2021.worldPriorR w = ↑(BumfordRett2021.worldPrior w)

theorem BumfordRett2021.worldPriorR_nonneg (w : EvalWorld) : 0 ≤ worldPriorR w

def BumfordRett2021.costN : Utterance → ℕ

Utterance cost as a natural exponent: exp(−α·C(u)) = e^(costN u) at the paper's α = 4, where e := exp(−4).

Equations

• BumfordRett2021.costN BumfordRett2021.Utterance.unmarked = 1
• BumfordRett2021.costN BumfordRett2021.Utterance.marked = 2
• BumfordRett2021.costN BumfordRett2021.Utterance.null = 0

Companion architecture on PMF, parameterized by the cost-factor base e (= exp(−4) at the paper's α = 4; only the speaker depends on e):

L₀(w | u, σ) ∝ ⟦u⟧(σ,w) · P(w)               (`meaningE`, `L0v`)
S₁(u | w, σ) ∝ L₀(w | u, σ)⁴ · e^C(u)         (`Sk`)
L₁(w, σ | u) ∝ S₁(u | w, σ) · P(w) · P(σ)     (`listener`, `PMF.posterior`)

The prior is baked into the graded L₀ kernel (eq 10, L₀ ∝ P(w)·⟦u⟧(w)); null is licensed everywhere, so the speaker normaliser vanishes only at invalid (zero-prior) worlds, which carry joint weight 0 and are handled by a dite wrapper. Statements are e-generic over 0 < e < 1; exp(−4) is instantiated only in bridging corollaries.

def BumfordRett2021.meaningE (sem : Utterance → Sigma → EvalWorld → Bool) (σ : Sigma) (u : Utterance) (w : EvalWorld) : ENNReal

Prior-weighted meaning ⟦u⟧(σ,w) · P(w), lifted to ℝ≥0∞.

Equations

• BumfordRett2021.meaningE sem σ u w = if sem u σ w = true then ENNReal.ofReal ↑(BumfordRett2021.worldPrior w) else 0

noncomputable def BumfordRett2021.L0v (sem : Utterance → Sigma → EvalWorld → Bool) (σ : Sigma) (u : Utterance) (w : EvalWorld) : ENNReal

Literal-listener value L₀(w | u, σ) = ⟦u⟧(σ,w)·P(w) / D (well-defined and 0 on empty extensions, since 0 · ⊤ = 0 in ℝ≥0∞).

Equations

• BumfordRett2021.L0v sem σ u w = BumfordRett2021.meaningE sem σ u w * (∑' (w' : BumfordRett2021.EvalWorld), BumfordRett2021.meaningE sem σ u w')⁻¹

noncomputable def BumfordRett2021.spkW (sem : Utterance → Sigma → EvalWorld → Bool) (e : ℝ) (s : EvalWorld × Sigma) (u : Utterance) : ENNReal

Speaker weight L₀(w|u,σ)⁴ · e^C(u).

Equations

• BumfordRett2021.spkW sem e s u = BumfordRett2021.L0v sem s.2 u s.1 ^ 4 * ENNReal.ofReal (e ^ BumfordRett2021.costN u)

noncomputable def BumfordRett2021.Sk (sem : Utterance → Sigma → EvalWorld → Bool) (e : ℝ) (s : EvalWorld × Sigma) : PMF Utterance

Speaker S₁(· | w, σ) : PMF Utterance, dite-guarded so it is total even at invalid worlds (where every weight vanishes; those carry joint prior 0).

Equations

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

def BumfordRett2021.jointW (s : EvalWorld × Sigma) : ENNReal

Unnormalised joint prior P(w) · P(σ) (uniform latent absorbed).

Equations

• BumfordRett2021.jointW s = ENNReal.ofReal ↑(BumfordRett2021.worldPrior s.1)

def BumfordRett2021.mkW (h : Fin 9) (m : Fin 5) : EvalWorld

Concise world constructor: mkW h m = (Fin h, Fin m).

Equations

• BumfordRett2021.mkW h m = (h, m)

noncomputable def BumfordRett2021.jointK : PMF (EvalWorld × Sigma)

Listener's joint prior over world × σ.

Equations

• BumfordRett2021.jointK = PMF.normalize BumfordRett2021.jointW BumfordRett2021.jointW_tsum_ne_zero✝ BumfordRett2021.jointW_tsum_ne_top✝

theorem BumfordRett2021.marg_ne_zero {sem : Utterance → Sigma → EvalWorld → Bool} {e : ℝ} (he0 : 0 < e) {u : Utterance} {w0 : EvalWorld} {σ0 : Sigma} (hval : worldPrior w0 ≠ 0) (hnull : sem Utterance.null σ0 w0 = true) (hlic : sem u σ0 w0 = true) : PMF.marginal (Sk sem e) jointK u ≠ 0

Single-witness discharge of the listener's marginal positivity: a valid world w0 licensed for u at some σ0 (with null also licensed there).

Structural speaker/listener monotonicity

Evaluativity is proved structurally, with no normaliser computation: the per-latent speaker order follows from licensing-set inclusion between two equal-prior worlds. Two equal-prior worlds with the same licensing bit for u have identical speaker numerators; a wider licensing set only enlarges the denominator. Hence a world that is licensed for fewer alternatives (its licensing set is contained in the other's) puts more mass on the observed u. Only 0 < e is used (for strict positivity); nothing needs e < 1.

def BumfordRett2021.posMeaning (u : Utterance) (σ : Sigma) (w : EvalWorld) : Bool

Positive construction meaning (eq 12):

• unmarked ("tall"): ht_w(j) ≥ μ_w + σ
• marked ("short"): ht_w(j) ≤ μ_w + σ
• null: true

Equations

• BumfordRett2021.posMeaning BumfordRett2021.Utterance.unmarked σ w = decide (BumfordRett2021.htVal w ≥ BumfordRett2021.muVal w + BumfordRett2021.sigmaVal σ)
• BumfordRett2021.posMeaning BumfordRett2021.Utterance.marked σ w = decide (BumfordRett2021.htVal w ≤ BumfordRett2021.muVal w + BumfordRett2021.sigmaVal σ)
• BumfordRett2021.posMeaning BumfordRett2021.Utterance.null σ w = true

noncomputable def BumfordRett2021.posL1 (u : Utterance) {e : ℝ} (he0 : 0 < e) : PMF (EvalWorld × Sigma)

Positive-construction pragmatic listener L₁(· | u) at cost base e.

Equations

• BumfordRett2021.posL1 u he0 = RSA.Canonical.L1 (BumfordRett2021.Sk BumfordRett2021.posMeaning e) BumfordRett2021.jointK u ⋯

Prediction 1: "Tall" shifts height above CC mean

Hearing "Jane is tall" (unmarked) shifts L₁'s posterior toward worlds where the subject's height exceeds the CC center. At fixed CC center μ = 5 (index 2), height 6 (index 5, dev = +1) becomes more likely than height 4 (index 3, dev = −1). Both worlds have equal prior (6), so the asymmetry is entirely due to pragmatic reasoning. The paper reports E[ht − μ] = 2.08 at L₁.

theorem BumfordRett2021.pos_tall_evaluative (e : ℝ) (he0 : 0 < e) : (posL1 Utterance.unmarked he0).fst (mkW 5 2) > (posL1 Utterance.unmarked he0).fst (mkW 3 2)

Prediction 2: "Short" shifts height below CC mean

Mirror image: hearing "Jane is short" (marked) shifts posterior toward worlds where height is below the CC center. E[ht − μ] = −3.18 at L₁. The marked form is even more evaluative than the unmarked form, because the extra cost signals that the speaker's reason for speaking must be particularly strong.

theorem BumfordRett2021.pos_short_evaluative (e : ℝ) (he0 : 0 < e) : (posL1 Utterance.marked he0).fst (mkW 3 2) > (posL1 Utterance.marked he0).fst (mkW 5 2)

def BumfordRett2021.kHeight : ℤ

Keisha's height k, fixed and known to both speaker and listener. In our scaled model: k = 5 (height index 4).

Equations

• BumfordRett2021.kHeight = 5

def BumfordRett2021.eqMeaning (u : Utterance) (σ : Sigma) (w : EvalWorld) : Bool

Exact equative meaning (eq 14):

• unmarked ("as tall as K"): ht = k ∧ k ≥ μ + σ
• marked ("as short as K"): ht = k ∧ k ≤ μ + σ
• null: true

The equative fixes height to k. The informative content is about where k sits relative to the CC center: does the threshold σ classify k as "tall-enough" (unmarked) or "short-enough" (marked)?

Equations

• One or more equations did not get rendered due to their size.
• BumfordRett2021.eqMeaning BumfordRett2021.Utterance.null σ w = true

noncomputable def BumfordRett2021.eqL1 (u : Utterance) {e : ℝ} (he0 : 0 < e) : PMF (EvalWorld × Sigma)

Exact-equative pragmatic listener L₁(· | u) at cost base e.

Equations

• BumfordRett2021.eqL1 u he0 = RSA.Canonical.L1 (BumfordRett2021.Sk BumfordRett2021.eqMeaning e) BumfordRett2021.jointK u ⋯

Prediction 3: Marked equative is evaluative

Hearing "Jane is as short as Keisha" (marked) shifts L₁'s posterior toward high-μ worlds where k = 5 is below the CC center — i.e., Keisha's height is atypically low. The paper reports E[k − μ] = −1.06 at L₁.

The mechanism: the speaker paid extra cost (C = 2) for the marked form. By [BLG16]'s logic, L₁ infers the speaker must have had a strong reason — the marked form is distinctively informative in worlds where k is atypically low.

theorem BumfordRett2021.eq_marked_evaluative (e : ℝ) (he0 : 0 < e) : (eqL1 Utterance.marked he0).fst (mkW 4 4) > (eqL1 Utterance.marked he0).fst (mkW 4 0)

Prediction 4: Unmarked equative is weakly evaluative

Hearing "Jane is as tall as Keisha" (unmarked) produces a weak evaluative inference: the posterior slightly favors worlds where k is above the CC center (μ < k). The paper reports E[k − μ] = 0.84 at L₁, much weaker than the marked form's −1.06.

This asymmetry — marked evaluative, unmarked weakly/not evaluative — is the antonym-sensitive pattern that [Ret15] identifies categorically and this model derives gradiently.

theorem BumfordRett2021.eq_unmarked_weakly_evaluative (e : ℝ) (he0 : 0 < e) : (eqL1 Utterance.unmarked he0).fst (mkW 4 0) > (eqL1 Utterance.unmarked he0).fst (mkW 4 4)

≥ Equative (Minimum-Standard) Semantics

The "at least as tall as" equative uses ≥ instead of = for height. Unlike the exact equative, the unmarked and marked forms are NOT synonymous: "at least as tall as K" and "at least as short as K" have different truth conditions. Antonymic competition is therefore partial, predicting evaluativity intermediate between the exact equative (full synonymy) and the comparative (no overlap).

def BumfordRett2021.geqMeaning (u : Utterance) (σ : Sigma) (w : EvalWorld) : Bool

≥ equative meaning (eq 16):

• unmarked ("at least as tall as K"): ht ≥ k ∧ k ≥ μ + σ
• marked ("at least as short as K"): ht ≤ k ∧ k ≤ μ + σ
• null: true

Equations

• One or more equations did not get rendered due to their size.
• BumfordRett2021.geqMeaning BumfordRett2021.Utterance.null σ w = true

noncomputable def BumfordRett2021.geqL1 (u : Utterance) {e : ℝ} (he0 : 0 < e) : PMF (EvalWorld × Sigma)

≥-equative pragmatic listener L₁(· | u) at cost base e.

Equations

• BumfordRett2021.geqL1 u he0 = RSA.Canonical.L1 (BumfordRett2021.Sk BumfordRett2021.geqMeaning e) BumfordRett2021.jointK u ⋯

Prediction 5: Marked ≥ equative is evaluative

Hearing "Jane is at least as short as Keisha" (marked) shifts L₁'s posterior toward worlds where k is below the CC center. The paper reports E[k − μ] = −1.52 at L₁.

theorem BumfordRett2021.geq_marked_evaluative (e : ℝ) (he0 : 0 < e) : (geqL1 Utterance.marked he0).fst (mkW 4 4) > (geqL1 Utterance.marked he0).fst (mkW 4 0)

Prediction 6: Unmarked ≥ equative is barely evaluative

Hearing "Jane is at least as tall as Keisha" (unmarked) barely shifts the posterior. The paper reports E[k − μ] = 0.11 at L₁ — the weakest evaluative effect of any construction.

theorem BumfordRett2021.geq_unmarked_barely_evaluative (e : ℝ) (he0 : 0 < e) : (geqL1 Utterance.unmarked he0).fst (mkW 4 0) > (geqL1 Utterance.unmarked he0).fst (mkW 4 4)

Comparative Semantics

The comparative uses strict inequality for height (ht > k / ht < k). Unlike the equatives, the comparative forms have NO semantic overlap: "taller than K" and "shorter than K" are not even close to synonymous. With no antonymic competition and high informativity (the comparative provides clear information worth the cost), there is no pressure for evaluative inference.

The paper predicts E[k − μ] = −0.74 (unmarked) and −0.44 (marked) at L₁ — both close to zero. The listener guesses Keisha is slightly below the CC mean, but this is a generic probabilistic consequence of learning relative height, not an evaluative inference.

def BumfordRett2021.compMeaning (u : Utterance) (σ : Sigma) (w : EvalWorld) : Bool

Comparative meaning (eq 18):

• unmarked ("taller than K"): ht > k ∧ k ≥ μ + σ
• marked ("shorter than K"): ht < k ∧ k ≤ μ + σ
• null: true

Equations

• One or more equations did not get rendered due to their size.
• BumfordRett2021.compMeaning BumfordRett2021.Utterance.null σ w = true

noncomputable def BumfordRett2021.compL1 (u : Utterance) {e : ℝ} (he0 : 0 < e) : PMF (EvalWorld × Sigma)

Comparative pragmatic listener L₁(· | u) at cost base e.

Equations

• BumfordRett2021.compL1 u he0 = RSA.Canonical.L1 (BumfordRett2021.Sk BumfordRett2021.compMeaning e) BumfordRett2021.jointK u ⋯

Prediction 7: Comparative marked does not strongly shift k

Unlike the equative, the marked comparative does not push the listener toward worlds where k is far from the CC center. At equal prior (dev = ±1), the world with k near the mean is preferred over the world with k well above the mean. The paper reports E[k − μ] = −0.44 at L₁ — a very weak effect, unlike the equative's −1.06.

theorem BumfordRett2021.comp_marked_weak (e : ℝ) (he0 : 0 < e) : (compL1 Utterance.marked he0).fst (mkW 3 2) > (compL1 Utterance.marked he0).fst (mkW 3 0)

Prediction 8: Comparative unmarked is counter-evaluative

Hearing "Jane is taller than Keisha" (unmarked) does NOT make the listener infer that Keisha is tall. In fact, the paper reports E[k − μ] = −0.74, slightly negative: Keisha is inferred to be slightly below the CC mean. This is because knowing Jane exceeds Keisha's height leaves more room for Keisha to be below average.

theorem BumfordRett2021.comp_unmarked_counter_evaluative (e : ℝ) (he0 : 0 < e) (he_lo : 1 / 100 ≤ e) : (compL1 Utterance.unmarked he0).fst (mkW 5 3) > (compL1 Utterance.unmarked he0).fst (mkW 5 1)

Counter-evaluative comparative — a prior-magnitude effect, not a licensing one. Unlike the seven Tier-A predictions (which hold for every cost base e ∈ (0,1) via evaluative_of_incl's bare 0 < e), here the speaker distribution depends on a world only through its licensing set (the prior cancels inside Sk), so the 10:1 world prior of mkW 5 3 (k at the CC mean) over mkW 5 1 (k above it) is the sole asymmetry and it dominates.

The prior dominates only when markedness costs are not extreme. The sharp threshold is e ≥ (D_unm(1)/D_null)⁴ = (25/120)⁴ ≈ 0.0019: for e below it, the cost factor e^C so heavily discounts the informative "taller than" utterance in the high-threshold worlds that the informativity cost dominates the prior mass and the inequality flips. We therefore assume 1/100 ≤ e (comfortably above the threshold, and met by the paper's e = exp(−4) ≈ 0.018; see comp_unmarked_counter_evaluative_exp).

theorem BumfordRett2021.comp_unmarked_counter_evaluative_exp : (compL1 Utterance.unmarked ⋯).fst (mkW 5 3) > (compL1 Utterance.unmarked ⋯).fst (mkW 5 1)

The counter-evaluative comparative at the paper's cost base e = exp(−4). The hypothesis 1/100 ≤ exp(−4) reduces to exp 4 ≤ 100, and exp 4 = (exp 1)⁴ < 2.7182818286⁴ ≈ 54.6 < 100.

Gradient evaluativity ranking

The paper's central prediction (Table 1) is a strict ranking of evaluativity strength across constructions:

Construction	unmarked E[ht−μ]	marked E[ht−μ]	Evaluative?
Positive	2.08	−3.18	✓ ✓
= Equative	0.84	−1.06	✗ ✓
≥ Equative	0.11	−1.52	✗ ✓
Comparative	−0.74	−0.44	✗ ✗

This ranking emerges from two factors:

1. Informativity: The positive construction has an open degree argument (threshold is entirely unknown), making it maximally vague. Equatives fix height to k, reducing uncertainty. Comparatives provide strict ordering, leaving little room for evaluative inference.
2. Cost asymmetry: The marked form's extra cost (C = 2 vs 1) forces L₁ to seek explanations for the speaker's costly choice, driving evaluative inferences in worlds where the marked form is distinctively informative (i.e., atypical worlds).

The theorems above verify the key qualitative pattern across all four constructions:

• pos_tall_evaluative / pos_short_evaluative : positive ✓✓
• eq_marked_evaluative / eq_unmarked_weakly_evaluative : equative ✗✓
• geq_marked_evaluative / geq_unmarked_barely_evaluative : ≥ equative ✗✓
• comp_marked_weak / comp_unmarked_counter_evaluative : comparative ✗✗

RSA ↔ Neo-Gricean Agreement

[Ret15]'s Neo-Gricean account (formalized in Pragmatics/Implicature/Evaluativity.lean) classifies constructions categorically using AdjectivalConstruction and Polarity:

• Positive (.positive): evaluative for both polarities (Q-implicature)
• Equative (.equative): evaluative for .negative only (Manner/R-implicature)
• Comparative (.comparative): NOT evaluative (no applicable implicature)

This RSA model derives the same pattern gradiently: each L₁ prediction above confirms a qualitative directional prediction that matches the categorical classification. The RSA model adds:

1. Graded predictions — evaluativity has a continuous strength, not just ±
2. Unified mechanism — rational communication replaces separate Q/R principles
3. ≥ equative predictions — partial overlap produces intermediate evaluativity, a novel prediction the categorical account does not make

def BumfordRett2021.utterancePolarity : Utterance → Option Rett2015Implicature.Polarity

Map utterance polarity to the evaluativity Polarity type.

Equations

• BumfordRett2021.utterancePolarity BumfordRett2021.Utterance.unmarked = some Rett2015Implicature.Polarity.positive
• BumfordRett2021.utterancePolarity BumfordRett2021.Utterance.marked = some Rett2015Implicature.Polarity.negative
• BumfordRett2021.utterancePolarity BumfordRett2021.Utterance.null = none

@[reducible, inline]

abbrev BumfordRett2021.posConstruction : Degree.AdjectivalConstruction

Construction labels for each simulation, connecting to the AdjectivalConstruction type from Semantics/Degree/Gradability/Construction.lean.

Equations

• BumfordRett2021.posConstruction = Degree.AdjectivalConstruction.positive

@[reducible, inline]

abbrev BumfordRett2021.eqConstruction : Degree.AdjectivalConstruction

Equations

• BumfordRett2021.eqConstruction = Degree.AdjectivalConstruction.equative

@[reducible, inline]

abbrev BumfordRett2021.compConstruction : Degree.AdjectivalConstruction

Equations

• BumfordRett2021.compConstruction = Degree.AdjectivalConstruction.comparative

theorem BumfordRett2021.rsa_neo_gricean_agreement (e : ℝ) (he0 : 0 < e) : (Rett2015Implicature.deriveEvaluativity posConstruction Rett2015Implicature.Polarity.positive).isEvaluative = true ∧ (Rett2015Implicature.deriveEvaluativity posConstruction Rett2015Implicature.Polarity.negative).isEvaluative = true ∧ (posL1 Utterance.unmarked he0).fst (mkW 5 2) > (posL1 Utterance.unmarked he0).fst (mkW 3 2) ∧ (posL1 Utterance.marked he0).fst (mkW 3 2) > (posL1 Utterance.marked he0).fst (mkW 5 2) ∧ (Rett2015Implicature.deriveEvaluativity eqConstruction Rett2015Implicature.Polarity.positive).isEvaluative = false ∧ (Rett2015Implicature.deriveEvaluativity eqConstruction Rett2015Implicature.Polarity.negative).isEvaluative = true ∧ (eqL1 Utterance.marked he0).fst (mkW 4 4) > (eqL1 Utterance.marked he0).fst (mkW 4 0) ∧ (Rett2015Implicature.deriveEvaluativity compConstruction Rett2015Implicature.Polarity.positive).isEvaluative = false ∧ (Rett2015Implicature.deriveEvaluativity compConstruction Rett2015Implicature.Polarity.negative).isEvaluative = false

Cross-theory agreement: the RSA model and [Ret15]'s Neo-Gricean account agree on the full evaluativity paradigm.

• Positive: Neo-Gricean says evaluative for both polarities (Q-implicature). RSA confirms: both "tall" and "short" shift the posterior away from the CC mean.
• Equative: Neo-Gricean says evaluative for negative only (Manner implicature). RSA confirms: marked form shifts strongly, unmarked weakly.
• Comparative: Neo-Gricean says never evaluative (no applicable implicature). RSA confirms: neither polarity shifts strongly.

This theorem connects two independent formalizations — the categorical deriveEvaluativity function and the RSA L1 predictions — proving they make compatible predictions despite using entirely different mechanisms.

Relationship to [LG17]

LassiterGoodman2017PMF.lean formalizes the threshold RSA model for the positive construction only (1D world = height, latent = threshold). This file extends that model to 2D worlds (height × CC center) and adds cost-driven antonym competition. The positive construction predictions here subsume LassiterGoodman2017's: both show that hearing "tall"/"short" shifts the height posterior.

Architecture

The model runs on the mathlib-PMF RSA pipeline (RSA.Canonical.L1), with the latent threshold offset σ as the joint-listener's second coordinate:

• meaningE bakes the Gaussian 2D world prior into the graded L₀ kernel (L₀ ∝ P(w) · ⟦u⟧(σ,w)); L0v is its normalised value.
• Sk is the cost-sensitive speaker S₁(u | w,σ) ∝ L₀(w|u,σ)⁴ · e^C(u), with cost base e (= exp(−4) at α = 4). It is dite-guarded so it stays total at invalid worlds, which carry joint prior 0.
• jointK is the uniform-over-σ joint prior P(w)·P(σ); the listener is the joint Bayesian posterior over world × σ, world marginal via .fst.

Evaluativity (Tier A) is proved structurally from licensing-set inclusion and needs only 0 < e; the counter-evaluative comparative is the sole prior-magnitude case and needs 1/100 ≤ e.