Polarity Item Infrastructure

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

Language-neutral types for polarity-sensitive items, shared across all language fragments. These capture cross-linguistic generalizations about polarity types, licensing contexts, scalar direction, scalar value, canonicity, likelihood effect, morphological composition, and alternative types.

The Scalar Model of Polarity (@cite{israel-1996}, @cite{israel-2001})

Polarity items are characterized by two orthogonal scalar features:

• 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 Core.Lexical.PolarityItem.LicensingContext : Type

Contexts that can license polarity-sensitive items.

These are 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)

• negation : LicensingContext
• nobody : LicensingContext
• few : LicensingContext
• atMost : LicensingContext
• conditional_ant : LicensingContext
• before_clause : LicensingContext
• without_clause : LicensingContext
• only_focus : LicensingContext
• question : LicensingContext
• comparative : LicensingContext
• superlative : LicensingContext
• too_to : LicensingContext
• modal_possibility : LicensingContext
• modal_necessity : LicensingContext
• imperative : LicensingContext
• generic : LicensingContext
• adversative : LicensingContext
• since_temporal : LicensingContext
• free_relative : LicensingContext

instance Core.Lexical.PolarityItem.instDecidableEqLicensingContext : DecidableEq LicensingContext

Equations

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

def Core.Lexical.PolarityItem.instBEqLicensingContext.beq : LicensingContext → LicensingContext → Bool

Equations

• Core.Lexical.PolarityItem.instBEqLicensingContext.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Lexical.PolarityItem.instBEqLicensingContext : BEq LicensingContext

Equations

• Core.Lexical.PolarityItem.instBEqLicensingContext = { beq := Core.Lexical.PolarityItem.instBEqLicensingContext.beq }

instance Core.Lexical.PolarityItem.instReprLicensingContext : Repr LicensingContext

Equations

• Core.Lexical.PolarityItem.instReprLicensingContext = { reprPrec := Core.Lexical.PolarityItem.instReprLicensingContext.repr }

def Core.Lexical.PolarityItem.instReprLicensingContext.repr : LicensingContext → Nat → Std.Format

Equations

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

inductive Core.Lexical.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

instance Core.Lexical.PolarityItem.instDecidableEqScalarValue : DecidableEq ScalarValue

Equations

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

def Core.Lexical.PolarityItem.instBEqScalarValue.beq : ScalarValue → ScalarValue → Bool

Equations

• Core.Lexical.PolarityItem.instBEqScalarValue.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Lexical.PolarityItem.instBEqScalarValue : BEq ScalarValue

Equations

• Core.Lexical.PolarityItem.instBEqScalarValue = { beq := Core.Lexical.PolarityItem.instBEqScalarValue.beq }

instance Core.Lexical.PolarityItem.instReprScalarValue : Repr ScalarValue

Equations

• Core.Lexical.PolarityItem.instReprScalarValue = { reprPrec := Core.Lexical.PolarityItem.instReprScalarValue.repr }

def Core.Lexical.PolarityItem.instReprScalarValue.repr : ScalarValue → Nat → Std.Format

Equations

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

inductive Core.Lexical.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 (lift a finger) are idiomatic, not scalar.

@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

instance Core.Lexical.PolarityItem.instDecidableEqScalarDirection : DecidableEq ScalarDirection

Equations

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

def Core.Lexical.PolarityItem.instBEqScalarDirection.beq : ScalarDirection → ScalarDirection → Bool

Equations

• Core.Lexical.PolarityItem.instBEqScalarDirection.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Lexical.PolarityItem.instBEqScalarDirection : BEq ScalarDirection

Equations

• Core.Lexical.PolarityItem.instBEqScalarDirection = { beq := Core.Lexical.PolarityItem.instBEqScalarDirection.beq }

instance Core.Lexical.PolarityItem.instReprScalarDirection : Repr ScalarDirection

Equations

• Core.Lexical.PolarityItem.instReprScalarDirection = { reprPrec := Core.Lexical.PolarityItem.instReprScalarDirection.repr }

def Core.Lexical.PolarityItem.instReprScalarDirection.repr : ScalarDirection → Nat → Std.Format

Equations

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

inductive Core.Lexical.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} §3–4 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

instance Core.Lexical.PolarityItem.instDecidableEqCanonicity : DecidableEq Canonicity

Equations

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

instance Core.Lexical.PolarityItem.instBEqCanonicity : BEq Canonicity

Equations

• Core.Lexical.PolarityItem.instBEqCanonicity = { beq := Core.Lexical.PolarityItem.instBEqCanonicity.beq }

def Core.Lexical.PolarityItem.instBEqCanonicity.beq : Canonicity → Canonicity → Bool

Equations

• Core.Lexical.PolarityItem.instBEqCanonicity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Lexical.PolarityItem.instReprCanonicity : Repr Canonicity

Equations

• Core.Lexical.PolarityItem.instReprCanonicity = { reprPrec := Core.Lexical.PolarityItem.instReprCanonicity.repr }

def Core.Lexical.PolarityItem.instReprCanonicity.repr : Canonicity → Nat → Std.Format

Equations

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

inductive Core.Lexical.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

instance Core.Lexical.PolarityItem.instDecidableEqLikelihoodEffect : DecidableEq LikelihoodEffect

Equations

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

instance Core.Lexical.PolarityItem.instBEqLikelihoodEffect : BEq LikelihoodEffect

Equations

• Core.Lexical.PolarityItem.instBEqLikelihoodEffect = { beq := Core.Lexical.PolarityItem.instBEqLikelihoodEffect.beq }

def Core.Lexical.PolarityItem.instBEqLikelihoodEffect.beq : LikelihoodEffect → LikelihoodEffect → Bool

Equations

• Core.Lexical.PolarityItem.instBEqLikelihoodEffect.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Lexical.PolarityItem.instReprLikelihoodEffect : Repr LikelihoodEffect

Equations

• Core.Lexical.PolarityItem.instReprLikelihoodEffect = { reprPrec := Core.Lexical.PolarityItem.instReprLikelihoodEffect.repr }

def Core.Lexical.PolarityItem.instReprLikelihoodEffect.repr : LikelihoodEffect → Nat → Std.Format

Equations

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

inductive Core.Lexical.PolarityItem.PolarityType : Type

Type of polarity sensitivity.

• npiWeak : PolarityType
• npiStrong : PolarityType
• fci : PolarityType
• npi_fci : PolarityType
• ppi : PolarityType

instance Core.Lexical.PolarityItem.instDecidableEqPolarityType : DecidableEq PolarityType

Equations

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

instance Core.Lexical.PolarityItem.instBEqPolarityType : BEq PolarityType

Equations

• Core.Lexical.PolarityItem.instBEqPolarityType = { beq := Core.Lexical.PolarityItem.instBEqPolarityType.beq }

def Core.Lexical.PolarityItem.instBEqPolarityType.beq : PolarityType → PolarityType → Bool

Equations

• Core.Lexical.PolarityItem.instBEqPolarityType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Lexical.PolarityItem.instReprPolarityType : Repr PolarityType

Equations

• Core.Lexical.PolarityItem.instReprPolarityType = { reprPrec := Core.Lexical.PolarityItem.instReprPolarityType.repr }

def Core.Lexical.PolarityItem.instReprPolarityType.repr : PolarityType → Nat → Std.Format

Equations

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

inductive Core.Lexical.PolarityItem.BaseForce : Type

Base quantificational force (when interpretable).

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

instance Core.Lexical.PolarityItem.instDecidableEqBaseForce : DecidableEq BaseForce

Equations

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

instance Core.Lexical.PolarityItem.instBEqBaseForce : BEq BaseForce

Equations

• Core.Lexical.PolarityItem.instBEqBaseForce = { beq := Core.Lexical.PolarityItem.instBEqBaseForce.beq }

def Core.Lexical.PolarityItem.instBEqBaseForce.beq : BaseForce → BaseForce → Bool

Equations

• Core.Lexical.PolarityItem.instBEqBaseForce.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Core.Lexical.PolarityItem.instReprBaseForce.repr : BaseForce → Nat → Std.Format

Equations

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

instance Core.Lexical.PolarityItem.instReprBaseForce : Repr BaseForce

Equations

• Core.Lexical.PolarityItem.instReprBaseForce = { reprPrec := Core.Lexical.PolarityItem.instReprBaseForce.repr }

inductive Core.Lexical.PolarityItem.NPIMorphology : Type

Morphological composition of a polarity-sensitive item. @cite{lahiri-1998} shows Hindi NPIs are transparently indefinite + even. @cite{lee-horn-1994} document this pattern cross-linguistically.

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

instance Core.Lexical.PolarityItem.instDecidableEqNPIMorphology : DecidableEq NPIMorphology

Equations

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

def Core.Lexical.PolarityItem.instBEqNPIMorphology.beq : NPIMorphology → NPIMorphology → Bool

Equations

• Core.Lexical.PolarityItem.instBEqNPIMorphology.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Lexical.PolarityItem.instBEqNPIMorphology : BEq NPIMorphology

Equations

• Core.Lexical.PolarityItem.instBEqNPIMorphology = { beq := Core.Lexical.PolarityItem.instBEqNPIMorphology.beq }

instance Core.Lexical.PolarityItem.instReprNPIMorphology : Repr NPIMorphology

Equations

• Core.Lexical.PolarityItem.instReprNPIMorphology = { reprPrec := Core.Lexical.PolarityItem.instReprNPIMorphology.repr }

def Core.Lexical.PolarityItem.instReprNPIMorphology.repr : NPIMorphology → Nat → Std.Format

Equations

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

inductive Core.Lexical.PolarityItem.AlternativeType : Type

Type of alternatives introduced by the focused element. @cite{lahiri-1998} §8: 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

instance Core.Lexical.PolarityItem.instDecidableEqAlternativeType : DecidableEq AlternativeType

Equations

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

def Core.Lexical.PolarityItem.instBEqAlternativeType.beq : AlternativeType → AlternativeType → Bool

Equations

• Core.Lexical.PolarityItem.instBEqAlternativeType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Lexical.PolarityItem.instBEqAlternativeType : BEq AlternativeType

Equations

• Core.Lexical.PolarityItem.instBEqAlternativeType = { beq := Core.Lexical.PolarityItem.instBEqAlternativeType.beq }

def Core.Lexical.PolarityItem.instReprAlternativeType.repr : AlternativeType → Nat → Std.Format

Equations

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

instance Core.Lexical.PolarityItem.instReprAlternativeType : Repr AlternativeType

Equations

• Core.Lexical.PolarityItem.instReprAlternativeType = { reprPrec := Core.Lexical.PolarityItem.instReprAlternativeType.repr }

structure Core.Lexical.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)

• 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} §3)

• likelihoodEffect : LikelihoodEffect

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

• morphology : NPIMorphology

  Morphological composition (@cite{lahiri-1998})

• alternativeType : AlternativeType

  Type of alternatives introduced

• notes : String

  Notes

def Core.Lexical.PolarityItem.instReprPolarityItemEntry.repr : PolarityItemEntry → Nat → Std.Format

Equations

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

instance Core.Lexical.PolarityItem.instReprPolarityItemEntry : Repr PolarityItemEntry

Equations

• Core.Lexical.PolarityItem.instReprPolarityItemEntry = { reprPrec := Core.Lexical.PolarityItem.instReprPolarityItemEntry.repr }

def Core.Lexical.PolarityItem.isLicensedIn (item : PolarityItemEntry) (ctx : LicensingContext) : Bool

Check if a context licenses a polarity item.

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

Equations

• Core.Lexical.PolarityItem.isLicensedIn item ctx = item.licensingContexts.contains ctx

def Core.Lexical.PolarityItem.PolarityItemEntry.isNPI (p : PolarityItemEntry) : Bool

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

Equations

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

def Core.Lexical.PolarityItem.PolarityItemEntry.isFCI (p : PolarityItemEntry) : Bool

Check if an item is an FCI.

Equations

• p.isFCI = match p.polarityType with | Core.Lexical.PolarityItem.PolarityType.fci => true | Core.Lexical.PolarityItem.PolarityType.npi_fci => true | x => false

def Core.Lexical.PolarityItem.PolarityItemEntry.isPPI (p : PolarityItemEntry) : Bool

Check if an item is a PPI.

Equations

• p.isPPI = (p.polarityType == Core.Lexical.PolarityItem.PolarityType.ppi)

def Core.Lexical.PolarityItem.predictCanonicity (le : LikelihoodEffect) (pt : PolarityType) : Canonicity

Israel's prediction (@cite{israel-2001} §4): canonical/inverted is determined solely by likelihood effect (propositional role).

• Impeding roles → canonical items
• Facilitating roles → inverted items

This holds for both NPIs and PPIs, regardless of scalar value. Scalar value determines WHERE on the scale an item sits; likelihood effect determines WHETHER the item is canonical or inverted.

Equations

• Core.Lexical.PolarityItem.predictCanonicity le Core.Lexical.PolarityItem.PolarityType.fci = Core.Lexical.PolarityItem.Canonicity.unknown
• Core.Lexical.PolarityItem.predictCanonicity Core.Lexical.PolarityItem.LikelihoodEffect.impeding pt = Core.Lexical.PolarityItem.Canonicity.canonical
• Core.Lexical.PolarityItem.predictCanonicity Core.Lexical.PolarityItem.LikelihoodEffect.facilitating pt = Core.Lexical.PolarityItem.Canonicity.inverted
• Core.Lexical.PolarityItem.predictCanonicity Core.Lexical.PolarityItem.LikelihoodEffect.unknown pt = Core.Lexical.PolarityItem.Canonicity.unknown

def Core.Lexical.PolarityItem.PolarityItemEntry.canonicityConsistent (p : PolarityItemEntry) : Bool

Check if a polarity item's stated canonicity agrees with the prediction. Returns true if canonicity or likelihood effect is unknown (insufficient data), or if the stated canonicity matches the prediction from likelihood effect.

Equations

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