Semantics.Polarity.Licensing

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

Monotonicity-based licensing infrastructure for polarity-sensitive items: the LicensingContext enum (~22 contexts), the LicensingMechanism classification (K&L domain-widening + strengthening, plus refinements for non-K&L licensing), the ContextProperties synthesis bundling DE-strength signatures with mechanism + Strawson-DE flagging, and the canonical contextProperties map projecting each context to its theoretical lineage.

Provenance

Split from Core/Lexical/PolarityItem.lean in the cleanup that dissolved Core/Lexical/. The Israel scalar machinery (ScalarValue/ScalarDirection/Canonicity/LikelihoodEffect) moved to the sibling file Typology/PolarityItem.lean (which also holds PolarityItemEntry and predictCanonicity); the cross-file gap between Israel's scalar model and Ladusaw/K&L's monotonicity model is documented there.

Framework commitment

The contextProperties map encodes the monotonicity-based licensing tradition: [Lad79] (DE-licensing), [Zwa98] (anti-additive/anti-morphic refinement), [KL93] (domain widening + strengthening), [vF99a] (Strawson-DE extension), and the every-restrictor-as-LAA result (variously attributed to Zwarts 1981 / van Benthem 1986 / Sánchez Valencia 1991; none currently in references.bib). Per-paper classifiers (Ladusaw1979.licensingStrength, KadmonLandman1993.klExplanation) project from this single record rather than parallel-stipulating.

The LicensingMechanism 5-way enum refines the original 3-way {byStrengthening, byGenericIndefinite, byOtherMechanism} into the substantively distinct cases:

• byStrengthening: K&L-canonical DE + widening (covers Ladusaw 1979).
• byGenericIndefinite: non-DE FC any (modals, generics, free relatives).
• byStrawsonDE: licensing via Strawson entailment (superlatives) — [vF99a] / Herdan & Sharvit (UNVERIFIED — bib entry missing).
• 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).

The earlier byOtherMechanism constructor used by some study files (e.g., KadmonLandman1993.lean for ungrammatical examples) maps to strengtheningFails; the legitimate non-K&L cases (entropy questions, Strawson-DE superlatives) get their own dedicated constructors.

Out of scope: Israel↔Ladusaw cross-framework gap

This file's contextProperties.signature field is Ladusaw/Zwarts/P&W canonical: each context has one DE/anti-additive/anti-morphic signature, regardless of which item is being licensed. Israel's scalar model rejects this per-context signature framing — for him, polarity-sensitivity is determined by the item's scale + role, not by the context's monotonicity. The cross-framework gap is real and is NOT closed by this restructure; see Typology/PolarityItem.lean for the Israel-side machinery and the documented refutation-theorem TODO.

inductive Semantics.Polarity.Licensing.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

@[implicit_reducible]

instance Semantics.Polarity.Licensing.instDecidableEqLicensingMechanism : DecidableEq LicensingMechanism

Equations

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

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

Equations

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

@[implicit_reducible]

instance Semantics.Polarity.Licensing.instReprLicensingMechanism : Repr LicensingMechanism

Equations

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

structure Semantics.Polarity.Licensing.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 contextProperties, not parallel stipulations.

• strawsonSignature : NaturalLogic.EntailmentSig

  Icard signature modulo presuppositions ([vF99a]'s Strawson reading): the row a Strawson-relativized soundness statement (EntailmentSig.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.EntailmentSig

  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 EntailmentSig row is classically sound for them. Defaults to the Strawson row (the presupposition-free case).

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

Equations

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

@[implicit_reducible]

instance Semantics.Polarity.Licensing.instReprContextProperties : Repr ContextProperties

Equations

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

def Semantics.Polarity.Licensing.contextProperties : 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.

def Semantics.Polarity.Licensing.strengthLicenses (e : PolarityItemEntry) (c : LicensingContext) : Bool

Zwarts-strength licensing, derived ([Zwa98], [Gaj11]): the context's Strawson-operative row supplies at least the item's required strength (PolarityItemEntry.strength, itself derived from polarityType). false when either side is not strength-keyed — those items/contexts license via mechanism (LicensingMechanism), not signature.

Equations

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

@[reducible, inline]

abbrev Semantics.Polarity.Licensing.LicensedBySignature (e : PolarityItemEntry) (c : LicensingContext) : Prop

strengthLicenses as a proposition.

Equations

• Semantics.Polarity.Licensing.LicensedBySignature e c = (Semantics.Polarity.Licensing.strengthLicenses e c = true)

Polymorphic strength scales

strengthLicenses is the Zwarts/DEStrength instance of a general pattern: 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 it with different carriers — see scratch/npi-api-design.md.

structure Semantics.Polarity.Licensing.StrengthScale (Item : Type u_1) (Context : 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 : Item → Option S

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

• supplied : Context → Option S

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

def Semantics.Polarity.Licensing.StrengthScale.licenses {Item : Type u_1} {Context : Type u_2} {S : Type u_3} [Preorder S] (L : StrengthScale Item Context S) (i : Item) (c : Context) : Prop

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

Equations

• L.licenses i c = ∃ (r : S), r ∈ L.required i ∧ ∃ (s : S), s ∈ L.supplied c ∧ r ≤ s

def Semantics.Polarity.Licensing.zwartsScale : StrengthScale PolarityItemEntry LicensingContext NaturalLogic.DEStrength

The canonical Zwarts/[Lad79] scale: carrier DEStrength, item strength from PolarityItemEntry.strength, context strength from the row's Strawson signature. The first instance of StrengthScale.

Equations

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

theorem Semantics.Polarity.Licensing.zwartsScale_licenses_iff (e : PolarityItemEntry) (c : LicensingContext) : zwartsScale.licenses e c ↔ LicensedBySignature e c

The polymorphic scale subsumes the bespoke predicate: zwartsScale.licenses is exactly LicensedBySignature (derive-don't-duplicate).

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

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

Equations

• Semantics.Polarity.Licensing.IsStrawsonOnly c = ((Semantics.Polarity.Licensing.contextProperties c).classicalSignature = none)

theorem Semantics.Polarity.Licensing.classicalSignature_eq_strawson (c : LicensingContext) : (contextProperties c).classicalSignature = none ∨ (contextProperties c).classicalSignature = some (contextProperties c).strawsonSignature

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