Polarity items

[Lad79] [zwarts-1998] [Has97] [Lah98] [israel-1996] [Isr01] [israel-2011] [chierchia-2006]

PolarityItem, the lexical record for polarity-sensitive items, with its licensing parameters instantiated directly: licensor is the minimum Zwarts strength an environment must supply (none = not strength-licensed), freeChoice marks licensing by the generic-indefinite mechanism, and ppi marks positive-polarity blocking. Class labels are derived (isNPI, isFCI, isPPI), not stipulated: a weak NPI is an item with licensor = some .weak, a strict negative-concord item one with some .antiMorphic (clausal negation is the only anti-morphic environment), a non-strict one some .antiAdditive (concord under a negative quantifier is anti-additive licensing at this grain — the same requirement as an English strong NPI; the concord phenomenology itself is Studies/VanDerAuweraVanAlsenoy2016.lean territory). The item↔context licensing relation LicensingContext.licenses lives in Semantics/Polarity/Licensing.lean.

The record also carries the [israel-1996] scalar direction and the [Lah98]-style morphological-composition typology. The [Isr01] classification of items by quantity and propositional role lives with that paper in Studies/Israel2001.lean.

Main declarations

• PolarityItem — the polarity-item record.
• PolarityItem.isNPI, PolarityItem.isFCI, PolarityItem.isPPI — derived class labels.
• ScalarDirection — strengthening vs attenuating rhetorical force.
• NPIMorphology, AlternativeType — composition typology.

Scalar direction

inductive PolarityItem.ScalarDirection : Type

Rhetorical force: strengthening items (ever, any) make the assertion stronger than its scalar alternatives, attenuating ones (all that, long) weaker ([israel-1996], [israel-2011]). nonScalar is an editorial slot — Israel classifies most minimizers, including lift a finger, as scalar; leave the item's field none if unsure.

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

@[instance_reducible]

instance PolarityItem.instDecidableEqScalarDirection : DecidableEq ScalarDirection

Equations

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

def PolarityItem.instReprScalarDirection.repr : ScalarDirection → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance PolarityItem.instReprScalarDirection : Repr ScalarDirection

Equations

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

Force and composition typology

inductive PolarityItem.BaseForce : Type

Base quantificational force (when interpretable).

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

@[instance_reducible]

instance PolarityItem.instDecidableEqBaseForce : DecidableEq BaseForce

Equations

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

def PolarityItem.instReprBaseForce.repr : BaseForce → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance PolarityItem.instReprBaseForce : Repr BaseForce

Equations

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

inductive PolarityItem.NPIMorphology : Type

Morphological composition of a polarity-sensitive item ([Lah98]: Hindi NPIs are transparently indefinite + even). indefPlusNeg covers genuine indefinite + negation morphology (Romanian nimic, some Slavic n-words).

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

@[instance_reducible]

instance PolarityItem.instDecidableEqNPIMorphology : DecidableEq NPIMorphology

Equations

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

def PolarityItem.instReprNPIMorphology.repr : NPIMorphology → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance PolarityItem.instReprNPIMorphology : Repr NPIMorphology

Equations

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

inductive PolarityItem.AlternativeType : Type

Type of alternatives the item activates: cardinality (ek bhii), contextually salient properties (koii bhii) ([Lah98]), or subdomain alternatives ([chierchia-2006]).

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

@[instance_reducible]

instance PolarityItem.instDecidableEqAlternativeType : DecidableEq AlternativeType

Equations

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

@[instance_reducible]

instance PolarityItem.instReprAlternativeType : Repr AlternativeType

Equations

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

def PolarityItem.instReprAlternativeType.repr : AlternativeType → ℕ → Std.Format

Equations

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

The polarity item

structure PolarityItem : Type

A lexical entry for a polarity-sensitive item, with the licensing parameters instantiated directly: licensor (minimum Zwarts strength of a licensing environment), freeChoice (generic-indefinite mechanism), ppi (blocked in DE). Class labels derive from these — see isNPI/isFCI/isPPI and the docstring conventions in the module header. licensingContexts is the attested distribution the keystone (LicensingContext.licenses) checks the parameters against.

• form : String

  Surface form

• baseForce : BaseForce

  Base quantificational/semantic force

• licensor : Option DEStrength

  Minimum Zwarts strength of a licensing environment (none = not strength-licensed).

• freeChoice : Bool

  Licensed by the generic-indefinite mechanism (modals, generics, imperatives, free relatives).

• ppi : Bool

  Positive polarity: blocked in DE environments.

• licensingContexts : List LicensingContext

  Attested licensing environments (empty = needs positive contexts).

• scalarDirection : Option ScalarDirection

  Scalar direction ([israel-1996]); none = unclassified.

• morphology : NPIMorphology

  Morphological composition ([Lah98])

• alternativeType : AlternativeType

  Type of alternatives introduced

def PolarityItem.instRepr.repr : PolarityItem → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance PolarityItem.instRepr : Repr PolarityItem

Equations

• PolarityItem.instRepr = { reprPrec := PolarityItem.instRepr.repr }

Derived class labels

@[reducible, inline]

abbrev PolarityItem.isNPI (e : PolarityItem) : Prop

An NPI is an item with a strength requirement.

Equations

• e.isNPI = (e.licensor.isSome = true)

@[reducible, inline]

abbrev PolarityItem.isFCI (e : PolarityItem) : Prop

A free choice item is one licensed by the generic-indefinite mechanism (dual NPI/FCIs like any also carry a licensor).

Equations

• e.isFCI = (e.freeChoice = true)

@[reducible, inline]

abbrev PolarityItem.isPPI (e : PolarityItem) : Prop

A positive polarity item.

Equations

• e.isPPI = (e.ppi = true)