Israel (2001): Minimizers, Maximizers and the Rhetoric of Scalar Reasoning

This file formalizes Israel's Scalar Model of polarity sensitivity. A scalar model, after Fillmore, Kay and O'Connor, is a propositional function over an ordered scale whose values pragmatically entail one another; a polarity item encodes a quantity relative to the scalar norm and a rhetorical force, emphatic when the proposition it expresses entails the norm's and attenuating when it is entailed by it (Emphatic, Attenuating). Scale preserving contexts are the strictly monotone maps on propositions and scale reversing ones the strictly antitone maps, the positive and negative directions of Polarity.StrictMonoBy, and the direction of the expressed propositional function decides which quantities are emphatic (felicitous_iff_of_strictMonoBy). The four cells of Figure 1 follow: emphatic items with low values and attenuating items with high values need reversing contexts, the negative polarity items, the other two cells preserving contexts. The inverted items of Section 4, maximizing NPIs like wild horses and minimizing PPIs like for peanuts, follow from the thematic logic of Section 5: a propositional role either impedes the eventuality, so that the function is antitone in quantity, or facilitates it, so that it is monotone (Role). Directions compose as polarities multiply, so that the licensing context of any item is the product of the signs of its force, quantity and role (licensingContext, felicitous_iff). The pecuniary paradox dissolves because a resource is impeding and a reward facilitating, and the ambiguous superlatives of Section 7 are the same composition with an existential and a perceptual-ability scale.

Implementation notes

• Pragmatic entailment between the propositions of a scalar model is modelled as inclusion of sets of worlds; the paper's point that the relevant inferences may be pragmatic rather than logical is not represented.
• The paper's classifications of the English items of Fragments/English/PolarityItems.lean by force, quantity and role live here (classified), and the derived licensing context is checked against the fragment's record of each item as an NPI or PPI.

References

• [Isr01]
• [Isr96]
• [FKOC88]
• [Fau75]
• [Lad79]

inductive Israel2001.Force : Type

Rhetorical force: the expressed proposition is more informative than the scalar norm, or less.

• emphatic : Force
• attenuating : Force

@[instance_reducible]

instance Israel2001.instDecidableEqForce : DecidableEq Force

Equations

• Israel2001.instDecidableEqForce x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Israel2001.Force.sign : Force → Polarity

The sign of a force: emphatic items are negative, attenuating ones positive.

Equations

• Israel2001.Force.emphatic.sign = Polarity.negative
• Israel2001.Force.attenuating.sign = Polarity.positive

inductive Israel2001.Quantity : Type

Quantity relative to the norm: the size, amount or degree the item denotes.

• small : Quantity
• large : Quantity

@[instance_reducible]

instance Israel2001.instDecidableEqQuantity : DecidableEq Quantity

Equations

• Israel2001.instDecidableEqQuantity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Israel2001.Quantity.sign : Quantity → Polarity

The sign of a quantity relative to the norm: small is negative, large positive.

Equations

• Israel2001.Quantity.small.sign = Polarity.negative
• Israel2001.Quantity.large.sign = Polarity.positive

def Israel2001.Quantity.Rel {α : Type u_1} [LinearOrder α] : Quantity → α → α → Prop

A quantity x stands to the norm n as the item's quantity says.

Equations

• Israel2001.Quantity.small.Rel x✝¹ x✝ = (x✝¹ < x✝)
• Israel2001.Quantity.large.Rel x✝¹ x✝ = (x✝ < x✝¹)

inductive Israel2001.Role : Type

The effect of a propositional role on the likelihood of the eventuality (Section 5): a patient, theme, increment, expense or duration impedes it, the bigger the less likely, and an agent, stimulus, reward, instrument or interval facilitates it.

• impeding : Role
• facilitating : Role

@[instance_reducible]

instance Israel2001.instDecidableEqRole : DecidableEq Role

Equations

• Israel2001.instDecidableEqRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Israel2001.Role.sign : Role → Polarity

The direction of the propositional function of a role: strictly antitone in quantity for an impeding role, so that bigger values entail smaller ones, strictly monotone for a facilitating one.

Equations

• Israel2001.Role.impeding.sign = Polarity.negative
• Israel2001.Role.facilitating.sign = Polarity.positive

def Israel2001.Emphatic {α : Type u_1} {W : Type u_2} (Q : α → Set W) (n x : α) : Prop

The proposition expressed with quantity x is emphatic when it pragmatically entails the proposition at the norm.

Equations

• Israel2001.Emphatic Q n x = (Q x ⊂ Q n)

def Israel2001.Attenuating {α : Type u_1} {W : Type u_2} (Q : α → Set W) (n x : α) : Prop

It is attenuating when the proposition at the norm entails it.

Equations

• Israel2001.Attenuating Q n x = (Q n ⊂ Q x)

def Israel2001.Felicitous {α : Type u_1} {W : Type u_2} : Force → (α → Set W) → α → α → Prop

An item of a given force is felicitous when the proposition expressed has that force.

Equations

• Israel2001.Felicitous Israel2001.Force.emphatic x✝² x✝¹ x✝ = Israel2001.Emphatic x✝² x✝¹ x✝
• Israel2001.Felicitous Israel2001.Force.attenuating x✝² x✝¹ x✝ = Israel2001.Attenuating x✝² x✝¹ x✝

theorem Israel2001.emphatic_iff_of_strictMono {α : Type u_1} {W : Type u_2} [LinearOrder α] {Q : α → Set W} {n x : α} (h : StrictMono Q) (hx : x ≠ n) : Emphatic Q n x ↔ x < n

When the expressed function is strictly monotone, inferences run from low values to high ones and the emphatic propositions are the ones below the norm.

theorem Israel2001.emphatic_iff_of_strictAnti {α : Type u_1} {W : Type u_2} [LinearOrder α] {Q : α → Set W} {n x : α} (h : StrictAnti Q) (hx : x ≠ n) : Emphatic Q n x ↔ n < x

When it is strictly antitone, inferences run from high values to low ones and the emphatic propositions are the ones above the norm.

theorem Israel2001.attenuating_iff_of_strictMono {α : Type u_1} {W : Type u_2} [LinearOrder α] {Q : α → Set W} {n x : α} (h : StrictMono Q) (hx : x ≠ n) : Attenuating Q n x ↔ n < x

theorem Israel2001.attenuating_iff_of_strictAnti {α : Type u_1} {W : Type u_2} [LinearOrder α] {Q : α → Set W} {n x : α} (h : StrictAnti Q) (hx : x ≠ n) : Attenuating Q n x ↔ x < n

theorem Israel2001.felicitous_iff_of_strictMono {α : Type u_1} {W : Type u_2} [LinearOrder α] {Q : α → Set W} {n x : α} (h : StrictMono Q) (hx : x ≠ n) (d : Force) : Felicitous d Q n x ↔ (d = Force.emphatic ↔ x < n)

Under a strictly monotone expressed function an emphatic item needs a low value and an attenuating one a high value.

theorem Israel2001.felicitous_iff_of_strictAnti {α : Type u_1} {W : Type u_2} [LinearOrder α] {Q : α → Set W} {n x : α} (h : StrictAnti Q) (hx : x ≠ n) (d : Force) : Felicitous d Q n x ↔ (d = Force.emphatic ↔ n < x)

Under a strictly antitone one the values are reversed.

def Israel2001.licensingContext (d : Force) (q : Quantity) (r : Role) : Polarity

The direction of the context in which an item of a given force, quantity and role is felicitous, scale preserving (positive) or scale reversing (negative), the scalar logic of Sections 2 and 5: the product of the three signs. Emphatic small items in impeding roles and emphatic large items in facilitating roles are NPIs, needing scale reversal, as are attenuating items of the opposite quantities; the remaining cells are PPIs.

Equations

• Israel2001.licensingContext d q r = d.sign * q.sign * r.sign

theorem Israel2001.Quantity.lt_iff_of_rel {α : Type u_1} [LinearOrder α] {n x : α} {q : Quantity} (hq : q.Rel x n) : x < n ↔ q = small

A quantity standing to the norm as the item says is below it exactly for a small item.

theorem Israel2001.Quantity.gt_iff_of_rel {α : Type u_1} [LinearOrder α] {n x : α} {q : Quantity} (hq : q.Rel x n) : n < x ↔ q = large

And above it exactly for a large item.

theorem Israel2001.felicitous_iff_of_strictMonoBy {α : Type u_1} {W : Type u_2} [LinearOrder α] {Q : α → Set W} {n x : α} {δ : Polarity} {q : Quantity} (h : δ.StrictMonoBy Q) (hq : q.Rel x n) (d : Force) : Felicitous d Q n x ↔ d.sign = δ * q.sign

An item is felicitous exactly when its force has the sign of the direction of the expressed function times that of its quantity.

theorem Israel2001.felicitous_iff {α : Type u_1} {W : Type u_2} [LinearOrder α] {n x : α} {P : α → Set W} {f : Set W → Set W} {r : Role} {c : Polarity} {d : Force} {q : Quantity} (hr : r.sign.StrictMonoBy P) (hc : c.StrictMonoBy f) (hq : q.Rel x n) : Felicitous d (f ∘ P) n x ↔ c = licensingContext d q r

Figures 1 and 3: an item is felicitous exactly in contexts of its licensing direction, for any scalar model of its role and any quantity standing to the norm as the item says.

theorem Israel2001.pecuniary_paradox {α : Type u_1} {W : Type u_2} [LinearOrder α] {n x : α} {res rew : α → Set W} {f : Set W → Set W} (hres : StrictAnti res) (hrew : StrictMono rew) (hf : StrictAnti f) (hx : x < n) : Emphatic (f ∘ res) n x ∧ ¬Emphatic (f ∘ rew) n x ∧ Emphatic rew n x ∧ ¬Emphatic res n x

The pecuniary paradox, (15) and (16): the same small amount is emphatic under negation as a resource, a red cent, and not as a reward, for peanuts, which is emphatic in the affirmative instead.

theorem Israel2001.superlative_ambiguity {α : Type u_1} {W : Type u_2} [LinearOrder α] {n : α} {exist ability : α → Set W} {f : Set W → Set W} (hex : StrictAnti exist) (hab : StrictMono ability) (hf : StrictAnti f) {lo hi : α} (hlo : lo < n) (hhi : n < hi) : Emphatic (f ∘ exist) n lo ∧ Emphatic (f ∘ ability) n hi

Ambiguous superlatives, (22): under negation the same frame is emphatic at the bottom of an existential scale, the faintest noise, and at the top of a perceptual-ability scale, the loudest noise, the stimulus impeding its own existence and facilitating its perception.

The classified lexicon

structure Israel2001.Classified : Type

A fragment entry with the paper's classification by force, quantity and role.

• item : PolarityItem
• force : Force
• quantity : Quantity
• role : Role

def Israel2001.classified : List Classified

The paper's classifications of the fragment's items: the canonical minimizers and the degree items of Figure 1 in impeding roles, the maximizing NPIs and minimizing PPIs of Section 4 in facilitating roles.

Equations

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

def Israel2001.PolarityItem.contextType (e : PolarityItem) : Option Polarity

The direction of the context the fragment records an item as sensitive to: preserving for a PPI, reversing for an NPI.

Equations

• Israel2001.PolarityItem.contextType e = if e.antiLicensor.isSome = true then some Polarity.positive else if e.licensor.isSome = true then some Polarity.negative else none

theorem Israel2001.classified_licensingContext (c : Classified) : c ∈ classified → PolarityItem.contextType c.item = some (licensingContext c.force c.quantity c.role)

Every classified item's derived licensing context is the one the fragment records.