@cite{nouwen-2024} Deadjectival Intensifiers

@cite{lassiter-goodman-2017} @cite{nouwen-2024}

"The semantics and probabilistic pragmatics of deadjectival intensifiers" Semantics and Pragmatics, Volume 17, Article 2.

Empirical Generalizations

1. Goldilocks effect: Negative-evaluative bases (horrible, terrible) yield high-degree intensifiers; positive-evaluative bases (pleasant, nice) yield moderate-degree intensifiers.

2. Zwicky's generalization: Modal adjectives with negative polarity (unusual, surprising, impossible) can intensify, but their positive counterparts (usual, expected, possible) cannot.

RSA Model

Extends @cite{lassiter-goodman-2017} threshold RSA with evaluative measures: deadjectival adverbs (horribly, pleasantly) derive their degree function from the evaluative meaning of their adjectival base.

Two-Threshold Simultaneous Model

P_L1(h, θ, θ_e | u) ∝ P_S1(u | h, θ, θ_e) × P(h) × P(θ) × P(θ_e)

The listener jointly infers height h, adjective threshold θ, and evaluative threshold θ_e. The meaning function is an intersection:

• bare_warm: h > θ
• horribly_warm: (h > θ) ∧ (μ_horrible(h) > θ_e)
• pleasantly_warm: (h > θ) ∧ (μ_pleasant(h) > θ_e)
• silent: ⊤

Sequential Model (@cite{nouwen-2024}'s key innovation)

The evaluative adverb updates the prior before the adjective threshold applies: Step 1 infers P₁(h | "horribly"), Step 2 infers P₂(h | "warm") using P₁ as prior.

RSAConfig Mapping

• U = Utterance (bare_warm, horribly_warm, pleasantly_warm, silent)
• W = Height (Degree 6, 7 values: h0–h6)
• Latent = Threshold × Threshold (36 values: θ_adj × θ_eval)
• s1Score = beliefAction: exp(α · (log L0 − C(u)))
• α = 4 (matching @cite{lassiter-goodman-2017})
• C(bare) = 1, C(horribly/pleasantly) = 2, C(∅) = 0

Performance Note

Uses scale n=6 (7 heights, 6 thresholds) rather than the paper's continuous distribution or @cite{lassiter-goodman-2017}'s n=10, giving 4.4× fewer L0 cells in the simultaneous model (1008 vs 4400) and 2.6× fewer in the sequential model. All qualitative Goldilocks predictions are preserved.

inductive Phenomena.Gradability.Intensifiers.IntensifierClass : Type

Intensifier degree class (Figure 2).

• H (high): targets extreme degrees ("horribly warm" ≈ very warm)
• M (moderate): targets moderate degrees ("pleasantly warm" ≈ nicely warm)

• H : IntensifierClass
• M : IntensifierClass

instance Phenomena.Gradability.Intensifiers.instReprIntensifierClass : Repr IntensifierClass

Equations

• Phenomena.Gradability.Intensifiers.instReprIntensifierClass = { reprPrec := Phenomena.Gradability.Intensifiers.instReprIntensifierClass.repr }

def Phenomena.Gradability.Intensifiers.instReprIntensifierClass.repr : IntensifierClass → ℕ → Std.Format

Equations

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

instance Phenomena.Gradability.Intensifiers.instDecidableEqIntensifierClass : DecidableEq IntensifierClass

Equations

• Phenomena.Gradability.Intensifiers.instDecidableEqIntensifierClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Gradability.Intensifiers.instBEqIntensifierClass : BEq IntensifierClass

Equations

• Phenomena.Gradability.Intensifiers.instBEqIntensifierClass = { beq := Phenomena.Gradability.Intensifiers.instBEqIntensifierClass.beq }

def Phenomena.Gradability.Intensifiers.instBEqIntensifierClass.beq : IntensifierClass → IntensifierClass → Bool

Equations

• Phenomena.Gradability.Intensifiers.instBEqIntensifierClass.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure Phenomena.Gradability.Intensifiers.IntensifierEntry : Type

A deadjectival intensifier entry.

Records the adverb form, its adjectival base, evaluative properties, modal status, and attestation pattern.

• adverb : String

  Adverb form

• adjBase : String

  Adjectival base

• valence : Semantics.Lexical.Adjective.Intensification.EvaluativeValence

  Evaluative valence of the base

• class_ : IntensifierClass

  Degree class as intensifier

• isModal : Bool

  Whether the base is a modal adjective

• modalPolarity : Option Semantics.Lexical.Adjective.Intensification.EvaluativeValence

  For modal bases: polarity of the modal (negative = unlikely/impossible)

• bleached : Bool

  Whether the evaluative content is bleached in adverbial use

• attested : Bool

  Whether the intensifier use is attested

def Phenomena.Gradability.Intensifiers.instReprIntensifierEntry.repr : IntensifierEntry → ℕ → Std.Format

Equations

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

instance Phenomena.Gradability.Intensifiers.instReprIntensifierEntry : Repr IntensifierEntry

Equations

• Phenomena.Gradability.Intensifiers.instReprIntensifierEntry = { reprPrec := Phenomena.Gradability.Intensifiers.instReprIntensifierEntry.repr }

def Phenomena.Gradability.Intensifiers.horribly : IntensifierEntry

Equations

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

def Phenomena.Gradability.Intensifiers.terribly : IntensifierEntry

Equations

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

def Phenomena.Gradability.Intensifiers.awfully : IntensifierEntry

Equations

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

def Phenomena.Gradability.Intensifiers.dreadfully : IntensifierEntry

Equations

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

def Phenomena.Gradability.Intensifiers.frighteningly : IntensifierEntry

Equations

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

def Phenomena.Gradability.Intensifiers.pleasantly : IntensifierEntry

Equations

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

def Phenomena.Gradability.Intensifiers.nicely : IntensifierEntry

Equations

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

def Phenomena.Gradability.Intensifiers.decently : IntensifierEntry

Equations

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

def Phenomena.Gradability.Intensifiers.unusually : IntensifierEntry

Equations

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

def Phenomena.Gradability.Intensifiers.surprisingly : IntensifierEntry

Equations

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

def Phenomena.Gradability.Intensifiers.impossibly : IntensifierEntry

Equations

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

def Phenomena.Gradability.Intensifiers.remarkably : IntensifierEntry

Equations

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

def Phenomena.Gradability.Intensifiers.usually_ : IntensifierEntry

Equations

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

def Phenomena.Gradability.Intensifiers.expectedly_ : IntensifierEntry

Equations

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

def Phenomena.Gradability.Intensifiers.possibly_ : IntensifierEntry

Equations

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

def Phenomena.Gradability.Intensifiers.allEntries : List IntensifierEntry

Equations

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

def Phenomena.Gradability.Intensifiers.goldilocksHolds (e : IntensifierEntry) : Bool

The Goldilocks effect: evaluative valence determines degree class.

• Negative-evaluative bases yield high-degree (H) intensifiers
• Positive-evaluative bases yield moderate-degree (M) intensifiers

Equations

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

theorem Phenomena.Gradability.Intensifiers.horribly_goldilocks : goldilocksHolds horribly = true

theorem Phenomena.Gradability.Intensifiers.terribly_goldilocks : goldilocksHolds terribly = true

theorem Phenomena.Gradability.Intensifiers.awfully_goldilocks : goldilocksHolds awfully = true

theorem Phenomena.Gradability.Intensifiers.dreadfully_goldilocks : goldilocksHolds dreadfully = true

theorem Phenomena.Gradability.Intensifiers.frighteningly_goldilocks : goldilocksHolds frighteningly = true

theorem Phenomena.Gradability.Intensifiers.pleasantly_goldilocks : goldilocksHolds pleasantly = true

theorem Phenomena.Gradability.Intensifiers.nicely_goldilocks : goldilocksHolds nicely = true

theorem Phenomena.Gradability.Intensifiers.decently_goldilocks : goldilocksHolds decently = true

def Phenomena.Gradability.Intensifiers.zwickyHolds (e : IntensifierEntry) : Bool

Zwicky's generalization: modal adjectives with negative polarity can serve as intensifiers; positive-polarity modal adjectives cannot.

• "unusually warm" ✓ (negative modal → attested)
• "*usually warm" ✗ (positive modal → unattested)

Equations

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

theorem Phenomena.Gradability.Intensifiers.unusually_zwicky : zwickyHolds unusually = true

theorem Phenomena.Gradability.Intensifiers.surprisingly_zwicky : zwickyHolds surprisingly = true

theorem Phenomena.Gradability.Intensifiers.impossibly_zwicky : zwickyHolds impossibly = true

theorem Phenomena.Gradability.Intensifiers.remarkably_zwicky : zwickyHolds remarkably = true

theorem Phenomena.Gradability.Intensifiers.usually_zwicky : zwickyHolds usually_ = true

theorem Phenomena.Gradability.Intensifiers.expectedly_zwicky : zwickyHolds expectedly_ = true

theorem Phenomena.Gradability.Intensifiers.possibly_zwicky : zwickyHolds possibly_ = true

def Phenomena.Gradability.Intensifiers.attestedCount : ℕ

Count of attested intensifiers

Equations

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

def Phenomena.Gradability.Intensifiers.unattestedCount : ℕ

Count of unattested intensifiers

Equations

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

instance RSA.Nouwen2024.instNeZeroNatOfNat_linglib : NeZero 6

@[reducible, inline]

abbrev RSA.Nouwen2024.Height : Type

Equations

• RSA.Nouwen2024.Height = Core.Scale.Degree 6

@[reducible, inline]

abbrev RSA.Nouwen2024.Threshold : Type

Equations

• RSA.Nouwen2024.Threshold = Core.Scale.Threshold 6

def RSA.Nouwen2024.tallMeaning (θ : Threshold) (h : Height) : Bool

⟦tall⟧(θ)(x) = 1 iff height(x) > θ, specialized to scale 6.

Equations

• RSA.Nouwen2024.tallMeaning θ h = Semantics.Degree.positiveMeaning h θ

def RSA.Nouwen2024.heightPrior (h : Height) : ℚ

Height prior: discretized bell curve centered at h3 (norm for scale 6). Weights: [1, 5, 10, 20, 10, 5, 1] (sum = 52).

Equations

• RSA.Nouwen2024.heightPrior h = match Core.Scale.Degree.toNat h with | 0 => 1 | 1 => 5 | 2 => 10 | 3 => 20 | 4 => 10 | 5 => 5 | x => 1

noncomputable def RSA.Nouwen2024.heightPriorR (h : Height) : ℝ

Equations

• RSA.Nouwen2024.heightPriorR h = ↑(RSA.Nouwen2024.heightPrior h)

theorem RSA.Nouwen2024.heightPriorR_nonneg (h : Height) : 0 ≤ heightPriorR h

inductive RSA.Nouwen2024.Utterance : Type

Utterances about warmth with optional deadjectival intensifier.

The utterance set extends bare "warm" with intensified variants.

• bare_warm : Utterance
• horribly_warm : Utterance
• pleasantly_warm : Utterance
• silent : Utterance

instance RSA.Nouwen2024.instReprUtterance : Repr Utterance

Equations

• RSA.Nouwen2024.instReprUtterance = { reprPrec := RSA.Nouwen2024.instReprUtterance.repr }

def RSA.Nouwen2024.instReprUtterance.repr : Utterance → ℕ → Std.Format

Equations

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

instance RSA.Nouwen2024.instDecidableEqUtterance : DecidableEq Utterance

Equations

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

instance RSA.Nouwen2024.instBEqUtterance : BEq Utterance

Equations

• RSA.Nouwen2024.instBEqUtterance = { beq := RSA.Nouwen2024.instBEqUtterance.beq }

def RSA.Nouwen2024.instBEqUtterance.beq : Utterance → Utterance → Bool

Equations

• RSA.Nouwen2024.instBEqUtterance.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance RSA.Nouwen2024.instFintypeUtterance : Fintype Utterance

Equations

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

def RSA.Nouwen2024.allUtterances : List Utterance

Equations

• RSA.Nouwen2024.allUtterances = [RSA.Nouwen2024.Utterance.bare_warm, RSA.Nouwen2024.Utterance.horribly_warm, RSA.Nouwen2024.Utterance.pleasantly_warm, RSA.Nouwen2024.Utterance.silent]

def RSA.Nouwen2024.muHorrible (h : Height) : ℕ

Evaluative measure for "horrible" applied to the Height domain.

μ_horrible(h) = |h - norm|

Heights far from the norm (3) are evaluated as more "horrible". Agrees with Intensification.muHorrible 6 (see meaning_grounded_horribly).

Equations

• RSA.Nouwen2024.muHorrible h = if Core.Scale.Degree.toNat h ≥ 3 then Core.Scale.Degree.toNat h - 3 else 3 - Core.Scale.Degree.toNat h

def RSA.Nouwen2024.muPleasant (h : Height) : ℕ

Evaluative measure for "pleasant" applied to the Height domain.

μ_pleasant(h) = norm - |h - norm|

Heights near the norm (3) are evaluated as more "pleasant". Agrees with Intensification.muPleasant 6 (see meaning_grounded_pleasantly).

Equations

• RSA.Nouwen2024.muPleasant h = if Core.Scale.Degree.toNat h ≥ 3 then 6 - Core.Scale.Degree.toNat h else Core.Scale.Degree.toNat h

def RSA.Nouwen2024.meaning (u : Utterance) (h : Height) (θ θ_e : Threshold) : Bool

Full meaning function.

• bare_warm: h > θ (standard @cite{lassiter-goodman-2017})
• horribly_warm: (h > θ) ∧ (μ_horrible(h) > θ_e)
• pleasantly_warm: (h > θ) ∧ (μ_pleasant(h) > θ_e)
• silent: always true

Equations

• RSA.Nouwen2024.meaning RSA.Nouwen2024.Utterance.bare_warm h θ θ_e = RSA.Nouwen2024.tallMeaning θ h
• RSA.Nouwen2024.meaning RSA.Nouwen2024.Utterance.horribly_warm h θ θ_e = (RSA.Nouwen2024.tallMeaning θ h && decide (RSA.Nouwen2024.muHorrible h > Core.Scale.Threshold.toNat θ_e))
• RSA.Nouwen2024.meaning RSA.Nouwen2024.Utterance.pleasantly_warm h θ θ_e = (RSA.Nouwen2024.tallMeaning θ h && decide (RSA.Nouwen2024.muPleasant h > Core.Scale.Threshold.toNat θ_e))
• RSA.Nouwen2024.meaning RSA.Nouwen2024.Utterance.silent h θ θ_e = true

theorem RSA.Nouwen2024.meaning_grounded_horribly (h : Height) (θ θ_e : Threshold) : meaning Utterance.horribly_warm h θ θ_e = Semantics.Lexical.Adjective.Intensification.intensifiedMeaning (Semantics.Lexical.Adjective.Intensification.muHorrible 6) h θ θ_e

The local horribly_warm meaning agrees with theory-layer intensifiedMeaning for all inputs. This bridges the ℕ-valued local measures to the ℚ-valued theory-layer Intensification.muHorrible.

theorem RSA.Nouwen2024.meaning_grounded_pleasantly (h : Height) (θ θ_e : Threshold) : meaning Utterance.pleasantly_warm h θ θ_e = Semantics.Lexical.Adjective.Intensification.intensifiedMeaning (Semantics.Lexical.Adjective.Intensification.muPleasant 6) h θ θ_e

The local pleasantly_warm meaning agrees with theory-layer intensifiedMeaning for all inputs. This bridges the ℕ-valued local measures to the ℚ-valued theory-layer Intensification.muPleasant.

def RSA.Nouwen2024.muUsual : Semantics.Lexical.Adjective.Intensification.EvaluativeMeasure 6

Constant evaluative measure (no evaluative content).

Models adverbs like "*usually" — a constant measure provides no discriminating information about degree, which is why "*usually warm" is vacuous (Zwicky's generalization).

Equations

• RSA.Nouwen2024.muUsual = { form := "usual", valence := Semantics.Lexical.Adjective.Intensification.EvaluativeValence.neutral, mu := fun (x : ℕ) => 3 }

theorem RSA.Nouwen2024.usual_constant (h₁ h₂ : Height) : muUsual.mu (Core.Scale.Degree.toNat h₁) = muUsual.mu (Core.Scale.Degree.toNat h₂)

A constant evaluative measure provides no information: for any two heights, the measure value is identical.

def RSA.Nouwen2024.utteranceCost : Utterance → ℚ

Intensified utterances are costlier than bare utterances.

assumes that "horribly warm" has higher production cost than "warm" because it contains more morphological material. This cost differential drives the pragmatic reasoning.

Equations

• RSA.Nouwen2024.utteranceCost RSA.Nouwen2024.Utterance.bare_warm = 1
• RSA.Nouwen2024.utteranceCost RSA.Nouwen2024.Utterance.horribly_warm = 2
• RSA.Nouwen2024.utteranceCost RSA.Nouwen2024.Utterance.pleasantly_warm = 2
• RSA.Nouwen2024.utteranceCost RSA.Nouwen2024.Utterance.silent = 0

noncomputable def RSA.Nouwen2024.utteranceCostR (u : Utterance) : ℝ

Equations

• RSA.Nouwen2024.utteranceCostR u = ↑(RSA.Nouwen2024.utteranceCost u)

noncomputable def RSA.Nouwen2024.intensifierS1Score : (Utterance → Height → ℝ) → ℝ → Threshold × Threshold → Height → Utterance → ℝ

S1 scoring rule: exp(α · (log L0(h|u,θ,θ_e) − C(u))), gated at L0=0. Identical to @cite{lassiter-goodman-2017}'s beliefAction but with Latent = Threshold × Threshold for the dual-threshold model.

Equations

• RSA.Nouwen2024.intensifierS1Score l0 α x✝ w u = if l0 u w = 0 then 0 else Real.exp (α * (Real.log (l0 u w) - RSA.Nouwen2024.utteranceCostR u))

theorem RSA.Nouwen2024.intensifierS1Score_nonneg (l0 : Utterance → Height → ℝ) (α : ℝ) (l : Threshold × Threshold) (w : Height) (u : Utterance) : (∀ (u' : Utterance) (w' : Height), 0 ≤ l0 u' w') → 0 < α → 0 ≤ intensifierS1Score l0 α l w u

@[reducible]

noncomputable def RSA.Nouwen2024.nouwenCfg : RSAConfig Utterance Height

RSAConfig for the simultaneous dual-threshold model.

Extends @cite{lassiter-goodman-2017} threshold RSA with a second threshold for the evaluative adverb. L1 jointly infers height, adjective threshold, and evaluative threshold:

P_L1(h, θ, θ_e | u) ∝ P_S1(u | h, θ, θ_e) · P(h) · P(θ) · P(θ_e)

The meaning function uses local ℕ-valued evaluative measures, proved equivalent to Intensification.intensifiedMeaning by meaning_grounded_horribly and meaning_grounded_pleasantly.

Equations

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

H-adverb: "horribly warm" shifts height toward extremes

The Goldilocks effect for negative-evaluative bases: μ_horrible(h) = |h − norm| peaks at extremes, so L1 hearing "horribly warm" concentrates probability on extreme heights. Heights near the norm (h=3) have μ_horrible = 0 and cannot satisfy the evaluative positive form at any θ_e.

theorem RSA.Nouwen2024.horribly_shifts_upward : nouwenCfg.L1 Utterance.horribly_warm (Core.Scale.deg 5 ⋯) > nouwenCfg.L1 Utterance.horribly_warm (Core.Scale.deg 2 ⋯)

theorem RSA.Nouwen2024.horribly_implies_warm : nouwenCfg.L1 Utterance.horribly_warm (Core.Scale.deg 5 ⋯) > nouwenCfg.L1 Utterance.horribly_warm (Core.Scale.deg 1 ⋯)

M-adverb: "pleasantly warm" concentrates at moderate heights

The Goldilocks effect for positive-evaluative bases: μ_pleasant(h) = norm − |h − norm| peaks at the norm (h=3), so L1 hearing "pleasantly warm" concentrates probability on moderate heights. Extreme heights (h=5,6) have low μ_pleasant and cannot satisfy the evaluative positive form.

theorem RSA.Nouwen2024.pleasantly_prefers_moderate : nouwenCfg.L1 Utterance.pleasantly_warm (Core.Scale.deg 4 ⋯) > nouwenCfg.L1 Utterance.pleasantly_warm (Core.Scale.deg 6 ⋯)

theorem RSA.Nouwen2024.pleasantly_implies_warm : nouwenCfg.L1 Utterance.pleasantly_warm (Core.Scale.deg 4 ⋯) > nouwenCfg.L1 Utterance.pleasantly_warm (Core.Scale.deg 1 ⋯)

Cross-utterance Goldilocks predictions

The core Goldilocks effect is a cross-utterance phenomenon: intensifiers redistribute probability mass relative to the bare adjective. "Horribly warm" assigns MORE probability to extreme heights than "warm" does; "pleasantly warm" assigns MORE to moderate heights than "warm" does.

theorem RSA.Nouwen2024.horribly_above_bare_at_extreme : nouwenCfg.L1 Utterance.horribly_warm (Core.Scale.deg 5 ⋯) > nouwenCfg.L1 Utterance.bare_warm (Core.Scale.deg 5 ⋯)

At extreme heights, "horribly warm" assigns more probability than "warm".

theorem RSA.Nouwen2024.pleasantly_above_bare_at_moderate : nouwenCfg.L1 Utterance.pleasantly_warm (Core.Scale.deg 4 ⋯) > nouwenCfg.L1 Utterance.bare_warm (Core.Scale.deg 4 ⋯)

At moderate heights, "pleasantly warm" assigns more probability than "warm".

theorem RSA.Nouwen2024.horribly_dominates_pleasantly_at_extreme : nouwenCfg.L1 Utterance.horribly_warm (Core.Scale.deg 6 ⋯) > nouwenCfg.L1 Utterance.pleasantly_warm (Core.Scale.deg 6 ⋯)

At extreme heights, "horribly warm" dominates "pleasantly warm".

theorem RSA.Nouwen2024.pleasantly_dominates_horribly_at_moderate : nouwenCfg.L1 Utterance.pleasantly_warm (Core.Scale.deg 4 ⋯) > nouwenCfg.L1 Utterance.horribly_warm (Core.Scale.deg 4 ⋯)

At moderate heights, "pleasantly warm" dominates "horribly warm".

Sequential Dual-Threshold Model

key theoretical contribution: the evaluative adverb and base adjective apply sequentially rather than simultaneously. The listener first updates beliefs via the evaluative measure, then applies the adjective threshold to the resulting posterior:

Step 1: P₁(h | "horribly") ∝ P_S1(eval_pos | h, θ_e) · P(h) · P(θ_e) Step 2: P₂(h | "warm") ∝ P_S1(warm | h, θ) · P₁(h) · P(θ)

This sequential model makes the same Goldilocks predictions as the simultaneous model for simple cases, but differs for complex constructions (e.g., "horribly pleasantly warm").

Implementation

Two RSAConfigs composed: the evaluative step's L1 posterior feeds as the adjective step's worldPrior. This uses RSAConfig composition rather than the Ctx/transition machinery, which is designed for sequential production (word-by-word S1 choices), not sequential comprehension (listener updating beliefs step by step).

inductive RSA.Nouwen2024.EvalUtterance : Type

Utterances for the evaluative step: either the evaluative positive form ("the degree is horribly/pleasantly X") or silence.

• eval_pos : EvalUtterance
• silent : EvalUtterance

instance RSA.Nouwen2024.instReprEvalUtterance : Repr EvalUtterance

Equations

• RSA.Nouwen2024.instReprEvalUtterance = { reprPrec := RSA.Nouwen2024.instReprEvalUtterance.repr }

def RSA.Nouwen2024.instReprEvalUtterance.repr : EvalUtterance → ℕ → Std.Format

Equations

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

instance RSA.Nouwen2024.instDecidableEqEvalUtterance : DecidableEq EvalUtterance

Equations

• RSA.Nouwen2024.instDecidableEqEvalUtterance x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def RSA.Nouwen2024.instBEqEvalUtterance.beq : EvalUtterance → EvalUtterance → Bool

Equations

• RSA.Nouwen2024.instBEqEvalUtterance.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance RSA.Nouwen2024.instBEqEvalUtterance : BEq EvalUtterance

Equations

• RSA.Nouwen2024.instBEqEvalUtterance = { beq := RSA.Nouwen2024.instBEqEvalUtterance.beq }

instance RSA.Nouwen2024.instFintypeEvalUtterance : Fintype EvalUtterance

Equations

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

def RSA.Nouwen2024.evalMeaning (evalMu : Height → ℕ) (u : EvalUtterance) (h : Height) (θ_e : Threshold) : Bool

Evaluative meaning for step 1. The evaluative positive form checks only μ_eval(h) > θ_e, without the base adjective. This is the decomposed evaluative component.

Equations

• RSA.Nouwen2024.evalMeaning evalMu RSA.Nouwen2024.EvalUtterance.eval_pos h θ_e = decide (evalMu h > Core.Scale.Threshold.toNat θ_e)
• RSA.Nouwen2024.evalMeaning evalMu RSA.Nouwen2024.EvalUtterance.silent h θ_e = true

def RSA.Nouwen2024.evalCost : EvalUtterance → ℚ

Evaluative step cost: the evaluative adverb costs 1, silence costs 0.

Equations

• RSA.Nouwen2024.evalCost RSA.Nouwen2024.EvalUtterance.eval_pos = 1
• RSA.Nouwen2024.evalCost RSA.Nouwen2024.EvalUtterance.silent = 0

noncomputable def RSA.Nouwen2024.evalCostR (u : EvalUtterance) : ℝ

Equations

• RSA.Nouwen2024.evalCostR u = ↑(RSA.Nouwen2024.evalCost u)

noncomputable def RSA.Nouwen2024.evalS1Score : (EvalUtterance → Height → ℝ) → ℝ → Threshold → Height → EvalUtterance → ℝ

Equations

• RSA.Nouwen2024.evalS1Score l0 α x✝ w u = if l0 u w = 0 then 0 else Real.exp (α * (Real.log (l0 u w) - RSA.Nouwen2024.evalCostR u))

theorem RSA.Nouwen2024.evalS1Score_nonneg (l0 : EvalUtterance → Height → ℝ) (α : ℝ) (l : Threshold) (w : Height) (u : EvalUtterance) : (∀ (u' : EvalUtterance) (w' : Height), 0 ≤ l0 u' w') → 0 < α → 0 ≤ evalS1Score l0 α l w u

@[reducible]

noncomputable def RSA.Nouwen2024.evalCfg (evalMu : Height → ℕ) : RSAConfig EvalUtterance Height

RSAConfig for the evaluative step with a given measure function.

L1 hears the evaluative form and infers a posterior over heights, marginalizing over the evaluative threshold θ_e.

Equations

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

inductive RSA.Nouwen2024.AdjUtterance : Type

Utterances for the adjective step.

• warm : AdjUtterance
• silent : AdjUtterance

instance RSA.Nouwen2024.instReprAdjUtterance : Repr AdjUtterance

Equations

• RSA.Nouwen2024.instReprAdjUtterance = { reprPrec := RSA.Nouwen2024.instReprAdjUtterance.repr }

def RSA.Nouwen2024.instReprAdjUtterance.repr : AdjUtterance → ℕ → Std.Format

Equations

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

instance RSA.Nouwen2024.instDecidableEqAdjUtterance : DecidableEq AdjUtterance

Equations

• RSA.Nouwen2024.instDecidableEqAdjUtterance x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def RSA.Nouwen2024.instBEqAdjUtterance.beq : AdjUtterance → AdjUtterance → Bool

Equations

• RSA.Nouwen2024.instBEqAdjUtterance.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance RSA.Nouwen2024.instBEqAdjUtterance : BEq AdjUtterance

Equations

• RSA.Nouwen2024.instBEqAdjUtterance = { beq := RSA.Nouwen2024.instBEqAdjUtterance.beq }

instance RSA.Nouwen2024.instFintypeAdjUtterance : Fintype AdjUtterance

Equations

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

def RSA.Nouwen2024.adjMeaning (u : AdjUtterance) (h : Height) (θ : Threshold) : Bool

Adjective meaning for step 2: just the base positive form h > θ.

Equations

• RSA.Nouwen2024.adjMeaning RSA.Nouwen2024.AdjUtterance.warm h θ = RSA.Nouwen2024.tallMeaning θ h
• RSA.Nouwen2024.adjMeaning RSA.Nouwen2024.AdjUtterance.silent h θ = true

def RSA.Nouwen2024.adjCost : AdjUtterance → ℚ

Equations

• RSA.Nouwen2024.adjCost RSA.Nouwen2024.AdjUtterance.warm = 1
• RSA.Nouwen2024.adjCost RSA.Nouwen2024.AdjUtterance.silent = 0

noncomputable def RSA.Nouwen2024.adjCostR (u : AdjUtterance) : ℝ

Equations

• RSA.Nouwen2024.adjCostR u = ↑(RSA.Nouwen2024.adjCost u)

noncomputable def RSA.Nouwen2024.adjS1Score : (AdjUtterance → Height → ℝ) → ℝ → Threshold → Height → AdjUtterance → ℝ

Equations

• RSA.Nouwen2024.adjS1Score l0 α x✝ w u = if l0 u w = 0 then 0 else Real.exp (α * (Real.log (l0 u w) - RSA.Nouwen2024.adjCostR u))

theorem RSA.Nouwen2024.adjS1Score_nonneg (l0 : AdjUtterance → Height → ℝ) (α : ℝ) (l : Threshold) (w : Height) (u : AdjUtterance) : (∀ (u' : AdjUtterance) (w' : Height), 0 ≤ l0 u' w') → 0 < α → 0 ≤ adjS1Score l0 α l w u

@[reducible]

noncomputable def RSA.Nouwen2024.seqAdjCfg (evalMu : Height → ℕ) : RSAConfig AdjUtterance Height

RSAConfig for the adjective step with an evaluative posterior as worldPrior.

The worldPrior is the L1 posterior from the evaluative step: the listener has already processed the evaluative adverb and now hears "warm". This implements the sequential composition:

P₂(h | "warm") ∝ P_S1("warm" | h, θ) · L1_eval(h | eval_pos) · P(θ)

Equations

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

noncomputable def RSA.Nouwen2024.seqL1_horribly (h : Height) : ℝ

Sequential L1 posterior for "horribly warm": evaluative step uses μ_horrible, then adjective step applies the base "warm" meaning.

Equations

• RSA.Nouwen2024.seqL1_horribly h = (RSA.Nouwen2024.seqAdjCfg RSA.Nouwen2024.muHorrible).L1 RSA.Nouwen2024.AdjUtterance.warm h

noncomputable def RSA.Nouwen2024.seqL1_pleasantly (h : Height) : ℝ

Sequential L1 posterior for "pleasantly warm": evaluative step uses μ_pleasant, then adjective step applies the base "warm" meaning.

Equations

• RSA.Nouwen2024.seqL1_pleasantly h = (RSA.Nouwen2024.seqAdjCfg RSA.Nouwen2024.muPleasant).L1 RSA.Nouwen2024.AdjUtterance.warm h

Sequential Goldilocks: same qualitative predictions as simultaneous

The sequential model produces the same Goldilocks pattern: "horribly warm" shifts probability toward extremes, "pleasantly warm" concentrates at moderate heights. The sequential decomposition affects the quantitative distribution but preserves the qualitative ordering.

theorem RSA.Nouwen2024.seq_horribly_shifts_upward : (seqAdjCfg muHorrible).L1 AdjUtterance.warm (Core.Scale.deg 5 ⋯) > (seqAdjCfg muHorrible).L1 AdjUtterance.warm (Core.Scale.deg 2 ⋯)

Sequential "horribly warm" shifts upward (Goldilocks).

theorem RSA.Nouwen2024.seq_pleasantly_prefers_moderate : (seqAdjCfg muPleasant).L1 AdjUtterance.warm (Core.Scale.deg 4 ⋯) > (seqAdjCfg muPleasant).L1 AdjUtterance.warm (Core.Scale.deg 6 ⋯)

Sequential "pleasantly warm" prefers moderate heights (Goldilocks).

Zwicky Vacuity: Derived from RSA

§5: Positive modal adverbs (*usually, *expectedly) cannot serve as intensifiers because their evaluative measure is constant across heights, providing no discriminating information about degree. In the sequential model, the evaluative step with a constant measure preserves the prior's bell-curve shape — "usually warm" offers no intensifying information beyond bare "warm".

In contrast, negative modal measures (unusual ≈ horrible) peak at extremes, shifting the evaluative posterior away from the norm and producing genuine intensification. This is why negative modals pattern with negative evaluatives in the Goldilocks effect.

The theorems below derive Zwicky's generalization from the sequential RSA model, connecting the data-layer check (zwickyHolds) to L1 posterior predictions.

def RSA.Nouwen2024.muUsualN : Height → ℕ

ℕ-valued constant measure for the sequential model. Models "usual": μ_usual(h) = 3 for all h (no height discrimination).

Equations

• RSA.Nouwen2024.muUsualN x✝ = 3

def RSA.Nouwen2024.muUnusualN : Height → ℕ

μ_unusual has the same shape as μ_horrible: peaks at extremes. Negative modals pattern with negative evaluatives because both assign high values to heights far from the norm.

Equations

• RSA.Nouwen2024.muUnusualN = RSA.Nouwen2024.muHorrible

theorem RSA.Nouwen2024.muUnusualN_eq_muHorrible : muUnusualN = muHorrible

Negative modal and negative evaluative measures are structurally identical. This is the semantic foundation of why both types make good intensifiers (§5: "the corresponding measure function has a shape similar to that of negative evaluatives").

@[reducible]

noncomputable def RSA.Nouwen2024.bareAdjCfg : RSAConfig AdjUtterance Height

Bare adjective RSAConfig: "warm" vs silence with the original height prior. This is the baseline — what "warm" means without any evaluative step.

Equations

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

Evaluative Step: Constant vs Extreme Measures

theorem RSA.Nouwen2024.eval_constant_preserves_peak : (evalCfg muUsualN).L1 EvalUtterance.eval_pos (Core.Scale.deg 3 ⋯) > (evalCfg muUsualN).L1 EvalUtterance.eval_pos (Core.Scale.deg 6 ⋯)

Constant-measure evaluative step preserves the prior's peak at the norm.

theorem RSA.Nouwen2024.eval_unusual_boosts_extreme : (evalCfg muUnusualN).L1 EvalUtterance.eval_pos (Core.Scale.deg 6 ⋯) > (evalCfg muUsualN).L1 EvalUtterance.eval_pos (Core.Scale.deg 6 ⋯)

Extreme measure (unusual/horrible) boosts extreme heights in L1 beyond what the constant measure assigns.

Sequential Model: Zwicky Predictions

theorem RSA.Nouwen2024.usually_warm_prefers_moderate : (seqAdjCfg muUsualN).L1 AdjUtterance.warm (Core.Scale.deg 4 ⋯) > (seqAdjCfg muUsualN).L1 AdjUtterance.warm (Core.Scale.deg 6 ⋯)

"Usually warm" preserves moderate-height preference (like bare "warm").

theorem RSA.Nouwen2024.unusually_warm_shifts_extreme : (seqAdjCfg muUnusualN).L1 AdjUtterance.warm (Core.Scale.deg 5 ⋯) > (seqAdjCfg muUnusualN).L1 AdjUtterance.warm (Core.Scale.deg 2 ⋯)

"Unusually warm" shifts toward extremes (like "horribly warm"). Note: muUnusualN = muHorrible by muUnusualN_eq_muHorrible, so this is structurally the same prediction as seq_horribly_shifts_upward.

theorem RSA.Nouwen2024.zwicky_extreme_discrimination : (seqAdjCfg muUnusualN).L1 AdjUtterance.warm (Core.Scale.deg 6 ⋯) > (seqAdjCfg muUsualN).L1 AdjUtterance.warm (Core.Scale.deg 6 ⋯)

Zwicky's generalization, derived: at extreme heights, "unusually warm" assigns more probability than "usually warm". Negative modal intensifiers are more informative than positive modal ones because μ_unusual discriminates heights while μ_usual does not.

theorem RSA.Nouwen2024.zwicky_moderate_discrimination : (seqAdjCfg muUsualN).L1 AdjUtterance.warm (Core.Scale.deg 4 ⋯) > (seqAdjCfg muUnusualN).L1 AdjUtterance.warm (Core.Scale.deg 4 ⋯)

Converse: at moderate heights, "usually warm" dominates "unusually warm". The constant measure concentrates mass near the prior peak, while the extreme measure depletes mass at moderate heights.

theorem RSA.Nouwen2024.bare_warm_prefers_moderate : bareAdjCfg.L1 AdjUtterance.warm (Core.Scale.deg 4 ⋯) > bareAdjCfg.L1 AdjUtterance.warm (Core.Scale.deg 6 ⋯)

Bare "warm" baseline: prefers moderate heights (deg 4 > deg 6). Demonstrates that the bare model and "usually warm" agree qualitatively.