Core Negation Types

Framework-agnostic types for negation phenomena shared across fragments and phenomena layers.

Expletive Negation Classification

Two orthogonal classifications of expletive negation (EN):

• ENType (high/low) — @cite{rett-2026}'s position-based classification
• ENStrength (weak/strong) — @cite{greco-2020}'s polarity-based classification
• PolarityClass / PolarityLicensing — polarity-sensitive element classes and their licensing profiles

These types are framework-agnostic: they classify EN constructions by their empirical properties without committing to a syntactic analysis. The syntactic derivation (from merge position in the extended projection) lives in Phenomena.Negation.Studies.Greco2020 under namespace Minimalist.NegScope.

inductive Phenomena.Negation.ExpletiveNegation.ENBlockingReason : Type

Cross-linguistic reasons why a trigger class may not license expletive negation in a particular language (@cite{jin-koenig-2021} §7).

• modalRestriction : ENBlockingReason

  Language disprefers modal operators in complement clauses

• npOnlyComplement : ENBlockingReason

  Comparative complements only allow NPs, not clauses

• analyticNegation : ENBlockingReason

  Concept expressed analytically with necessary (non-expletive) negation

@[implicit_reducible]

instance Phenomena.Negation.ExpletiveNegation.instDecidableEqENBlockingReason : DecidableEq ENBlockingReason

Equations

• Phenomena.Negation.ExpletiveNegation.instDecidableEqENBlockingReason x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.Negation.ExpletiveNegation.instReprENBlockingReason : Repr ENBlockingReason

Equations

• Phenomena.Negation.ExpletiveNegation.instReprENBlockingReason = { reprPrec := Phenomena.Negation.ExpletiveNegation.instReprENBlockingReason.repr }

def Phenomena.Negation.ExpletiveNegation.instReprENBlockingReason.repr : ENBlockingReason → ℕ → Std.Format

Equations

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

inductive Phenomena.Negation.ExpletiveNegation.ENType : Type

Two syntactic types of expletive negation (@cite{rett-2026}).

High EN appears above TP, targets non-truth-conditional content (exclamatives, surprise negation). It is obligatory where licensed.

Low EN appears below TP (VP-level), targets truth-conditional content in ambidirectional environments. It is optional and triggers a manner implicature (evaluativity).

• high : ENType
• low : ENType

@[implicit_reducible]

instance Phenomena.Negation.ExpletiveNegation.instDecidableEqENType : DecidableEq ENType

Equations

• Phenomena.Negation.ExpletiveNegation.instDecidableEqENType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Negation.ExpletiveNegation.instReprENType.repr : ENType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Negation.ExpletiveNegation.instReprENType : Repr ENType

Equations

• Phenomena.Negation.ExpletiveNegation.instReprENType = { reprPrec := Phenomena.Negation.ExpletiveNegation.instReprENType.repr }

def Phenomena.Negation.ExpletiveNegation.ENType.equivBool : ENType ≃ Bool

ENType ≃ Bool: low ↦ false, high ↦ true.

Equations

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

@[implicit_reducible]

instance Phenomena.Negation.ExpletiveNegation.instFintypeENType : Fintype ENType

Equations

• Phenomena.Negation.ExpletiveNegation.instFintypeENType = Fintype.ofEquiv Bool Phenomena.Negation.ExpletiveNegation.ENType.equivBool.symm

def Phenomena.Negation.ExpletiveNegation.ENType.toNat : ENType → ℕ

Numeric embedding: low ↦ 0, high ↦ 1. Ordering: low < high (truth-conditional before non-truth-conditional).

Equations

• Phenomena.Negation.ExpletiveNegation.ENType.low.toNat = 0
• Phenomena.Negation.ExpletiveNegation.ENType.high.toNat = 1

@[implicit_reducible]

instance Phenomena.Negation.ExpletiveNegation.instLinearOrderENType : LinearOrder ENType

Equations

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

inductive Phenomena.Negation.ExpletiveNegation.ENStrength : Type

@cite{greco-2020} §2.1: EN constructions divide into two classes based on co-occurrence with polarity-sensitive elements.

Weak EN retains some polarity properties of standard negation: licenses weak NPIs and N-words (e.g. finché-clauses, unless-clauses).

Strong EN loses all polarity properties: rejects weak NPIs, strong NPIs, not-also conjunctions, and N-words (e.g. negative exclamatives, rhetorical questions, surprise negation).

• weak : ENStrength
• strong : ENStrength

@[implicit_reducible]

instance Phenomena.Negation.ExpletiveNegation.instDecidableEqENStrength : DecidableEq ENStrength

Equations

• Phenomena.Negation.ExpletiveNegation.instDecidableEqENStrength x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.Negation.ExpletiveNegation.instReprENStrength : Repr ENStrength

Equations

• Phenomena.Negation.ExpletiveNegation.instReprENStrength = { reprPrec := Phenomena.Negation.ExpletiveNegation.instReprENStrength.repr }

def Phenomena.Negation.ExpletiveNegation.instReprENStrength.repr : ENStrength → ℕ → Std.Format

Equations

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

def Phenomena.Negation.ExpletiveNegation.ENStrength.equivBool : ENStrength ≃ Bool

ENStrength ≃ Bool: weak ↦ false, strong ↦ true.

Equations

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

@[implicit_reducible]

instance Phenomena.Negation.ExpletiveNegation.instFintypeENStrength : Fintype ENStrength

Equations

• Phenomena.Negation.ExpletiveNegation.instFintypeENStrength = Fintype.ofEquiv Bool Phenomena.Negation.ExpletiveNegation.ENStrength.equivBool.symm

def Phenomena.Negation.ExpletiveNegation.ENStrength.toNat : ENStrength → ℕ

Numeric embedding: weak ↦ 0, strong ↦ 1. Ordering: weak < strong (retains-polarity before loses-polarity).

Equations

• Phenomena.Negation.ExpletiveNegation.ENStrength.weak.toNat = 0
• Phenomena.Negation.ExpletiveNegation.ENStrength.strong.toNat = 1

@[implicit_reducible]

instance Phenomena.Negation.ExpletiveNegation.instLinearOrderENStrength : LinearOrder ENStrength

Equations

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

inductive Phenomena.Negation.ExpletiveNegation.PolarityClass : Type

The four classes of polarity-sensitive elements tested by @cite{greco-2020} Table 1. Each EN environment either licenses or rejects each class, giving a four-bit fingerprint.

• weakNPI : PolarityClass
• strongNPI : PolarityClass
• notAlsoConj : PolarityClass
• nWord : PolarityClass

@[implicit_reducible]

instance Phenomena.Negation.ExpletiveNegation.instDecidableEqPolarityClass : DecidableEq PolarityClass

Equations

• Phenomena.Negation.ExpletiveNegation.instDecidableEqPolarityClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.Negation.ExpletiveNegation.instReprPolarityClass : Repr PolarityClass

Equations

• Phenomena.Negation.ExpletiveNegation.instReprPolarityClass = { reprPrec := Phenomena.Negation.ExpletiveNegation.instReprPolarityClass.repr }

def Phenomena.Negation.ExpletiveNegation.instReprPolarityClass.repr : PolarityClass → ℕ → Std.Format

Equations

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

def Phenomena.Negation.ExpletiveNegation.PolarityClass.equivFin : PolarityClass ≃ Fin 4

PolarityClass ≃ Fin 4: weakNPI ↦ 0, strongNPI ↦ 1, notAlsoConj ↦ 2, nWord ↦ 3.

Equations

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

@[implicit_reducible]

instance Phenomena.Negation.ExpletiveNegation.instFintypePolarityClass : Fintype PolarityClass

Equations

• Phenomena.Negation.ExpletiveNegation.instFintypePolarityClass = Fintype.ofEquiv (Fin 4) Phenomena.Negation.ExpletiveNegation.PolarityClass.equivFin.symm

structure Phenomena.Negation.ExpletiveNegation.PolarityLicensing : Type

Polarity licensing profile for an EN environment (@cite{greco-2020} Table 1). Each field records whether that class of polarity-sensitive element is grammatical in the construction.

• weakNPIs : Bool
• strongNPIs : Bool
• notAlsoConj : Bool
• nWords : Bool

def Phenomena.Negation.ExpletiveNegation.instDecidableEqPolarityLicensing.decEq (x✝ x✝¹ : PolarityLicensing) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Phenomena.Negation.ExpletiveNegation.instDecidableEqPolarityLicensing : DecidableEq PolarityLicensing

Equations

• Phenomena.Negation.ExpletiveNegation.instDecidableEqPolarityLicensing = Phenomena.Negation.ExpletiveNegation.instDecidableEqPolarityLicensing.decEq

@[implicit_reducible]

instance Phenomena.Negation.ExpletiveNegation.instReprPolarityLicensing : Repr PolarityLicensing

Equations

• Phenomena.Negation.ExpletiveNegation.instReprPolarityLicensing = { reprPrec := Phenomena.Negation.ExpletiveNegation.instReprPolarityLicensing.repr }

def Phenomena.Negation.ExpletiveNegation.instReprPolarityLicensing.repr : PolarityLicensing → ℕ → Std.Format

Equations

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

def Phenomena.Negation.ExpletiveNegation.PolarityLicensing.licenses (p : PolarityLicensing) : PolarityClass → Bool

Accessor: look up a polarity class in the licensing profile.

Equations

• p.licenses Phenomena.Negation.ExpletiveNegation.PolarityClass.weakNPI = p.weakNPIs
• p.licenses Phenomena.Negation.ExpletiveNegation.PolarityClass.strongNPI = p.strongNPIs
• p.licenses Phenomena.Negation.ExpletiveNegation.PolarityClass.notAlsoConj = p.notAlsoConj
• p.licenses Phenomena.Negation.ExpletiveNegation.PolarityClass.nWord = p.nWords

def Phenomena.Negation.ExpletiveNegation.weakENProfile : PolarityLicensing

Weak EN environments license weak NPIs and N-words but NOT strong NPIs or not-also conjunctions.

Equations

• Phenomena.Negation.ExpletiveNegation.weakENProfile = { weakNPIs := true, strongNPIs := false, notAlsoConj := false, nWords := true }

def Phenomena.Negation.ExpletiveNegation.strongENProfile : PolarityLicensing

Strong EN environments license NONE of the four polarity classes.

Equations

• Phenomena.Negation.ExpletiveNegation.strongENProfile = { weakNPIs := false, strongNPIs := false, notAlsoConj := false, nWords := false }

theorem Phenomena.Negation.ExpletiveNegation.strongEN_rejects_all (c : PolarityClass) : strongENProfile.licenses c = false

Strong EN rejects ALL polarity classes (universally quantified).

theorem Phenomena.Negation.ExpletiveNegation.weakEN_licenses_weakNPI : weakENProfile.licenses PolarityClass.weakNPI = true

Weak EN licenses exactly the weak NPIs and N-words.

theorem Phenomena.Negation.ExpletiveNegation.weakEN_licenses_nWord : weakENProfile.licenses PolarityClass.nWord = true

theorem Phenomena.Negation.ExpletiveNegation.weakEN_rejects_strongNPI : weakENProfile.licenses PolarityClass.strongNPI = false

theorem Phenomena.Negation.ExpletiveNegation.weakEN_rejects_notAlso : weakENProfile.licenses PolarityClass.notAlsoConj = false

def Phenomena.Negation.ExpletiveNegation.PolarityLicensing.equiv : PolarityLicensing ≃ Bool × Bool × Bool × Bool

Equivalence with Bool⁴ for Fintype derivation.

Equations

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

@[implicit_reducible]

instance Phenomena.Negation.ExpletiveNegation.instFintypePolarityLicensing : Fintype PolarityLicensing

Equations

• Phenomena.Negation.ExpletiveNegation.instFintypePolarityLicensing = Fintype.ofEquiv (Bool × Bool × Bool × Bool) Phenomena.Negation.ExpletiveNegation.PolarityLicensing.equiv.symm

@[implicit_reducible]

instance Phenomena.Negation.ExpletiveNegation.instPartialOrderPolarityLicensing : PartialOrder PolarityLicensing

Equations

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

@[implicit_reducible]

instance Phenomena.Negation.ExpletiveNegation.instDecidableRelPolarityLicensingLe : DecidableRel fun (x1 x2 : PolarityLicensing) => x1 ≤ x2

Equations

• Phenomena.Negation.ExpletiveNegation.instDecidableRelPolarityLicensingLe a b = instDecidableEqBool (Phenomena.Negation.ExpletiveNegation.PolarityLicensing.leBool✝ a b) true

@[implicit_reducible]

instance Phenomena.Negation.ExpletiveNegation.instLatticePolarityLicensing : Lattice PolarityLicensing

Equations

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

def Phenomena.Negation.ExpletiveNegation.standardNegProfile : PolarityLicensing

Standard negation profile: licenses all polarity-sensitive elements.

Equations

• Phenomena.Negation.ExpletiveNegation.standardNegProfile = { weakNPIs := true, strongNPIs := true, notAlsoConj := true, nWords := true }

@[implicit_reducible]

instance Phenomena.Negation.ExpletiveNegation.instOrderBotPolarityLicensing : OrderBot PolarityLicensing

Equations

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

@[implicit_reducible]

instance Phenomena.Negation.ExpletiveNegation.instOrderTopPolarityLicensing : OrderTop PolarityLicensing

Equations

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

theorem Phenomena.Negation.ExpletiveNegation.strongEN_le_weakEN : strongENProfile ≤ weakENProfile

Strong EN (⊥) ≤ weak EN in the licensing lattice.

def Phenomena.Negation.ExpletiveNegation.PolarityClass.toPolarityType? : PolarityClass → Option Typology.PolarityItem.PolarityType

Partial map from PolarityClass to PolarityType. Two of the four Greco classes correspond directly to PolarityType constructors. N-words and not-also conjunctions are Italian-specific categories without a PolarityType counterpart.

Equations

• Phenomena.Negation.ExpletiveNegation.PolarityClass.weakNPI.toPolarityType? = some Typology.PolarityItem.PolarityType.npiWeak
• Phenomena.Negation.ExpletiveNegation.PolarityClass.strongNPI.toPolarityType? = some Typology.PolarityItem.PolarityType.npiStrong
• x✝.toPolarityType? = none

def Phenomena.Negation.ExpletiveNegation.PolarityClass.fromPolarityType? : Typology.PolarityItem.PolarityType → Option PolarityClass

Inverse: map PolarityType to PolarityClass (partial — only NPIs).

Equations

• Phenomena.Negation.ExpletiveNegation.PolarityClass.fromPolarityType? Typology.PolarityItem.PolarityType.npiWeak = some Phenomena.Negation.ExpletiveNegation.PolarityClass.weakNPI
• Phenomena.Negation.ExpletiveNegation.PolarityClass.fromPolarityType? Typology.PolarityItem.PolarityType.npiStrong = some Phenomena.Negation.ExpletiveNegation.PolarityClass.strongNPI
• Phenomena.Negation.ExpletiveNegation.PolarityClass.fromPolarityType? x✝ = none

theorem Phenomena.Negation.ExpletiveNegation.PolarityClass.roundtrip_npiWeak : (fromPolarityType? Typology.PolarityItem.PolarityType.npiWeak).bind toPolarityType? = some Typology.PolarityItem.PolarityType.npiWeak

Round-trip: PolarityType → PolarityClass → PolarityType is identity (for the NPI types that have counterparts).

theorem Phenomena.Negation.ExpletiveNegation.PolarityClass.roundtrip_npiStrong : (fromPolarityType? Typology.PolarityItem.PolarityType.npiStrong).bind toPolarityType? = some Typology.PolarityItem.PolarityType.npiStrong

def Phenomena.Negation.ExpletiveNegation.PolarityLicensing.licensesType (p : PolarityLicensing) (t : Typology.PolarityItem.PolarityType) : Option Bool

Compose the bridges: look up a PolarityType in a licensing profile by routing through PolarityClass. Returns none for types without a PolarityClass counterpart (FCIs, PPIs, NPI-FCIs).

Equations

• p.licensesType t = Option.map p.licenses (Phenomena.Negation.ExpletiveNegation.PolarityClass.fromPolarityType? t)