Polarity licensing

[Lad79] [KL93] [Zwa98] [vF99a] [vR03b] [Hoe83] [BP04] [Hei06] [Iat00] [Day96] [Hor96] [vdW97]

The monotonicity-based licensing theory for Polarity.Item: LicensingContext.properties assigns every LicensingContext its Strawson and classical entailment signatures, its [KL93] licensing mechanism, and its citation lineage; StrengthScale is the polymorphic item↔context strength pattern with zwartsScale as its canonical instance; and the keystone LicensingContext.licenses dispatches on the row's mechanism — Zwarts strength on signature rows, free choice on generic-indefinite rows ([Day96]), entropy on questions ([vR03b]). Per-paper classifiers (Ladusaw1979, KadmonLandman1993) project from LicensingContext.properties rather than parallel-stipulating; the grounded grade — deriving the signatures from the model witnesses of Witnesses.lean via the Kadmon–Landman strengthening chain — is the planned next step.

Main declarations

• LicensingMechanism, ContextProperties, LicensingContext.properties — the per-context theory table.
• StrengthScale, zwartsScale — polymorphic strength licensing.
• LicensingContext.licenses — the item↔context licensing keystone.
• LicensingContext.IsStrawsonOnly and the Haspelmath-map grounding theorems.

Implementation notes

The table's signatures are Ladusaw/Zwarts/von-Fintel canonical — one row per context regardless of item; [Isr01]'s scalar model rejects exactly this framing (predictions in Semantics/Polarity/ScalarModel.lean). The NP-comparative row licenses nothing ([Hoe83]); surface NPIs in "than NP" route through the clausal row ([BP04], [Hei06]). The every-restrictor-as-LAA signature is standard but of contested attribution (Zwarts 1981 / van Benthem 1986 / Sánchez Valencia 1991; none in references.bib).

Licensing Mechanism (refined 5-way)

inductive Polarity.LicensingMechanism : Type

The mechanism by which a context licenses NPIs.

[KL93] unify NPI licensing under domain widening + strengthening. The substrate refines K&L's original 3-way classification into 5 substantively distinct cases.

• byStrengthening — DE contexts where widening strengthens the assertion. Covers [Lad79]'s monotonicity-based licensing.
• byGenericIndefinite — Non-DE contexts (modals, generics, free relatives) where any surfaces as the generic indefinite (FC any).
• byStrawsonDE — Strawson-DE licensing (superlatives per Herdan & Sharvit's superlative-NPI work [UNVERIFIED — bib entry missing] and [vF99a]).
• byEntropy — Entropy-based licensing (questions per [vR03b]).
• strengtheningFails — contexts that don't license despite surface appearance (e.g., NP-comparatives that lack covert clausal structure). Used by study files (e.g., KadmonLandman1993.lean) for ungrammatical examples, replacing the earlier byOtherMechanism constructor.

• byStrengthening : LicensingMechanism
• byGenericIndefinite : LicensingMechanism
• byStrawsonDE : LicensingMechanism
• byEntropy : LicensingMechanism
• strengtheningFails : LicensingMechanism

@[instance_reducible]

instance Polarity.instDecidableEqLicensingMechanism : DecidableEq LicensingMechanism

Equations

• Polarity.instDecidableEqLicensingMechanism x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Polarity.instReprLicensingMechanism : Repr LicensingMechanism

Equations

• Polarity.instReprLicensingMechanism = { reprPrec := Polarity.instReprLicensingMechanism.repr }

def Polarity.instReprLicensingMechanism.repr : LicensingMechanism → ℕ → Std.Format

Equations

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

Context Properties (single source of truth)

structure Polarity.ContextProperties : Type

The bundle of theory-relevant facts about a licensing context.

Every classification of LicensingContext (DE strength, K&L mechanism, canonical example, citation lineage) projects out of this single record. Per-paper classifiers (Ladusaw1979.licensingStrength, KadmonLandman1993.klExplanation) are derivations from LicensingContext.properties, not parallel stipulations.

• strawsonSignature : NaturalLogic.Signature

  Icard signature modulo presuppositions ([vF99a]'s Strawson reading): the row a Strawson-relativized soundness statement (Signature.StrawsonSoundFor) realizes. Coincides with the classical row for presupposition-free contexts.

• mechanism : LicensingMechanism

  K&L mechanism: how this context licenses NPIs.

• prototype : String

  A canonical English example.

• citations : List String

  BibTeX keys for the works that established this classification.

• classicalSignature : Option NaturalLogic.Signature

  Classical (presupposition-free) signature row, when one holds. none for the contexts [vF99a] showed to be only Strawson-DE — only-focus, adversatives, temporal since, superlatives: no Signature row is classically sound for them. Defaults to the Strawson row (the presupposition-free case).

def Polarity.instReprContextProperties.repr : ContextProperties → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Polarity.instReprContextProperties : Repr ContextProperties

Equations

• Polarity.instReprContextProperties = { reprPrec := Polarity.instReprContextProperties.repr }

def Polarity.LicensingContext.properties : LicensingContext → ContextProperties

Canonical map from licensing contexts to their theoretical properties.

UNVERIFIED: The "every-restrictor is LAA" result is variously attributed to Zwarts 1981 / van Benthem 1986 / Sánchez Valencia 1991; none currently in references.bib. The substrate uses the standard .antiAdd signature for .universalRestrictor without committing to a specific source.

Equations

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

Strength scales

A theory of NPI strength is an ordered carrier S plus how items and contexts project onto it, with licensing = ≤ on S. Different theories of strength (Gajewski plain-vs-exhaustified, Giannakidou veridicality, gradient) instantiate different carriers.

structure Polarity.StrengthScale (α : Type u_1) (β : Type u_2) (S : Type u_3) [Preorder S] : Type (max (max u_1 u_2) u_3)

A strength scale for NPI licensing: how items and contexts project onto an ordered strength carrier S. none on either side = "no strength here" (the item licenses via another mechanism, or the context supplies none).

• required : α → Option S

  The strength an item requires (none = not strength-licensed).

• supplied : β → Option S

  The strength a context supplies (none = supplies no strength).

def Polarity.StrengthScale.licenses {α : Type u_1} {β : Type u_2} {S : Type u_3} [Preorder S] (L : StrengthScale α β S) (i : α) (c : β) : Prop

Licensing on a scale: the context supplies at least the strength the item requires (both sides present).

Equations

• L.licenses i c = ∃ r ∈ L.required i, ∃ s ∈ L.supplied c, r ≤ s

@[instance_reducible]

instance Polarity.instDecidableLicensesOfDecidableRelLe {α : Type u_1} {β : Type u_2} {S : Type u_3} [Preorder S] [DecidableRel fun (x1 x2 : S) => x1 ≤ x2] (L : StrengthScale α β S) (i : α) (c : β) : Decidable (L.licenses i c)

Equations

• Polarity.instDecidableLicensesOfDecidableRelLe L i c = id inferInstance

def Polarity.zwartsScale : StrengthScale Item LicensingContext DEStrength

The canonical Zwarts scale ([Lad79], [Zwa98], [Gaj11]): carrier DEStrength, item strength from Item.licensor, context strength from the row's Strawson signature.

Equations

• Polarity.zwartsScale = { required := fun (e : Polarity.Item) => e.licensor, supplied := fun (c : Polarity.LicensingContext) => c.properties.strawsonSignature.toDEStrength }

The licensing keystone

def Polarity.LicensingContext.licenses (c : LicensingContext) (e : Item) : Prop

The item↔context licensing relation (stipulated grade), read context-side: c.licenses e says environment c licenses item e. Dispatched on the row's LicensingMechanism:

• signature rows (byStrengthening, byStrawsonDE): Zwarts-strength licensing — the row's Strawson signature supplies at least e.licensor (n-words require anti-morphic strength, so clausal negation is the only qualifying row);
• byGenericIndefinite rows license free choice items;
• byEntropy rows (questions, [vR03b]) license weak NPIs;
• strengtheningFails rows license nothing.

The grounded grade — deriving the signature side from the context witnesses of Witnesses.lean via the Kadmon–Landman strengthening chain — is planned (N1 of the NPI-API sweep).

Equations

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

@[instance_reducible]

instance Polarity.instDecidableLicenses (c : LicensingContext) (e : Item) : Decidable (c.licenses e)

Equations

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

The Haspelmath map meets the licensing table

Polarity.LicensingContext.haspelmathFunction (in Features/Indefinite.lean) classifies each licensing environment by the [Has97] map function it realizes. The theorems here ground the map's stipulated polarity-side classifiers (HaspelmathFunction.isDE/isFC) in LicensingContext.properties.

theorem Polarity.haspelmathFunction_freeChoice_iff_genericIndefinite (c : LicensingContext) : c.haspelmathFunction = some Indefinite.HaspelmathFunction.freeChoice ↔ c.properties.mechanism = LicensingMechanism.byGenericIndefinite

[Has97]'s free-choice region coincides exactly with the [KL93] generic-indefinite mechanism class: a context realizes the freeChoice function iff its licensing mechanism is byGenericIndefinite.

theorem Polarity.haspelmathFunction_npi_region_licensable (c : LicensingContext) (f : Indefinite.HaspelmathFunction) (hf : c.haspelmathFunction = some f) (hDE : f.isDE = true) : c.properties.strawsonSignature.toDEStrength.isSome = true ∨ c.properties.mechanism = LicensingMechanism.byEntropy

Every context realizing an NPI-region function (HaspelmathFunction.isDE: question through direct negation) either supplies Zwarts strength or is the entropy row — the map's classical NPI region is weak-NPI-licensable, though not uniformly DE (questions license by entropy, [vR03b]).

def Polarity.LicensingContext.IsStrawsonOnly (c : LicensingContext) : Prop

A context is Strawson-only when no classical signature row holds ([vF99a]): only-focus, adversatives, temporal since, superlatives.

Equations

• c.IsStrawsonOnly = (c.properties.classicalSignature = none)

theorem Polarity.classicalSignature_eq_strawson (c : LicensingContext) : c.properties.classicalSignature = none ∨ c.properties.classicalSignature = some c.properties.strawsonSignature

When a classical row exists it coincides with the Strawson row: presupposition-free contexts carry a single signature.