Documentation

Linglib.Phenomena.Polarity.Studies.Ladusaw1979

Ladusaw (1979): Polarity Sensitivity as Inherent Scope Relations #

@cite{ladusaw-1979}

Ladusaw's dissertation established the foundational generalization connecting NPI licensing to downward entailingness (DE). The core claim:

Weak NPIs are licensed in downward-entailing contexts.

This file bridges the GQ monotonicity proofs from Core.Quantification and Semantics.Lexical.Determiner.Quantifier to the NPI licensing data in Phenomena.Polarity.NPIs, making the DE ↔ NPI connection formally explicit.

Key connections #

  1. Scope DE → weak NPI licensing: ScopeDownwardMono licenses weak NPIs in the scope of a quantifier (e.g., "No student saw anyone").
  2. Restrictor DE → weak NPI licensing: RestrictorDownwardMono licenses weak NPIs in the restrictor (e.g., "Everyone who saw anyone was questioned").
  3. Left anti-additivity → strong NPI licensing: LeftAntiAdditive licenses strong NPIs (e.g., "Nobody lifted a finger"). Mere DE ("few") is insufficient for strong NPIs.
source
inductive Phenomena.Polarity.Studies.Ladusaw1979.LicensingStrength :
Type

The monotonicity-based licensing strength of a context. @cite{ladusaw-1979}: DE licenses weak NPIs. @cite{zwarts-1998}: anti-additive licenses strong NPIs.

Instances For
    source
    instance Phenomena.Polarity.Studies.Ladusaw1979.instDecidableEqLicensingStrength :
    DecidableEq LicensingStrength
    Equations
    source
    def Phenomena.Polarity.Studies.Ladusaw1979.instBEqLicensingStrength.beq :
    LicensingStrength → LicensingStrength → Bool
    Equations
    Instances For
      source
      instance Phenomena.Polarity.Studies.Ladusaw1979.instBEqLicensingStrength :
      BEq LicensingStrength
      Equations
      source
      instance Phenomena.Polarity.Studies.Ladusaw1979.instReprLicensingStrength :
      Repr LicensingStrength
      Equations
      source
      def Phenomena.Polarity.Studies.Ladusaw1979.instReprLicensingStrength.repr :
      LicensingStrength → ℕ → Std.Format
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Phenomena.Polarity.Studies.Ladusaw1979.licensingStrength :
        NPIs.LicensingContext → LicensingStrength

        Classify NPI licensing contexts by their monotonicity-based strength. Anti-additive contexts (negation, "without", "no one", universal restrictor) license strong NPIs. Merely DE contexts ("few", conditionals) license only weak NPIs. Non-DE contexts (questions, superlatives) license NPIs via other mechanisms.

        Equations
        Instances For
          source
          structure Phenomena.Polarity.Studies.Ladusaw1979.ScopeDELicensesWeakNPIs {m : Semantics.Montague.Model} (q : m.interpTy Semantics.Lexical.Determiner.Quantifier.Ty.det) :
          Type

          The core Ladusaw generalization: scope-DE quantifiers license weak NPIs in their scope. Formally: ScopeDownwardMono q implies that the scope of q is a weak-NPI-licensing environment.

          Verified instances:

          • no_scope_down: "No student saw anyone" ✓
          • few_scope_down: "Few students saw anyone" ✓
          Instances For
            source
            def Phenomena.Polarity.Studies.Ladusaw1979.no_scope_licenses_weak {m : Semantics.Montague.Model} [Fintype m.Entity] :
            ScopeDELicensesWeakNPIs (Semantics.Lexical.Determiner.Quantifier.no_sem m)

            "No" licenses weak NPIs in scope via scope-↓ monotonicity.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Phenomena.Polarity.Studies.Ladusaw1979.few_scope_licenses_weak {m : Semantics.Montague.Model} [Fintype m.Entity] :
              ScopeDELicensesWeakNPIs (Semantics.Lexical.Determiner.Quantifier.few_sem m)

              "Few" licenses weak NPIs in scope via scope-↓ monotonicity.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                structure Phenomena.Polarity.Studies.Ladusaw1979.RestrictorDELicensesWeakNPIs {m : Semantics.Montague.Model} (q : m.interpTy Semantics.Lexical.Determiner.Quantifier.Ty.det) :
                Type

                The restrictor Ladusaw generalization: restrictor-DE quantifiers license weak NPIs in their restrictor.

                Verified instances:

                • every_restrictor_down: "Everyone who saw anyone was questioned" ✓
                • no_restrictor_down: "No one who saw anyone was questioned" ✓
                Instances For
                  source
                  def Phenomena.Polarity.Studies.Ladusaw1979.every_restrictor_licenses_weak {m : Semantics.Montague.Model} [Fintype m.Entity] :
                  RestrictorDELicensesWeakNPIs (Semantics.Lexical.Determiner.Quantifier.every_sem m)

                  "Every" licenses weak NPIs in restrictor via restrictor-↓ monotonicity.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def Phenomena.Polarity.Studies.Ladusaw1979.no_restrictor_licenses_weak {m : Semantics.Montague.Model} [Fintype m.Entity] :
                    RestrictorDELicensesWeakNPIs (Semantics.Lexical.Determiner.Quantifier.no_sem m)

                    "No" licenses weak NPIs in restrictor via restrictor-↓ monotonicity.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      structure Phenomena.Polarity.Studies.Ladusaw1979.AntiAddLicensesStrongNPIs {m : Semantics.Montague.Model} (q : m.interpTy Semantics.Lexical.Determiner.Quantifier.Ty.det) :
                      Type

                      @cite{zwarts-1998}: anti-additive contexts license strong NPIs. LeftAntiAdditive q means the restrictor of q is anti-additive, licensing strong NPIs like "lift a finger" and "in years".

                      Verified instances:

                      • every_laa: "Everyone who ever lifted a finger..." ✓
                      • no_laa: "Nobody lifted a finger" ✓

                      Counter-example: "few" is merely DE, not anti-additive:

                      • *"Few people lifted a finger to help" ✗
                      Instances For
                        source
                        def Phenomena.Polarity.Studies.Ladusaw1979.every_laa_licenses_strong {m : Semantics.Montague.Model} [Fintype m.Entity] :
                        AntiAddLicensesStrongNPIs (Semantics.Lexical.Determiner.Quantifier.every_sem m)

                        "Every" is left-anti-additive → licenses strong NPIs in restrictor. P&W Prop 13: the restrictor of "every" is anti-additive (not just DE).

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          def Phenomena.Polarity.Studies.Ladusaw1979.no_laa_licenses_strong {m : Semantics.Montague.Model} [Fintype m.Entity] :
                          AntiAddLicensesStrongNPIs (Semantics.Lexical.Determiner.Quantifier.no_sem m)

                          "No" is left-anti-additive → licenses strong NPIs in restrictor.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            structure Phenomena.Polarity.Studies.Ladusaw1979.ScopeAALicensesStrongNPIs {m : Semantics.Montague.Model} (q : m.interpTy Semantics.Lexical.Determiner.Quantifier.Ty.det) :
                            Type

                            Scope-level anti-additivity also licenses strong NPIs. RightAntiAdditive q means the scope of q is anti-additive. "Nobody lifted a finger" is licensed by scope-level AA of no.

                            Instances For
                              source
                              def Phenomena.Polarity.Studies.Ladusaw1979.no_raa_licenses_strong {m : Semantics.Montague.Model} [Fintype m.Entity] :
                              ScopeAALicensesStrongNPIs (Semantics.Lexical.Determiner.Quantifier.no_sem m)

                              "No" is right-anti-additive → licenses strong NPIs in scope. "Nobody lifted a finger" / "Nobody saw anyone".

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                source
                                theorem Phenomena.Polarity.Studies.Ladusaw1979.few_DE_not_RAA :
                                Core.Quantification.ScopeDownwardMono (Semantics.Lexical.Determiner.Quantifier.few_sem Semantics.Montague.toyModel) ∧ ¬Core.Quantification.RightAntiAdditive (Semantics.Lexical.Determiner.Quantifier.few_sem Semantics.Montague.toyModel)

                                "Few" is DE but NOT right-anti-additive in scope: few(R, S∨S') ≠ few(R,S) ∧ few(R,S') in general. This is why *"Few people lifted a finger" is bad — strong NPIs need AA.

                                Counterexample: R = {john, mary, pizza}, S = {john}, S' = {mary}.

                                • few(R, S∨S') = (2 < 1) = false
                                • few(R, S) = (1 < 2) = true, few(R, S') = (1 < 2) = true
                                • true ∧ true ≠ false
                                source
                                theorem Phenomena.Polarity.Studies.Ladusaw1979.ladusaw_hierarchy :
                                licensingStrength NPIs.LicensingContext.sententialNegation = LicensingStrength.antiAdditive ∧ licensingStrength NPIs.LicensingContext.fewNP = LicensingStrength.downwardEntailing ∧ licensingStrength NPIs.LicensingContext.question = LicensingStrength.nonDE

                                The Ladusaw hierarchy: AA ⊂ DE ⊂ NV (nonveridical). Strong NPIs need AA; weak NPIs need DE; "any" in questions needs NV. "Few" is DE but not AA, explaining the licensing contrast: ✓ "Few students saw anyone" (weak NPI in DE) vs ✗ "*Few people lifted a finger" (strong NPI needs AA).

                                source
                                theorem Phenomena.Polarity.Studies.Ladusaw1979.de_contexts_license_weak_npis :
                                licensingStrength NPIs.LicensingContext.universalRestrictor ≠ LicensingStrength.nonDE ∧ licensingStrength NPIs.LicensingContext.fewNP ≠ LicensingStrength.nonDE ∧ licensingStrength NPIs.LicensingContext.sententialNegation ≠ LicensingStrength.nonDE ∧ licensingStrength NPIs.LicensingContext.constituentNegation ≠ LicensingStrength.nonDE ∧ licensingStrength NPIs.LicensingContext.withoutClause ≠ LicensingStrength.nonDE ∧ licensingStrength NPIs.LicensingContext.beforeClause ≠ LicensingStrength.nonDE ∧ licensingStrength NPIs.LicensingContext.conditional ≠ LicensingStrength.nonDE

                                Prediction: all NPI licensing contexts classified as DE or AA should produce grammatical NPI sentences. This is verified by the anyData checks in NPIs.lean (#guard at line 695-696).

                                source
                                theorem Phenomena.Polarity.Studies.Ladusaw1979.strong_npi_requires_aa :
                                licensingStrength NPIs.LicensingContext.sententialNegation = LicensingStrength.antiAdditive ∧ licensingStrength NPIs.LicensingContext.withoutClause = LicensingStrength.antiAdditive ∧ licensingStrength NPIs.LicensingContext.fewNP ≠ LicensingStrength.antiAdditive

                                Strong NPI prediction: only AA contexts license strong NPIs. "Few" (merely DE) does not license "lift a finger".