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 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

@[instance_reducible]

instance Negation.instDecidableEqENBlockingReason : DecidableEq ENBlockingReason

Equations

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

@[instance_reducible]

instance Negation.instReprENBlockingReason : Repr ENBlockingReason

Equations

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

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

Equations

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

EN type classification

inductive 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

@[instance_reducible]

instance Negation.instDecidableEqENType : DecidableEq ENType

Equations

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

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

Equations

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

@[instance_reducible]

instance Negation.instReprENType : Repr ENType

Equations

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

def Negation.ENType.equivBool : ENType ≃ Bool

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

Equations

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

@[instance_reducible]

instance Negation.instFintypeENType : Fintype ENType

Equations

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

def Negation.ENType.toNat : ENType → ℕ

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

Equations

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

@[instance_reducible]

instance Negation.instLinearOrderENType : LinearOrder ENType

Equations

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

EN strength classification

inductive 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

@[instance_reducible]

instance Negation.instDecidableEqENStrength : DecidableEq ENStrength

Equations

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

@[instance_reducible]

instance Negation.instReprENStrength : Repr ENStrength

Equations

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

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

Equations

• Negation.instReprENStrength.repr Negation.ENStrength.weak prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Negation.ENStrength.weak")).group prec✝
• Negation.instReprENStrength.repr Negation.ENStrength.strong prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Negation.ENStrength.strong")).group prec✝

def Negation.ENStrength.equivBool : ENStrength ≃ Bool

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

Equations

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

@[instance_reducible]

instance Negation.instFintypeENStrength : Fintype ENStrength

Equations

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

def Negation.ENStrength.toNat : ENStrength → ℕ

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

Equations

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

@[instance_reducible]

instance Negation.instLinearOrderENStrength : LinearOrder ENStrength

Equations

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

Polarity classes and licensing profiles

inductive 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

@[instance_reducible]

instance Negation.instDecidableEqPolarityClass : DecidableEq PolarityClass

Equations

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

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

Equations

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

@[instance_reducible]

instance Negation.instReprPolarityClass : Repr PolarityClass

Equations

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

def 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.

@[instance_reducible]

instance Negation.instFintypePolarityClass : Fintype PolarityClass

Equations

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

structure 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

@[instance_reducible]

instance Negation.instDecidableEqPolarityLicensing : DecidableEq PolarityLicensing

Equations

• Negation.instDecidableEqPolarityLicensing = Negation.instDecidableEqPolarityLicensing.decEq

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

Equations

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

@[instance_reducible]

instance Negation.instReprPolarityLicensing : Repr PolarityLicensing

Equations

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

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

Equations

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

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

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

Equations

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

def Negation.weakENProfile : PolarityLicensing

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

Equations

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

def Negation.strongENProfile : PolarityLicensing

Strong EN environments license NONE of the four polarity classes.

Equations

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

def Negation.ENStrength.profile : ENStrength → PolarityLicensing

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

Equations

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

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

Strong EN rejects ALL polarity classes (universally quantified).

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

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

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

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

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

def 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.

@[instance_reducible]

instance Negation.instFintypePolarityLicensing : Fintype PolarityLicensing

Equations

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

@[instance_reducible]

instance Negation.instPartialOrderPolarityLicensing : PartialOrder PolarityLicensing

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

instance Negation.instLatticePolarityLicensing : Lattice PolarityLicensing

Equations

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

def Negation.standardNegProfile : PolarityLicensing

Standard negation profile: licenses all polarity-sensitive elements.

Equations

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

@[instance_reducible]

instance Negation.instOrderBotPolarityLicensing : OrderBot PolarityLicensing

Equations

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

@[instance_reducible]

instance Negation.instOrderTopPolarityLicensing : OrderTop PolarityLicensing

Equations

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

theorem Negation.strongEN_le_weakEN : strongENProfile ≤ weakENProfile

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