Typology.PolarityItem

@cite{lahiri-1998} @cite{haspelmath-1997} @cite{chierchia-2006} @cite{israel-1996} @cite{israel-2001} @cite{israel-2011} @cite{schwab-2022}

(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 Theories/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 @cite{israel-1996}, @cite{israel-2001}, @cite{israel-2011}. Treats polarity-sensitivity as a scalar-rhetorical phenomenon (high/low + strengthening/attenuating) orthogonal to monotonicity.

• Monotonicity-based licensing (in companion file Theories/Semantics/Polarity/Licensing.lean): the @cite{ladusaw-1979} / @cite{kadmon-landman-1993} / @cite{zwarts-1998} / @cite{chierchia-2006} 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 @cite{chierchia-2006}. 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 Phenomena/Polarity/Studies/Israel2001.lean. The natural witness is Israel's pecuniary paradox (@cite{israel-2001}): 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:

• @cite{lahiri-1998}: even-based scalar analysis grounding bhii / koii bhii in cardinality vs contextually-salient property alternatives. Israel positions himself against this.
• @cite{chierchia-2006}: 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 (@cite{israel-1996}, @cite{israel-2001}):

• 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 Phenomena/Polarity/Studies/Israel2001.lean.

inductive Typology.PolarityItem.ScalarValue : Type

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

@cite{israel-2001}: 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 Typology.PolarityItem.instDecidableEqScalarValue : DecidableEq ScalarValue

Equations

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

@[implicit_reducible]

instance Typology.PolarityItem.instReprScalarValue : Repr ScalarValue

Equations

• Typology.PolarityItem.instReprScalarValue = { reprPrec := Typology.PolarityItem.instReprScalarValue.repr }

def Typology.PolarityItem.instReprScalarValue.repr : ScalarValue → Nat → Std.Format

Equations

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

inductive Typology.PolarityItem.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 (@cite{israel-2001}'s "emphatic" items).
• Attenuating items (all that, so recht, long) make the assertion weaker than its scalar alternatives (@cite{israel-2001}'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.

@cite{israel-1996}. Polarity sensitivity as lexical semantics. L&P 19(6). @cite{israel-2011}. The Grammar of Polarity. CUP. @cite{schwab-2022}. Lexical variation in NPI illusions.

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

@[implicit_reducible]

instance Typology.PolarityItem.instDecidableEqScalarDirection : DecidableEq ScalarDirection

Equations

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

@[implicit_reducible]

instance Typology.PolarityItem.instReprScalarDirection : Repr ScalarDirection

Equations

• Typology.PolarityItem.instReprScalarDirection = { reprPrec := Typology.PolarityItem.instReprScalarDirection.repr }

def Typology.PolarityItem.instReprScalarDirection.repr : ScalarDirection → Nat → Std.Format

Equations

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

inductive Typology.PolarityItem.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)

@cite{israel-2001} 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 Typology.PolarityItem.instDecidableEqCanonicity : DecidableEq Canonicity

Equations

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

def Typology.PolarityItem.instReprCanonicity.repr : Canonicity → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.PolarityItem.instReprCanonicity : Repr Canonicity

Equations

• Typology.PolarityItem.instReprCanonicity = { reprPrec := Typology.PolarityItem.instReprCanonicity.repr }

inductive Typology.PolarityItem.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 @cite{israel-2001}'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 Typology.PolarityItem.instDecidableEqLikelihoodEffect : DecidableEq LikelihoodEffect

Equations

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

@[implicit_reducible]

instance Typology.PolarityItem.instReprLikelihoodEffect : Repr LikelihoodEffect

Equations

• Typology.PolarityItem.instReprLikelihoodEffect = { reprPrec := Typology.PolarityItem.instReprLikelihoodEffect.repr }

def Typology.PolarityItem.instReprLikelihoodEffect.repr : LikelihoodEffect → Nat → Std.Format

Equations

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

inductive Typology.PolarityItem.PolarityType : Type

Type of polarity sensitivity.

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

@[implicit_reducible]

instance Typology.PolarityItem.instDecidableEqPolarityType : DecidableEq PolarityType

Equations

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

def Typology.PolarityItem.instReprPolarityType.repr : PolarityType → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.PolarityItem.instReprPolarityType : Repr PolarityType

Equations

• Typology.PolarityItem.instReprPolarityType = { reprPrec := Typology.PolarityItem.instReprPolarityType.repr }

inductive Typology.PolarityItem.BaseForce : Type

Base quantificational force (when interpretable).

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

@[implicit_reducible]

instance Typology.PolarityItem.instDecidableEqBaseForce : DecidableEq BaseForce

Equations

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

def Typology.PolarityItem.instReprBaseForce.repr : BaseForce → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.PolarityItem.instReprBaseForce : Repr BaseForce

Equations

• Typology.PolarityItem.instReprBaseForce = { reprPrec := Typology.PolarityItem.instReprBaseForce.repr }

inductive Typology.PolarityItem.NPIMorphology : Type

Morphological composition of a polarity-sensitive item. @cite{lahiri-1998} 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 Typology.PolarityItem.instDecidableEqNPIMorphology : DecidableEq NPIMorphology

Equations

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

@[implicit_reducible]

instance Typology.PolarityItem.instReprNPIMorphology : Repr NPIMorphology

Equations

• Typology.PolarityItem.instReprNPIMorphology = { reprPrec := Typology.PolarityItem.instReprNPIMorphology.repr }

def Typology.PolarityItem.instReprNPIMorphology.repr : NPIMorphology → Nat → Std.Format

Equations

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

inductive Typology.PolarityItem.AlternativeType : Type

Type of alternatives introduced by the focused element. @cite{lahiri-1998}: ek bhii introduces cardinality alternatives, koii bhii introduces contextually salient property alternatives. @cite{chierchia-2006}: subdomain (D-)alternatives for domain widening.

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

@[implicit_reducible]

instance Typology.PolarityItem.instDecidableEqAlternativeType : DecidableEq AlternativeType

Equations

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

def Typology.PolarityItem.instReprAlternativeType.repr : AlternativeType → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.PolarityItem.instReprAlternativeType : Repr AlternativeType

Equations

• Typology.PolarityItem.instReprAlternativeType = { reprPrec := Typology.PolarityItem.instReprAlternativeType.repr }

structure Typology.PolarityItem.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 Theories/Semantics/Polarity/Licensing.lean.

• scalarDirection : ScalarDirection

  Scalar direction: strengthening, attenuating, or non-scalar

• scalarValue : ScalarValue

  Scalar value: high or low on the relevant scale (@cite{israel-2001})

• canonicity : Canonicity

  Canonical or inverted (@cite{israel-2001})

• likelihoodEffect : LikelihoodEffect

  Propositional role's likelihood effect (@cite{israel-2001})

• morphology : NPIMorphology

  Morphological composition (@cite{lahiri-1998})

• alternativeType : AlternativeType

  Type of alternatives introduced

• notes : String

  Notes

@[implicit_reducible]

instance Typology.PolarityItem.instReprPolarityItemEntry : Repr PolarityItemEntry

Equations

• Typology.PolarityItem.instReprPolarityItemEntry = { reprPrec := Typology.PolarityItem.instReprPolarityItemEntry.repr }

def Typology.PolarityItem.instReprPolarityItemEntry.repr : PolarityItemEntry → Nat → Std.Format

Equations

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

@[reducible, inline]

abbrev Typology.PolarityItem.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

• Typology.PolarityItem.isLicensedIn item ctx = (ctx ∈ item.licensingContexts)

@[reducible, inline]

abbrev Typology.PolarityItem.PolarityItemEntry.isNPI (p : PolarityItemEntry) : Prop

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

Equations

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

@[reducible, inline]

abbrev Typology.PolarityItem.PolarityItemEntry.isFCI (p : PolarityItemEntry) : Prop

Check if an item is an FCI.

Equations

• p.isFCI = (p.polarityType = Typology.PolarityItem.PolarityType.fci ∨ p.polarityType = Typology.PolarityItem.PolarityType.npiFci)

@[reducible, inline]

abbrev Typology.PolarityItem.PolarityItemEntry.isPPI (p : PolarityItemEntry) : Prop

Check if an item is a PPI.

Equations

• p.isPPI = (p.polarityType = Typology.PolarityItem.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 Theories/Semantics/Polarity/Israel.lean (sibling of Theories/Semantics/Polarity/Licensing.lean). This file holds only the substrate enums Fragments populate, not Israel's predictions about how those enum-valued fields relate.