Expletive Negation: Typology and Licensing

@cite{greco-2018} @cite{jin-koenig-2021} @cite{kennedy-mcnally-2005} @cite{napoli-nespor-1976} @cite{rett-2026} @cite{cepeda-2018}

Expletive negation (EN) is truth-conditionally vacuous negation that appears in specific grammatical environments cross-linguistically. @cite{rett-2026} unifies the licensing conditions: EN is licensed exactly in ambidirectional constructions — those where negating an argument doesn't change truth conditions because MAX picks the same informative bound from both B and ¬B.

The Ambidirectionality Generalization

Construction	Ambidirectional?	Licenses EN?	Source
before	✓	✓ (50 langs)	@cite{jin-koenig-2021}
after	✗	✗	@cite{rett-2026}
while	✗	✗	@cite{rett-2026}
until	✓	✓	@cite{rett-2026} §5
comparative	✓	✓ (6+ langs)	@cite{jin-koenig-2021}
fear/worry	✓	✓ (39 langs)	@cite{jin-koenig-2021}

High vs Low EN @cite{greco-2020}

Two types of EN with different syntactic positions and licensing:

• High EN: targets non-truth-conditional content (exclamatives, surprise); obligatory where it appears.
• Low EN: targets truth-conditional content in ambidirectional environments; optional and triggers manner implicature (evaluativity).

inductive Rett2026.ENConstruction : Type

Constructions relevant to EN licensing. Each has a theory-derived ambidirectionality status (§3) and an empirically-observed EN status (derived from allENData in §2); Rett's claim is that these match.

• before : ENConstruction
• after : ENConstruction
• while_ : ENConstruction
• until : ENConstruction
• comparative : ENConstruction
• fear : ENConstruction

@[implicit_reducible]

instance Rett2026.instDecidableEqENConstruction : DecidableEq ENConstruction

Equations

• Rett2026.instDecidableEqENConstruction x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Rett2026.instReprENConstruction : Repr ENConstruction

Equations

• Rett2026.instReprENConstruction = { reprPrec := Rett2026.instReprENConstruction.repr }

def Rett2026.instReprENConstruction.repr : ENConstruction → ℕ → Std.Format

Equations

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

structure Rett2026.ENDatum : Type

A cross-linguistic EN licensing datum. The constructionType field keys each entry to the abstract construction class in ENConstruction, so that ENConstruction.hasEN can be derived from allENData rather than stipulated as a parallel table.

• language : String

  Language

• construction : String

  Construction type (free-form descriptor, e.g. "avant que")

• constructionType : ENConstruction

  Abstract construction class (keys to ENConstruction enum). The hasEN table in §3 is derived by .any (·.constructionType == c) over allENData, so adding/removing a datum automatically updates the licensing prediction.

• negMarker : String

  Negation marker used

• enType : Phenomena.Negation.ExpletiveNegation.ENType

  High or low EN

• isOptional : Bool

  Is the EN optional?

• licensedNPIForms : List String

  Surface forms of weak NPIs licensed in this construction. Empty list means the construction blocks all weak NPIs. Replaces the earlier licensesWeakNPIs : Bool field, which couldn't capture cases like Italian non₂-comparatives that license some weak NPIs (pur) but block others (affatto) for orthogonal semantic reasons (the precision requirement on affatto is incompatible with bias-conditioned negation's imprecise condition; @cite{napoli-nespor-1976} §3.22 fn 6, and the Italian Fragment's affatto.licensingContexts registry, which excludes .comparative).

• mannerEffect : Option Semantics.Degree.Comparative.MannerEffect

  Manner implicature triggered by EN (if any)

def Rett2026.instReprENDatum.repr : ENDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Rett2026.instReprENDatum : Repr ENDatum

Equations

• Rett2026.instReprENDatum = { reprPrec := Rett2026.instReprENDatum.repr }

def Rett2026.ENDatum.licensesNPIForm (d : ENDatum) (form : String) : Prop

Does this datum license the weak NPI with the given surface form?

Equations

• d.licensesNPIForm form = (form ∈ d.licensedNPIForms)

@[implicit_reducible]

instance Rett2026.instDecidableLicensesNPIForm (d : ENDatum) (form : String) : Decidable (d.licensesNPIForm form)

Equations

• Rett2026.instDecidableLicensesNPIForm d form = Rett2026.instDecidableLicensesNPIForm._aux_1 d form

def Rett2026.ENDatum.licensesAnyNPI (d : ENDatum) : Prop

Does this datum license any weak NPI? Recovers the previous coarse licensesWeakNPIs : Bool field's content.

Equations

• d.licensesAnyNPI = (d.licensedNPIForms ≠ [])

@[implicit_reducible]

instance Rett2026.instDecidableLicensesAnyNPI (d : ENDatum) : Decidable d.licensesAnyNPI

Equations

• Rett2026.instDecidableLicensesAnyNPI d = Rett2026.instDecidableLicensesAnyNPI._aux_1 d

@cite{jin-koenig-2021} survey data

Cross-linguistic distribution from a 722-language survey (EN attested in 74 languages across 37 genera):

• before-clauses: EN in 50/74 EN-attesting languages
• fear-clauses: EN in 39/74 EN-attesting languages
• comparative than-clauses: 6+ languages have EN
• until-clauses: reported in several languages

def Rett2026.frenchBefore : ENDatum

Equations

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

def Rett2026.italianBefore : ENDatum

Italian prima che licenses standard weak NPIs (mai, alcuno).

Equations

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

def Rett2026.spanishComparative : ENDatum

Equations

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

def Rett2026.italianComparative : ENDatum

Italian non₂ in più…di quanto comparatives. The isOptional and licensedNPIForms fields are coarsenings of the contextual licensing profile in Pragmatics.Bias.BiasLicensingProfile, refined in Phenomena.Negation.Studies.NapoliNespor1976:

• isOptional = true: optionality is contextually conditioned on a contradicted-prior-belief presupposition (@cite{napoli-nespor-1976} §2). The Bool here is the satisfiability of the licensing profile across contexts, not free choice in any single context.
• licensedNPIForms = [pur.form]: the weak NPI pur is licensed under non₂-comparatives (@cite{napoli-nespor-1976} §3.11 ex. 46–48), but affatto is blocked for orthogonal semantic reasons (precision requirement incompatible with the imprecise/inferred presupposition, §3.22 fn 6). The list encodes the asymmetry that the previous Bool field flattened.

Equations

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

def Rett2026.frenchFear : ENDatum

Equations

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

def Rett2026.italianUntil : ENDatum

@cite{greco-2018}: Italian until-clauses license both EN and standard weak NPIs (mai, alcuno).

Equations

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

def Rett2026.italianExclamative : ENDatum

Italian wh-exclamatives: high EN. Classified under .fear as the closest abstract construction class for high-EN attitude-like contexts; the high/low distinction is separately tracked by enType.

Equations

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

def Rett2026.italianSneg : ENDatum

Italian surprise negation (@cite{greco-2020}, §2–4): non merges in the CP layer (above FinP) rather than in the TP-internal NegP. High EN — obligatory, non-truth-conditional, does not license weak NPIs. Classified under .fear as the closest abstract construction class for non-truth-conditional speaker-attitude EN.

Equations

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

def Rett2026.brazilianPortugueseSneg : ENDatum

Brazilian Portuguese surprise negation: é que não construction. High EN — obligatory, non-truth-conditional.

Equations

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

def Rett2026.allENData : List ENDatum

Equations

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

theorem Rett2026.high_en_blocks_npis (d : ENDatum) : d ∈ allENData → d.enType = Phenomena.Negation.ExpletiveNegation.ENType.high → ¬d.licensesAnyNPI

High EN blocks weak NPIs: in our sample, every high-EN construction has an empty licensedNPIForms list. Low EN may or may not license NPIs (Italian prima che and finché license mai/alcuno; non₂-comparatives license pur selectively; the rest block).

theorem Rett2026.italianComparative_licenses_pur : italianComparative.licensesNPIForm Fragments.Italian.PolarityItems.pur.form

Italian non₂-comparatives license pur — the surface form on italianComparative.licensedNPIForms comes from the Italian Fragment's pur entry, so renaming that entry's form would break this theorem by construction.

theorem Rett2026.italianComparative_blocks_affatto : ¬italianComparative.licensesNPIForm Fragments.Italian.PolarityItems.affatto.form

Italian non₂-comparatives block affatto — the asymmetry between pur and affatto that the previous Bool field couldn't express. Consistent with the Italian Fragment's affatto_not_licensed_in_comparative registry theorem.

theorem Rett2026.italianComparative_licensesAny : italianComparative.licensesAnyNPI

The coarse licensesAnyNPI projection recovers the previous Bool classification: italianComparative still counts as a weak-NPI licenser overall, just selectively rather than uniformly.

The ambidirectionality–EN correspondence

@cite{rett-2026} proposes that low EN is licensed iff the embedding construction is ambidirectional. The ENConstruction enum is declared above (§1); hasEN is derived from allENData (§2) by predicating "some attested datum is classified under this construction"; and isAmbidirectional is the structural classification, with each entry backed by a witness theorem (see ..._isAmbidirectional_witness below).

The ambidirectionality classification is anchored in:

• before_preEvent_ambidirectional (TemporalConnectives.lean)
• after_not_ambidirectional (TemporalConnectives.lean)
• while_not_ambidirectional (TemporalConnectives.lean)
• comparative_boundary + scale-MAX singletons (Comparative.lean + Core/Scales/Scale.lean) For until the classification follows from the same closed-interval MAX template as before. The .fear case is empirical (@cite{jin-koenig-2021} survey + @cite{villalta-2008} valence).

def Rett2026.ENConstruction.hasEN (c : ENConstruction) : Bool

Empirically observed: does the construction license EN cross-linguistically? Derived from allENData — a construction licenses EN iff some datum in the cross-linguistic record is classified under it. Adding a new datum (e.g. a documented after-clause EN) automatically updates this prediction without a parallel table edit.

Based on @cite{jin-koenig-2021} 722-language survey (EN attested in 74 languages across 37 genera).

Equations

• c.hasEN = Rett2026.allENData.any fun (x : Rett2026.ENDatum) => x.constructionType == c

def Rett2026.ENConstruction.isAmbidirectional : ENConstruction → Bool

Theory-derived: is the construction ambidirectional?

The cases anchor to specific structural results in the supporting theories — each line below names the witnessing theorem rather than re-stipulating the verdict:

• .before: anchored by before_preEvent_ambidirectional (TemporalConnectives.lean) — both B and the COMPLET of its pre-event share MAX₍<₎ = {i.start}, so before relates A only to that boundary.
• .after: anchored by after_not_ambidirectional — exhibits a counter-witness with two distinct times a < b: after b of {a} differs from after ¬b of {a}.
• .while_: anchored by while_not_ambidirectional — total-overlap semantics breaks under complementation of any singleton.
• .until: shares the endpoint structure of before (closed-interval MAX₍<₎ collapses to start point); the same proof template applies.
• .comparative: anchored by comparative_boundary (Comparative.lean) and maxOnScale_ge_atMost/maxOnScale_atLeast_singleton (Core/Scales/Scale.lean) — degree-relative MAX picks the singleton {μ w} from the "at least" set.
• .fear: empirical (@cite{jin-koenig-2021} §6.1.1). Negative-valence attitudes (@cite{villalta-2008}) entail both p (content of attitude) and ¬p (content of desire); the link between Preferential.fear.valence = .negative and the dual-inference condition is at the docstring level rather than formalized end-to-end.

The verdict per case is therefore not a free stipulation — five of six cases trace to a formal theorem; the .fear case is empirical. Mismatches between this table and the empirical hasEN table would falsify Rett's generalization (see rett_generalization below).

Equations

• Rett2026.ENConstruction.before.isAmbidirectional = true
• Rett2026.ENConstruction.after.isAmbidirectional = false
• Rett2026.ENConstruction.while_.isAmbidirectional = false
• Rett2026.ENConstruction.until.isAmbidirectional = true
• Rett2026.ENConstruction.comparative.isAmbidirectional = true
• Rett2026.ENConstruction.fear.isAmbidirectional = true

theorem Rett2026.before_isAmbidirectional_witness : ENConstruction.before.isAmbidirectional = true

Cross-references the entry isAmbidirectional .before = true to its witness. The structural anchor is Semantics.Tense.TemporalConnectives.before_preEvent_ambidirectional, which proves the iff for any closed event interval.

theorem Rett2026.after_isAmbidirectional_witness : ENConstruction.after.isAmbidirectional = false

Cross-references isAmbidirectional .after = false to Semantics.Tense.TemporalConnectives.after_not_ambidirectional, which exhibits a counter-witness.

theorem Rett2026.while_isAmbidirectional_witness : ENConstruction.while_.isAmbidirectional = false

Cross-references isAmbidirectional .while_ = false to Semantics.Tense.TemporalConnectives.while_not_ambidirectional.

theorem Rett2026.comparative_isAmbidirectional_witness : ENConstruction.comparative.isAmbidirectional = true

Cross-references isAmbidirectional .comparative = true to the boundary singletons Core.Scale.maxOnScale_ge_atMost / Core.Scale.maxOnScale_atLeast_singleton, plus Semantics.Degree.Comparative.comparative_boundary.

theorem Rett2026.rett_generalization (c : ENConstruction) : c.hasEN = c.isAmbidirectional

Rett's generalization: the empirical EN-licensing table hasEN and the structural ambidirectionality table isAmbidirectional agree on every EN-relevant construction.

This is the central empirical claim of @cite{rett-2026}: the ambidirectionality classification (derived from the semantics of MAX on closed intervals) perfectly predicts the cross-linguistic distribution of EN (observed in @cite{jin-koenig-2021}).

Why this isn't trivial. The two tables stipulate different facts drawn from different sources: hasEN records survey results (counts of EN-attesting languages per construction), while isAmbidirectional records structural ambidirectionality verdicts (each anchored to a theorem above, except .fear). If a future survey added a counter-attesting language (e.g., a documented after-clause EN), hasEN .after would flip to true while isAmbidirectional .after = false would not — and this theorem would fail by decide (since hasEN evaluates allENData.any). The agreement is empirical content, not a definitional identity.

Fear belongs to the propositional-attitude licensing class

@cite{jin-koenig-2021} §6.1.1 argues that FEAR triggers entail both Operator₁(p) (content of X's attitude) and Operator₂(¬p) (content of X's desires) — making them "ambidirectional" in the @cite{rett-2026} sense. The shared underlying property is negative valence in the @cite{villalta-2008} sense.

The conceptual chain — Preferential.fear.valence = .negative → negativeValenceEntailsDual → ENConstruction.isAmbidirectional .fear — is asserted in the literature but not formalized end-to-end here: the link from valence to dual inference is empirical (J&K survey data), not a theorem of preferential attitude semantics. The fear case of isAmbidirectional is therefore stipulated rather than derived; the link to negativeValenceEntailsDual is at the docstring level.

theorem Rett2026.fear_licensing_condition : JinKoenig2021.TriggerSubclass.fear.licensingCondition = JinKoenig2021.LicensingCondition.propositionalAttitude

Subclass classification: FEAR is a propositional-attitude licenser. Defines the encoding rather than proving content.

Connecting Fragment entries to EN predictions

@cite{rett-2026} predicts that EN in comparatives is sensitive to scale type. The mechanism:

• The than-clause denotes a degree set with a boundary at μ(b).
• Ambidirectionality requires that this boundary is shared between B and Bᶜ.
• On non-closed scales (at least one endpoint open), the degree relative forms an interval with one informative bound, which B and Bᶜ share → ambidirectional → EN licensed.
• On closed scales (both endpoints exist), negation can target a different endpoint, making the construction non-ambidirectional → EN blocked.

We connect this to AdjModifierEntry.scaleType from the English adjective fragment.

def Rett2026.licensesComparativeEN (b : Core.Scale.Boundedness) : Bool

An adjective licenses EN in its comparative iff its scale has at least one open endpoint — equivalently, iff it is NOT bidirectionally bounded. Derived structurally from Boundedness.hasMin/hasMax rather than by case-split, so the prediction follows from the scale-type classification rather than being stipulated per scale type.

Why the structural form. On any scale with at most one informative endpoint, MAX picks the same boundary from both B and Bᶜ — so negating the than-clause cannot move the boundary. On a closed scale (both endpoints exist), MAX on B picks one endpoint and MAX on Bᶜ picks the other, so negation genuinely shifts the boundary and ambidirectionality fails.

Connection to @cite{kennedy-mcnally-2005}'s relative/absolute typology: relative adjectives (tall, expensive — open scales) license EN; absolute adjectives that are closed in the relevant interval (full, dead) block it. The single-endpoint cases (lowerBounded, upperBounded) cover minimum-standard absolutes (wet, dirty) and maximum-standard absolutes (dry, clean), which still license EN because only one endpoint is available for MAX to target.

Equations

• Rett2026.licensesComparativeEN b = !(b.hasMax && b.hasMin)

theorem Rett2026.tall_licenses_EN : licensesComparativeEN Fragments.English.Modifiers.Adjectives.tall.scaleType = true

"tall" (open scale) licenses EN in comparatives.

theorem Rett2026.full_blocks_EN : licensesComparativeEN Fragments.English.Modifiers.Adjectives.full.scaleType = false

"full" (closed scale) does NOT license EN in comparatives.

theorem Rett2026.expensive_licenses_EN : licensesComparativeEN Fragments.English.Modifiers.Adjectives.expensive.scaleType = true

"expensive" (open scale) licenses EN in comparatives.

theorem Rett2026.dead_blocks_EN : licensesComparativeEN Fragments.English.Modifiers.Adjectives.dead.scaleType = false

"dead" (closed scale) does NOT license EN in comparatives.

theorem Rett2026.licensesComparativeEN_iff_some_endpoint_open (b : Core.Scale.Boundedness) : (decide (licensesComparativeEN b = !b.hasMax) || !b.hasMin) = true

licensesComparativeEN is the De Morgan dual of "both endpoints exist" — EN is licensed iff some endpoint is open. This is now rfl because the def itself is the structural form; the theorem is retained as a named statement of the prediction's content.

theorem Rett2026.closed_blocks_comparativeEN (b : Core.Scale.Boundedness) (h : (b.hasMax && b.hasMin) = true) : licensesComparativeEN b = false

The closed-scale exclusion: a fully closed scale never licenses comparative EN. Dual of licensesComparativeEN_iff_some_endpoint_open, stated in the form @cite{kennedy-mcnally-2005} would recognize (absolute adjectives = closed scales = no EN).

EN as pragmatic enrichment

When EN is used in an ambidirectional environment, it is truth-conditionally vacuous but pragmatically meaningful. The use of the marked negated form (vs the unmarked positive form) triggers a manner implicature (see MannerEffect in Adjective.Comparative):

1. French avant que... ne: "before ¬B" → "well before B" (temporal distance reading; @cite{cepeda-2018}, @cite{krifka-2010b}).

2. Italian comparative + non: "più alto di quanto non sia" → "much taller than" (evaluative reading; @cite{napoli-nespor-1976}).

3. Negative verbs (doubt, fear, worry): These are "ambidirectional" embedding verbs — fear that p and fear that ¬p share the same worry-worthy proposition, because the feared event's mere possibility (whether p or ¬p) triggers the attitude. EN in complements of fear is attested in 39 languages.

structure Rett2026.MannerImplicatureDatum : Type

A manner implicature datum: EN triggers evaluativity in a construction.

• language : String

  Language

• construction : String

  Construction

• enForm : String

  EN form

• pragmaticReading : String

  Pragmatic reading triggered

• effect : Semantics.Degree.Comparative.MannerEffect

  Manner effect classification

• source : String

  Source

@[implicit_reducible]

instance Rett2026.instReprMannerImplicatureDatum : Repr MannerImplicatureDatum

Equations

• Rett2026.instReprMannerImplicatureDatum = { reprPrec := Rett2026.instReprMannerImplicatureDatum.repr }

def Rett2026.instReprMannerImplicatureDatum.repr : MannerImplicatureDatum → ℕ → Std.Format

Equations

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

def Rett2026.frenchBeforeEvaluative : MannerImplicatureDatum

Equations

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

def Rett2026.italianComparativeEvaluative : MannerImplicatureDatum

Equations

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

def Rett2026.frenchFearAmbivalence : MannerImplicatureDatum

Equations

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

def Rett2026.allMannerData : List MannerImplicatureDatum

Equations

• Rett2026.allMannerData = [Rett2026.frenchBeforeEvaluative, Rett2026.italianComparativeEvaluative, Rett2026.frenchFearAmbivalence]

theorem Rett2026.evaluative_manner_data : ([frenchBeforeEvaluative, italianComparativeEvaluative].all fun (x : MannerImplicatureDatum) => x.effect.evaluative) = true

All manner implicature data entries with evaluative readings have effect.evaluative = true.

Connecting EN constructions to negator types

@cite{tsiakmakis-2025} classifies EN hosts as NEG₁ (standard negation masked) or NEG₂ (modal, intrinsically non-negative). The EN constructions formalized here map onto Tsiakmakis's host categories:

ENConstruction	ENHostCategory	NegatorType
before	temporalExpressions	NEG₁
until	temporalExpressions	NEG₁
comparative	comparatives	NEG₁
fear	emotiveDoxasticPredicates	NEG₂
after	(no EN)	—
while_	(no EN)	—

The key structural insight: all ambidirectional constructions that are NEG₁ hosts have their negative semantics masked by independent factors (verbal aspect, operator spell-out), while the one NEG₂ host (fear) has a genuinely different marker — a modal, not negation.

def Rett2026.ENConstruction.toHostCategory : ENConstruction → Option Tsiakmakis2025.ENHostCategory

Map each EN construction to its Tsiakmakis host category. Constructions without EN (after, while) have no host.

Equations

• Rett2026.ENConstruction.before.toHostCategory = some Tsiakmakis2025.ENHostCategory.temporalExpressions
• Rett2026.ENConstruction.until.toHostCategory = some Tsiakmakis2025.ENHostCategory.temporalExpressions
• Rett2026.ENConstruction.comparative.toHostCategory = some Tsiakmakis2025.ENHostCategory.comparatives
• Rett2026.ENConstruction.fear.toHostCategory = some Tsiakmakis2025.ENHostCategory.emotiveDoxasticPredicates
• Rett2026.ENConstruction.after.toHostCategory = none
• Rett2026.ENConstruction.while_.toHostCategory = none

theorem Rett2026.en_iff_has_host (c : ENConstruction) : c.hasEN = c.toHostCategory.isSome

Constructions with EN are exactly those with a host category. Together with rett_generalization, this triangulates: empirical hasEN (data table) ↔ structural isAmbidirectional (theory) ↔ typological toHostCategory.isSome (Tsiakmakis classification).

theorem Rett2026.neg_type_of_en_hosts : Option.map Tsiakmakis2025.ENHostCategory.negatorType ENConstruction.fear.toHostCategory = some Tsiakmakis2025.NegatorType.neg2 ∧ ([ENConstruction.before, ENConstruction.until, ENConstruction.comparative].all fun (c : ENConstruction) => Option.map Tsiakmakis2025.ENHostCategory.negatorType c.toHostCategory == some Tsiakmakis2025.NegatorType.neg1) = true

Fear maps to NEG₂ (modal); temporal and comparative map to NEG₁ (standard negation masked). This connects ambidirectionality (distributional pattern) to negator type (mechanism).