Features.LicensingContext

@cite{ladusaw-1979} @cite{kadmon-landman-1993}

The 22-case enum of licensing contexts for polarity-sensitive items. Theory-neutral data substrate: every framework that talks about polarity licensing (Ladusaw monotonicity, K&L domain widening, Israel scalar model, Chierchia exhaustification, Giannakidou nonveridicality) needs to talk about these context labels.

Provenance

Extracted from Theories/Semantics/Polarity/Licensing.lean after audit consensus that LicensingContext is data, not theory: the 22 cases are observational labels for syntactic environments, while only the signatures assigned to them in contextProperties (in the Theories file) carry theoretical commitment. Co-locating the enum here makes it Fragment-importable substrate without dragging in the Ladusaw/K&L theoretical apparatus.

The earlier 2-way split (Theories/Polarity/Licensing.lean for the enum + theory together; Typology/PolarityItem.lean for entry + Israel) forced Typology/PolarityItem.lean to import from Theories/, the only such cross-layer import in linglib. This file breaks that inversion: Typology/ and Theories/Semantics/Polarity/ both import from Features/, no peer-layer crossings.

Framework commitment

The 22-case enum is theory-laden in its naming (constructor names like adversative, doubtVerb, denyVerb, comparativeS reflect specific traditions' classification of contexts), but the cases themselves enumerate empirically-attested licensing environments any framework needs to talk about. The DE/anti-additive/anti-morphic labelling of these contexts is theory-laden and lives in Theories/Semantics/Polarity/Licensing.lean::contextProperties (Ladusaw/Zwarts canonical) — not here.

UNVERIFIED: The 22-case carve-up is English-anchored and may need cross-linguistic restructuring (e.g., factor by veridicality + monotonicity per Giannakidou 1998, rather than by surface construction); see the Theories/Semantics/Polarity/Licensing.lean "Out of scope" section for the documented gap.

inductive Features.LicensingContext : Type

Contexts that can license polarity-sensitive items.

Characterized by their logical properties:

• DE (Downward Entailing): reverses entailment direction
• Anti-additive: DE + distributes over disjunction
• Anti-morphic: anti-additive + distributes over conjunction (= negation)

Per-context theoretical classifications (DE strength, K&L mechanism, Strawson-DE flagging) live in Theories/Semantics/Polarity/Licensing.lean::contextProperties.

• negation : LicensingContext
• nobody : LicensingContext
• few : LicensingContext
• atMost : LicensingContext
• conditionalAntecedent : LicensingContext
• beforeClause : LicensingContext
• withoutClause : LicensingContext
• onlyFocus : LicensingContext
• question : LicensingContext
• comparativeNP : LicensingContext
• comparativeS : LicensingContext
• superlative : LicensingContext
• tooTo : LicensingContext
• modalPossibility : LicensingContext
• modalNecessity : LicensingContext
• imperative : LicensingContext
• generic : LicensingContext
• adversative : LicensingContext
• sinceTemporal : LicensingContext
• freeRelative : LicensingContext
• universalRestrictor : LicensingContext
• doubtVerb : LicensingContext
• denyVerb : LicensingContext

@[implicit_reducible]

instance Features.instDecidableEqLicensingContext : DecidableEq LicensingContext

Equations

• Features.instDecidableEqLicensingContext x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Features.instReprLicensingContext.repr : LicensingContext → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Features.instReprLicensingContext : Repr LicensingContext

Equations

• Features.instReprLicensingContext = { reprPrec := Features.instReprLicensingContext.repr }