[TG22]: Warm (for Winter)

[TG22] [LG17]

Cognitive Science 46 (2022) e13095.

Core Insight

Comparison class inference uses the SAME uncertain threshold mechanism as adjective interpretation ([LG17]). The listener jointly infers the degree x AND the comparison class c (Eq. 1):

L₁(x, c | u, k) ∝ S₁(u | x, c) · P(x | k) · P(c | k)

The comparison class c determines L0's height prior: subordinate uses the kind's distribution (e.g., basketball players), superordinate uses the general population (people). The threshold θ is marginalized analytically following [LG17]'s threshold RSA framework (the height priors are identical — see personWeight_eq_lassiterGoodman and basketballWeight_eq_lassiterGoodman).

Main Prediction: Polarity × Expectations Interaction

• "tall basketball player" → superordinate (people) comparison class
• "short basketball player" → subordinate (basketball players) comparison class
• Pattern reverses for jockeys (expected short)

The interaction emerges from RSA reasoning: a speaker saying "tall" about a basketball player is more informative under superordinate comparison (the L0 normalization Z_c(tall) differs by comparison class because the height distribution shifts), so L1 infers superordinate. For "short," subordinate comparison is more informative.

Simplifications

• α = 1 (the paper fits α₁ ≈ 1.45, α₂ ≈ 5.31; α=1 suffices for qualitative predictions since S₁ ∝ L₀^α is monotone in α)
• No utterance costs (Note 3: costs assumed equal for all utterances, so S₁(u | x, c) ∝ L₀(x | u, c)^α; cf. [LG17] which has C(tall)=C(short)=2, C(∅)=0)
• Flat comparison class prior (P(c|k) uniform; the paper's "Flat prior" model variant from Table 2; the full model fits basic-level bias + frequency effects, but the flat prior already yields the qualitative polarity × expectations pattern)
• Two extreme categories (basketball=high, jockey=low; the paper uses three per item set including a medium control like soccer player/golfer where no polarity effect is predicted)

Model Architecture

Per-kind mathlib-PMF pipeline with latent ComparisonClass, world Height:

• meaningE(k, c, u, h) = P(h | c) · |{θ : ⟦u⟧(h,θ)}| (marginalized threshold)
• jointW(k) world prior = P(h | k) (L1's kind-specific height prior)
• flat comparison-class prior P(c | k) (absorbed into jointW)
• speaker Sk (α = 1, no cost); listener listenerK = RSA.Canonical.L1

Verified Predictions

S1 Endorsement (speaker-level)

#	Prediction	Kind	Height	Comp. Class	Theorem
1	"tall" endorsed	basketball	h=6	super	basketball_tall_endorsed_super
2	"tall" NOT endorsed	basketball	h=6	sub	basketball_tall_not_endorsed_sub
3	"short" endorsed	basketball	h=5	sub	basketball_short_endorsed_sub
4	"short" NOT endorsed	basketball	h=5	super	basketball_short_not_endorsed_super
5	"tall" endorsed	jockey	h=4	sub	jockey_tall_endorsed_sub
6	"tall" NOT endorsed	jockey	h=4	super	jockey_tall_not_endorsed_super
7	"short" endorsed	jockey	h=4	super	jockey_short_endorsed_super
8	"short" NOT endorsed	jockey	h=4	sub	jockey_short_not_endorsed_sub

L1 Comparison Class Inference (Eq. 1 — the paper's main prediction)

#	Adj	Kind	Inferred CC	Theorem
9	tall	basketball	super	basketball_tall_infers_super
10	short	basketball	sub	basketball_short_infers_sub
11	tall	jockey	sub	jockey_tall_infers_sub
12	short	jockey	super	jockey_short_infers_super

Alternative Literal Listener (Eq. 6, Fig. 2 — opposite predictions)

#	Kind	Adj	Literal	Pragmatic	Theorem
13	basketball	tall	sub	super (#9)	literal_basketball_tall_sub
14	basketball	short	super	sub (#10)	literal_basketball_short_super
15	jockey	tall	super	sub (#11)	literal_jockey_tall_super
16	jockey	short	sub	super (#12)	literal_jockey_short_sub

@[reducible, inline]

abbrev TesslerGoodman2022.Height : Type

Discretized height: 0 through 10 in discrete steps (11 values).

Equations

• TesslerGoodman2022.Height = Degree.Degree 10

inductive TesslerGoodman2022.ComparisonClass : Type

Comparison classes: subordinate (the kind itself) or superordinate (the general population).

• subordinate : ComparisonClass
• superordinate : ComparisonClass

def TesslerGoodman2022.instReprComparisonClass.repr : ComparisonClass → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance TesslerGoodman2022.instReprComparisonClass : Repr ComparisonClass

Equations

• TesslerGoodman2022.instReprComparisonClass = { reprPrec := TesslerGoodman2022.instReprComparisonClass.repr }

@[implicit_reducible]

instance TesslerGoodman2022.instDecidableEqComparisonClass : DecidableEq ComparisonClass

Equations

• TesslerGoodman2022.instDecidableEqComparisonClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance TesslerGoodman2022.instFintypeComparisonClass : Fintype ComparisonClass

Equations

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

inductive TesslerGoodman2022.Kind : Type

Kinds (nominals) that can be modified by adjectives.

• person : Kind
• basketballPlayer : Kind
• jockey : Kind

@[implicit_reducible]

instance TesslerGoodman2022.instReprKind : Repr Kind

Equations

• TesslerGoodman2022.instReprKind = { reprPrec := TesslerGoodman2022.instReprKind.repr }

def TesslerGoodman2022.instReprKind.repr : Kind → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance TesslerGoodman2022.instDecidableEqKind : DecidableEq Kind

Equations

• TesslerGoodman2022.instDecidableEqKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance TesslerGoodman2022.instFintypeKind : Fintype Kind

Equations

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

inductive TesslerGoodman2022.Utterance : Type

Utterances: positive adjective, negative adjective, or silence.

• tall : Utterance
• short : Utterance
• silent : Utterance

@[implicit_reducible]

instance TesslerGoodman2022.instReprUtterance : Repr Utterance

Equations

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

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

Equations

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

@[implicit_reducible]

instance TesslerGoodman2022.instDecidableEqUtterance : DecidableEq Utterance

Equations

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

@[implicit_reducible]

instance TesslerGoodman2022.instFintypeUtterance : Fintype Utterance

Equations

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

def TesslerGoodman2022.personHeightWeight (h : Height) : ℕ

Height weight for generic people: symmetric, peaked at h=5. Approximates a discretized normal centered at the population mean.

Equations

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

def TesslerGoodman2022.basketballHeightWeight (h : Height) : ℕ

Height weight for basketball players: shifted right, peaked at h=7.

Equations

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

def TesslerGoodman2022.jockeyHeightWeight (h : Height) : ℕ

Height weight for jockeys: shifted left, peaked at h=3.

Equations

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

def TesslerGoodman2022.heightWeight (k : Kind) : Height → ℕ

Height weight for a given kind: P(h | k) (unnormalized).

Equations

• TesslerGoodman2022.heightWeight TesslerGoodman2022.Kind.person = TesslerGoodman2022.personHeightWeight
• TesslerGoodman2022.heightWeight TesslerGoodman2022.Kind.basketballPlayer = TesslerGoodman2022.basketballHeightWeight
• TesslerGoodman2022.heightWeight TesslerGoodman2022.Kind.jockey = TesslerGoodman2022.jockeyHeightWeight

def TesslerGoodman2022.l0HeightWeight (c : ComparisonClass) (k : Kind) : Height → ℕ

L0's height weight conditioned on comparison class. Subordinate uses the kind's own distribution; superordinate uses people.

Equations

• TesslerGoodman2022.l0HeightWeight TesslerGoodman2022.ComparisonClass.subordinate k = TesslerGoodman2022.heightWeight k
• TesslerGoodman2022.l0HeightWeight TesslerGoodman2022.ComparisonClass.superordinate k = TesslerGoodman2022.personHeightWeight

def TesslerGoodman2022.compClassWeight (_k : Kind) : ComparisonClass → ℕ

Comparison class prior weights: P(c | k) (unnormalized). Flat prior: subordinate and superordinate equally likely a priori. The qualitative polarity × expectations interaction emerges entirely from pragmatic reasoning about informativity, not from prior bias. (Paper Table 2: "Flat prior" model variant, r² = 0.136 for CC inference.)

Equations

• TesslerGoodman2022.compClassWeight _k x✝ = 1

def TesslerGoodman2022.thresholdCount (u : Utterance) (h : Height) : ℕ

Number of thresholds θ ∈ {0,...,9} satisfying ⟦u⟧(h,θ) = true.

For tall (positiveMeaning): |{θ : h > θ}| = h.toNat For short (negativeMeaning): |{θ : h < θ}| = 9 - h.toNat For silent: 10 (all thresholds pass)

Equations

• TesslerGoodman2022.thresholdCount TesslerGoodman2022.Utterance.tall h = Degree.Degree.toNat h
• TesslerGoodman2022.thresholdCount TesslerGoodman2022.Utterance.short h = 9 - Degree.Degree.toNat h
• TesslerGoodman2022.thresholdCount TesslerGoodman2022.Utterance.silent h = 10

theorem TesslerGoodman2022.thresholdCount_tall_eq_card (h : Height) : thresholdCount Utterance.tall h = {θ : Degree.Threshold 10 | Degree.positiveMeaning h θ}.card

Grounding: thresholdCount .tall equals the count of thresholds satisfying positiveMeaning.

theorem TesslerGoodman2022.thresholdCount_short_eq_card (h : Height) : thresholdCount Utterance.short h = {θ : Degree.Threshold 10 | Degree.negativeMeaning h θ}.card

Grounding: thresholdCount .short equals the count of thresholds satisfying negativeMeaning.

The model is [LG17]'s threshold RSA with the threshold θ marginalised analytically (into thresholdCount) and the comparison class c promoted to the Latent variable the listener infers:

L₀(x | u, c) ∝ P(x | c) · |{θ : ⟦u⟧(x, θ)}|         (`meaningE`, `L0k`)
S₁(u | x, c) ∝ L₀(x | u, c)  (α = 1, no cost)       (`Sk`)
L₁(x, c | u, k) ∝ S₁(u | x, c) · P(x | k) · P(c | k) (`listenerK`)

Sk is a total speaker (a dite wrapper over PMF.normalize): at heights with zero prior weight for a kind (basketball at h ∈ {0,1}, jockey at h ∈ {9,10}) every utterance has literal mass 0, so the softmax normaliser vanishes and no ViableSpeaker instance exists; the junk uniform branch there is harmless because those heights carry joint prior weight 0 in L1.

def TesslerGoodman2022.meaningE (k : Kind) (c : ComparisonClass) (u : Utterance) (h : Height) : ENNReal

Graded literal meaning P(h | c) · |{θ : ⟦u⟧(h, θ)}|, the ℕ product l0HeightWeight · thresholdCount cast to ℝ≥0∞.

Equations

• TesslerGoodman2022.meaningE k c u h = ↑(TesslerGoodman2022.l0HeightWeight c k h * TesslerGoodman2022.thresholdCount u h)

noncomputable def TesslerGoodman2022.L0k (k : Kind) (c : ComparisonClass) (u : Utterance) : PMF Height

Per-kind literal listener L₀(· | u, c) : PMF Height, uniform-in-θ meaning normalised over heights.

Equations

• TesslerGoodman2022.L0k k c u = RSA.L0OfMeaning (TesslerGoodman2022.meaningE k c) u ⋯ ⋯

theorem TesslerGoodman2022.L0_val (N D : ℕ) {k : Kind} {c : ComparisonClass} {u : Utterance} {h : Height} {q : ℝ} (hN : l0HeightWeight c k h * thresholdCount u h = N) (hD : ∑ h' : Height, l0HeightWeight c k h' * thresholdCount u h' = D) (hDpos : 0 < D) (hq : ↑N / ↑D = q) : (L0k k c u) h = ENNReal.ofReal q

L0 value: L₀(h | u, c) = P(h|c)·|{θ:⟦u⟧(h)}| / D_c(u), an exact ENNReal.ofReal rational.

noncomputable def TesslerGoodman2022.Sk (k : Kind) (s : Height × ComparisonClass) : PMF Utterance

Total speaker S₁(· | h, c) : PMF Utterance, the α = 1 softmax of the literal listener, guarded by a dite so it is defined even where the softmax normaliser vanishes (see the section note).

Equations

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

theorem TesslerGoodman2022.Sk_val {k : Kind} {c : ComparisonClass} {u : Utterance} {h : Height} {p z q : ℝ} (hp : (L0k k c u) h = ENNReal.ofReal p) (hZ : ∑' (u' : Utterance), (L0k k c u') h = ENNReal.ofReal z) (hppos : 0 ≤ p) (hz : 0 < z) (hq : p / z = q) : (Sk k (h, c)) u = ENNReal.ofReal q

Speaker value: S₁(u | h, c) = L₀(h | u, c) / Z(h, c), an exact ENNReal.ofReal rational.

def TesslerGoodman2022.jointW (k : Kind) (s : Height × ComparisonClass) : ENNReal

Unnormalised joint prior P(x | k) · P(c | k) — world prior is the kind's height distribution, latent (comparison-class) prior is flat, so the weight is P(x | k), independent of c.

Equations

• TesslerGoodman2022.jointW k s = ↑(TesslerGoodman2022.heightWeight k s.1)

noncomputable def TesslerGoodman2022.jointK (k : Kind) : PMF (Height × ComparisonClass)

The listener's joint prior over Height × ComparisonClass.

Equations

• TesslerGoodman2022.jointK k = PMF.normalize (TesslerGoodman2022.jointW k) ⋯ ⋯

theorem TesslerGoodman2022.margK (k : Kind) (u : Utterance) : PMF.marginal (Sk k) (jointK k) u ≠ 0

The listener marginal is non-zero for every kind and utterance: at (deg 5, subordinate) the joint prior and the literal listener are both positive (all height weights and threshold counts are non-zero at h = 5).

noncomputable def TesslerGoodman2022.listenerK (k : Kind) (u : Utterance) : PMF (Height × ComparisonClass)

The pragmatic listener L₁(x, c | u, k) : PMF (Height × ComparisonClass).

Equations

• TesslerGoodman2022.listenerK k u = RSA.Canonical.L1 (TesslerGoodman2022.Sk k) (TesslerGoodman2022.jointK k) u ⋯

The per-(kind, class, height) literal-listener values L₀, speaker normalisers Z, and speaker masses S₁ below are exact ENNReal.ofReal rationals, verified by decide (integer denominators) and norm_num (rational arithmetic). They feed the endorsement comparisons (§ 6) and the pooled listener sums (§ 8).

Bball literal listener, normaliser, and speaker values

Jockey literal listener, normaliser, and speaker values

Each listener latent comparison reduces (listener_snd_lt) to these prior-weighted pooled speaker sums, one per (kind, utterance, class).

theorem TesslerGoodman2022.basketball_expected_taller_than_person : ∑ h : Height, basketballHeightWeight h * Degree.Degree.toNat h > ∑ h : Height, personHeightWeight h * Degree.Degree.toNat h

Basketball players' weighted height sum exceeds the person mean: Σ P(h|bball)·h = 568 > 430 = Σ P(h|person)·h (unnormalized).

theorem TesslerGoodman2022.jockey_expected_shorter_than_person : ∑ h : Height, jockeyHeightWeight h * Degree.Degree.toNat h < ∑ h : Height, personHeightWeight h * Degree.Degree.toNat h

Jockeys' weighted height sum is below the person mean.

theorem TesslerGoodman2022.person_classes_identical (h : Height) : l0HeightWeight ComparisonClass.subordinate Kind.person h = l0HeightWeight ComparisonClass.superordinate Kind.person h

For person, subordinate and superordinate use the same height distribution, so comparison class makes no difference.

theorem TesslerGoodman2022.silent_no_cc_preference : (listenerK Kind.person Utterance.silent).snd ComparisonClass.subordinate = (listenerK Kind.person Utterance.silent).snd ComparisonClass.superordinate

Sanity check: silence doesn't discriminate between comparison classes.

For the person kind (where subordinate = superordinate by person_classes_identical), L1 hearing silence assigns equal posterior to both comparison classes. This confirms the model's baseline: only informative utterances (tall/short) shift CC inference.

Basketball Player (expected tall)

At height 6 (above person mean 5, below basketball mean ~6.8):

• Under superordinate (people): "tall" IS endorsed (h=6 > E[person]=5)
• Under subordinate (basketball): "tall" NOT endorsed (h=6 < E[basketball]≈6.8)

At height 5 (at person mean, well below basketball mean):

• Under subordinate (basketball): "short" IS endorsed
• Under superordinate (people): "short" NOT endorsed (h=5 ≈ E[person]=5)

theorem TesslerGoodman2022.basketball_tall_endorsed_super : (Sk Kind.basketballPlayer (Degree.deg 6 ⋯, ComparisonClass.superordinate)) Utterance.tall > (Sk Kind.basketballPlayer (Degree.deg 6 ⋯, ComparisonClass.superordinate)) Utterance.silent

"Tall" endorsed under superordinate at h=6: a basketball player of height 6 is tall for a person (6 > person mean = 5).

theorem TesslerGoodman2022.basketball_tall_not_endorsed_sub : ¬(Sk Kind.basketballPlayer (Degree.deg 6 ⋯, ComparisonClass.subordinate)) Utterance.tall > (Sk Kind.basketballPlayer (Degree.deg 6 ⋯, ComparisonClass.subordinate)) Utterance.silent

"Tall" NOT endorsed under subordinate at h=6: a basketball player of height 6 is average for a basketball player (6 < basketball mean ≈ 6.8).

theorem TesslerGoodman2022.basketball_short_endorsed_sub : (Sk Kind.basketballPlayer (Degree.deg 5 ⋯, ComparisonClass.subordinate)) Utterance.short > (Sk Kind.basketballPlayer (Degree.deg 5 ⋯, ComparisonClass.subordinate)) Utterance.silent

"Short" endorsed under subordinate at h=5: height 5 is well below the basketball mean, so "short" is informative within basketball players.

theorem TesslerGoodman2022.basketball_short_not_endorsed_super : ¬(Sk Kind.basketballPlayer (Degree.deg 5 ⋯, ComparisonClass.superordinate)) Utterance.short > (Sk Kind.basketballPlayer (Degree.deg 5 ⋯, ComparisonClass.superordinate)) Utterance.silent

"Short" NOT endorsed under superordinate at h=5: height 5 is exactly the person mean, so "short" is uninformative relative to people.

Jockey (expected short)

At height 4 (below person mean 5, above jockey mean ~3.2):

• Under subordinate (jockeys): "tall" IS endorsed (h=4 > E[jockey]≈3.2)
• Under superordinate (people): "tall" NOT endorsed (h=4 < E[person]=5)
• Under superordinate (people): "short" IS endorsed (h=4 < E[person]=5)
• Under subordinate (jockeys): "short" NOT endorsed (h=4 > E[jockey]≈3.2)

theorem TesslerGoodman2022.jockey_tall_endorsed_sub : (Sk Kind.jockey (Degree.deg 4 ⋯, ComparisonClass.subordinate)) Utterance.tall > (Sk Kind.jockey (Degree.deg 4 ⋯, ComparisonClass.subordinate)) Utterance.silent

"Tall" endorsed under subordinate at h=4: a jockey of height 4 is tall for a jockey (4 > jockey mean ≈ 3.2).

theorem TesslerGoodman2022.jockey_tall_not_endorsed_super : ¬(Sk Kind.jockey (Degree.deg 4 ⋯, ComparisonClass.superordinate)) Utterance.tall > (Sk Kind.jockey (Degree.deg 4 ⋯, ComparisonClass.superordinate)) Utterance.silent

"Tall" NOT endorsed under superordinate at h=4: height 4 is below the person mean, so "tall" is uninformative relative to people.

theorem TesslerGoodman2022.jockey_short_endorsed_super : (Sk Kind.jockey (Degree.deg 4 ⋯, ComparisonClass.superordinate)) Utterance.short > (Sk Kind.jockey (Degree.deg 4 ⋯, ComparisonClass.superordinate)) Utterance.silent

"Short" endorsed under superordinate at h=4: height 4 is below the person mean (4 < E[person]=5).

theorem TesslerGoodman2022.jockey_short_not_endorsed_sub : ¬(Sk Kind.jockey (Degree.deg 4 ⋯, ComparisonClass.subordinate)) Utterance.short > (Sk Kind.jockey (Degree.deg 4 ⋯, ComparisonClass.subordinate)) Utterance.silent

"Short" NOT endorsed under subordinate at h=4: a jockey of height 4 is average for a jockey, so "short" is uninformative.

This model extends [LG17]'s threshold RSA. The key structural relationship:

• LG2017 treats the threshold θ as a Latent variable (L1 infers θ)
• TG2022 marginalizes θ analytically (via thresholdCount) and adds comparison class c as the Latent variable (L1 infers c)

The height priors used here (personHeightWeight, basketballHeightWeight) match [LG17]'s general-population and basketball-player priors respectively — same empirical domain, different question. The cross-paper compatibility was previously enforced via personWeight_eq_lassiterGoodman / basketballWeight_eq_lassiterGoodman bridge theorems referencing RSA.LassiterGoodman2017.heightPrior; those were removed when L&G's old bundled-config formalisation was retired. The PMF formalisation (LassiterGoodman2017PMF.lean) does not duplicate the empirical priors.

The paper's main prediction: L1 comparison class inference

The S1 endorsement theorems (§ 6) show that S1 behaves differently under each comparison class. The paper's Eq. 1 prediction is about the LISTENER: after hearing an adjective about a kind, which comparison class does L1 infer?

L₁(x, c | u, k) ∝ S₁(u | x, c) · P(x | k) · P(c | k)

After marginalizing over height x, the posterior over comparison classes is (listenerK k u).snd. The polarity × expectations interaction:

• Expected adjective (tall basketball, short jockey) → superordinate
• Unexpected adjective (short basketball, tall jockey) → subordinate

theorem TesslerGoodman2022.basketball_tall_infers_super : (listenerK Kind.basketballPlayer Utterance.tall).snd ComparisonClass.superordinate > (listenerK Kind.basketballPlayer Utterance.tall).snd ComparisonClass.subordinate

Basketball + "tall" → listener infers superordinate: a basketball player described as "tall" is tall even for a person — unexpected, hence informative under the superordinate comparison class.

theorem TesslerGoodman2022.basketball_short_infers_sub : (listenerK Kind.basketballPlayer Utterance.short).snd ComparisonClass.subordinate > (listenerK Kind.basketballPlayer Utterance.short).snd ComparisonClass.superordinate

Basketball + "short" → listener infers subordinate: "short for a basketball player" is more informative than "short for a person" (since basketball players are expected to be tall).

theorem TesslerGoodman2022.jockey_tall_infers_sub : (listenerK Kind.jockey Utterance.tall).snd ComparisonClass.subordinate > (listenerK Kind.jockey Utterance.tall).snd ComparisonClass.superordinate

Jockey + "tall" → listener infers subordinate: "tall for a jockey" is more informative than "tall for a person" (since jockeys are expected to be short).

theorem TesslerGoodman2022.jockey_short_infers_super : (listenerK Kind.jockey Utterance.short).snd ComparisonClass.superordinate > (listenerK Kind.jockey Utterance.short).snd ComparisonClass.subordinate

Jockey + "short" → listener infers superordinate: a jockey described as "short" is short even for a person — unexpected, hence informative under the superordinate comparison class.

The polarity × expectations interaction from §§ 6, 8 grounds the rows in Data/Examples/TesslerGoodman2022.json (§3.2.1, Fig. 3): in every row, the EXPECTED adjective (consistent with the kind's height distribution) is attested with SUPERORDINATE comparison and the UNEXPECTED adjective with SUBORDINATE comparison. L1_matches_all_rows replicates the paper's Eq. 1 prediction for each row.

def TesslerGoodman2022.kindOf (row : Data.Examples.LinguisticExample) : Option Kind

Kind adapter: the row's noun feature as a Kind.

Equations

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

def TesslerGoodman2022.uttOf (row : Data.Examples.LinguisticExample) : Option Utterance

Utterance adapter: the row's adjective feature as an Utterance.

Equations

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

def TesslerGoodman2022.ccOf (row : Data.Examples.LinguisticExample) : Option ComparisonClass

Comparison-class adapter: the row's attested inferred_class feature.

Equations

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

def TesslerGoodman2022.ComparisonClass.flip : ComparisonClass → ComparisonClass

The alternative comparison class.

Equations

• TesslerGoodman2022.ComparisonClass.subordinate.flip = TesslerGoodman2022.ComparisonClass.superordinate
• TesslerGoodman2022.ComparisonClass.superordinate.flip = TesslerGoodman2022.ComparisonClass.subordinate

def TesslerGoodman2022.L1Matches (row : Data.Examples.LinguisticExample) : Prop

The pragmatic listener prefers the row's attested comparison class over the alternative (vacuous when a row lacks the adapter features).

Equations

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

theorem TesslerGoodman2022.L1_matches_all_rows (row : Data.Examples.LinguisticExample) : row ∈ Examples.all → L1Matches row

Transfer theorem (Eq. 1, Fig. 3): on every row, L1's posterior prefers the attested comparison class.

The literal model makes the OPPOSITE predictions

[TG22] §2 contrasts the pragmatic listener (Eq. 1) with an alternative literal listener (Eq. 6) that does not reason about a rational speaker:

L₀(x, θ, c | u, k) ∝ δ_{⟦u⟧}(x,θ) · P(x | c) · P(θ) · P(c | k)

This model updates beliefs about x and c jointly via the literal meaning, using the comparison-class-specific prior P(x | c), but without S1 informativity. It effectively asks: under which comparison class is the utterance more likely to be literally true? For "tall basketball player," tallness is more probable under the basketball distribution (shifted right), so the literal model prefers subordinate — the OPPOSITE of the pragmatic model and the data.

The pragmatic model inverts this because S1 normalizes by the total literal-listener mass Z_c(u), penalizing classes where the utterance is uninformative (too many heights satisfy it) and rewarding classes where the utterance is surprising.

def TesslerGoodman2022.literalClassScore (k : Kind) (c : ComparisonClass) (u : Utterance) : ℕ

Unnormalized literal score: Σ_h P(h|c) · |{θ : ⟦u⟧(h,θ)}|. Total literal-listener mass for comparison class c, marginalized over heights and thresholds.

Equations

• TesslerGoodman2022.literalClassScore k c u = ∑ h : TesslerGoodman2022.Height, TesslerGoodman2022.l0HeightWeight c k h * TesslerGoodman2022.thresholdCount u h

theorem TesslerGoodman2022.literal_basketball_tall_sub : literalClassScore Kind.basketballPlayer ComparisonClass.subordinate Utterance.tall > literalClassScore Kind.basketballPlayer ComparisonClass.superordinate Utterance.tall

Literal: basketball + "tall" → subordinate. Basketball players' rightward-shifted heights make "tall" more often literally true under subordinate comparison. Opposite of pragmatic basketball_tall_infers_super.

theorem TesslerGoodman2022.literal_basketball_short_super : literalClassScore Kind.basketballPlayer ComparisonClass.superordinate Utterance.short > literalClassScore Kind.basketballPlayer ComparisonClass.subordinate Utterance.short

Literal: basketball + "short" → superordinate. Opposite of pragmatic basketball_short_infers_sub.

theorem TesslerGoodman2022.literal_jockey_tall_super : literalClassScore Kind.jockey ComparisonClass.superordinate Utterance.tall > literalClassScore Kind.jockey ComparisonClass.subordinate Utterance.tall

Literal: jockey + "tall" → superordinate. Opposite of pragmatic jockey_tall_infers_sub.

theorem TesslerGoodman2022.literal_jockey_short_sub : literalClassScore Kind.jockey ComparisonClass.subordinate Utterance.short > literalClassScore Kind.jockey ComparisonClass.superordinate Utterance.short

Literal: jockey + "short" → subordinate. Opposite of pragmatic jockey_short_infers_super.

theorem TesslerGoodman2022.pragmatic_reverses_literal : (listenerK Kind.basketballPlayer Utterance.tall).snd ComparisonClass.superordinate > (listenerK Kind.basketballPlayer Utterance.tall).snd ComparisonClass.subordinate ∧ (listenerK Kind.basketballPlayer Utterance.short).snd ComparisonClass.subordinate > (listenerK Kind.basketballPlayer Utterance.short).snd ComparisonClass.superordinate ∧ (listenerK Kind.jockey Utterance.tall).snd ComparisonClass.subordinate > (listenerK Kind.jockey Utterance.tall).snd ComparisonClass.superordinate ∧ (listenerK Kind.jockey Utterance.short).snd ComparisonClass.superordinate > (listenerK Kind.jockey Utterance.short).snd ComparisonClass.subordinate

Every literal prediction is reversed by the pragmatic model (Fig. 2). This is the paper's key scientific claim: comparison class inference requires social reasoning via S1, not just Bayesian updating on literal truth conditions.

The paper's title example uses temperature, not height. The model is dimension-general: any relative gradable adjective whose comparison class shifts the degree prior produces the polarity × expectations interaction.

The temperature domain maps onto the height domain:

• Winter (expected cold) ↔ Jockey (expected short): prior peaked at 3
• Summer (expected warm) ↔ Basketball (expected tall): prior peaked at 7
• warm ↔ tall (positive adjective), cold ↔ short (negative adjective)

Since the weight functions are identical, the § 8 predictions transfer:

Context	Adjective	Inferred CC	Height analogue
winter	warm	subordinate	jockey_tall_infers_sub
winter	cold	superordinate	jockey_short_infers_super
summer	warm	superordinate	basketball_tall_infers_super
summer	cold	subordinate	basketball_short_infers_sub

This connects to Semantics.Gradability.Dimension.temperature: temperature adjectives (warm/cold) are open-scale relative gradable adjectives, so — like tall — they require a comparison class (open_scale_requires_cc_inference; [Ken07]).

theorem TesslerGoodman2022.literal_reversal_transfers_to_temp : literalClassScore Kind.jockey ComparisonClass.superordinate Utterance.tall > literalClassScore Kind.jockey ComparisonClass.subordinate Utterance.tall ∧ (listenerK Kind.jockey Utterance.tall).snd ComparisonClass.subordinate > (listenerK Kind.jockey Utterance.tall).snd ComparisonClass.superordinate

The literal/pragmatic reversal transfers to temperature via the winter ↔ jockey mapping. The literal model predicts "warm in winter" → superordinate (warm is more often literally true in the general population than in winter), but the pragmatic model correctly predicts subordinate: "warm for winter" is informative within the season.

Why this model applies to "tall" but not "full"

[Ken07]'s Interpretive Economy (§4.3, p. 36) determines the standard of comparison from scale structure. For open-scale (relative) adjectives like "tall", the standard-fixing function s requires contextual domain information — "the distribution of objects in some domain (a comparison class)" (p. 42). For closed-scale (absolute) adjectives like "full", the standard is the scale endpoint — fixed regardless of context.

Crucially, Kennedy argues (§2.3, p. 16) that the comparison class is NOT a semantic argument of pos (contra [Kle80]), but rather contextual information that feeds into s. [TG22] provides the computational mechanism for determining this contextual parameter: the comparison class is inferred pragmatically via RSA as a latent variable. This is architecturally compatible with Kennedy's view — the CC is pragmatic/contextual, not a constituent of the logical form.

open scale → contextual standard → CC feeds into s → L1 infers it
bounded scale → endpoint standard → s fixed by scale → nothing to infer

The chain connects three independent modules:

1. Degree.interpretiveEconomy (Theory: scale → standard type)
2. Degree.PositiveStandard.RequiresComparisonClass (Theory: standard → domain-dependent?)
3. listenerK with latent ComparisonClass (this file: infer CC)

theorem TesslerGoodman2022.height_is_classA : Degree.IsClassA Core.Order.Boundedness.open_

Height is an open-scale dimension: "tall" is relative (Class A).

theorem TesslerGoodman2022.open_scale_requires_cc_inference : (Degree.interpretiveEconomy Core.Order.Boundedness.open_).RequiresComparisonClass

Open scale → contextual domain inference applies (the full chain). This is a three-step argument:

1. "tall" has an open scale (lexical fact)
2. Open scale → contextual standard via s (Interpretive Economy)
3. Contextual s → needs domain information (Kennedy 2007, p. 42) Therefore the domain (descriptively: comparison class) must be inferred — exactly what listenerK models with latent ComparisonClass. This is compatible with Kennedy's view: the CC is pragmatic/contextual (inferred by L1), not a semantic argument of pos.

theorem TesslerGoodman2022.closed_scale_no_cc_inference : ¬(Degree.interpretiveEconomy Core.Order.Boundedness.closed).RequiresComparisonClass

Closed scale → contextual domain inference is irrelevant. "Full" has an endpoint standard via Interpretive Economy; the threshold is the scale maximum regardless of context. No domain to infer.

Threshold semantics for gradable adjectives generalizes to generic language: "Birds fly south in the winter" ≈ P(x flies south | x is a bird) > θ ([TG19]). Both models share:

1. A threshold variable θ setting the standard
2. A prior P(x | c) conditioned on category membership
3. Pragmatic inference about the contextually appropriate threshold/class

The comparison class model (this file) infers which c maximizes the pragmatic listener's posterior. The generics model infers which θ is pragmatically optimal. Same RSA machinery applied to different latent variables.

The comparison class hierarchy is structurally a DDRP: subordinate (restricted) ⊆ superordinate (unrestricted). Going from subordinate to superordinate widens the reference population.

This connects comparison class inference to the same nesting pattern used by [RS24a]'s domain restriction possibilities.

@[implicit_reducible]

instance TesslerGoodman2022.instLinearOrderComparisonClass : LinearOrder ComparisonClass

Equations

• TesslerGoodman2022.instLinearOrderComparisonClass = LinearOrder.lift' TesslerGoodman2022.ComparisonClass.toFin✝ TesslerGoodman2022.ComparisonClass.toFin_injective✝

@[implicit_reducible]

instance TesslerGoodman2022.instOrderTopComparisonClass : OrderTop ComparisonClass

Equations

• TesslerGoodman2022.instOrderTopComparisonClass = { top := TesslerGoodman2022.ComparisonClass.superordinate, le_top := TesslerGoodman2022.instOrderTopComparisonClass._proof_1 }

def TesslerGoodman2022.isTypical (k : Kind) (h : Height) : Bool

Whether a height has nonzero prior weight for a given kind.

Equations

• TesslerGoodman2022.isTypical k h = decide (TesslerGoodman2022.heightWeight k h > 0)

def TesslerGoodman2022.compClassRestriction (k : Kind) : Quantification.DomainRestriction.DDRP ComparisonClass Height

The comparison class hierarchy as a nested restriction on heights.

Equations

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

theorem TesslerGoodman2022.compClass_nesting (k : Kind) (h : Height) : h ∈ (compClassRestriction k).region ComparisonClass.subordinate → h ∈ (compClassRestriction k).region ComparisonClass.superordinate

Nesting: subordinate ⊆ superordinate for all kinds.