Tsiakmakis (2025): On the Non-Homogeneity of Expletive Negation

@cite{tsiakmakis-2025}

Linguistics (2025). DOI: 10.1515/ling-2024-0063.

Expletive negation (EN) is not a uniform phenomenon. Greek distinguishes two negation markers that appear in EN environments: the indicative negator dhen (NEG₁) and the modal/subjunctive negator min (NEG₂). These correspond to two fundamentally different kinds of EN:

1. NEG₁ / Apparent EN hosts: The negator is standard sentential negation (⟦NEG₁⟧ = λp.¬p). Its negative semantics is masked by independent factors — rhetoricity, verbal aspect, negative concord, or the semantics of the embedding operator.

2. NEG₂ / EN hosts proper: The negator is a biased epistemic modal. It retains the modal component of its negative counterpart but lacks negation: ⟦NEG₂⟧^g(w) = λp. ∀w' ∈ Best_g(w) : p(w').

The paper argues this bipartite classification extends cross-linguistically: even in languages without overt morphological distinction (French ne, Italian non), the two types can be diagnosed by NCI licensing, co-occurrence with canonical negation, and syntactic position.

Diagnostics for NEG₁ vs NEG₂

Property	NEG₁ (apparent)	NEG₂ (proper)
Licenses NCIs (tipota)	✓	✗
Co-occurs with canonical neg	✗ (double neg)	✓ (min dhen)
Syntactic position	TP-internal	Left periphery
Has modal semantic component	✗	✓ (Best worlds)
Negative truth-conditions	✓ (masked)	✗ (intrinsic)

Revised EN Host Inventory (§5.12, ex. 95)

Apparent EN hosts (NEG₁): i. Temporal expressions (before, until, since) ii. Negative adverbials (without) iii. Comparatives (more ... than) iv. Optionally biased polar questions v. Rhetorical questions vi. Exclamatives

EN hosts proper (NEG₂): i. Emotive doxastic predicates (fear, worry) ii. Negative predicates (forbid, deny) iii. Dubitative predicates (doubt) iv. Biased questions v. (Conditionals) vi. (Free relatives — tentative)

Connection to @cite{jin-koenig-2021}

The bipartite classification cross-cuts Jin & Koenig's trigger taxonomy: their propositional attitude triggers (FEAR, DENY) map to NEG₂ (modal semantics), while temporal and logical operator triggers (BEFORE, WITHOUT, UNLESS) map to NEG₁ (standard negation masked). Comparative triggers are classified as NEG₁ (negation is a spell-out of the comparative operator's built-in negation). The FORGET class is heterogeneous — some members pattern with NEG₂ (modal), others with NEG₁ (factual ¬p in w₀).

Connection to Kratzer Modality

NEG₂ is formally a Kratzer necessity operator with an ordering source: ⟦NEG₂⟧^g(w) = λp. ∀w' ∈ Best_g(w) : p(w'). The ordering source varies by host:

• Fear predicates: deontic ordering (speaker's preferences)
• Negative predicates (forbid): deontic ordering (norms)
• Dubitative predicates: epistemic ordering (speaker's beliefs)
• Conditionals: circumstantial + deontic ordering
• Biased questions: epistemic ordering (speaker's bias)

inductive Phenomena.Negation.Studies.Tsiakmakis2025.NegatorType : Type

The two types of expletive negation markers.

Greek overtly distinguishes these: dhen = NEG₁, min = NEG₂. Other languages (French, Italian, Spanish) use the same surface form for both, but the distinction can be diagnosed by NCI licensing, co-occurrence with canonical negation, and syntactic position.

• neg1 : NegatorType

  Standard sentential negation whose negative semantics is masked by independent factors (rhetoricity, aspect, NC, operator semantics). ⟦NEG₁⟧ = λp.¬p

• neg2 : NegatorType

  Biased epistemic modal retaining the modal component of negative min but lacking negation. ⟦NEG₂⟧^g(w) = λp. ∀w' ∈ Best_g(w) : p(w')

instance Phenomena.Negation.Studies.Tsiakmakis2025.instDecidableEqNegatorType : DecidableEq NegatorType

Equations

• Phenomena.Negation.Studies.Tsiakmakis2025.instDecidableEqNegatorType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Negation.Studies.Tsiakmakis2025.instBEqNegatorType : BEq NegatorType

Equations

• Phenomena.Negation.Studies.Tsiakmakis2025.instBEqNegatorType = { beq := Phenomena.Negation.Studies.Tsiakmakis2025.instBEqNegatorType.beq }

def Phenomena.Negation.Studies.Tsiakmakis2025.instBEqNegatorType.beq : NegatorType → NegatorType → Bool

Equations

• Phenomena.Negation.Studies.Tsiakmakis2025.instBEqNegatorType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Negation.Studies.Tsiakmakis2025.instReprNegatorType : Repr NegatorType

Equations

• Phenomena.Negation.Studies.Tsiakmakis2025.instReprNegatorType = { reprPrec := Phenomena.Negation.Studies.Tsiakmakis2025.instReprNegatorType.repr }

def Phenomena.Negation.Studies.Tsiakmakis2025.instReprNegatorType.repr : NegatorType → ℕ → Std.Format

Equations

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

def Phenomena.Negation.Studies.Tsiakmakis2025.neg1Sem (p : Semantics.Attitudes.Intensional.World → Bool) : Semantics.Attitudes.Intensional.World → Bool

NEG₁ semantics: standard sentential negation.

⟦NEG₁⟧ = λp.¬p (eq. 37, 70, 73, 79, 88, 91, 93)

Equations

• Phenomena.Negation.Studies.Tsiakmakis2025.neg1Sem p w = !p w

def Phenomena.Negation.Studies.Tsiakmakis2025.neg2Sem (f : Semantics.Modality.Kratzer.ModalBase) (g : Semantics.Modality.Kratzer.OrderingSource) (p : BProp Semantics.Attitudes.Intensional.World) (w : Semantics.Attitudes.Intensional.World) : Bool

NEG₂ semantics: Kratzer necessity over Best worlds.

⟦NEG₂⟧^g(w) = λp. ∀w' ∈ Best_g(w) : p(w') (eq. 58, 60, 63, 66, 94)

This is exactly Kratzer's necessity operator. The ordering source varies by host (deontic for fear/forbid, epistemic for doubt/questions).

Equations

• Phenomena.Negation.Studies.Tsiakmakis2025.neg2Sem f g p w = Semantics.Modality.Kratzer.necessity f g p w

theorem Phenomena.Negation.Studies.Tsiakmakis2025.neg2_is_kratzer_necessity (f : Semantics.Modality.Kratzer.ModalBase) (g : Semantics.Modality.Kratzer.OrderingSource) (p : BProp Semantics.Attitudes.Intensional.World) (w : Semantics.Attitudes.Intensional.World) : neg2Sem f g p w = Semantics.Modality.Kratzer.necessity f g p w

NEG₂ is formally identical to Kratzer necessity.

structure Phenomena.Negation.Studies.Tsiakmakis2025.NegatorDiagnostics : Type

Diagnostic properties that distinguish NEG₁ from NEG₂.

Based on Greek evidence (§§2–4) and cross-linguistic extension (§5).

• negType : NegatorType
• licensesNCIs : Bool

  Can the marker license Negative Concord Items (NCIs)? NEG₁ (dhen) can license tipota 'nothing'; NEG₂ (min) cannot. (§4.1, ex. 40 vs 41; §4.2, ex. 46; §4.3, ex. 52)

• cooccursWithCanonicalNeg : Bool

  Can the marker co-occur with canonical sentential negation? NEG₂ (min) co-occurs with dhen (ex. 39, 41, 47, 53); NEG₁ (dhen) alone IS the canonical negation.

• mergesInLeftPeriphery : Bool

  Is the marker merged in the left periphery (outside TP)? NEG₂ (min) merges high — informationally unmarked subjects cannot precede it (ex. 44, 48, 54). NEG₁ (dhen) is TP-internal.

• hasModalComponent : Bool

  Does the marker have a modal semantic component? NEG₂ involves an ordering source and Best worlds; NEG₁ is pure truth-functional negation.

def Phenomena.Negation.Studies.Tsiakmakis2025.instReprNegatorDiagnostics.repr : NegatorDiagnostics → ℕ → Std.Format

Equations

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

instance Phenomena.Negation.Studies.Tsiakmakis2025.instReprNegatorDiagnostics : Repr NegatorDiagnostics

Equations

• Phenomena.Negation.Studies.Tsiakmakis2025.instReprNegatorDiagnostics = { reprPrec := Phenomena.Negation.Studies.Tsiakmakis2025.instReprNegatorDiagnostics.repr }

def Phenomena.Negation.Studies.Tsiakmakis2025.neg1Diagnostics : NegatorDiagnostics

Diagnostic profile for NEG₁ (Greek dhen).

Equations

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

def Phenomena.Negation.Studies.Tsiakmakis2025.neg2Diagnostics : NegatorDiagnostics

Diagnostic profile for NEG₂ (Greek min).

Equations

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

theorem Phenomena.Negation.Studies.Tsiakmakis2025.diagnostics_fully_distinguish : neg1Diagnostics.licensesNCIs ≠ neg2Diagnostics.licensesNCIs ∧ neg1Diagnostics.cooccursWithCanonicalNeg ≠ neg2Diagnostics.cooccursWithCanonicalNeg ∧ neg1Diagnostics.mergesInLeftPeriphery ≠ neg2Diagnostics.mergesInLeftPeriphery ∧ neg1Diagnostics.hasModalComponent ≠ neg2Diagnostics.hasModalComponent

NEG₁ and NEG₂ differ on every diagnostic.

inductive Phenomena.Negation.Studies.Tsiakmakis2025.ENHostCategory : Type

EN host categories from the revised inventory (§5.12, ex. 95).

"Apparent" hosts feature NEG₁ (standard negation masked); "proper" hosts feature NEG₂ (modal, intrinsically non-negative).

• temporalExpressions : ENHostCategory
• negativeAdverbials : ENHostCategory
• comparatives : ENHostCategory
• optionallyBiasedPolarQs : ENHostCategory
• rhetoricalQuestions : ENHostCategory
• exclamatives : ENHostCategory
• emotiveDoxasticPredicates : ENHostCategory
• negativePredicates : ENHostCategory
• dubitativePredicates : ENHostCategory
• biasedQuestions : ENHostCategory
• conditionals : ENHostCategory
• freeRelatives : ENHostCategory

instance Phenomena.Negation.Studies.Tsiakmakis2025.instDecidableEqENHostCategory : DecidableEq ENHostCategory

Equations

• Phenomena.Negation.Studies.Tsiakmakis2025.instDecidableEqENHostCategory x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Negation.Studies.Tsiakmakis2025.instBEqENHostCategory : BEq ENHostCategory

Equations

• Phenomena.Negation.Studies.Tsiakmakis2025.instBEqENHostCategory = { beq := Phenomena.Negation.Studies.Tsiakmakis2025.instBEqENHostCategory.beq }

def Phenomena.Negation.Studies.Tsiakmakis2025.instBEqENHostCategory.beq : ENHostCategory → ENHostCategory → Bool

Equations

• Phenomena.Negation.Studies.Tsiakmakis2025.instBEqENHostCategory.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Negation.Studies.Tsiakmakis2025.instReprENHostCategory : Repr ENHostCategory

Equations

• Phenomena.Negation.Studies.Tsiakmakis2025.instReprENHostCategory = { reprPrec := Phenomena.Negation.Studies.Tsiakmakis2025.instReprENHostCategory.repr }

def Phenomena.Negation.Studies.Tsiakmakis2025.instReprENHostCategory.repr : ENHostCategory → ℕ → Std.Format

Equations

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

def Phenomena.Negation.Studies.Tsiakmakis2025.ENHostCategory.negatorType : ENHostCategory → NegatorType

Each host category's negator type.

Equations

• Phenomena.Negation.Studies.Tsiakmakis2025.ENHostCategory.temporalExpressions.negatorType = Phenomena.Negation.Studies.Tsiakmakis2025.NegatorType.neg1
• Phenomena.Negation.Studies.Tsiakmakis2025.ENHostCategory.negativeAdverbials.negatorType = Phenomena.Negation.Studies.Tsiakmakis2025.NegatorType.neg1
• Phenomena.Negation.Studies.Tsiakmakis2025.ENHostCategory.comparatives.negatorType = Phenomena.Negation.Studies.Tsiakmakis2025.NegatorType.neg1
• Phenomena.Negation.Studies.Tsiakmakis2025.ENHostCategory.optionallyBiasedPolarQs.negatorType = Phenomena.Negation.Studies.Tsiakmakis2025.NegatorType.neg1
• Phenomena.Negation.Studies.Tsiakmakis2025.ENHostCategory.rhetoricalQuestions.negatorType = Phenomena.Negation.Studies.Tsiakmakis2025.NegatorType.neg1
• Phenomena.Negation.Studies.Tsiakmakis2025.ENHostCategory.exclamatives.negatorType = Phenomena.Negation.Studies.Tsiakmakis2025.NegatorType.neg1
• Phenomena.Negation.Studies.Tsiakmakis2025.ENHostCategory.emotiveDoxasticPredicates.negatorType = Phenomena.Negation.Studies.Tsiakmakis2025.NegatorType.neg2
• Phenomena.Negation.Studies.Tsiakmakis2025.ENHostCategory.negativePredicates.negatorType = Phenomena.Negation.Studies.Tsiakmakis2025.NegatorType.neg2
• Phenomena.Negation.Studies.Tsiakmakis2025.ENHostCategory.dubitativePredicates.negatorType = Phenomena.Negation.Studies.Tsiakmakis2025.NegatorType.neg2
• Phenomena.Negation.Studies.Tsiakmakis2025.ENHostCategory.biasedQuestions.negatorType = Phenomena.Negation.Studies.Tsiakmakis2025.NegatorType.neg2
• Phenomena.Negation.Studies.Tsiakmakis2025.ENHostCategory.conditionals.negatorType = Phenomena.Negation.Studies.Tsiakmakis2025.NegatorType.neg2
• Phenomena.Negation.Studies.Tsiakmakis2025.ENHostCategory.freeRelatives.negatorType = Phenomena.Negation.Studies.Tsiakmakis2025.NegatorType.neg2

Mapping trigger subclasses to negator types

Each of @cite{jin-koenig-2021}'s trigger subclasses is classified as hosting NEG₁ or NEG₂. The negator type is derived from the host category: negatorType t = (t.toHostCategory.map negatorType).getD .neg1. This makes the trigger-level and host-level classifications agree by construction, not by bridge theorem.

@[reducible]

def Phenomena.Negation.Studies.Tsiakmakis2025.triggerToHost : JinKoenig2021.TriggerSubclass → Option ENHostCategory

Map each trigger subclass to its EN host category (partial).

The mapping is partial because some trigger subclasses do not correspond to any EN host in @cite{tsiakmakis-2025}'s inventory:

• FORGET: semantically heterogeneous (§6.1.4 of @cite{jin-koenig-2021})
• RARELY/IMPOSSIBLE: not listed as EN hosts in §5.12

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Negation.Studies.Tsiakmakis2025.triggerToHost Phenomena.Negation.Studies.JinKoenig2021.TriggerSubclass.tooTo = some Phenomena.Negation.Studies.Tsiakmakis2025.ENHostCategory.comparatives
• Phenomena.Negation.Studies.Tsiakmakis2025.triggerToHost Phenomena.Negation.Studies.JinKoenig2021.TriggerSubclass.forget = none
• Phenomena.Negation.Studies.Tsiakmakis2025.triggerToHost Phenomena.Negation.Studies.JinKoenig2021.TriggerSubclass.rarely = none
• Phenomena.Negation.Studies.Tsiakmakis2025.triggerToHost Phenomena.Negation.Studies.JinKoenig2021.TriggerSubclass.impossible = none

@[reducible]

def Phenomena.Negation.Studies.Tsiakmakis2025.negatorType (t : JinKoenig2021.TriggerSubclass) : NegatorType

Negator type for each trigger subclass, derived from its host category.

When a trigger maps to a host category, its negator type is the host's. Unmapped triggers (forget, rarely, impossible) default to NEG₁ — all involve standard negation, not modal semantics.

Equations

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

theorem Phenomena.Negation.Studies.Tsiakmakis2025.apparent_hosts_are_neg1 : ([ENHostCategory.temporalExpressions, ENHostCategory.negativeAdverbials, ENHostCategory.comparatives, ENHostCategory.optionallyBiasedPolarQs, ENHostCategory.rhetoricalQuestions, ENHostCategory.exclamatives].all fun (x : ENHostCategory) => x.negatorType == NegatorType.neg1) = true

All apparent hosts are NEG₁.

theorem Phenomena.Negation.Studies.Tsiakmakis2025.proper_hosts_are_neg2 : ([ENHostCategory.emotiveDoxasticPredicates, ENHostCategory.negativePredicates, ENHostCategory.dubitativePredicates, ENHostCategory.biasedQuestions, ENHostCategory.conditionals, ENHostCategory.freeRelatives].all fun (x : ENHostCategory) => x.negatorType == NegatorType.neg2) = true

All proper hosts are NEG₂.

Negator classification across languages

The NEG₁/NEG₂ distinction is overt in Greek (dhen vs min) and Classical Greek (ou(k) vs me:). In other languages, the same surface form may instantiate either type depending on context.

Cross-linguistic evidence from §5:

• French: ne is NEG₁ in temporals/comparatives, NEG₂ in fear-predicate complements (@cite{tahar-2021})
• Italian: non is NEG₁ in finché-clauses (§5.4) and comparatives (§5.7), NEG₂ tentatively in fear contexts
• Spanish: no is NEG₁ in comparatives, NEG₂ in dudar complements
• Classical Greek: ou(k) = NEG₁, me: = NEG₂ (§5.1, §5.3)
• Latin: non = NEG₁ in questions (§5.8), -ne = NEG₂ in questions (§5.8, ex. 84)

structure Phenomena.Negation.Studies.Tsiakmakis2025.NegatorDatum : Type

A cross-linguistic EN negator datum.

• language : String

  Language

• form : String

  Surface form of the negator

• negType : NegatorType

  NEG₁ or NEG₂

• hostCategory : ENHostCategory

  EN host category where this negator appears

• construction : String

  Brief description of the construction

instance Phenomena.Negation.Studies.Tsiakmakis2025.instReprNegatorDatum : Repr NegatorDatum

Equations

• Phenomena.Negation.Studies.Tsiakmakis2025.instReprNegatorDatum = { reprPrec := Phenomena.Negation.Studies.Tsiakmakis2025.instReprNegatorDatum.repr }

def Phenomena.Negation.Studies.Tsiakmakis2025.instReprNegatorDatum.repr : NegatorDatum → ℕ → Std.Format

Equations

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

def Phenomena.Negation.Studies.Tsiakmakis2025.greekDhenExclamative : NegatorDatum

Greek dhen in exclamatives: ⟦dhen⟧ = λp.¬p, masked by extreme-degree semantics (§3.1, ex. 22–24).

Equations

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

def Phenomena.Negation.Studies.Tsiakmakis2025.greekDhenRhetoricalQ : NegatorDatum

Greek dhen in negative rhetorical questions: ⟦dhen⟧ = λp.¬p, masked by rhetoricity / polarity reversal (§3.2, ex. 26–29; eq. 30).

Equations

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

def Phenomena.Negation.Studies.Tsiakmakis2025.greekDhenPolarQ : NegatorDatum

Greek dhen in preposed negation questions: ⟦dhen⟧ = λp.¬p, masked by speaker's epistemic bias (§3.3, ex. 31–36; eq. 36–37).

Equations

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

def Phenomena.Negation.Studies.Tsiakmakis2025.greekMinFear : NegatorDatum

Equations

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

def Phenomena.Negation.Studies.Tsiakmakis2025.greekMinConditional : NegatorDatum

Equations

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

def Phenomena.Negation.Studies.Tsiakmakis2025.greekMinQuestion : NegatorDatum

Equations

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

def Phenomena.Negation.Studies.Tsiakmakis2025.frenchNeFear : NegatorDatum

Equations

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

def Phenomena.Negation.Studies.Tsiakmakis2025.frenchNeForbid : NegatorDatum

Equations

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

def Phenomena.Negation.Studies.Tsiakmakis2025.italianNonTemporal : NegatorDatum

Equations

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

def Phenomena.Negation.Studies.Tsiakmakis2025.italianNonComparative : NegatorDatum

Equations

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

def Phenomena.Negation.Studies.Tsiakmakis2025.spanishNoDubitative : NegatorDatum

Equations

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

def Phenomena.Negation.Studies.Tsiakmakis2025.classicalGreekMeDubitative : NegatorDatum

Equations

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

def Phenomena.Negation.Studies.Tsiakmakis2025.hebrewLoFear : NegatorDatum

Equations

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

def Phenomena.Negation.Studies.Tsiakmakis2025.latinNeQuestion : NegatorDatum

Equations

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

def Phenomena.Negation.Studies.Tsiakmakis2025.allNegatorData : List NegatorDatum

Equations

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

theorem Phenomena.Negation.Studies.Tsiakmakis2025.greek_min_is_neg2 : ((List.filter (fun (x : NegatorDatum) => x.form == "min") allNegatorData).all fun (x : NegatorDatum) => x.negType == NegatorType.neg2) = true

Greek min always corresponds to NEG₂.

theorem Phenomena.Negation.Studies.Tsiakmakis2025.greek_dhen_is_neg1 : ((List.filter (fun (x : NegatorDatum) => x.form == "dhen") allNegatorData).all fun (x : NegatorDatum) => x.negType == NegatorType.neg1) = true

Greek dhen always corresponds to NEG₁.

theorem Phenomena.Negation.Studies.Tsiakmakis2025.italian_non_is_neg1 : ((List.filter (fun (x : NegatorDatum) => x.form == "non") allNegatorData).all fun (x : NegatorDatum) => x.negType == NegatorType.neg1) = true

Italian non in temporals and comparatives is NEG₁.

Connecting negator types to licensing conditions

The central structural claim: NEG₂ hosts correspond to @cite{jin-koenig-2021}'s propositional attitude licensing condition, while NEG₁ hosts correspond to temporal, logical, and comparative conditions.

theorem Phenomena.Negation.Studies.Tsiakmakis2025.neg2_triggers_are_propositional_attitude : ([JinKoenig2021.TriggerSubclass.fear, JinKoenig2021.TriggerSubclass.regret, JinKoenig2021.TriggerSubclass.deny].all fun (t : JinKoenig2021.TriggerSubclass) => negatorType t == NegatorType.neg2 && t.licensingCondition == JinKoenig2021.LicensingCondition.propositionalAttitude) = true

All NEG₂ trigger subclasses have the propositional attitude licensing condition. This is non-trivial: it shows that the negator-type classification aligns with the licensing-condition classification for the modal (NEG₂) cases.

theorem Phenomena.Negation.Studies.Tsiakmakis2025.temporal_triggers_are_neg1 : ([JinKoenig2021.TriggerSubclass.before, JinKoenig2021.TriggerSubclass.cannotWait, JinKoenig2021.TriggerSubclass.since, JinKoenig2021.TriggerSubclass.rarely].all fun (t : JinKoenig2021.TriggerSubclass) => negatorType t == NegatorType.neg1) = true

All temporal triggers are NEG₁.

theorem Phenomena.Negation.Studies.Tsiakmakis2025.logical_triggers_are_neg1 : ([JinKoenig2021.TriggerSubclass.impossible, JinKoenig2021.TriggerSubclass.without, JinKoenig2021.TriggerSubclass.unless].all fun (t : JinKoenig2021.TriggerSubclass) => negatorType t == NegatorType.neg1) = true

All logical operator triggers are NEG₁.

theorem Phenomena.Negation.Studies.Tsiakmakis2025.comparative_triggers_are_neg1 : ([JinKoenig2021.TriggerSubclass.moreThan, JinKoenig2021.TriggerSubclass.differentThan, JinKoenig2021.TriggerSubclass.tooTo].all fun (t : JinKoenig2021.TriggerSubclass) => negatorType t == NegatorType.neg1) = true

All comparative triggers are NEG₁.

theorem Phenomena.Negation.Studies.Tsiakmakis2025.neg1_iff_not_core_attitude (t : JinKoenig2021.TriggerSubclass) : negatorType t = NegatorType.neg1 ↔ t.licensingCondition ≠ JinKoenig2021.LicensingCondition.propositionalAttitude ∨ t = JinKoenig2021.TriggerSubclass.forget

NEG₁ triggers are exactly the non-propositional-attitude triggers plus FORGET (the heterogeneous attitude class).

Modal flavor of NEG₂ across hosts

All NEG₂ hosts share the formal semantics ⟦NEG₂⟧ = λp. ∀w' ∈ Best_g(w) : p(w'), but the ordering source g varies:

• Fear predicates: deontic (desires/preferences) — p worlds are ranked higher than ¬p worlds by the speaker's preferences (§5.1, eq. 60)
• Negative predicates (forbid): deontic (norms/standards) — p worlds ranked higher by social/moral norms (§5.2, eq. 63: "deontically modal")
• Dubitative predicates (doubt): epistemic (beliefs) — p worlds ranked higher by the speaker's epistemic state (§5.3, eq. 66)
• Conditionals: circumstantial + habit/norm (§4.2, eq. 50) — p worlds ranked by what has happened before
• Biased questions: epistemic (speaker's prior belief) — p worlds ranked higher by positive speaker bias (§4.3, eq. 56)

def Phenomena.Negation.Studies.Tsiakmakis2025.ENHostCategory.orderingFlavor : ENHostCategory → Option Core.Modality.ModalFlavor

Each proper EN host category maps to a Kratzer modal flavor.

NEG₂'s ordering source varies by host; the flavor tag is exactly Core.Modality.ModalFlavor, reused here rather than duplicated. "Habitual" (conditionals) maps to .circumstantial — both concern facts and what has happened, following Kratzer's subsumption.

Equations

• Phenomena.Negation.Studies.Tsiakmakis2025.ENHostCategory.emotiveDoxasticPredicates.orderingFlavor = some Core.Modality.ModalFlavor.deontic
• Phenomena.Negation.Studies.Tsiakmakis2025.ENHostCategory.negativePredicates.orderingFlavor = some Core.Modality.ModalFlavor.deontic
• Phenomena.Negation.Studies.Tsiakmakis2025.ENHostCategory.dubitativePredicates.orderingFlavor = some Core.Modality.ModalFlavor.epistemic
• Phenomena.Negation.Studies.Tsiakmakis2025.ENHostCategory.biasedQuestions.orderingFlavor = some Core.Modality.ModalFlavor.epistemic
• Phenomena.Negation.Studies.Tsiakmakis2025.ENHostCategory.conditionals.orderingFlavor = some Core.Modality.ModalFlavor.circumstantial
• Phenomena.Negation.Studies.Tsiakmakis2025.ENHostCategory.freeRelatives.orderingFlavor = some Core.Modality.ModalFlavor.epistemic
• Phenomena.Negation.Studies.Tsiakmakis2025.ENHostCategory.temporalExpressions.orderingFlavor = none
• Phenomena.Negation.Studies.Tsiakmakis2025.ENHostCategory.negativeAdverbials.orderingFlavor = none
• Phenomena.Negation.Studies.Tsiakmakis2025.ENHostCategory.comparatives.orderingFlavor = none
• Phenomena.Negation.Studies.Tsiakmakis2025.ENHostCategory.optionallyBiasedPolarQs.orderingFlavor = none
• Phenomena.Negation.Studies.Tsiakmakis2025.ENHostCategory.rhetoricalQuestions.orderingFlavor = none
• Phenomena.Negation.Studies.Tsiakmakis2025.ENHostCategory.exclamatives.orderingFlavor = none

theorem Phenomena.Negation.Studies.Tsiakmakis2025.ordering_flavor_iff_neg2 (h : ENHostCategory) : h.orderingFlavor.isSome = (h.negatorType == NegatorType.neg2)

NEG₂ hosts always have an ordering flavor; NEG₁ hosts never do.

Why NEG₁ appears expletive

NEG₁ has genuine negative semantics (λp.¬p), but its negativity is masked — obscured by independent factors. The masking mechanism differs by host type (§3.4, §5.4, §5.5, §5.7, §5.9, §5.10):

• Temporal expressions: negation obscured by verbal aspect (achievement verbs make the endpoint coincide, so the non-variant and the bare variant are truth-conditionally equivalent; @cite{tovena-1996}, §5.4)
• Negative adverbials (without): Negative Concord between the adverbial and the EN marker (§5.5)
• Comparatives: negation is a spell-out of the comparative operator's built-in negation (∃d. tall(G,d) ∧ ¬tall(P,d); §5.7)
• Rhetorical questions: polarity reversal from rhetoricity is independent of the negation marker (§5.9)
• Exclamatives: polarity reversal from extreme-degree semantics (§5.10)
• Optionally biased polar questions: speaker's epistemic bias masks the negative meaning (§3.3)

inductive Phenomena.Negation.Studies.Tsiakmakis2025.MaskingMechanism : Type

The mechanism that masks NEG₁'s negative semantics.

• verbalAspect : MaskingMechanism

  Verbal aspect makes negated/non-negated variants equivalent (temporal expressions with achievement verbs; @cite{tovena-1996})

• negativeConcord : MaskingMechanism

  Negative Concord between embedding operator and NEG₁ (negative adverbials; §5.5)

• operatorSpellOut : MaskingMechanism

  Negation is spell-out of operator's built-in negation (comparatives: ∃d. Q(Y,d) ∧ ¬Q(Z,d); §5.7)

• rhetoricity : MaskingMechanism

  Polarity reversal from rhetoricity (rhetorical questions; §5.9)

• extremeDegree : MaskingMechanism

  Extreme-degree semantics triggers reversal (exclamatives; §5.10)

• speakerBias : MaskingMechanism

  Speaker's epistemic bias overrides negative reading (optionally biased polar questions; §3.3)

instance Phenomena.Negation.Studies.Tsiakmakis2025.instDecidableEqMaskingMechanism : DecidableEq MaskingMechanism

Equations

• Phenomena.Negation.Studies.Tsiakmakis2025.instDecidableEqMaskingMechanism x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Negation.Studies.Tsiakmakis2025.instBEqMaskingMechanism : BEq MaskingMechanism

Equations

• Phenomena.Negation.Studies.Tsiakmakis2025.instBEqMaskingMechanism = { beq := Phenomena.Negation.Studies.Tsiakmakis2025.instBEqMaskingMechanism.beq }

def Phenomena.Negation.Studies.Tsiakmakis2025.instBEqMaskingMechanism.beq : MaskingMechanism → MaskingMechanism → Bool

Equations

• Phenomena.Negation.Studies.Tsiakmakis2025.instBEqMaskingMechanism.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Negation.Studies.Tsiakmakis2025.instReprMaskingMechanism.repr : MaskingMechanism → ℕ → Std.Format

Equations

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

instance Phenomena.Negation.Studies.Tsiakmakis2025.instReprMaskingMechanism : Repr MaskingMechanism

Equations

• Phenomena.Negation.Studies.Tsiakmakis2025.instReprMaskingMechanism = { reprPrec := Phenomena.Negation.Studies.Tsiakmakis2025.instReprMaskingMechanism.repr }

def Phenomena.Negation.Studies.Tsiakmakis2025.ENHostCategory.maskingMechanism : ENHostCategory → Option MaskingMechanism

Each apparent (NEG₁) host has a specific masking mechanism.

Equations

• Phenomena.Negation.Studies.Tsiakmakis2025.ENHostCategory.temporalExpressions.maskingMechanism = some Phenomena.Negation.Studies.Tsiakmakis2025.MaskingMechanism.verbalAspect
• Phenomena.Negation.Studies.Tsiakmakis2025.ENHostCategory.negativeAdverbials.maskingMechanism = some Phenomena.Negation.Studies.Tsiakmakis2025.MaskingMechanism.negativeConcord
• Phenomena.Negation.Studies.Tsiakmakis2025.ENHostCategory.comparatives.maskingMechanism = some Phenomena.Negation.Studies.Tsiakmakis2025.MaskingMechanism.operatorSpellOut
• Phenomena.Negation.Studies.Tsiakmakis2025.ENHostCategory.rhetoricalQuestions.maskingMechanism = some Phenomena.Negation.Studies.Tsiakmakis2025.MaskingMechanism.rhetoricity
• Phenomena.Negation.Studies.Tsiakmakis2025.ENHostCategory.exclamatives.maskingMechanism = some Phenomena.Negation.Studies.Tsiakmakis2025.MaskingMechanism.extremeDegree
• Phenomena.Negation.Studies.Tsiakmakis2025.ENHostCategory.optionallyBiasedPolarQs.maskingMechanism = some Phenomena.Negation.Studies.Tsiakmakis2025.MaskingMechanism.speakerBias
• Phenomena.Negation.Studies.Tsiakmakis2025.ENHostCategory.emotiveDoxasticPredicates.maskingMechanism = none
• Phenomena.Negation.Studies.Tsiakmakis2025.ENHostCategory.negativePredicates.maskingMechanism = none
• Phenomena.Negation.Studies.Tsiakmakis2025.ENHostCategory.dubitativePredicates.maskingMechanism = none
• Phenomena.Negation.Studies.Tsiakmakis2025.ENHostCategory.biasedQuestions.maskingMechanism = none
• Phenomena.Negation.Studies.Tsiakmakis2025.ENHostCategory.conditionals.maskingMechanism = none
• Phenomena.Negation.Studies.Tsiakmakis2025.ENHostCategory.freeRelatives.maskingMechanism = none

theorem Phenomena.Negation.Studies.Tsiakmakis2025.masking_mechanism_iff_neg1 (h : ENHostCategory) : h.maskingMechanism.isSome = (h.negatorType == NegatorType.neg1)

NEG₁ hosts always have a masking mechanism; NEG₂ hosts never do. This is the structural complement of ordering_flavor_iff_neg2.

theorem Phenomena.Negation.Studies.Tsiakmakis2025.neg1_neg2_complementary (h : ENHostCategory) : h.orderingFlavor.isSome = !h.maskingMechanism.isSome

The two classifications are complementary: every host has either an ordering flavor (NEG₂) or a masking mechanism (NEG₁), never both.

Non-homogeneity refines ambidirectionality

The ambidirectionality generalization (formalized in Rett2026.lean) predicts EN licensing at the construction level. The non-homogeneity claim here refines this by distinguishing the nature of the negation:

• In NEG₁ hosts (before, than), ambidirectionality explains why standard negation is truth-conditionally vacuous → appears "expletive"
• In NEG₂ hosts (fear, doubt), the marker is not negation at all but a modal — so "ambidirectionality" applies to the modal component (both p and ¬p worlds are relevant to the ordering)

The two accounts are compatible: the ambidirectionality generalization covers the distributional pattern (where EN appears), while the non-homogeneity distinction explains the mechanism (what kind of marker appears).

Note: The formal bridge theorem mapping ENConstruction to ENHostCategory lives in Rett2026.lean (chronological direction: Rett 2026 can reference Tsiakmakis 2025, not vice versa).

Fear predicates: negative valence → dual inference → NEG₂

The connection between NEG₂ classification of fear predicates and @cite{villalta-2008}'s negative valence, mediated by @cite{jin-koenig-2021}:

1. Fear has negative valence (Preferential.lean)
2. Negative valence → dual inference (@cite{jin-koenig-2021} §5.5, §6.1.1)
3. Propositional attitude licensing condition (@cite{jin-koenig-2021} (13a))
4. NEG₂ classification with deontic ordering (@cite{tsiakmakis-2025} §5.1, eq. 60)

This is a four-layer argumentation chain connecting attitude semantics to the negator-type classification.

theorem Phenomena.Negation.Studies.Tsiakmakis2025.fear_neg2_from_negative_valence : JinKoenig2021.negativeValenceEntailsDual Semantics.Attitudes.Preferential.AttitudeValence.negative = true ∧ JinKoenig2021.TriggerSubclass.fear.licensingCondition = JinKoenig2021.LicensingCondition.propositionalAttitude ∧ negatorType JinKoenig2021.TriggerSubclass.fear = NegatorType.neg2 ∧ ENHostCategory.emotiveDoxasticPredicates.orderingFlavor = some Core.Modality.ModalFlavor.deontic

Fear predicates: the full chain from negative valence to NEG₂.

1. negativeValenceEntailsDual .negative = true (valence → dual inference)
2. fear.licensingCondition = .propositionalAttitude (J&K licensing)
3. negatorType .fear = .neg2 (Tsiakmakis classification)
4. emotiveDoxasticPredicates.orderingFlavor = some .deontic (modal flavor)

theorem Phenomena.Negation.Studies.Tsiakmakis2025.deny_neg2_with_deontic_ordering : negatorType JinKoenig2021.TriggerSubclass.deny = NegatorType.neg2 ∧ JinKoenig2021.TriggerSubclass.deny.licensingCondition = JinKoenig2021.LicensingCondition.propositionalAttitude ∧ ENHostCategory.negativePredicates.orderingFlavor = some Core.Modality.ModalFlavor.deontic

Deny predicates: NEG₂ with deontic ordering.

DENY triggers entail that X believes ¬p or says ¬p (@cite{jin-koenig-2021} §6.1.3). This propositional attitude licensing condition maps to NEG₂ with a deontic ordering source (the speaker's beliefs about what the denier believes).

theorem Phenomena.Negation.Studies.Tsiakmakis2025.data_consistent_with_classification : (allNegatorData.all fun (d : NegatorDatum) => d.negType == d.hostCategory.negatorType) = true

The cross-linguistic data is internally consistent: each datum's host category matches its negator type.

theorem Phenomena.Negation.Studies.Tsiakmakis2025.negatorType_total : [JinKoenig2021.TriggerSubclass.fear, JinKoenig2021.TriggerSubclass.regret, JinKoenig2021.TriggerSubclass.deny, JinKoenig2021.TriggerSubclass.forget, JinKoenig2021.TriggerSubclass.before, JinKoenig2021.TriggerSubclass.cannotWait, JinKoenig2021.TriggerSubclass.since, JinKoenig2021.TriggerSubclass.rarely, JinKoenig2021.TriggerSubclass.impossible, JinKoenig2021.TriggerSubclass.without, JinKoenig2021.TriggerSubclass.unless, JinKoenig2021.TriggerSubclass.moreThan, JinKoenig2021.TriggerSubclass.differentThan, JinKoenig2021.TriggerSubclass.tooTo].length = 14

Every trigger subclass is classified (total function check).

theorem Phenomena.Negation.Studies.Tsiakmakis2025.negatorType_counts : (List.filter (fun (t : JinKoenig2021.TriggerSubclass) => negatorType t == NegatorType.neg2) [JinKoenig2021.TriggerSubclass.fear, JinKoenig2021.TriggerSubclass.regret, JinKoenig2021.TriggerSubclass.deny, JinKoenig2021.TriggerSubclass.forget, JinKoenig2021.TriggerSubclass.before, JinKoenig2021.TriggerSubclass.cannotWait, JinKoenig2021.TriggerSubclass.since, JinKoenig2021.TriggerSubclass.rarely, JinKoenig2021.TriggerSubclass.impossible, JinKoenig2021.TriggerSubclass.without, JinKoenig2021.TriggerSubclass.unless, JinKoenig2021.TriggerSubclass.moreThan, JinKoenig2021.TriggerSubclass.differentThan, JinKoenig2021.TriggerSubclass.tooTo]).length = 3 ∧ (List.filter (fun (t : JinKoenig2021.TriggerSubclass) => negatorType t == NegatorType.neg1) [JinKoenig2021.TriggerSubclass.fear, JinKoenig2021.TriggerSubclass.regret, JinKoenig2021.TriggerSubclass.deny, JinKoenig2021.TriggerSubclass.forget, JinKoenig2021.TriggerSubclass.before, JinKoenig2021.TriggerSubclass.cannotWait, JinKoenig2021.TriggerSubclass.since, JinKoenig2021.TriggerSubclass.rarely, JinKoenig2021.TriggerSubclass.impossible, JinKoenig2021.TriggerSubclass.without, JinKoenig2021.TriggerSubclass.unless, JinKoenig2021.TriggerSubclass.moreThan, JinKoenig2021.TriggerSubclass.differentThan, JinKoenig2021.TriggerSubclass.tooTo]).length = 11

The 14 trigger subclasses split 3 NEG₂ + 11 NEG₁.

Negative min = modal ∘ negation

The paper's central formal insight: negative min (eq. 13) differs from expletive min (eq. 58) only by the presence of negation inside the modal.

• ⟦min_negative⟧(p)(w) = ∀w' ∈ Best. **¬**p(w') = NEG₂(NEG₁(p))(w)
• ⟦min_expletive⟧(p)(w) = ∀w' ∈ Best. p(w') = NEG₂(p)(w)

Expletive min is therefore negative min with the negation stripped out. Equivalently, feeding ¬p to negative min cancels the double negation and yields expletive min's semantics.

def Phenomena.Negation.Studies.Tsiakmakis2025.negativeMinSem (f : Semantics.Modality.Kratzer.ModalBase) (g : Semantics.Modality.Kratzer.OrderingSource) (p : BProp Semantics.Attitudes.Intensional.World) (w : Semantics.Attitudes.Intensional.World) : Bool

Negative min: modal necessity over ¬p (eq. 13).

Equations

• Phenomena.Negation.Studies.Tsiakmakis2025.negativeMinSem f g p w = Phenomena.Negation.Studies.Tsiakmakis2025.neg2Sem f g (Phenomena.Negation.Studies.Tsiakmakis2025.neg1Sem p) w

theorem Phenomena.Negation.Studies.Tsiakmakis2025.negative_min_is_modal_of_negation (f : Semantics.Modality.Kratzer.ModalBase) (g : Semantics.Modality.Kratzer.OrderingSource) (p : BProp Semantics.Attitudes.Intensional.World) (w : Semantics.Attitudes.Intensional.World) : negativeMinSem f g p w = neg2Sem f g (neg1Sem p) w

Negative min decomposes as NEG₂ ∘ NEG₁.

theorem Phenomena.Negation.Studies.Tsiakmakis2025.expletive_from_negative_double_neg (f : Semantics.Modality.Kratzer.ModalBase) (g : Semantics.Modality.Kratzer.OrderingSource) (p : BProp Semantics.Attitudes.Intensional.World) (w : Semantics.Attitudes.Intensional.World) : neg2Sem f g p w = negativeMinSem f g (neg1Sem p) w

Expletive min = negative min with double negation cancelled: ⟦NEG₂⟧(p) = negativeMin(¬p). Feeding ¬p into negative min cancels the inner negation (!!p = p), recovering expletive semantics.

Greek and Italian data derive from fragment entries

The NegatorDatum records for Greek and Italian derive their surface forms from Fragments.Greek.Negation and Fragments.Italian.Negation respectively — the connection is true by construction, not by bridge theorem.

theorem Phenomena.Negation.Studies.Tsiakmakis2025.greek_dhen_form_grounded : greekDhenExclamative.form = Fragments.Greek.Negation.dhen.form

Greek dhen data derives its form from the Greek negation fragment.

theorem Phenomena.Negation.Studies.Tsiakmakis2025.greek_min_form_grounded : greekMinFear.form = Fragments.Greek.Negation.min.form

Greek min data derives its form from the Greek negation fragment.

theorem Phenomena.Negation.Studies.Tsiakmakis2025.italian_non_form_grounded : italianNonTemporal.form = Fragments.Italian.Negation.negMarker

Italian non data derives its form from the Italian negation fragment.