Expletive Negation Typology

Pre-Fragment typological substrate for expletive negation (EN): framework-agnostic classification types that Fragments and Studies import to type their per-language EN data. The trigger-class / licensing apparatus traces to [Esp92]'s logical-absorption account, on which the [Gre20] / [Ret26] refinements build.

Two orthogonal classifications:

• ENType (high/low) — [Ret26]'s position-based classification
• ENStrength (weak/strong) — [Gre20]'s polarity-based classification
• PolarityClass / PolarityLicensing — polarity-sensitive element classes and their licensing profiles

These types 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 Studies/Greco2020.lean under namespace Minimalist.NegScope.

EN blocking reasons

inductive Semantics.Negation.ENBlockingReason : Type

Cross-linguistic reasons why a trigger class may not license expletive negation in a particular language ([JK21] §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 Semantics.Negation.instDecidableEqENBlockingReason : DecidableEq ENBlockingReason

Equations

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

def Semantics.Negation.instReprENBlockingReason.repr : ENBlockingReason → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Negation.instReprENBlockingReason : Repr ENBlockingReason

Equations

• Semantics.Negation.instReprENBlockingReason = { reprPrec := Semantics.Negation.instReprENBlockingReason.repr }

EN type classification

inductive Semantics.Negation.ENType : Type

Two syntactic types of expletive negation ([Ret26]).

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 Semantics.Negation.instDecidableEqENType : DecidableEq ENType

Equations

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

@[implicit_reducible]

instance Semantics.Negation.instReprENType : Repr ENType

Equations

• Semantics.Negation.instReprENType = { reprPrec := Semantics.Negation.instReprENType.repr }

def Semantics.Negation.instReprENType.repr : ENType → ℕ → Std.Format

Equations

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

def Semantics.Negation.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 Semantics.Negation.instFintypeENType : Fintype ENType

Equations

• Semantics.Negation.instFintypeENType = Fintype.ofEquiv Bool Semantics.Negation.ENType.equivBool.symm

def Semantics.Negation.ENType.toNat : ENType → ℕ

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

Equations

• Semantics.Negation.ENType.low.toNat = 0
• Semantics.Negation.ENType.high.toNat = 1

@[implicit_reducible]

instance Semantics.Negation.instLinearOrderENType : LinearOrder ENType

Equations

• Semantics.Negation.instLinearOrderENType = LinearOrder.lift' Semantics.Negation.ENType.toNat Semantics.Negation.instLinearOrderENType._proof_1

EN strength classification

inductive Semantics.Negation.ENStrength : Type

[Gre20] §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 Semantics.Negation.instDecidableEqENStrength : DecidableEq ENStrength

Equations

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

def Semantics.Negation.instReprENStrength.repr : ENStrength → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Negation.instReprENStrength : Repr ENStrength

Equations

• Semantics.Negation.instReprENStrength = { reprPrec := Semantics.Negation.instReprENStrength.repr }

def Semantics.Negation.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 Semantics.Negation.instFintypeENStrength : Fintype ENStrength

Equations

• Semantics.Negation.instFintypeENStrength = Fintype.ofEquiv Bool Semantics.Negation.ENStrength.equivBool.symm

def Semantics.Negation.ENStrength.toNat : ENStrength → ℕ

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

Equations

• Semantics.Negation.ENStrength.weak.toNat = 0
• Semantics.Negation.ENStrength.strong.toNat = 1

@[implicit_reducible]

instance Semantics.Negation.instLinearOrderENStrength : LinearOrder ENStrength

Equations

• Semantics.Negation.instLinearOrderENStrength = LinearOrder.lift' Semantics.Negation.ENStrength.toNat Semantics.Negation.instLinearOrderENStrength._proof_1

Polarity classes and licensing profiles

inductive Semantics.Negation.PolarityClass : Type

The four classes of polarity-sensitive elements tested by [Gre20] 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 Semantics.Negation.instDecidableEqPolarityClass : DecidableEq PolarityClass

Equations

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

def Semantics.Negation.instReprPolarityClass.repr : PolarityClass → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Negation.instReprPolarityClass : Repr PolarityClass

Equations

• Semantics.Negation.instReprPolarityClass = { reprPrec := Semantics.Negation.instReprPolarityClass.repr }

def Semantics.Negation.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 Semantics.Negation.instFintypePolarityClass : Fintype PolarityClass

Equations

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

structure Semantics.Negation.PolarityLicensing : Type

Polarity licensing profile for an EN environment ([Gre20] 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 Semantics.Negation.instDecidableEqPolarityLicensing.decEq (x✝ x✝¹ : PolarityLicensing) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Semantics.Negation.instDecidableEqPolarityLicensing : DecidableEq PolarityLicensing

Equations

• Semantics.Negation.instDecidableEqPolarityLicensing = Semantics.Negation.instDecidableEqPolarityLicensing.decEq

def Semantics.Negation.instReprPolarityLicensing.repr : PolarityLicensing → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Negation.instReprPolarityLicensing : Repr PolarityLicensing

Equations

• Semantics.Negation.instReprPolarityLicensing = { reprPrec := Semantics.Negation.instReprPolarityLicensing.repr }

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

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

Equations

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

def Semantics.Negation.weakENProfile : PolarityLicensing

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

Equations

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

def Semantics.Negation.strongENProfile : PolarityLicensing

Strong EN environments license NONE of the four polarity classes.

Equations

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

def Semantics.Negation.ENStrength.profile : ENStrength → PolarityLicensing

The licensing profile determined by an EN strength class ([Gre20] Table 1: rows are uniform within each class).

Equations

• Semantics.Negation.ENStrength.weak.profile = Semantics.Negation.weakENProfile
• Semantics.Negation.ENStrength.strong.profile = Semantics.Negation.strongENProfile

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

Strong EN rejects ALL polarity classes (universally quantified).

theorem Semantics.Negation.weakEN_licenses_weakNPI : weakENProfile.licenses PolarityClass.weakNPI = true

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

theorem Semantics.Negation.weakEN_licenses_nWord : weakENProfile.licenses PolarityClass.nWord = true

theorem Semantics.Negation.weakEN_rejects_strongNPI : weakENProfile.licenses PolarityClass.strongNPI = false

theorem Semantics.Negation.weakEN_rejects_notAlso : weakENProfile.licenses PolarityClass.notAlsoConj = false

def Semantics.Negation.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 Semantics.Negation.instFintypePolarityLicensing : Fintype PolarityLicensing

Equations

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

@[implicit_reducible]

instance Semantics.Negation.instPartialOrderPolarityLicensing : PartialOrder PolarityLicensing

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance Semantics.Negation.instLatticePolarityLicensing : Lattice PolarityLicensing

Equations

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

def Semantics.Negation.standardNegProfile : PolarityLicensing

Standard negation profile: licenses all polarity-sensitive elements.

Equations

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

@[implicit_reducible]

instance Semantics.Negation.instOrderBotPolarityLicensing : OrderBot PolarityLicensing

Equations

• Semantics.Negation.instOrderBotPolarityLicensing = { bot := Semantics.Negation.strongENProfile, bot_le := Semantics.Negation.instOrderBotPolarityLicensing._proof_1 }

@[implicit_reducible]

instance Semantics.Negation.instOrderTopPolarityLicensing : OrderTop PolarityLicensing

Equations

• Semantics.Negation.instOrderTopPolarityLicensing = { top := Semantics.Negation.standardNegProfile, le_top := Semantics.Negation.instOrderTopPolarityLicensing._proof_1 }

theorem Semantics.Negation.strongEN_le_weakEN : strongENProfile ≤ weakENProfile

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

Bridge: PolarityClass ↔ PolarityType

def Semantics.Negation.PolarityClass.toPolarityType? : PolarityClass → Option Polarity.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

• Semantics.Negation.PolarityClass.weakNPI.toPolarityType? = some Semantics.Polarity.PolarityType.npiWeak
• Semantics.Negation.PolarityClass.strongNPI.toPolarityType? = some Semantics.Polarity.PolarityType.npiStrong
• x✝.toPolarityType? = none

def Semantics.Negation.PolarityClass.fromPolarityType? : Polarity.PolarityType → Option PolarityClass

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

Equations

• Semantics.Negation.PolarityClass.fromPolarityType? Semantics.Polarity.PolarityType.npiWeak = some Semantics.Negation.PolarityClass.weakNPI
• Semantics.Negation.PolarityClass.fromPolarityType? Semantics.Polarity.PolarityType.npiStrong = some Semantics.Negation.PolarityClass.strongNPI
• Semantics.Negation.PolarityClass.fromPolarityType? x✝ = none

theorem Semantics.Negation.PolarityClass.roundtrip_npiWeak : (fromPolarityType? Polarity.PolarityType.npiWeak).bind toPolarityType? = some Polarity.PolarityType.npiWeak

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

theorem Semantics.Negation.PolarityClass.roundtrip_npiStrong : (fromPolarityType? Polarity.PolarityType.npiStrong).bind toPolarityType? = some Polarity.PolarityType.npiStrong

def Semantics.Negation.PolarityLicensing.licensesType (p : PolarityLicensing) (t : Polarity.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 (Semantics.Negation.PolarityClass.fromPolarityType? t)