Documentation

Linglib.Semantics.Polarity.Licensing

Polarity licensing #

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/Polarity/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 #

Main results #

References #

source
def PolarityItem.Licenser.Licenses (L : Licenser) (e : PolarityItem) :
Prop

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.

Equations
Instances For
    source
    def PolarityItem.Licenser.AntiLicenses (L : Licenser) (e : PolarityItem) :
    Prop

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

    Equations
    Instances For
      source
      def PolarityItem.Licenser.Admits (L : Licenser) (e : PolarityItem) :
      Prop

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

      Equations
      Instances For
        source
        theorem PolarityItem.Licenser.admits_iff_licenses {L : Licenser} {e : PolarityItem} (h : e.antiLicensor = none) (he : e.IsNPI ∨ e.IsFCI) :
        L.Admits e ↔ L.Licenses e
        source
        theorem PolarityItem.Licenser.admits_iff_not_antiLicenses {L : Licenser} {e : PolarityItem} (hn : ¬e.IsNPI) (hf : ¬e.IsFCI) :
        L.Admits e ↔ ¬L.AntiLicenses e

        The profiles of the licensers #

        source
        @[simp]
        theorem PolarityItem.Licenser.not_antiLicenses_modal {L : Licenser} {e : PolarityItem} {F : ModalFamily} (hc : L = modal F) :
        ¬L.AntiLicenses e
        source
        @[instance_reducible]
        instance PolarityItem.Licenser.instDecidablePredAdmitsOfLicensesOfAntiLicenses {L : Licenser} [DecidablePred L.Licenses] [DecidablePred L.AntiLicenses] :
        DecidablePred L.Admits
        Equations

        The theory #

        source
        theorem PolarityItem.Licenser.licenses_iff_carries {L : Licenser} {e : PolarityItem} {r : DEStrength} (he : e.licensor = some r) (hr : r ≠ DEStrength.weak) (hf : ¬e.IsFCI) :
        L.Licenses e ↔ L.Carries r

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

        source
        theorem PolarityItem.Licenser.antiLicenses_iff_licenses {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'

        A non-trivial classical context blocks the positive polarity items of a class exactly where it licenses the negative polarity items of that class (the mirror image of [vdW97]'s (181)).

        source
        theorem PolarityItem.Licenser.Licenses.of_licensor_le {L : Licenser} {e e' : PolarityItem} {r r' : DEStrength} (he : e.licensor = some r) (he' : e'.licensor = some r') (hr : r' ≤ r) (hf : e.IsFCI → e'.IsFCI) (hl : L.Licenses e) :
        L.Licenses e'

        A context licensing an item licenses every item with a weaker licensor that is a free choice item if the first is.

        source
        @[simp]
        theorem PolarityItem.LicensingContext.licenses_negation {e : PolarityItem} :
        negation.licenser.Licenses e ↔ e.IsNPI
        source
        @[simp]
        theorem PolarityItem.LicensingContext.antiLicenses_negation_iff {e : PolarityItem} :
        negation.licenser.AntiLicenses e ↔ e.IsPPI
        source
        @[simp]
        theorem PolarityItem.LicensingContext.licenses_nobody {e : PolarityItem} :
        nobody.licenser.Licenses e ↔ ∃ r ∈ e.licensor, r ≤ DEStrength.antiAdditive
        source
        @[simp]
        theorem PolarityItem.LicensingContext.antiLicenses_nobody {e : PolarityItem} :
        nobody.licenser.AntiLicenses e ↔ ∃ r ∈ e.antiLicensor, r ≤ DEStrength.antiAdditive
        source
        @[simp]
        theorem PolarityItem.LicensingContext.licenses_few {e : PolarityItem} :
        few.licenser.Licenses e ↔ ∃ r ∈ e.licensor, r ≤ DEStrength.weak
        source
        @[simp]
        theorem PolarityItem.LicensingContext.antiLicenses_few {e : PolarityItem} :
        few.licenser.AntiLicenses e ↔ ∃ r ∈ e.antiLicensor, r ≤ DEStrength.weak
        source
        @[simp]
        theorem PolarityItem.LicensingContext.licenses_atMost {e : PolarityItem} :
        atMost.licenser.Licenses e ↔ ∃ r ∈ e.licensor, r ≤ DEStrength.weak
        source
        @[simp]
        theorem PolarityItem.LicensingContext.antiLicenses_atMost {e : PolarityItem} :
        atMost.licenser.AntiLicenses e ↔ ∃ r ∈ e.antiLicensor, r ≤ DEStrength.weak
        source
        @[simp]
        theorem PolarityItem.LicensingContext.licenses_universalRestrictor {e : PolarityItem} :
        universalRestrictor.licenser.Licenses e ↔ ∃ r ∈ e.licensor, r ≤ DEStrength.antiAdditive
        source
        @[simp]
        theorem PolarityItem.LicensingContext.antiLicenses_universalRestrictor {e : PolarityItem} :
        universalRestrictor.licenser.AntiLicenses e ↔ ∃ r ∈ e.antiLicensor, r ≤ DEStrength.antiAdditive
        source
        @[simp]
        theorem PolarityItem.LicensingContext.licenses_withoutClause {e : PolarityItem} :
        withoutClause.licenser.Licenses e ↔ ∃ r ∈ e.licensor, r ≤ DEStrength.antiAdditive
        source
        @[simp]
        theorem PolarityItem.LicensingContext.antiLicenses_withoutClause {e : PolarityItem} :
        withoutClause.licenser.AntiLicenses e ↔ ∃ r ∈ e.antiLicensor, r ≤ DEStrength.antiAdditive
        source
        @[simp]
        theorem PolarityItem.LicensingContext.licenses_beforeClause {e : PolarityItem} :
        beforeClause.licenser.Licenses e ↔ ∃ r ∈ e.licensor, r ≤ DEStrength.antiAdditive
        source
        @[simp]
        theorem PolarityItem.LicensingContext.antiLicenses_beforeClause {e : PolarityItem} :
        beforeClause.licenser.AntiLicenses e ↔ ∃ r ∈ e.antiLicensor, r ≤ DEStrength.antiAdditive
        source
        @[simp]
        theorem PolarityItem.LicensingContext.licenses_clausalComparative {e : PolarityItem} :
        clausalComparative.licenser.Licenses e ↔ ∃ r ∈ e.licensor, r ≤ DEStrength.antiAdditive
        source
        @[simp]
        theorem PolarityItem.LicensingContext.antiLicenses_clausalComparative {e : PolarityItem} :
        clausalComparative.licenser.AntiLicenses e ↔ ∃ r ∈ e.antiLicensor, r ≤ DEStrength.antiAdditive
        source
        @[simp]
        theorem PolarityItem.LicensingContext.licenses_tooTo {e : PolarityItem} :
        tooTo.licenser.Licenses e ↔ ∃ r ∈ e.licensor, r ≤ DEStrength.antiAdditive
        source
        @[simp]
        theorem PolarityItem.LicensingContext.antiLicenses_tooTo {e : PolarityItem} :
        tooTo.licenser.AntiLicenses e ↔ ∃ r ∈ e.antiLicensor, r ≤ DEStrength.antiAdditive
        source
        @[simp]
        theorem PolarityItem.LicensingContext.licenses_doubtVerb {e : PolarityItem} :
        doubtVerb.licenser.Licenses e ↔ ∃ r ∈ e.licensor, r ≤ DEStrength.weak
        source
        @[simp]
        theorem PolarityItem.LicensingContext.antiLicenses_doubtVerb {e : PolarityItem} :
        doubtVerb.licenser.AntiLicenses e ↔ ∃ r ∈ e.antiLicensor, r ≤ DEStrength.weak
        source
        @[simp]
        theorem PolarityItem.LicensingContext.licenses_denyVerb {e : PolarityItem} :
        denyVerb.licenser.Licenses e ↔ ∃ r ∈ e.licensor, r ≤ DEStrength.antiAdditive
        source
        @[simp]
        theorem PolarityItem.LicensingContext.antiLicenses_denyVerb {e : PolarityItem} :
        denyVerb.licenser.AntiLicenses e ↔ ∃ r ∈ e.antiLicensor, r ≤ DEStrength.antiAdditive
        source
        @[simp]
        theorem PolarityItem.LicensingContext.licenses_onlyFocus {e : PolarityItem} :
        onlyFocus.licenser.Licenses e ↔ e.licensor = some DEStrength.weak
        source
        @[simp]
        theorem PolarityItem.LicensingContext.not_antiLicenses_onlyFocus {e : PolarityItem} :
        ¬onlyFocus.licenser.AntiLicenses e
        source
        @[simp]
        theorem PolarityItem.LicensingContext.licenses_adversative {e : PolarityItem} :
        adversative.licenser.Licenses e ↔ e.licensor = some DEStrength.weak
        source
        @[simp]
        theorem PolarityItem.LicensingContext.not_antiLicenses_adversative {e : PolarityItem} :
        ¬adversative.licenser.AntiLicenses e
        source
        @[simp]
        theorem PolarityItem.LicensingContext.licenses_superlative {e : PolarityItem} :
        superlative.licenser.Licenses e ↔ e.licensor = some DEStrength.weak
        source
        @[simp]
        theorem PolarityItem.LicensingContext.not_antiLicenses_superlative {e : PolarityItem} :
        ¬superlative.licenser.AntiLicenses e
        source
        @[simp]
        theorem PolarityItem.LicensingContext.licenses_conditionalAntecedent {e : PolarityItem} :
        conditionalAntecedent.licenser.Licenses e ↔ e.licensor = some DEStrength.weak
        source
        @[simp]
        theorem PolarityItem.LicensingContext.not_antiLicenses_conditionalAntecedent {e : PolarityItem} :
        ¬conditionalAntecedent.licenser.AntiLicenses e
        source
        @[simp]
        theorem PolarityItem.LicensingContext.licenses_sinceTemporal {e : PolarityItem} :
        sinceTemporal.licenser.Licenses e ↔ e.licensor = some DEStrength.weak
        source
        @[simp]
        theorem PolarityItem.LicensingContext.not_antiLicenses_sinceTemporal {e : PolarityItem} :
        ¬sinceTemporal.licenser.AntiLicenses e
        source
        @[simp]
        theorem PolarityItem.LicensingContext.licenses_question {e : PolarityItem} :
        question.licenser.Licenses e ↔ e.licensor = some DEStrength.weak
        source
        @[simp]
        theorem PolarityItem.LicensingContext.not_antiLicenses_question {e : PolarityItem} :
        ¬question.licenser.AntiLicenses e
        source
        @[simp]
        theorem PolarityItem.LicensingContext.licenses_modalPossibility {e : PolarityItem} :
        modalPossibility.licenser.Licenses e ↔ e.IsFCI
        source
        @[simp]
        theorem PolarityItem.LicensingContext.licenses_modalNecessity {e : PolarityItem} :
        modalNecessity.licenser.Licenses e ↔ e.IsFCI
        source
        @[simp]
        theorem PolarityItem.LicensingContext.licenses_imperative {e : PolarityItem} :
        imperative.licenser.Licenses e ↔ e.IsFCI
        source
        @[simp]
        theorem PolarityItem.LicensingContext.licenses_generic {e : PolarityItem} :
        generic.licenser.Licenses e ↔ e.IsFCI
        source
        @[simp]
        theorem PolarityItem.LicensingContext.licenses_freeRelative {e : PolarityItem} :
        freeRelative.licenser.Licenses e ↔ e.IsFCI
        source
        @[simp]
        theorem PolarityItem.LicensingContext.not_antiLicenses_modalPossibility {e : PolarityItem} :
        ¬modalPossibility.licenser.AntiLicenses e
        source
        @[simp]
        theorem PolarityItem.LicensingContext.not_antiLicenses_modalNecessity {e : PolarityItem} :
        ¬modalNecessity.licenser.AntiLicenses e
        source
        @[simp]
        theorem PolarityItem.LicensingContext.not_antiLicenses_imperative {e : PolarityItem} :
        ¬imperative.licenser.AntiLicenses e
        source
        @[simp]
        theorem PolarityItem.LicensingContext.not_antiLicenses_generic {e : PolarityItem} :
        ¬generic.licenser.AntiLicenses e
        source
        @[simp]
        theorem PolarityItem.LicensingContext.not_antiLicenses_freeRelative {e : PolarityItem} :
        ¬freeRelative.licenser.AntiLicenses e

        Deciding licensing at the named contexts #

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

        source
        @[instance_reducible]
        instance PolarityItem.LicensingContext.instDecidablePredLicensesLicenser (c : LicensingContext) :
        DecidablePred c.licenser.Licenses
        Equations
        source
        @[instance_reducible]
        instance PolarityItem.LicensingContext.instDecidablePredAntiLicensesLicenser (c : LicensingContext) :
        DecidablePred c.licenser.AntiLicenses
        Equations
        source
        @[instance_reducible]
        instance PolarityItem.LicensingContext.instDecidablePredAdmitsLicenser (c : LicensingContext) :
        DecidablePred c.licenser.Admits

        Admission at a named context is decided without computing its licenser.

        Equations
        source
        theorem PolarityItem.LicensingContext.antiLicenses_negation {e : PolarityItem} (h : e.IsPPI) :
        negation.licenser.AntiLicenses e

        Clausal negation blocks every positive polarity item, since its licenser holds the top of the chain ([vdW97]'s (169)).