Documentation

Linglib.Theories.Semantics.Polarity.Licensing

Semantics.Polarity.Licensing #

@cite{ladusaw-1979} @cite{kadmon-landman-1993} @cite{zwarts-1998} @cite{von-fintel-1999} @cite{chierchia-2006} @cite{horn-1996} @cite{hoeksema-1983} @cite{bhatt-pancheva-2004} @cite{heim-2006} @cite{iatridou-2000} @cite{dayal-1996} @cite{van-rooy-2003}

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: @cite{ladusaw-1979} (DE-licensing), @cite{zwarts-1998} (anti-additive/anti-morphic refinement), @cite{kadmon-landman-1993} (domain widening + strengthening), @cite{von-fintel-1999} (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:

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.

source
inductive Semantics.Polarity.Licensing.LicensingMechanism :
Type

The mechanism by which a context licenses NPIs.

@cite{kadmon-landman-1993} 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 @cite{ladusaw-1979}'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 @cite{von-fintel-1999}).
  • byEntropy — Entropy-based licensing (questions per @cite{van-rooy-2003}).
  • 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.
Instances For
    source
    @[implicit_reducible]
    instance Semantics.Polarity.Licensing.instDecidableEqLicensingMechanism :
    DecidableEq LicensingMechanism
    Equations
    source
    @[implicit_reducible]
    instance Semantics.Polarity.Licensing.instReprLicensingMechanism :
    Repr LicensingMechanism
    Equations
    source
    def Semantics.Polarity.Licensing.instReprLicensingMechanism.repr :
    LicensingMechanism → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      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.

      • signature : Core.NaturalLogic.EntailmentSig

        Icard signature: locates the context in the natural-logic lattice.

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

      • isStrawsonOnly : Bool

        Strawson-DE flag (@cite{von-fintel-1999}): when true, the signature field over-promises classical DE — the context is in fact only DE under presupposition (Strawson-DE), not classically. Default false (the signature stands as a classical claim).

        Examples requiring this flag: .onlyFocus, .adversative, .sinceTemporal — classical-DE-on-paper but shown by @cite{von-fintel-1999} to be only Strawson-DE. The byStrawsonDE mechanism case is for items whose licensing primarily comes from Strawson-DE (e.g., superlative); isStrawsonOnly is for cases where the signature also needs qualification.

      Instances For
        source
        def Semantics.Polarity.Licensing.instReprContextProperties.repr :
        ContextProperties → ℕ → Std.Format
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[implicit_reducible]
          instance Semantics.Polarity.Licensing.instReprContextProperties :
          Repr ContextProperties
          Equations
          source
          def Semantics.Polarity.Licensing.contextProperties :
          Features.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.
          Instances For