Nouwen (2024): The Semantics and Probabilistic Pragmatics of Deadjectival Intensifiers

This file formalizes Nouwen's probabilistic account of deadjectival intensifiers such as horribly warm and pleasantly warm. The adverb contributes a second positive form: its adjectival base measures the proposition that the subject has the degree it actually has, so over the cells of the question under discussion raised by the adjective both the adjective and the adverb are measure functions on the same states. Each positive form is interpreted as in Lassiter and Goodman's threshold model, with a costly positive form competing against a free silent message, and the listener's posterior over states is the state marginal of the joint posterior over states and thresholds (update).

Because a speaker sees a state only through the thresholds the state meets, the posterior is the prior reweighted by a quantity that grows with the set of thresholds met (update_mul_le_mul, strictly in update_mul_lt_mul). For a single positive form this is the upward shift along the measure function (positiveForm_mul_le_mul). The conjunctive model resolves the two thresholds in tandem (simultaneous) and is ordered only by the two measures jointly; Nouwen's final proposal backgrounds the adverb, updating first with the adverb's positive form and then interpreting the adjective against that posterior (sequential), so that the last update is ordered by the adjective's measure alone. The Goldilocks effect of evaluation, negative evaluation growing and positive evaluation shrinking with excess, fixes the direction of the shift (sequential_mul_le_mul_of_negative, sequential_mul_le_mul_of_positive), with the valence read off the English fragment (horribly_mul_le_mul, pleasantly_mul_le_mul). A measure function that does not distinguish the states leaves the prior unchanged (update_eq_self). This is the intuition Nouwen offers for the generalisation he credits to Zwicky, that positive modal adjectives such as usual do not form intensifiers: if usual conveyed the prior, the intensified adjective would be indistinguishable from the bare one (sequential_eq_positiveForm). Nouwen notes that the intuition faces complications.

Implementation notes

States are an arbitrary finite type standing for the cells of the question under discussion, and a measure function is any map from states to a linear order, so the adverb's measure of the proposition a cell expresses is a function on states like the adjective's. The three models are instances of one update over a family of extensions indexed by a latent parameter: a threshold, or a pair of thresholds for the conjunctive model. The threshold prior is a parameter; the paper sums over thresholds unweighted.

TODO

The simulations behind the paper's figures are not stated. In particular the residual mass that the conjunctive model leaves on the cold extreme for horribly warm, the reason the paper rejects it, is a quantitative fact about a discretized normal prior and a quadratic measure, and so is the comparison between the intensified and the bare posterior. The paper's discussion of why a predicative normal is informative while the adverb is not is not formalized.

References

• R. Nouwen, The Semantics and Probabilistic Pragmatics of Deadjectival Intensifiers (2024)
• D. Lassiter and N. D. Goodman, Adjectival Vagueness in a Bayesian Model of Interpretation (2017)
• A. M. Zwicky, Usually and Unusually (1970)

inductive Nouwen2024.Message : Type

The messages of the threshold model are the positive form and saying nothing.

• positive : Message
• silent : Message

@[instance_reducible]

instance Nouwen2024.instDecidableEqMessage : DecidableEq Message

Equations

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

def Nouwen2024.instReprMessage.repr : Message → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Nouwen2024.instReprMessage.repr Nouwen2024.Message.silent prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Nouwen2024.Message.silent")).group prec✝

@[instance_reducible]

instance Nouwen2024.instReprMessage : Repr Message

Equations

• Nouwen2024.instReprMessage = { reprPrec := Nouwen2024.instReprMessage.repr }

@[instance_reducible]

instance Nouwen2024.instFintypeMessage : Fintype Message

Equations

• Nouwen2024.instFintypeMessage = { elems := { val := ↑Nouwen2024.Message.enumList, nodup := Nouwen2024.Message.enumList_nodup }, complete := Nouwen2024.instFintypeMessage._proof_1 }

@[instance_reducible]

instance Nouwen2024.instMeasurableSpaceMessage : MeasurableSpace Message

Equations

• Nouwen2024.instMeasurableSpaceMessage = ⊤

instance Nouwen2024.instDiscreteMeasurableSpaceMessage : DiscreteMeasurableSpace Message

instance Nouwen2024.instNonemptyMessage : Nonempty Message

def Nouwen2024.cost (c : ℝ) : Message → ℝ

The positive form costs c and silence costs nothing.

Equations

• Nouwen2024.cost c Nouwen2024.Message.positive = c
• Nouwen2024.cost c Nouwen2024.Message.silent = 0

The update with a positive form

def Nouwen2024.sem {S : Type u_1} {Λ : Type u_2} (E : Λ → Set S) (l : Λ) : Message → Set S

The meaning of a message under a latent parameter is the parameter's extension for the positive form and every state for silence.

Equations

• Nouwen2024.sem E l Nouwen2024.Message.positive = E l
• Nouwen2024.sem E l Nouwen2024.Message.silent = Set.univ

noncomputable def Nouwen2024.L0 {S : Type u_1} {Λ : Type u_2} [MeasurableSpace S] (P : MeasureTheory.Measure S) (E : Λ → Set S) (l : Λ) : ProbabilityTheory.Kernel Message S

The literal listener at a latent parameter conditions the prior on the truth of the message.

Equations

• Nouwen2024.L0 P E l = RSA.listener P (RSA.truthful fun (u : Nouwen2024.Message) => Nouwen2024.sem E l u)

instance Nouwen2024.instIsFiniteKernelMessageL0 {S : Type u_1} {Λ : Type u_2} [MeasurableSpace S] (P : MeasureTheory.Measure S) (E : Λ → Set S) (l : Λ) : ProbabilityTheory.IsFiniteKernel (L0 P E l)

noncomputable def Nouwen2024.S1 {S : Type u_1} {Λ : Type u_2} [Fintype S] [MeasurableSpace S] [DiscreteMeasurableSpace S] (P : MeasureTheory.Measure S) (E : Λ → Set S) (α c : ℝ) (p : S × Λ) : MeasureTheory.Measure Message

The speaker at a state and a latent parameter soft-maximizes the literal listener's log probability of the state minus the cost of the message.

Equations

• Nouwen2024.S1 P E α c p = (RSA.speaker α (Nouwen2024.cost c) (⇑(Nouwen2024.L0 P E p.2)) MeasureTheory.Measure.dirac) p.1

instance Nouwen2024.instIsFiniteMeasureMessageS1 {S : Type u_1} {Λ : Type u_2} [Fintype S] [MeasurableSpace S] [DiscreteMeasurableSpace S] (P : MeasureTheory.Measure S) (E : Λ → Set S) (α c : ℝ) (p : S × Λ) : MeasureTheory.IsFiniteMeasure (S1 P E α c p)

theorem Nouwen2024.S1_apply_singleton_ne_zero_iff {S : Type u_1} {Λ : Type u_2} [Fintype S] [MeasurableSpace S] [DiscreteMeasurableSpace S] (P : MeasureTheory.Measure S) [MeasureTheory.IsFiniteMeasure P] (E : Λ → Set S) (α c : ℝ) (hα : 0 < α) (s : S) (l : Λ) (u : Message) : (S1 P E α c (s, l)) {u} ≠ 0 ↔ s ∈ sem E l u ∧ P {s} ≠ 0

The speaker produces a message at a state and a latent parameter exactly when it is true there and the state has positive prior.

theorem Nouwen2024.S1_congr {S : Type u_1} {Λ : Type u_2} [Fintype S] [MeasurableSpace S] [DiscreteMeasurableSpace S] {P : MeasureTheory.Measure S} [MeasureTheory.IsFiniteMeasure P] {E : Λ → Set S} {α : ℝ} (c : ℝ) (hα : 0 < α) {s t : S} {l : Λ} (hs : P {s} ≠ 0) (ht : P {t} ≠ 0) (hsl : s ∈ E l) (htl : t ∈ E l) : S1 P E α c (t, l) = S1 P E α c (s, l)

The speaker treats alike two states of positive prior in the extension of a latent parameter.

theorem Nouwen2024.S1_real_positive_le {S : Type u_1} {Λ : Type u_2} [Fintype S] [MeasurableSpace S] [DiscreteMeasurableSpace S] {P : MeasureTheory.Measure S} [MeasureTheory.IsFiniteMeasure P] {E : Λ → Set S} {α : ℝ} (c : ℝ) (hα : 0 < α) {s t : S} (hs : P {s} ≠ 0) (ht : P {t} ≠ 0) {l : Λ} (h : s ∈ E l → t ∈ E l) : (S1 P E α c (s, l)).real {Message.positive} ≤ (S1 P E α c (t, l)).real {Message.positive}

At each latent parameter the speaker is no less likely to produce the positive form at a state that lies in its extension whenever another state does.

def Nouwen2024.Assertable {S : Type u_1} {Λ : Type u_2} [MeasurableSpace S] [MeasurableSpace Λ] (P : MeasureTheory.Measure S) (ν : MeasureTheory.Measure Λ) (E : Λ → Set S) : Prop

The positive form is assertable when some state of positive prior lies in the extension of some latent parameter of positive prior.

Equations

• Nouwen2024.Assertable P ν E = ∃ (s : S) (l : Λ), P {s} ≠ 0 ∧ ν {l} ≠ 0 ∧ s ∈ E l

noncomputable def Nouwen2024.L1 {S : Type u_1} {Λ : Type u_2} [Fintype S] [MeasurableSpace S] [DiscreteMeasurableSpace S] [MeasurableSpace Λ] (P : MeasureTheory.Measure S) (ν : MeasureTheory.Measure Λ) (E : Λ → Set S) (α c : ℝ) : ProbabilityTheory.Kernel Message (S × Λ)

The pragmatic listener inverts the speaker against the product of the state prior and the prior over latent parameters.

Equations

• Nouwen2024.L1 P ν E α c = RSA.listener (P.prod ν) (Nouwen2024.S1 P E α c)

noncomputable def Nouwen2024.update {S : Type u_1} {Λ : Type u_2} [Fintype S] [MeasurableSpace S] [DiscreteMeasurableSpace S] [MeasurableSpace Λ] (P : MeasureTheory.Measure S) (ν : MeasureTheory.Measure Λ) (E : Λ → Set S) (α c : ℝ) : MeasureTheory.Measure S

The update of a prior with the positive form is the state marginal of the pragmatic listener's posterior.

Equations

• Nouwen2024.update P ν E α c = ((Nouwen2024.L1 P ν E α c) Nouwen2024.Message.positive).fst

instance Nouwen2024.instIsFiniteMeasureUpdate {S : Type u_1} {Λ : Type u_2} [Fintype S] [MeasurableSpace S] [DiscreteMeasurableSpace S] [MeasurableSpace Λ] (P : MeasureTheory.Measure S) (ν : MeasureTheory.Measure Λ) (E : Λ → Set S) (α c : ℝ) : MeasureTheory.IsFiniteMeasure (update P ν E α c)

noncomputable def Nouwen2024.production {S : Type u_1} {Λ : Type u_2} [Fintype S] [MeasurableSpace S] [DiscreteMeasurableSpace S] [MeasurableSpace Λ] (P : MeasureTheory.Measure S) (ν : MeasureTheory.Measure Λ) (E : Λ → Set S) (α c : ℝ) [Fintype Λ] (s : S) : ℝ

The production weight of a state is the prior-averaged probability that the speaker produces the positive form there.

Equations

• Nouwen2024.production P ν E α c s = ∑ l : Λ, ν.real {l} * (Nouwen2024.S1 P E α c (s, l)).real {Nouwen2024.Message.positive}

theorem Nouwen2024.production_le_production {S : Type u_1} {Λ : Type u_2} [Fintype S] [MeasurableSpace S] [DiscreteMeasurableSpace S] [MeasurableSpace Λ] {P : MeasureTheory.Measure S} [MeasureTheory.IsFiniteMeasure P] {ν : MeasureTheory.Measure Λ} {E : Λ → Set S} {α : ℝ} (c : ℝ) [Fintype Λ] (hα : 0 < α) {s t : S} (hs : P {s} ≠ 0) (ht : P {t} ≠ 0) (h : ∀ (l : Λ), s ∈ E l → t ∈ E l) : production P ν E α c s ≤ production P ν E α c t

A state that lies in no more extensions than another has no greater production weight.

theorem Nouwen2024.production_lt_production {S : Type u_1} {Λ : Type u_2} [Fintype S] [MeasurableSpace S] [DiscreteMeasurableSpace S] [MeasurableSpace Λ] {P : MeasureTheory.Measure S} [MeasureTheory.IsFiniteMeasure P] {ν : MeasureTheory.Measure Λ} {E : Λ → Set S} {α : ℝ} (c : ℝ) [Fintype Λ] [MeasureTheory.IsFiniteMeasure ν] (hα : 0 < α) {s t : S} (hs : P {s} ≠ 0) (ht : P {t} ≠ 0) (h : ∀ (l : Λ), s ∈ E l → t ∈ E l) {l₀ : Λ} (hl₀ : ν {l₀} ≠ 0) (hs₀ : s ∉ E l₀) (ht₀ : t ∈ E l₀) : production P ν E α c s < production P ν E α c t

The production weight is strictly greater when a latent parameter of positive prior separates the two states.

theorem Nouwen2024.Assertable.sum_pos {S : Type u_1} {Λ : Type u_2} [Fintype S] [MeasurableSpace S] [DiscreteMeasurableSpace S] [MeasurableSpace Λ] {P : MeasureTheory.Measure S} [MeasureTheory.IsFiniteMeasure P] {ν : MeasureTheory.Measure Λ} {E : Λ → Set S} {α : ℝ} (c : ℝ) [Fintype Λ] [MeasureTheory.IsFiniteMeasure ν] (h : Assertable P ν E) (hα : 0 < α) : 0 < ∑ p : S × Λ, (P.prod ν).real {p} * (S1 P E α c p).real {Message.positive}

An assertable positive form is produced with positive probability.

theorem Nouwen2024.Assertable.isProbabilityMeasure_update {S : Type u_1} {Λ : Type u_2} [Fintype S] [MeasurableSpace S] [DiscreteMeasurableSpace S] [MeasurableSpace Λ] {P : MeasureTheory.Measure S} [MeasureTheory.IsFiniteMeasure P] {ν : MeasureTheory.Measure Λ} {E : Λ → Set S} {α : ℝ} (c : ℝ) [Fintype Λ] [MeasureTheory.IsFiniteMeasure ν] [DiscreteMeasurableSpace Λ] (h : Assertable P ν E) (hα : 0 < α) : MeasureTheory.IsProbabilityMeasure (update P ν E α c)

The update with an assertable positive form is a probability measure.

theorem Nouwen2024.update_real_singleton {S : Type u_1} {Λ : Type u_2} [Fintype S] [MeasurableSpace S] [DiscreteMeasurableSpace S] [MeasurableSpace Λ] {P : MeasureTheory.Measure S} [MeasureTheory.IsFiniteMeasure P] {ν : MeasureTheory.Measure Λ} {E : Λ → Set S} {α : ℝ} (c : ℝ) [Fintype Λ] [MeasureTheory.IsFiniteMeasure ν] [DiscreteMeasurableSpace Λ] (s : S) : (update P ν E α c).real {s} = P.real {s} * production P ν E α c s / ∑ p : S × Λ, (P.prod ν).real {p} * (S1 P E α c p).real {Message.positive}

The posterior of a state is its prior times its production weight, normalized.

theorem Nouwen2024.update_apply_singleton_ne_zero_iff {S : Type u_1} {Λ : Type u_2} [Fintype S] [MeasurableSpace S] [DiscreteMeasurableSpace S] [MeasurableSpace Λ] {P : MeasureTheory.Measure S} [MeasureTheory.IsFiniteMeasure P] {ν : MeasureTheory.Measure Λ} {E : Λ → Set S} {α : ℝ} (c : ℝ) [Fintype Λ] [MeasureTheory.IsFiniteMeasure ν] [DiscreteMeasurableSpace Λ] (hα : 0 < α) (s : S) : (update P ν E α c) {s} ≠ 0 ↔ P {s} ≠ 0 ∧ ∃ (l : Λ), ν {l} ≠ 0 ∧ s ∈ E l

The update keeps exactly the states of positive prior that lie in the extension of some latent parameter of positive prior.

theorem Nouwen2024.assertable_update {S : Type u_1} {Λ : Type u_2} [Fintype S] [MeasurableSpace S] [DiscreteMeasurableSpace S] [MeasurableSpace Λ] {P : MeasureTheory.Measure S} [MeasureTheory.IsFiniteMeasure P] {ν : MeasureTheory.Measure Λ} {E : Λ → Set S} {α : ℝ} (c : ℝ) [Fintype Λ] [MeasureTheory.IsFiniteMeasure ν] [DiscreteMeasurableSpace Λ] {Λ' : Type u_3} [MeasurableSpace Λ'] {ν' : MeasureTheory.Measure Λ'} {E' : Λ' → Set S} (hα : 0 < α) {s : S} {l : Λ} {l' : Λ'} (hs : P {s} ≠ 0) (hl : ν {l} ≠ 0) (hsl : s ∈ E l) (hl' : ν' {l'} ≠ 0) (hsl' : s ∈ E' l') : Assertable (update P ν E α c) ν' E'

A further positive form is assertable against the updated prior when some state of positive prior lies in an extension of positive prior for each of the two forms.

theorem Nouwen2024.update_mul_le_mul {S : Type u_1} {Λ : Type u_2} [Fintype S] [MeasurableSpace S] [DiscreteMeasurableSpace S] [MeasurableSpace Λ] {P : MeasureTheory.Measure S} [MeasureTheory.IsFiniteMeasure P] {ν : MeasureTheory.Measure Λ} {E : Λ → Set S} {α : ℝ} (c : ℝ) [Fintype Λ] [MeasureTheory.IsFiniteMeasure ν] [DiscreteMeasurableSpace Λ] (hα : 0 < α) {s t : S} (h : ∀ (l : Λ), s ∈ E l → t ∈ E l) : (update P ν E α c).real {s} * P.real {t} ≤ (update P ν E α c).real {t} * P.real {s}

The update shifts mass toward states that lie in more extensions, in that the ratio of posterior to prior is monotone in the set of latent parameters whose extension contains the state.

theorem Nouwen2024.update_mul_lt_mul {S : Type u_1} {Λ : Type u_2} [Fintype S] [MeasurableSpace S] [DiscreteMeasurableSpace S] [MeasurableSpace Λ] {P : MeasureTheory.Measure S} [MeasureTheory.IsFiniteMeasure P] {ν : MeasureTheory.Measure Λ} {E : Λ → Set S} {α : ℝ} (c : ℝ) [Fintype Λ] [MeasureTheory.IsFiniteMeasure ν] [DiscreteMeasurableSpace Λ] (hα : 0 < α) {s t : S} (hs : P {s} ≠ 0) (ht : P {t} ≠ 0) (h : ∀ (l : Λ), s ∈ E l → t ∈ E l) {l₀ : Λ} (hl₀ : ν {l₀} ≠ 0) (hs₀ : s ∉ E l₀) (ht₀ : t ∈ E l₀) : (update P ν E α c).real {s} * P.real {t} < (update P ν E α c).real {t} * P.real {s}

The shift is strict between two states of positive prior separated by a latent parameter of positive prior.

theorem Nouwen2024.update_eq_self {S : Type u_1} {Λ : Type u_2} [Fintype S] [MeasurableSpace S] [DiscreteMeasurableSpace S] [MeasurableSpace Λ] {P : MeasureTheory.Measure S} [MeasureTheory.IsFiniteMeasure P] {ν : MeasureTheory.Measure Λ} {E : Λ → Set S} {α : ℝ} (c : ℝ) [Fintype Λ] [MeasureTheory.IsFiniteMeasure ν] [DiscreteMeasurableSpace Λ] [MeasureTheory.IsProbabilityMeasure P] (hα : 0 < α) (hE : Assertable P ν E) (h : ∀ (l : Λ) (s t : S), s ∈ E l → t ∈ E l) : update P ν E α c = P

A positive form whose extensions do not distinguish the states leaves a probability prior unchanged.

Positive forms of measure functions

def Nouwen2024.atLeast {S : Type u_1} {D : Type u_3} [LinearOrder D] (m : S → D) (θ : D) : Set S

The extension of a positive form at a threshold holds the states whose measure meets the threshold.

Equations

• Nouwen2024.atLeast m θ = {s : S | θ ≤ m s}

@[reducible, inline]

noncomputable abbrev Nouwen2024.positiveForm {S : Type u_1} [Fintype S] [MeasurableSpace S] [DiscreteMeasurableSpace S] {D : Type u_3} [LinearOrder D] [MeasurableSpace D] (P : MeasureTheory.Measure S) [MeasureTheory.IsFiniteMeasure P] (νA : MeasureTheory.Measure D) [MeasureTheory.IsFiniteMeasure νA] (mA : S → D) (α c : ℝ) : MeasureTheory.Measure S

The interpretation of a bare positive form updates the prior with the extensions of the adjective's measure function.

Equations

• Nouwen2024.positiveForm P νA mA α c = Nouwen2024.update P νA (Nouwen2024.atLeast mA) α c

@[reducible, inline]

noncomputable abbrev Nouwen2024.simultaneous {S : Type u_1} [Fintype S] [MeasurableSpace S] [DiscreteMeasurableSpace S] {D : Type u_3} {D' : Type u_4} [LinearOrder D] [MeasurableSpace D] [LinearOrder D'] [MeasurableSpace D'] (P : MeasureTheory.Measure S) [MeasureTheory.IsFiniteMeasure P] (νA : MeasureTheory.Measure D) [MeasureTheory.IsFiniteMeasure νA] (νD : MeasureTheory.Measure D') [MeasureTheory.IsFiniteMeasure νD] (mA : S → D) (mD : S → D') (α c : ℝ) : MeasureTheory.Measure S

The conjunctive model of an intensified adjective resolves the thresholds of the adjective and the adverb in tandem, as one update over pairs of thresholds.

Equations

• Nouwen2024.simultaneous P νA νD mA mD α c = Nouwen2024.update P (νA.prod νD) (fun (θ : D × D') => Nouwen2024.atLeast mA θ.1 ∩ Nouwen2024.atLeast mD θ.2) α c

@[reducible, inline]

noncomputable abbrev Nouwen2024.sequential {S : Type u_1} [Fintype S] [MeasurableSpace S] [DiscreteMeasurableSpace S] {D : Type u_3} {D' : Type u_4} [LinearOrder D] [MeasurableSpace D] [LinearOrder D'] [MeasurableSpace D'] (P : MeasureTheory.Measure S) [MeasureTheory.IsFiniteMeasure P] (νA : MeasureTheory.Measure D) [MeasureTheory.IsFiniteMeasure νA] (νD : MeasureTheory.Measure D') [MeasureTheory.IsFiniteMeasure νD] (mA : S → D) (mD : S → D') (α c c' : ℝ) : MeasureTheory.Measure S

The backgrounded model of an intensified adjective first updates the prior with the adverb's positive form at cost c' and then interprets the adjective's positive form against that posterior.

Equations

• Nouwen2024.sequential P νA νD mA mD α c c' = Nouwen2024.positiveForm (Nouwen2024.positiveForm P νD mD α c') νA mA α c

theorem Nouwen2024.positiveForm_mul_le_mul {S : Type u_1} [Fintype S] [MeasurableSpace S] [DiscreteMeasurableSpace S] {P : MeasureTheory.Measure S} [MeasureTheory.IsFiniteMeasure P] {α : ℝ} (c : ℝ) {D : Type u_3} [LinearOrder D] [Fintype D] [MeasurableSpace D] [DiscreteMeasurableSpace D] {νA : MeasureTheory.Measure D} [MeasureTheory.IsFiniteMeasure νA] {mA : S → D} (hα : 0 < α) {s t : S} (h : mA s ≤ mA t) : (positiveForm P νA mA α c).real {s} * P.real {t} ≤ (positiveForm P νA mA α c).real {t} * P.real {s}

A positive form shifts mass toward the states of higher measure.

theorem Nouwen2024.positiveForm_mul_lt_mul {S : Type u_1} [Fintype S] [MeasurableSpace S] [DiscreteMeasurableSpace S] {P : MeasureTheory.Measure S} [MeasureTheory.IsFiniteMeasure P] {α : ℝ} (c : ℝ) {D : Type u_3} [LinearOrder D] [Fintype D] [MeasurableSpace D] [DiscreteMeasurableSpace D] {νA : MeasureTheory.Measure D} [MeasureTheory.IsFiniteMeasure νA] {mA : S → D} (hα : 0 < α) {s t : S} (hs : P {s} ≠ 0) (ht : P {t} ≠ 0) (h : mA s < mA t) (hν : νA {mA t} ≠ 0) : (positiveForm P νA mA α c).real {s} * P.real {t} < (positiveForm P νA mA α c).real {t} * P.real {s}

The shift is strict between two states of positive prior when the higher measure is a threshold of positive prior.

theorem Nouwen2024.simultaneous_mul_le_mul {S : Type u_1} [Fintype S] [MeasurableSpace S] [DiscreteMeasurableSpace S] {P : MeasureTheory.Measure S} [MeasureTheory.IsFiniteMeasure P] {α : ℝ} (c : ℝ) {D : Type u_3} {D' : Type u_4} [LinearOrder D] [Fintype D] [MeasurableSpace D] [DiscreteMeasurableSpace D] [LinearOrder D'] [Fintype D'] [MeasurableSpace D'] [DiscreteMeasurableSpace D'] {νA : MeasureTheory.Measure D} [MeasureTheory.IsFiniteMeasure νA] {νD : MeasureTheory.Measure D'} [MeasureTheory.IsFiniteMeasure νD] {mA : S → D} {mD : S → D'} (hα : 0 < α) {s t : S} (hA : mA s ≤ mA t) (hD : mD s ≤ mD t) : (simultaneous P νA νD mA mD α c).real {s} * P.real {t} ≤ (simultaneous P νA νD mA mD α c).real {t} * P.real {s}

The conjunctive model is ordered by the two measures jointly, in that mass shifts toward a state only when it is at least as high on the adjective's scale and on the adverb's.

theorem Nouwen2024.sequential_mul_le_mul {S : Type u_1} [Fintype S] [MeasurableSpace S] [DiscreteMeasurableSpace S] {P : MeasureTheory.Measure S} [MeasureTheory.IsFiniteMeasure P] {α : ℝ} (c : ℝ) {D : Type u_3} {D' : Type u_4} [LinearOrder D] [Fintype D] [MeasurableSpace D] [DiscreteMeasurableSpace D] [LinearOrder D'] [Fintype D'] [MeasurableSpace D'] [DiscreteMeasurableSpace D'] {νA : MeasureTheory.Measure D} [MeasureTheory.IsFiniteMeasure νA] {νD : MeasureTheory.Measure D'} [MeasureTheory.IsFiniteMeasure νD] {mA : S → D} {mD : S → D'} (c' : ℝ) (hα : 0 < α) {s t : S} (hmA : mA s ≤ mA t) (hmD : mD s ≤ mD t) : (sequential P νA νD mA mD α c c').real {s} * P.real {t} ≤ (sequential P νA νD mA mD α c c').real {t} * P.real {s}

Relative to the original prior the backgrounded model is also ordered by the two measures jointly; relative to the backgrounded posterior its last update is ordered by the adjective's measure alone, by positiveForm_mul_le_mul.

The Goldilocks effect and vacuous intensifiers

def Nouwen2024.Goldilocks {S : Type u_1} {D' : Type u_4} {X : Type u_5} [LinearOrder D'] [Preorder X] (a : Degree.GradableAdjective) (excess : S → X) (m : S → D') : Prop

The Goldilocks effect of evaluation constrains the measure function of an evaluative base over a scale of excess, so that a negative evaluation grows with excess and a positive evaluation shrinks with it.

Equations

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

theorem Nouwen2024.sequential_mul_le_mul_of_negative {S : Type u_1} [Fintype S] [MeasurableSpace S] [DiscreteMeasurableSpace S] {P : MeasureTheory.Measure S} [MeasureTheory.IsFiniteMeasure P] {α : ℝ} (c : ℝ) {D : Type u_3} {D' : Type u_4} {X : Type u_5} [LinearOrder D] [Fintype D] [MeasurableSpace D] [DiscreteMeasurableSpace D] [LinearOrder D'] [Fintype D'] [MeasurableSpace D'] [DiscreteMeasurableSpace D'] [Preorder X] {νA : MeasureTheory.Measure D} [MeasureTheory.IsFiniteMeasure νA] {νD : MeasureTheory.Measure D'} [MeasureTheory.IsFiniteMeasure νD] {mA : S → D} {mD : S → D'} (c' : ℝ) {a : Degree.GradableAdjective} {excess : S → X} (ha : a.evaluativeValence = some Degree.EvaluativeValence.negative) (hm : Goldilocks a excess mD) (hα : 0 < α) {s t : S} (hmA : mA s ≤ mA t) (hx : excess s ≤ excess t) : (sequential P νA νD mA mD α c c').real {s} * P.real {t} ≤ (sequential P νA νD mA mD α c c').real {t} * P.real {s}

An intensifier with a negatively evaluative base shifts mass toward the states that are higher on the adjective's scale and more excessive, which is intensification to a high degree.

theorem Nouwen2024.sequential_mul_le_mul_of_positive {S : Type u_1} [Fintype S] [MeasurableSpace S] [DiscreteMeasurableSpace S] {P : MeasureTheory.Measure S} [MeasureTheory.IsFiniteMeasure P] {α : ℝ} (c : ℝ) {D : Type u_3} {D' : Type u_4} {X : Type u_5} [LinearOrder D] [Fintype D] [MeasurableSpace D] [DiscreteMeasurableSpace D] [LinearOrder D'] [Fintype D'] [MeasurableSpace D'] [DiscreteMeasurableSpace D'] [Preorder X] {νA : MeasureTheory.Measure D} [MeasureTheory.IsFiniteMeasure νA] {νD : MeasureTheory.Measure D'} [MeasureTheory.IsFiniteMeasure νD] {mA : S → D} {mD : S → D'} (c' : ℝ) {a : Degree.GradableAdjective} {excess : S → X} (ha : a.evaluativeValence = some Degree.EvaluativeValence.positive) (hm : Goldilocks a excess mD) (hα : 0 < α) {s t : S} (hmA : mA s ≤ mA t) (hx : excess t ≤ excess s) : (sequential P νA νD mA mD α c c').real {s} * P.real {t} ≤ (sequential P νA νD mA mD α c c').real {t} * P.real {s}

An intensifier with a positively evaluative base shifts mass toward the states that are higher on the adjective's scale and less excessive, which is intensification to a moderate degree.

theorem Nouwen2024.horribly_mul_le_mul {S : Type u_1} [Fintype S] [MeasurableSpace S] [DiscreteMeasurableSpace S] {P : MeasureTheory.Measure S} [MeasureTheory.IsFiniteMeasure P] {α : ℝ} (c : ℝ) {D : Type u_3} {D' : Type u_4} {X : Type u_5} [LinearOrder D] [Fintype D] [MeasurableSpace D] [DiscreteMeasurableSpace D] [LinearOrder D'] [Fintype D'] [MeasurableSpace D'] [DiscreteMeasurableSpace D'] [Preorder X] {νA : MeasureTheory.Measure D} [MeasureTheory.IsFiniteMeasure νA] {νD : MeasureTheory.Measure D'} [MeasureTheory.IsFiniteMeasure νD] {mA : S → D} {mD : S → D'} (c' : ℝ) {excess : S → X} (hm : Goldilocks English.Adjectives.horrible excess mD) (hα : 0 < α) {s t : S} (hmA : mA s ≤ mA t) (hx : excess s ≤ excess t) : (sequential P νA νD mA mD α c c').real {s} * P.real {t} ≤ (sequential P νA νD mA mD α c c').real {t} * P.real {s}

The English fragment records horrible as negatively evaluative, so horribly intensifies to a high degree.

theorem Nouwen2024.pleasantly_mul_le_mul {S : Type u_1} [Fintype S] [MeasurableSpace S] [DiscreteMeasurableSpace S] {P : MeasureTheory.Measure S} [MeasureTheory.IsFiniteMeasure P] {α : ℝ} (c : ℝ) {D : Type u_3} {D' : Type u_4} {X : Type u_5} [LinearOrder D] [Fintype D] [MeasurableSpace D] [DiscreteMeasurableSpace D] [LinearOrder D'] [Fintype D'] [MeasurableSpace D'] [DiscreteMeasurableSpace D'] [Preorder X] {νA : MeasureTheory.Measure D} [MeasureTheory.IsFiniteMeasure νA] {νD : MeasureTheory.Measure D'} [MeasureTheory.IsFiniteMeasure νD] {mA : S → D} {mD : S → D'} (c' : ℝ) {excess : S → X} (hm : Goldilocks English.Adjectives.pleasant excess mD) (hα : 0 < α) {s t : S} (hmA : mA s ≤ mA t) (hx : excess t ≤ excess s) : (sequential P νA νD mA mD α c c').real {s} * P.real {t} ≤ (sequential P νA νD mA mD α c c').real {t} * P.real {s}

The English fragment records pleasant as positively evaluative, so pleasantly intensifies to a moderate degree.

theorem Nouwen2024.sequential_eq_positiveForm {S : Type u_1} [Fintype S] [MeasurableSpace S] [DiscreteMeasurableSpace S] {P : MeasureTheory.Measure S} [MeasureTheory.IsFiniteMeasure P] {α : ℝ} (c : ℝ) {D : Type u_3} {D' : Type u_4} [LinearOrder D] [MeasurableSpace D] [LinearOrder D'] [Fintype D'] [MeasurableSpace D'] [DiscreteMeasurableSpace D'] {νA : MeasureTheory.Measure D} [MeasureTheory.IsFiniteMeasure νA] {νD : MeasureTheory.Measure D'} [MeasureTheory.IsFiniteMeasure νD] {mA : S → D} {mD : S → D'} (c' : ℝ) [MeasureTheory.IsProbabilityMeasure P] (hα : 0 < α) (hD : Assertable P νD (atLeast mD)) (h : ∀ (s t : S), mD s = mD t) : sequential P νA νD mA mD α c c' = positiveForm P νA mA α c

An adverb whose measure function does not distinguish the states, as that of usual would not if it conveyed the prior, is a vacuous intensifier, and the intensified adjective is interpreted as the bare adjective.