Polarity items: NPI/PPI typology

[Lah98] [Has97] [Chi06] [Isr96] [Isr01] [Isr11] [Sch22]

(Lee & Horn 1994 MS any as indefinite + EVEN cited in §6 below; not currently in references.bib.)

Per-language typological substrate for polarity-sensitive items: the PolarityItemEntry record schema used by Fragment files, the Israel scalar model machinery (ScalarValue × ScalarDirection × Canonicity × LikelihoodEffect), morphological-composition typology, and the canonicity-prediction function predictCanonicity.

Provenance

Split from Core/Lexical/PolarityItem.lean in the cleanup that dissolved Core/Lexical/. The companion file Semantics/Polarity/Licensing.lean holds the monotonicity-based licensing infrastructure (LicensingContext, LicensingMechanism, ContextProperties, contextProperties — the Ladusaw/Zwarts/K&L/von Fintel synthesis).

Cross-framework gap (Israel ↔ Ladusaw)

This file enshrines two distinct theoretical lineages without making the choice between them explicit at the type level:

• Israel scalar model (ScalarValue × ScalarDirection × LikelihoodEffect × Canonicity): the apparatus of [Isr96], [Isr01], [Isr11]. Treats polarity-sensitivity as a scalar-rhetorical phenomenon (high/low + strengthening/attenuating) orthogonal to monotonicity.

• Monotonicity-based licensing (in companion file Semantics/Polarity/Licensing.lean): the [Lad79] / [KL93] / [Zwa98] / [Chi06] lineage. Treats polarity-sensitivity as a monotonicity-licensing phenomenon with widening + strengthening as the unifying mechanism.

These two lineages give different predictions for cases like FCIs in modal contexts, NPIs in superlatives, and the "rescued" NPIs of [Chi06]. The cross-file gap is acknowledged but NOT closed by this restructure: the contextProperties.signature field in the companion file is Ladusaw/Zwarts/P&W canonical (Israel cannot project per-context signatures without scale/role parameters from the item itself).

The Israel↔Ladusaw refutation theorem — showing a context where the scalar model and the monotonicity model disagree — is planned for Studies/Israel2001.lean. The natural witness is Israel's pecuniary paradox ([Isr01]): a red cent (NPI, resource = impeding role) and for peanuts (PPI, reward = facilitating role) inhabit the same monetary semantic domain — pure-monotonicity accounts treat them uniformly, while Israel's role-likelihood mapping correctly predicts the polarity contrast. (NOTE: Israel2001.lean §8 currently formalizes Israel↔Ladusaw agreement via a ScaleDirection bridge enum — that's the wrong direction. The refutation work is genuinely deferred.)

Alternative scalar-tradition frameworks (not formalized in linglib)

The Israel scalar model is one of several scalar-tradition accounts:

• [Lah98]: even-based scalar analysis grounding bhii / koii bhii in cardinality vs contextually-salient property alternatives. Israel positions himself against this.
• [Chi06]: exhaustification + D-alternatives subsume Israel's mechanism via implicit EXH; differs from Israel on FCI rescue (any in non-DE contexts).
• Krifka 1995 (STA — "Sumarizing the alternatives"): different alternative structure from Israel's high/low scalar dimension. (Not currently in references.bib.)

The substrate's enums (ScalarValue, ScalarDirection, Canonicity, LikelihoodEffect) implement the Israel framework specifically; formalising these alternatives would need parallel substrate types.

The Scalar Model of Polarity

Polarity items are characterized by two orthogonal scalar features ([Isr96], [Isr01]):

• ScalarValue (high/low): where the item sits on its scale
• ScalarDirection (strengthening/attenuating): rhetorical force

These interact with LikelihoodEffect — whether the item's referent facilitates or impedes the event — to predict Canonicity (canonical vs inverted). See Studies/Israel2001.lean.

inductive Semantics.Polarity.ScalarValue : Type

Where the polarity item sits on its scale, relative to the scalar norm.

[Isr01]: polarity items conventionally encode a fixed position on a scalar ordering. Emphatic NPIs typically denote LOW values (a wink, an inch), while emphatic PPIs typically denote HIGH values (tons, utterly). Inverted items reverse this pattern.

• high : ScalarValue
• low : ScalarValue
• unknown : ScalarValue

@[implicit_reducible]

instance Semantics.Polarity.instDecidableEqScalarValue : DecidableEq ScalarValue

Equations

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

def Semantics.Polarity.instReprScalarValue.repr : ScalarValue → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Polarity.instReprScalarValue : Repr ScalarValue

Equations

• Semantics.Polarity.instReprScalarValue = { reprPrec := Semantics.Polarity.instReprScalarValue.repr }

inductive Semantics.Polarity.ScalarDirection : Type

Rhetorical force: does this item strengthen or attenuate the assertion? Orthogonal to both PolarityType and ScalarValue.

• Strengthening items (ever, any, jemals) make the assertion stronger than its scalar alternatives ([Isr01]'s "emphatic" items).
• Attenuating items (all that, so recht, long) make the assertion weaker than its scalar alternatives ([Isr01]'s "understating" items).
• NonScalar items: editorial slot for items genuinely lacking scalar structure. NOTE: lift a finger is sometimes used as the canonical example, but Israel actually classifies it as scalar (extreme low effort = a minimizer). True non-scalar polarity items are theoretically contested; if uncertain, prefer unknown.

[Isr96]. Polarity sensitivity as lexical semantics. L&P 19(6). [Isr11]. The Grammar of Polarity. CUP. [Sch22]. Lexical variation in NPI illusions.

• strengthening : ScalarDirection
• attenuating : ScalarDirection
• nonScalar : ScalarDirection
• unknown : ScalarDirection

@[implicit_reducible]

instance Semantics.Polarity.instDecidableEqScalarDirection : DecidableEq ScalarDirection

Equations

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

@[implicit_reducible]

instance Semantics.Polarity.instReprScalarDirection : Repr ScalarDirection

Equations

• Semantics.Polarity.instReprScalarDirection = { reprPrec := Semantics.Polarity.instReprScalarDirection.repr }

def Semantics.Polarity.instReprScalarDirection.repr : ScalarDirection → ℕ → Std.Format

Equations

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

inductive Semantics.Polarity.Canonicity : Type

Whether a polarity item is canonical or inverted.

Canonical items have the expected correlation between scalar value and polarity type:

• Canonical emphatic NPIs denote LOW values (a wink, an inch)
• Canonical emphatic PPIs denote HIGH values (tons, utterly)

Inverted items reverse this:

• Inverted emphatic NPIs denote HIGH values (wild horses, all the tea in China)
• Inverted emphatic PPIs denote LOW values (at the drop of a hat, for a pittance)

[Isr01] shows inversion tracks propositional role: canonical items fill impeding roles (patient/theme); inverted items fill facilitating roles (stimulus/instrument/reward).

• canonical : Canonicity
• inverted : Canonicity
• unknown : Canonicity

@[implicit_reducible]

instance Semantics.Polarity.instDecidableEqCanonicity : DecidableEq Canonicity

Equations

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

def Semantics.Polarity.instReprCanonicity.repr : Canonicity → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Polarity.instReprCanonicity : Repr Canonicity

Equations

• Semantics.Polarity.instReprCanonicity = { reprPrec := Semantics.Polarity.instReprCanonicity.repr }

inductive Semantics.Polarity.LikelihoodEffect : Type

How increasing the scalar value of an item's referent affects the likelihood of the proposition being true.

This is the key to [Isr01]'s resolution of the maximizer/minimizer puzzle:

• Facilitating roles (agent, stimulus, instrument, reward): bigger/more → event more likely → scale is inverted (e.g., wild horses — more powerful force → more likely to move you)

• Impeding roles (patient, theme, increment, resource/expense): bigger/more → event less likely → scale is canonical (e.g., lift a finger — more effort required → less likely to act)

The pecuniary paradox dissolves: a red cent (NPI, resource = impeding) vs for peanuts (PPI, reward = facilitating) — same monetary domain, different propositional roles.

• facilitating : LikelihoodEffect
• impeding : LikelihoodEffect
• unknown : LikelihoodEffect

@[implicit_reducible]

instance Semantics.Polarity.instDecidableEqLikelihoodEffect : DecidableEq LikelihoodEffect

Equations

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

@[implicit_reducible]

instance Semantics.Polarity.instReprLikelihoodEffect : Repr LikelihoodEffect

Equations

• Semantics.Polarity.instReprLikelihoodEffect = { reprPrec := Semantics.Polarity.instReprLikelihoodEffect.repr }

def Semantics.Polarity.instReprLikelihoodEffect.repr : LikelihoodEffect → ℕ → Std.Format

Equations

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

inductive Semantics.Polarity.PolarityType : Type

Type of polarity sensitivity.

• npiWeak : PolarityType
• npiStrong : PolarityType
• fci : PolarityType
• npiFci : PolarityType
• ppi : PolarityType

@[implicit_reducible]

instance Semantics.Polarity.instDecidableEqPolarityType : DecidableEq PolarityType

Equations

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

def Semantics.Polarity.instReprPolarityType.repr : PolarityType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Polarity.instReprPolarityType : Repr PolarityType

Equations

• Semantics.Polarity.instReprPolarityType = { reprPrec := Semantics.Polarity.instReprPolarityType.repr }

inductive Semantics.Polarity.BaseForce : Type

Base quantificational force (when interpretable).

• existential : BaseForce
• universal : BaseForce
• degree : BaseForce
• temporal : BaseForce
• manner : BaseForce
• additive : BaseForce

@[implicit_reducible]

instance Semantics.Polarity.instDecidableEqBaseForce : DecidableEq BaseForce

Equations

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

def Semantics.Polarity.instReprBaseForce.repr : BaseForce → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Polarity.instReprBaseForce : Repr BaseForce

Equations

• Semantics.Polarity.instReprBaseForce = { reprPrec := Semantics.Polarity.instReprBaseForce.repr }

inductive Semantics.Polarity.NPIMorphology : Type

Morphological composition of a polarity-sensitive item. [Lah98] shows Hindi NPIs are transparently indefinite + even. Lee & Horn 1994 MS any as indef + EVEN documents this pattern cross-linguistically (UNVERIFIED — bib entry missing).

NOTE on indefPlusNeg: covers items genuinely composed as indefinite + negation morphology (some Slavic n-words, Romanian nimic). Italian n-words (nessuno, niente, mai) are conventionally analyzed as negative-concord items rather than indef+neg morphology (Zanuttini, Penka, Déprez, Giannakidou); they should be classified via the negative-concord framework (planned), not via this morphology field.

• indefPlusEven : NPIMorphology
• indefPlusNeg : NPIMorphology
• plain : NPIMorphology
• idiomatic : NPIMorphology

@[implicit_reducible]

instance Semantics.Polarity.instDecidableEqNPIMorphology : DecidableEq NPIMorphology

Equations

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

@[implicit_reducible]

instance Semantics.Polarity.instReprNPIMorphology : Repr NPIMorphology

Equations

• Semantics.Polarity.instReprNPIMorphology = { reprPrec := Semantics.Polarity.instReprNPIMorphology.repr }

def Semantics.Polarity.instReprNPIMorphology.repr : NPIMorphology → ℕ → Std.Format

Equations

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

inductive Semantics.Polarity.AlternativeType : Type

Type of alternatives introduced by the focused element. [Lah98]: ek bhii introduces cardinality alternatives, koii bhii introduces contextually salient property alternatives. [Chi06]: subdomain (D-)alternatives for domain widening.

• cardinality : AlternativeType
• contextualProperty : AlternativeType
• domain : AlternativeType
• unspecified : AlternativeType

@[implicit_reducible]

instance Semantics.Polarity.instDecidableEqAlternativeType : DecidableEq AlternativeType

Equations

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

@[implicit_reducible]

instance Semantics.Polarity.instReprAlternativeType : Repr AlternativeType

Equations

• Semantics.Polarity.instReprAlternativeType = { reprPrec := Semantics.Polarity.instReprAlternativeType.repr }

def Semantics.Polarity.instReprAlternativeType.repr : AlternativeType → ℕ → Std.Format

Equations

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

structure Semantics.Polarity.PolarityItemEntry : Type

A lexical entry for a polarity-sensitive item.

Theory-neutral: captures distributional facts without committing to a particular analysis (exhaustification, domain widening, etc.).

• form : String

  Surface form

• polarityType : PolarityType

  Type of polarity sensitivity

• baseForce : BaseForce

  Base quantificational/semantic force

• licensingContexts : List LicensingContext

  Contexts where licensed (empty = needs positive). Refers to LicensingContext from the companion file Semantics/Polarity/Licensing.lean.

• scalarDirection : ScalarDirection

  Scalar direction: strengthening, attenuating, or non-scalar

• scalarValue : ScalarValue

  Scalar value: high or low on the relevant scale ([Isr01])

• canonicity : Canonicity

  Canonical or inverted ([Isr01])

• likelihoodEffect : LikelihoodEffect

  Propositional role's likelihood effect ([Isr01])

• morphology : NPIMorphology

  Morphological composition ([Lah98])

• alternativeType : AlternativeType

  Type of alternatives introduced

• nWordStatus : Option Features.NegativeConcord.NWordStatus

  Negative-concord / n-word status ([Gia00], [vdAVA16]). none for items outside the negative-concord system; strict-NC n-words set some .nWord here rather than leaning on a strong-NPI polarityType.

• notes : String

  Notes

@[implicit_reducible]

instance Semantics.Polarity.instReprPolarityItemEntry : Repr PolarityItemEntry

Equations

• Semantics.Polarity.instReprPolarityItemEntry = { reprPrec := Semantics.Polarity.instReprPolarityItemEntry.repr }

def Semantics.Polarity.instReprPolarityItemEntry.repr : PolarityItemEntry → ℕ → Std.Format

Equations

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

def Semantics.Polarity.PolarityItemEntry.strength (e : PolarityItemEntry) : Option NaturalLogic.DEStrength

The [Zwa98] strength class an item requires of its licensor, derived from polarityType: weak NPIs (and the NPI face of dual NPI/FCIs) need weak DE, strong NPIs need anti-additivity; FCIs and PPIs are not strength-keyed. The superstrong class (a tad bit, anti-morphic) has no registry items yet — extend PolarityType when one lands.

Equations

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

@[reducible, inline]

abbrev Semantics.Polarity.isLicensedIn (item : PolarityItemEntry) (ctx : LicensingContext) : Prop

Check if a context licenses a polarity item.

An item is licensed if the context is explicitly listed in licensingContexts.

Equations

• Semantics.Polarity.isLicensedIn item ctx = (ctx ∈ item.licensingContexts)

@[reducible, inline]

abbrev Semantics.Polarity.PolarityItemEntry.isNPI (p : PolarityItemEntry) : Prop

Check if an item is an NPI (weak or strong).

Equations

• p.isNPI = (p.polarityType = Semantics.Polarity.PolarityType.npiWeak ∨ p.polarityType = Semantics.Polarity.PolarityType.npiStrong ∨ p.polarityType = Semantics.Polarity.PolarityType.npiFci)

@[reducible, inline]

abbrev Semantics.Polarity.PolarityItemEntry.isFCI (p : PolarityItemEntry) : Prop

Check if an item is an FCI.

Equations

• p.isFCI = (p.polarityType = Semantics.Polarity.PolarityType.fci ∨ p.polarityType = Semantics.Polarity.PolarityType.npiFci)

@[reducible, inline]

abbrev Semantics.Polarity.PolarityItemEntry.isPPI (p : PolarityItemEntry) : Prop

Check if an item is a PPI.

Equations

• p.isPPI = (p.polarityType = Semantics.Polarity.PolarityType.ppi)

Israel's prediction functions live in Theories

Israel's main empirical claim — predictCanonicity (impeding role → canonical / facilitating role → inverted) and the PolarityItemEntry.canonicityConsistent validation predicate that checks whether stated canonicity matches the prediction — were moved to Semantics/Polarity/Israel.lean (sibling of Semantics/Polarity/Licensing.lean). This file holds only the substrate enums Fragments populate, not Israel's predictions about how those enum-valued fields relate.