Docs / Semantics / PolarityItem / Licensing

Polarity licensing

import Linglib.Semantics.PolarityItem.Licensing · namespace PolarityItem

A context licenses a polarity item when the licenser it places over the item carries the strength of negation the item needs, after Ladusaw, Zwarts and Gajewski; when it is a modal licenser licensing free choice and the item is a free choice item, after Kadmon and Landman and Chierchia; or when it is a question and the item a weak negative polarity item, after van Rooy. It anti-licenses an item when its licenser holds outright the strength that blocks it, after van der Wouden and Szabolcsi. What each context carries is a theorem about the operators it denotes (Semantics/PolarityItem/LicensingContext.lean), so what it licenses follows from what it means, and each fragment checks the theory against the contexts its entries are attested and excluded in.

Main declarations

PolarityItem.Licenser.Licenses, AntiLicenses, Admits: licensing is a property of the operator over the item's position, so a study can state it of a licenser of its own.
PolarityItem.LicensingContext.licenses_nobody, …: what each named context licenses, as a condition on the item, and the Decidable instances built from these lemmas by cases on the context, so that decide checks an item against any named context.

Main results

Licenser.licenses_iff_carries: an item needing a strength above weak, and not a free choice item, is licensed exactly by the licensers carrying that strength, so an item needing anti-morphic strength is licensed by clausal negation and by no other named context.
LicensingContext.antiLicenses_negation: clausal negation blocks every positive polarity item, van der Wouden's (169).
Licenser.antiLicenses_iff_licenses: a classical licenser blocks the positive polarity items of a class exactly where it licenses the negative polarity items of that class, the mirror image of van der Wouden's (181).

References

Ladusaw 1979, Polarity Sensitivity as Inherent Scope Relations formalized
Kadmon & Landman 1993, Any formalized
Zwarts 1998, Three Types of Polarity
van der Wouden 1997, Negative Contexts: Collocation, Polarity and Multiple Negation formalized
von Fintel 1999, NPI Licensing, Strawson Entailment, and Context Dependency formalized
Gajewski 2011, Licensing Strong NPIs formalized
Szabolcsi 2004, Positive Polarity – Negative Polarity formalized
van Rooy 2003, Negative Polarity Items in Questions: Strength as Relevance
Chierchia 2006, Broaden Your Views: Implicatures of Domain Widening and the “Logicality” of Language formalized

Declarations

A context licenses an item when its licenser carries the item's licensor, licenses free choice and the item is a free choice item, or licenses by relevance and the item is a weak negative polarity item.

def Licenser.Licenses L62–67

(L : Licenser) (e : PolarityItem) :

L.Licenses e = ((∃ r ∈ e.licensor, L.Carries r) ∨ L.LicensesFreeChoice ∧ e.IsFCI ∨ L.LicensesByRelevance ∧ e.licensor = some Negation.Strength.weak)

Instances BylininaNouwen2018.instDecidablePredPolarityItemLicensesDenote, BylininaNouwen2018.instDecidablePredPolarityItemLicensesZero

Used by Licenser.Admits, Licenser.admits_iff_licenses, Licenser.instDecidablePredAdmitsOfLicensesOfAntiLicenses, Licenser.licenses_iff_carries, Licenser.antiLicenses_iff_licenses, Licenser.Licenses.of_licensor_le, LicensingContext.licenses_negation, LicensingContext.licenses_nobody, LicensingContext.licenses_few, LicensingContext.licenses_atMost, LicensingContext.licenses_universalRestrictor, LicensingContext.licenses_withoutClause, LicensingContext.licenses_beforeClause, LicensingContext.licenses_clausalComparative, LicensingContext.licenses_tooTo, LicensingContext.licenses_doubtVerb, LicensingContext.licenses_denyVerb, LicensingContext.licenses_onlyFocus, LicensingContext.licenses_adversative, LicensingContext.licenses_superlative, LicensingContext.licenses_conditionalAntecedent, LicensingContext.licenses_sinceTemporal, LicensingContext.licenses_question, LicensingContext.licenses_modalPossibility, LicensingContext.licenses_modalNecessity, LicensingContext.licenses_imperative, LicensingContext.licenses_generic, LicensingContext.licenses_freeRelative, LicensingContext.instDecidablePredLicensesLicenser, LicensingContext.instDecidablePredAdmitsLicenser

Used in Fragments/Hungarian/PolarityItems, Fragments/Japanese/PolarityItems, Fragments/Korean/PolarityItems, Fragments/Mandarin/PolarityItems, Fragments/Slavic/Czech/PolarityItems and 9 more

A context anti-licenses an item when its licenser holds outright the strength that blocks the item.

def Licenser.AntiLicenses L69–71

(L : Licenser) (e : PolarityItem) :

L.AntiLicenses e = ∃ r ∈ e.antiLicensor, L.Holds r.toProjectivitySignature

Used by Licenser.Admits, Licenser.admits_iff_not_antiLicenses, Licenser.not_antiLicenses_modal, Licenser.instDecidablePredAdmitsOfLicensesOfAntiLicenses, Licenser.antiLicenses_iff_licenses, LicensingContext.antiLicenses_negation_iff, LicensingContext.antiLicenses_nobody, LicensingContext.antiLicenses_few, LicensingContext.antiLicenses_atMost, LicensingContext.antiLicenses_universalRestrictor, LicensingContext.antiLicenses_withoutClause, LicensingContext.antiLicenses_beforeClause, LicensingContext.antiLicenses_clausalComparative, LicensingContext.antiLicenses_tooTo, LicensingContext.antiLicenses_doubtVerb, LicensingContext.antiLicenses_denyVerb, LicensingContext.not_antiLicenses_onlyFocus, LicensingContext.not_antiLicenses_adversative, LicensingContext.not_antiLicenses_superlative, LicensingContext.not_antiLicenses_conditionalAntecedent, LicensingContext.not_antiLicenses_sinceTemporal, LicensingContext.not_antiLicenses_question, LicensingContext.not_antiLicenses_modalPossibility, LicensingContext.not_antiLicenses_modalNecessity, LicensingContext.not_antiLicenses_imperative, LicensingContext.not_antiLicenses_generic, LicensingContext.not_antiLicenses_freeRelative, LicensingContext.instDecidablePredAntiLicensesLicenser, LicensingContext.instDecidablePredAdmitsLicenser, LicensingContext.antiLicenses_negation

Used in Fragments/Slavic/Czech/PolarityItems, Ladusaw1979, Szabolcsi2004

A context admits an item when it licenses the item, if the item needs licensing, and does not anti-license it.

def Licenser.Admits L73–75

(L : Licenser) (e : PolarityItem) :

L.Admits e = ((e.IsNPI ∨ e.IsFCI → L.Licenses e) ∧ ¬L.AntiLicenses e)

Built from ,

Used by Licenser.admits_iff_licenses, Licenser.admits_iff_not_antiLicenses, Licenser.instDecidablePredAdmitsOfLicensesOfAntiLicenses, LicensingContext.instDecidablePredAdmitsLicenser

Used in Fragments/Finnish/PolarityItems, Fragments/German/PolarityItems, Fragments/Hungarian/PolarityItems, Fragments/Japanese/PolarityItems, Fragments/Korean/PolarityItems and 11 more

The profiles of the licensers

The theory

An item needing a strength above weak, and not a free choice item, is licensed exactly by the contexts whose licenser carries that strength.

theorem Licenser.licenses_iff_carries L136–146

{L : Licenser} {e : PolarityItem} {r : Negation.Strength} (he : e.licensor = some r) (hr : r ≠ Negation.Strength.weak) (hf : ¬e.IsFCI) :

L.Licenses e ↔ L.Carries r

Built from

A non-trivial classical context anti-licenses a class's PPIs exactly where it licenses its NPIs (mirroring van der Wouden 1997's (181)).

theorem Licenser.antiLicenses_iff_licenses L148–157

{L : Licenser} {e e' : PolarityItem} {F : OperatorFamily} (hc : L = classical F) (hn : ¬L.IsStrawsonUE) (h : e.antiLicensor = e'.licensor) :

L.AntiLicenses e ↔ L.Licenses e'

Built from ,

@[simp] theorem LicensingContext.licenses_nobody L194–196

{e : PolarityItem} :

nobody.licenser.Licenses e ↔ ∃ r ∈ e.licensor, r ≤ Negation.Strength.antiAdditive

Built from

Deciding licensing at the named contexts

What a named context licenses and anti-licenses is decided by the item, through the lemmas above.

Clausal negation blocks every positive polarity item, since its licenser holds the top of the chain (van der Wouden 1997's (169)).

theorem LicensingContext.antiLicenses_negation L408–411

{e : PolarityItem} (h : e.IsPPI) :

negation.licenser.AntiLicenses e

Built from