The scalar model of polarity items

[Isr96] [Isr01] [Isr11]

The scalar-model classification of polarity items and its canonicity prediction. ScalarItem extends Polarity.Item with the [Isr01] axes — scalar value, canonicity, and the propositional role's likelihood effect — and is built only for items that have the classification, so no axis carries an "unknown" case. The central empirical claim: for emphatic polarity items, canonical vs inverted is determined by likelihood effect (impeding roles → canonical, facilitating → inverted), dissolving the pecuniary paradox (a red cent NPI vs for peanuts PPI in one monetary domain) — explanatory weight that per-context monotonicity accounts lack. The Israel↔Ladusaw refutation theorem — a context where role-likelihood and monotonicity licensing diverge — remains deferred to Studies/Israel2001.lean.

Main declarations

• ScalarValue, Canonicity, LikelihoodEffect — the scalar-model axes.
• ScalarItem — a polarity item with its scalar-model classification.
• predictCanonicity, ScalarItem.canonicityConsistent — the role-likelihood prediction and its validation predicate (checked over the English lexicon and Studies/Israel2001.lean).

The scalar-model axes

inductive Polarity.ScalarValue : Type

Where the item sits on its scale relative to the norm: emphatic NPIs typically denote low values (a wink), emphatic PPIs high ones (tons); inverted items reverse the pattern ([Isr01]).

• high : ScalarValue
• low : ScalarValue

@[instance_reducible]

instance Polarity.instDecidableEqScalarValue : DecidableEq ScalarValue

Equations

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

@[instance_reducible]

instance Polarity.instReprScalarValue : Repr ScalarValue

Equations

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

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

Equations

• Polarity.instReprScalarValue.repr Polarity.ScalarValue.high prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Polarity.ScalarValue.high")).group prec✝
• Polarity.instReprScalarValue.repr Polarity.ScalarValue.low prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Polarity.ScalarValue.low")).group prec✝

inductive Polarity.Canonicity : Type

Whether scalar value tracks polarity in the default way (canonical emphatic NPIs low, PPIs high) or inversely (wild horses, at the drop of a hat); inversion tracks propositional role ([Isr01]).

• canonical : Canonicity
• inverted : Canonicity

@[instance_reducible]

instance Polarity.instDecidableEqCanonicity : DecidableEq Canonicity

Equations

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

@[instance_reducible]

instance Polarity.instReprCanonicity : Repr Canonicity

Equations

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

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

Equations

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

inductive Polarity.LikelihoodEffect : Type

How increasing the referent's scalar value affects event likelihood: facilitating roles (agent, stimulus, reward) invert the scale, impeding roles (patient, increment, expense) keep it canonical — [Isr01]'s resolution of the maximizer/minimizer puzzle.

• facilitating : LikelihoodEffect
• impeding : LikelihoodEffect

@[instance_reducible]

instance Polarity.instDecidableEqLikelihoodEffect : DecidableEq LikelihoodEffect

Equations

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

@[instance_reducible]

instance Polarity.instReprLikelihoodEffect : Repr LikelihoodEffect

Equations

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

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

Equations

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

The classified item

structure Polarity.ScalarItemextends Polarity.Item : Type

A polarity item together with its [Isr01] scalar-model classification. Built only for items the literature classifies; unclassified items stay plain Items. The likelihood effect is the propositional-role explanans of the canonicity — present exactly where the literature gives the role analysis.

• form : String
• baseForce : BaseForce
• licensor : Option DEStrength
• freeChoice : Bool
• ppi : Bool
• licensingContexts : List LicensingContext
• scalarDirection : Option ScalarDirection
• morphology : NPIMorphology
• alternativeType : AlternativeType
• scalarValue : ScalarValue

  Scalar value relative to the norm.

• canonicity : Canonicity

  Canonical or inverted value–polarity linkage.

• likelihoodEffect : Option LikelihoodEffect

  The propositional role's likelihood effect; none = no role analysis in the literature.

def Polarity.instReprScalarItem.repr : ScalarItem → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Polarity.instReprScalarItem : Repr ScalarItem

Equations

• Polarity.instReprScalarItem = { reprPrec := Polarity.instReprScalarItem.repr }

The canonicity prediction

def Polarity.predictCanonicity (le : LikelihoodEffect) (pureFC : Bool) : Option Canonicity

Israel's prediction ([Isr01]): for emphatic polarity items, canonical vs inverted is determined principally by likelihood effect — impeding roles → canonical, facilitating → inverted. Scalar value determines WHERE on the scale an item sits; likelihood effect determines WHETHER the item is canonical or inverted.

The pure-FC case returns none: an editorial decision that the substrate declines to predict canonicity for FCIs; Israel 2001 mostly bracketed FCIs rather than asserting they have no canonicity. The mapping is applied uniformly across item classes although it is most robust for emphatic strengtheners and PPIs; attenuators interact differently and Israel allows lexical exceptions — consumers should consult scalarDirection separately when distinguishing emphatic from attenuating items.

Equations

• Polarity.predictCanonicity Polarity.LikelihoodEffect.impeding pureFC = if pureFC = true then none else some Polarity.Canonicity.canonical
• Polarity.predictCanonicity Polarity.LikelihoodEffect.facilitating pureFC = if pureFC = true then none else some Polarity.Canonicity.inverted

@[reducible, inline]

abbrev Polarity.ScalarItem.canonicityConsistent (p : ScalarItem) : Prop

A classified item's stated canonicity agrees with the role-likelihood prediction, wherever a role analysis exists (vacuously for items without one and for pure FCIs, where the substrate declines to predict).

Equations

• p.canonicityConsistent = ∀ le ∈ p.likelihoodEffect, ∀ c ∈ Polarity.predictCanonicity le (p.freeChoice && p.licensor.isNone), p.canonicity = c