Gajewski (2011): Licensing strong NPIs

Gajewski explains why weak negative polarity items (any, ever) and strong ones (in weeks, either, until) part ways under only, conditional antecedents and sorry. These operators are Strawson anti-additive, the Strawson form of the anti-additivity Zwarts held strong items to need, yet they license only weak items. The two classes inspect different meanings: a weak item needs the plain meaning Strawson downward entailing, while a strong item needs the meaning enriched by Chierchia's exhaustivity operator, presuppositions included, downward entailing outright. A determiner at the bottom of its Horn scale, no, is its own enriched meaning and licenses both; one above the bottom exhaustifies to a meaning with an upward-entailing conjunct; and a presupposition trigger's full meaning fails plain downward entailment.

Main results

• strawsonAA_not_sufficient: only, would and sorry are Strawson anti-additive, yet their meanings are not downward entailing outright.
• licensed_iff: no is the only licenser of strong items and some the only non-licenser of weak ones, and rows_predicted checks this against the paper's judgments.
• isIntolerant_of_isAntiAdditive, few_isIntolerant, atMostThree_not_isIntolerant: Horn's Intolerance sits strictly between anti-additivity and downward entailment.

Implementation notes

• Entailment between scale-mates holds the restrictor fixed and quantifies over scopes, so no entails not every whenever the restrictor is nonempty, which is what makes no the bottom of its scale; letting the restrictor vary would break the entailment at an empty restrictor. The scale is the pair of ends the paper's computation of exhaustified not every uses.
• The presupposition triggers have no scale-mates, so their enriched meaning is their full meaning, presupposition included, and the strong principle asks for its plain downward entailment. The operators are von Fintel's, with their owners, and their Strawson properties are in Logic/Natural/Strawson.lean.
• At most five against at most four, and the cardinal fewer than four of the scale-truncation discussion, are checked on a six-element domain.

References

• [Gaj11]
• [vF99a]
• [Zwa98]
• [Chi06]
• [Hor89]

Enriched meanings

theorem Gajewski2011.exhaustified_notEvery {α : Type u_1} {A : α → Prop} {x y : α} (hx : A x) (hy : A y) (hxy : x ≠ y) : Quantifier.GQ.everyᶜ.exhaustified {Quantifier.GQ.no} A = fun (P : α → Prop) => Quantifier.GQ.some A P ∧ Quantifier.GQ.everyᶜ A P

Exhaustified not every is some but not every once the restrictor has two elements.

theorem Gajewski2011.not_scopeAntitone_exhaustified {α : Type u_1} {Q : Quantifier.GQ α} {C : Set (Quantifier.GQ α)} {A P : α → Prop} (hP : Q.exhaustified C A P) (h : ¬Q.exhaustified C A fun (x : α) => False) : ¬(Q.exhaustified C).ScopeAntitone

An enriched meaning satisfiable at a restrictor but excluded at the empty scope is not downward entailing in its scope.

The licensing principles

theorem Gajewski2011.no_strong {α : Type u_1} : (Quantifier.GQ.no.exhaustified {Quantifier.GQ.everyᶜ}).ScopeAntitone

Exhaustified no is downward entailing, so no licenses strong items.

theorem Gajewski2011.notEvery_not_strong {α : Type u_1} [Nontrivial α] : ¬(Quantifier.GQ.everyᶜ.exhaustified {Quantifier.GQ.no}).ScopeAntitone

Exhaustified not every is not downward entailing, since at the empty scope the stronger scale-mate no is true and excluded.

theorem Gajewski2011.some_not_strong {α : Type u_1} [Nontrivial α] : ¬(Quantifier.GQ.some.exhaustified {Quantifier.GQ.every}).ScopeAntitone

Exhaustified some is not downward entailing, since some itself fails at the empty scope.

theorem Gajewski2011.atMostFive_not_strong : ¬((Quantifier.GQ.atMost 5).exhaustified {Quantifier.GQ.atMost 4}).ScopeAntitone

At most five sits above at most four on its scale; excluding the scale-mate leaves exactly five, which is not downward entailing.

inductive Gajewski2011.Licenser : Type

The paper's licensers.

• no : Licenser
• atMostFive : Licenser
• some : Licenser
• only : Licenser
• conditional : Licenser
• sorryThat : Licenser

@[instance_reducible]

instance Gajewski2011.instDecidableEqLicenser : DecidableEq Licenser

Equations

• Gajewski2011.instDecidableEqLicenser x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Gajewski2011.instReprLicenser.repr : Licenser → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Gajewski2011.instReprLicenser : Repr Licenser

Equations

• Gajewski2011.instReprLicenser = { reprPrec := Gajewski2011.instReprLicenser.repr }

inductive Gajewski2011.Strength : Type

Weak items are any and ever, strong ones in weeks, either and until.

• weak : Strength
• strong : Strength

@[instance_reducible]

instance Gajewski2011.instDecidableEqStrength : DecidableEq Strength

Equations

• Gajewski2011.instDecidableEqStrength x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Gajewski2011.instReprStrength.repr : Strength → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Gajewski2011.instReprStrength : Repr Strength

Equations

• Gajewski2011.instReprStrength = { reprPrec := Gajewski2011.instReprStrength.repr }

def Gajewski2011.Licensed : Licenser → Strength → Prop

The two licensing principles applied to a licenser's analysis, on which a weak item needs the plain meaning Strawson downward entailing and a strong item needs the enriched meaning downward entailing, which for a presupposition trigger without scale-mates is its full meaning.

Equations

• One or more equations did not get rendered due to their size.
• Gajewski2011.Licensed Gajewski2011.Licenser.no Gajewski2011.Strength.weak = ∀ {α : Type}, Quantifier.GQ.no.ScopeAntitone
• Gajewski2011.Licensed Gajewski2011.Licenser.no Gajewski2011.Strength.strong = ∀ {α : Type}, (Quantifier.GQ.no.exhaustified {Quantifier.GQ.everyᶜ}).ScopeAntitone
• Gajewski2011.Licensed Gajewski2011.Licenser.atMostFive Gajewski2011.Strength.weak = ∀ {α : Type} [Fintype α], (Quantifier.GQ.atMost 5).ScopeAntitone
• Gajewski2011.Licensed Gajewski2011.Licenser.atMostFive Gajewski2011.Strength.strong = ∀ {α : Type} [Fintype α], ((Quantifier.GQ.atMost 5).exhaustified {Quantifier.GQ.atMost 4}).ScopeAntitone
• Gajewski2011.Licensed Gajewski2011.Licenser.some Gajewski2011.Strength.weak = ∀ {α : Type}, Quantifier.GQ.some.ScopeAntitone
• Gajewski2011.Licensed Gajewski2011.Licenser.some Gajewski2011.Strength.strong = ∀ {α : Type}, (Quantifier.GQ.some.exhaustified {Quantifier.GQ.every}).ScopeAntitone
• Gajewski2011.Licensed Gajewski2011.Licenser.only Gajewski2011.Strength.weak = ∀ {ι W : Type} (x : ι), NaturalLogic.IsStrawsonDE (NaturalLogic.only x)
• Gajewski2011.Licensed Gajewski2011.Licenser.only Gajewski2011.Strength.strong = ∀ {ι W : Type} (x : ι), Antitone fun (P : ι → Set W) => Trivalent.posExt (NaturalLogic.only x P)

theorem Gajewski2011.strawsonAA_not_sufficient : (∀ {ι W : Type} (x : ι), NaturalLogic.IsStrawsonAntiAdditive (NaturalLogic.only x)) ∧ (∀ {W : Type} (horizon : W → Set W) (q : Set W), NaturalLogic.IsStrawsonAntiAdditive fun (x : Set W) => Conditional.horizonCounterfactual horizon x q) ∧ (∀ {W : Type} (dox base : W → Set W) (g : W → Set (W → Prop)), NaturalLogic.IsStrawsonAntiAdditive (Desire.BestWorlds.regret dox base g)) ∧ ¬Licensed Licenser.only Strength.strong ∧ ¬Licensed Licenser.conditional Strength.strong ∧ ¬Licensed Licenser.sorryThat Strength.strong

The puzzle is that only, would and sorry are Strawson anti-additive, the Strawson form of what strong items were held to need, yet none licenses them.

theorem Gajewski2011.licensed_strong_iff (L : Licenser) : Licensed L Strength.strong ↔ L = Licenser.no

No is the only one of the paper's licensers whose enriched meaning is downward entailing.

theorem Gajewski2011.licensed_weak_iff (L : Licenser) : Licensed L Strength.weak ↔ L ≠ Licenser.some

Some is the only one of the paper's licensers whose plain meaning is not Strawson downward entailing.

theorem Gajewski2011.licensed_iff (L : Licenser) (s : Strength) : Licensed L s ↔ s = Strength.weak ∧ L ≠ Licenser.some ∨ s = Strength.strong ∧ L = Licenser.no

The library's licensing

The library keeps Zwarts's strengths and asks for them of the meaning with the licenser's direct implicature factored in, where the principles ask only for downward entailment of that meaning; on the paper's licensers the two agree, as the paper's conjecture (48) has it for scale endpoints.

def Gajewski2011.Licenser.context : Licenser → Option PolarityItem.LicensingContext

The library's context for each licenser that has one. Some NP licenses nothing and has none.

Equations

• Gajewski2011.Licenser.no.context = some PolarityItem.LicensingContext.nobody
• Gajewski2011.Licenser.atMostFive.context = some PolarityItem.LicensingContext.atMost
• Gajewski2011.Licenser.some.context = none
• Gajewski2011.Licenser.only.context = some PolarityItem.LicensingContext.onlyFocus
• Gajewski2011.Licenser.conditional.context = some PolarityItem.LicensingContext.conditionalAntecedent
• Gajewski2011.Licenser.sorryThat.context = some PolarityItem.LicensingContext.adversative

def Gajewski2011.Strength.item : Strength → PolarityItem

An English item of each strength, ever and in years.

Equations

• Gajewski2011.Strength.weak.item = English.PolarityItems.ever
• Gajewski2011.Strength.strong.item = English.PolarityItems.inYears

theorem Gajewski2011.licensed_iff_licenses (L : Licenser) (s : Strength) {c : PolarityItem.LicensingContext} (hc : L.context = some c) : Licensed L s ↔ c.licenser.Licenses s.item

The two principles agree with the library's licensing on every licenser it has a context for.

Intolerance

def Gajewski2011.IsTrivial {α : Type u_1} (f : Set α → Prop) : Prop

A function of properties is trivial when it is constantly true or constantly false.

Equations

• Gajewski2011.IsTrivial f = ((∀ (x : Set α), f x) ∨ ∀ (x : Set α), ¬f x)

def Gajewski2011.IsIntolerant {α : Type u_1} (f : Set α → Prop) : Prop

A nontrivial function of properties is Intolerant when it never accepts both a property and its complement, as the items above the midpoint of their scale do ([Hor89]).

Equations

• Gajewski2011.IsIntolerant f = (¬Gajewski2011.IsTrivial f → ∀ (x : Set α), ¬f x ∨ ¬f xᶜ)

theorem Gajewski2011.isIntolerant_of_isAntiAdditive {α : Type u_1} {f : Set α → Prop} (h : NaturalLogic.IsAntiAdditive f) : IsIntolerant f

Anti-additivity implies Intolerance, since accepting x and xᶜ means accepting everything.

theorem Gajewski2011.few_isIntolerant {α : Type u_1} (A : α → Prop) : IsIntolerant (Quantifier.GQ.few A)

Proportional few is Intolerant, since fewer than half in and fewer than half out is impossible.

theorem Gajewski2011.atMostThree_not_isIntolerant : ¬IsIntolerant (Quantifier.GQ.atMost 3 fun (x : Fin 6) => True)

Cardinal fewer than four is not Intolerant, since with six elements three are in and three out.

theorem Gajewski2011.few_not_rightAntiAdditive : ¬Quantifier.GQ.few.RightAntiAdditive

Proportional few is downward entailing and Intolerant but not anti-additive, so Intolerance is a proper intermediate between anti-additivity and downward entailment.

The paper's sentences

structure Gajewski2011.Row : Type

A sentence of the paper records its licenser, the strength of its polarity item, and the judgment.

• licenser : Licenser
• strength : Strength
• judgment : Judgment

@[instance_reducible]

instance Gajewski2011.instDecidableEqRow : DecidableEq Row

Equations

• Gajewski2011.instDecidableEqRow = Gajewski2011.instDecidableEqRow.decEq

def Gajewski2011.instDecidableEqRow.decEq (x✝ x✝¹ : Row) : Decidable (x✝ = x✝¹)

Equations

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

def Gajewski2011.instReprRow.repr : Row → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Gajewski2011.instReprRow : Repr Row

Equations

• Gajewski2011.instReprRow = { reprPrec := Gajewski2011.instReprRow.repr }

def Gajewski2011.Row.ofDatum (ex : Datum) : Option Row

Equations

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

def Gajewski2011.rows : List Row

Equations

• Gajewski2011.rows = List.filterMap Gajewski2011.Row.ofDatum Gajewski2011.Examples.all

theorem Gajewski2011.rows_predicted (r : Row) : r ∈ rows → (r.judgment = Judgment.acceptable ↔ Licensed r.licenser r.strength)

Every judgment in the paper follows from the two licensing principles.