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.Quantification.Quantifier to the NPI licensing classification indexed by Typology.PolarityItem.LicensingContext, 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.

inductive 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.

A coarsening of Core.NaturalLogic.DEStrength that collapses the .antiMorphic and .antiAdditive cases (Ladusaw treats them identically: both license strong NPIs).

• antiAdditive : LicensingStrength
• downwardEntailing : LicensingStrength
• nonDE : LicensingStrength

@[implicit_reducible]

instance Ladusaw1979.instDecidableEqLicensingStrength : DecidableEq LicensingStrength

Equations

• Ladusaw1979.instDecidableEqLicensingStrength x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Ladusaw1979.instReprLicensingStrength.repr : LicensingStrength → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Ladusaw1979.instReprLicensingStrength : Repr LicensingStrength

Equations

• Ladusaw1979.instReprLicensingStrength = { reprPrec := Ladusaw1979.instReprLicensingStrength.repr }

def Ladusaw1979.LicensingStrength.ofDEStrength : Option Core.NaturalLogic.DEStrength → LicensingStrength

Coarsen a DEStrength to Ladusaw's three-way classification.

Equations

• Ladusaw1979.LicensingStrength.ofDEStrength (some Core.NaturalLogic.DEStrength.antiMorphic) = Ladusaw1979.LicensingStrength.antiAdditive
• Ladusaw1979.LicensingStrength.ofDEStrength (some Core.NaturalLogic.DEStrength.antiAdditive) = Ladusaw1979.LicensingStrength.antiAdditive
• Ladusaw1979.LicensingStrength.ofDEStrength (some Core.NaturalLogic.DEStrength.weak) = Ladusaw1979.LicensingStrength.downwardEntailing
• Ladusaw1979.LicensingStrength.ofDEStrength none = Ladusaw1979.LicensingStrength.nonDE

def Ladusaw1979.licensingStrength (c : Features.LicensingContext) : LicensingStrength

Classify NPI licensing contexts by their monotonicity-based strength, derived from Semantics.Polarity.Licensing.contextProperties. The Ladusaw classification is a coarsening of the Icard signature lattice.

Equations

• Ladusaw1979.licensingStrength c = Ladusaw1979.LicensingStrength.ofDEStrength (Semantics.Polarity.Licensing.contextProperties c).signature.toDEStrength

structure Ladusaw1979.ScopeDELicensesWeakNPIs {m : Core.Logic.Intensional.Frame} (q : m.Denot Semantics.Quantification.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" ✓

• scopeDE : Core.Quantification.ScopeDownwardMono q
• context : Features.LicensingContext

  The licensing context this corresponds to

• isDE : licensingStrength self.context = LicensingStrength.downwardEntailing ∨ licensingStrength self.context = LicensingStrength.antiAdditive

  The context is classified as at least DE

def Ladusaw1979.no_scope_licenses_weak {m : Core.Logic.Intensional.Frame} [Fintype m.Entity] : ScopeDELicensesWeakNPIs (Semantics.Quantification.Quantifier.no_sem m)

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

Equations

• Ladusaw1979.no_scope_licenses_weak = { scopeDE := ⋯, context := Features.LicensingContext.nobody, isDE := Ladusaw1979.no_scope_licenses_weak._proof_1 }

def Ladusaw1979.few_scope_licenses_weak {m : Core.Logic.Intensional.Frame} [Fintype m.Entity] : ScopeDELicensesWeakNPIs (Semantics.Quantification.Quantifier.few_sem m)

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

Equations

• Ladusaw1979.few_scope_licenses_weak = { scopeDE := ⋯, context := Features.LicensingContext.few, isDE := Ladusaw1979.few_scope_licenses_weak._proof_1 }

structure Ladusaw1979.RestrictorDELicensesWeakNPIs {m : Core.Logic.Intensional.Frame} (q : m.Denot Semantics.Quantification.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" ✓

• restrictorDE : Core.Quantification.RestrictorDownwardMono q
• context : Features.LicensingContext
• isDE : licensingStrength self.context = LicensingStrength.downwardEntailing ∨ licensingStrength self.context = LicensingStrength.antiAdditive

def Ladusaw1979.every_restrictor_licenses_weak {m : Core.Logic.Intensional.Frame} [Fintype m.Entity] [DecidableEq m.Entity] : RestrictorDELicensesWeakNPIs (Semantics.Quantification.Quantifier.every_sem m)

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

Equations

• Ladusaw1979.every_restrictor_licenses_weak = { restrictorDE := ⋯, context := Features.LicensingContext.universalRestrictor, isDE := Ladusaw1979.every_restrictor_licenses_weak._proof_1 }

def Ladusaw1979.no_restrictor_licenses_weak {m : Core.Logic.Intensional.Frame} [Fintype m.Entity] [DecidableEq m.Entity] : RestrictorDELicensesWeakNPIs (Semantics.Quantification.Quantifier.no_sem m)

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

Equations

• Ladusaw1979.no_restrictor_licenses_weak = { restrictorDE := ⋯, context := Features.LicensingContext.nobody, isDE := Ladusaw1979.no_scope_licenses_weak._proof_1 }

structure Ladusaw1979.AntiAddLicensesStrongNPIs {m : Core.Logic.Intensional.Frame} (q : m.Denot Semantics.Quantification.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" ✗

• laa : Core.Quantification.LeftAntiAdditive q
• context : Features.LicensingContext
• isAA : licensingStrength self.context = LicensingStrength.antiAdditive

def Ladusaw1979.every_laa_licenses_strong {m : Core.Logic.Intensional.Frame} [Fintype m.Entity] [DecidableEq m.Entity] : AntiAddLicensesStrongNPIs (Semantics.Quantification.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

• Ladusaw1979.every_laa_licenses_strong = { laa := ⋯, context := Features.LicensingContext.universalRestrictor, isAA := Ladusaw1979.every_laa_licenses_strong._proof_1 }

def Ladusaw1979.no_laa_licenses_strong {m : Core.Logic.Intensional.Frame} [Fintype m.Entity] [DecidableEq m.Entity] : AntiAddLicensesStrongNPIs (Semantics.Quantification.Quantifier.no_sem m)

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

Equations

• Ladusaw1979.no_laa_licenses_strong = { laa := ⋯, context := Features.LicensingContext.nobody, isAA := Ladusaw1979.no_laa_licenses_strong._proof_1 }

structure Ladusaw1979.ScopeAALicensesStrongNPIs {m : Core.Logic.Intensional.Frame} (q : m.Denot Semantics.Quantification.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.

• raa : Core.Quantification.RightAntiAdditive q
• context : Features.LicensingContext
• isAA : licensingStrength self.context = LicensingStrength.antiAdditive

def Ladusaw1979.no_raa_licenses_strong {m : Core.Logic.Intensional.Frame} [Fintype m.Entity] [DecidableEq m.Entity] : ScopeAALicensesStrongNPIs (Semantics.Quantification.Quantifier.no_sem m)

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

Equations

• Ladusaw1979.no_raa_licenses_strong = { raa := ⋯, context := Features.LicensingContext.nobody, isAA := Ladusaw1979.no_laa_licenses_strong._proof_1 }

theorem Ladusaw1979.few_DE_not_RAA : Core.Quantification.ScopeDownwardMono (Semantics.Quantification.Quantifier.few_sem Semantics.Montague.toyModel) ∧ ¬Core.Quantification.RightAntiAdditive (Semantics.Quantification.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

theorem Ladusaw1979.ladusaw_hierarchy : licensingStrength Features.LicensingContext.negation = LicensingStrength.antiAdditive ∧ licensingStrength Features.LicensingContext.few = LicensingStrength.downwardEntailing ∧ licensingStrength Features.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).

theorem Ladusaw1979.de_contexts_license_weak_npis : licensingStrength Features.LicensingContext.universalRestrictor ≠ LicensingStrength.nonDE ∧ licensingStrength Features.LicensingContext.few ≠ LicensingStrength.nonDE ∧ licensingStrength Features.LicensingContext.negation ≠ LicensingStrength.nonDE ∧ licensingStrength Features.LicensingContext.nobody ≠ LicensingStrength.nonDE ∧ licensingStrength Features.LicensingContext.withoutClause ≠ LicensingStrength.nonDE ∧ licensingStrength Features.LicensingContext.beforeClause ≠ LicensingStrength.nonDE ∧ licensingStrength Features.LicensingContext.conditionalAntecedent ≠ LicensingStrength.nonDE

Prediction: all NPI licensing contexts classified as DE or AA should produce grammatical NPI sentences.

theorem Ladusaw1979.strong_npi_requires_aa : licensingStrength Features.LicensingContext.negation = LicensingStrength.antiAdditive ∧ licensingStrength Features.LicensingContext.withoutClause = LicensingStrength.antiAdditive ∧ licensingStrength Features.LicensingContext.few ≠ LicensingStrength.antiAdditive

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