Documentation

Linglib.Phenomena.Negation.Studies.Rett2026

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 Phenomena.Negation.Studies.Rett2026.ENType :

Two syntactic types of expletive negation.

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

Instances For

instance Phenomena.Negation.Studies.Rett2026.instDecidableEqENType :

DecidableEq ENType

Equations

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

instance Phenomena.Negation.Studies.Rett2026.instBEqENType :

Equations

Phenomena.Negation.Studies.Rett2026.instBEqENType = { beq := Phenomena.Negation.Studies.Rett2026.instBEqENType.beq }

def Phenomena.Negation.Studies.Rett2026.instBEqENType.beq :

ENType → ENType → Bool

Equations

Phenomena.Negation.Studies.Rett2026.instBEqENType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Phenomena.Negation.Studies.Rett2026.instReprENType :

Equations

Phenomena.Negation.Studies.Rett2026.instReprENType = { reprPrec := Phenomena.Negation.Studies.Rett2026.instReprENType.repr }

def Phenomena.Negation.Studies.Rett2026.instReprENType.repr :

ENType → ℕ → Std.Format

Equations

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

Instances For

structure Phenomena.Negation.Studies.Rett2026.ENDatum :

A cross-linguistic EN licensing datum.

language : String
Language
construction : String
Construction type
negMarker : String
Negation marker used
enType : ENType
High or low EN
isOptional : Bool
Is the EN optional?
licensesWeakNPIs : Bool
Does the construction also license weak NPIs?
mannerEffect : Option Semantics.Degree.Comparative.MannerEffect
Manner implicature triggered by EN (if any)

Instances For

instance Phenomena.Negation.Studies.Rett2026.instReprENDatum :

Equations

Phenomena.Negation.Studies.Rett2026.instReprENDatum = { reprPrec := Phenomena.Negation.Studies.Rett2026.instReprENDatum.repr }

def Phenomena.Negation.Studies.Rett2026.instReprENDatum.repr :

ENDatum → ℕ → Std.Format

Equations

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

Instances For

@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 Phenomena.Negation.Studies.Rett2026.frenchBefore :

Equations

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

Instances For

def Phenomena.Negation.Studies.Rett2026.italianBefore :

Equations

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

Instances For

def Phenomena.Negation.Studies.Rett2026.spanishComparative :

Equations

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

Instances For

def Phenomena.Negation.Studies.Rett2026.italianComparative :

Equations

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

Instances For

def Phenomena.Negation.Studies.Rett2026.frenchFear :

Equations

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

Instances For

def Phenomena.Negation.Studies.Rett2026.italianUntil :

@cite{greco-2018}: Italian until-clauses license both EN and weak NPIs.

Equations

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

Instances For

def Phenomena.Negation.Studies.Rett2026.italianExclamative :

Italian wh-exclamatives: high EN.

Equations

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

Instances For

def Phenomena.Negation.Studies.Rett2026.italianSneg :

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.

Equations

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

Instances For

def Phenomena.Negation.Studies.Rett2026.brazilianPortugueseSneg :

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.

Instances For

def Phenomena.Negation.Studies.Rett2026.allENData :

Equations

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

Instances For

theorem Phenomena.Negation.Studies.Rett2026.high_en_blocks_npis :

(allENData.all fun (d : ENDatum) => if (d.enType == ENType.high) = true then !d.licensesWeakNPIs else true) = true

High EN blocks weak NPIs: in our sample, every high-EN construction has licensesWeakNPIs = false. Low EN may or may not license NPIs (Italian prima che and finché do).

The ambidirectionality–EN correspondence #

@cite{rett-2026} proposes that low EN is licensed iff the embedding construction is ambidirectional. We formalize this as a correspondence between an enumeration of EN-relevant constructions (with their theory-derived ambidirectionality classification) and the empirical record of which constructions license EN cross-linguistically.

The ambidirectionality classification is derived from:

before_ambidirectional (TemporalConnectives.lean)
after_not_ambidirectional (TemporalConnectives.lean)
while_not_ambidirectional (TemporalConnectives.lean)
comparative_boundary (Comparative.lean) For until and fear, the classification follows from the same structural argument as before (shared endpoint / shared possibility).

inductive Phenomena.Negation.Studies.Rett2026.ENConstruction :

Constructions relevant to EN licensing. Each has a theory-derived ambidirectionality status and an empirically-observed EN status; Rett's claim is that these match.

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

Instances For

instance Phenomena.Negation.Studies.Rett2026.instDecidableEqENConstruction :

DecidableEq ENConstruction

Equations

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

instance Phenomena.Negation.Studies.Rett2026.instBEqENConstruction :

BEq ENConstruction

Equations

Phenomena.Negation.Studies.Rett2026.instBEqENConstruction = { beq := Phenomena.Negation.Studies.Rett2026.instBEqENConstruction.beq }

def Phenomena.Negation.Studies.Rett2026.instBEqENConstruction.beq :

ENConstruction → ENConstruction → Bool

Equations

Phenomena.Negation.Studies.Rett2026.instBEqENConstruction.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Phenomena.Negation.Studies.Rett2026.instReprENConstruction :

Repr ENConstruction

Equations

Phenomena.Negation.Studies.Rett2026.instReprENConstruction = { reprPrec := Phenomena.Negation.Studies.Rett2026.instReprENConstruction.repr }

def Phenomena.Negation.Studies.Rett2026.instReprENConstruction.repr :

ENConstruction → ℕ → Std.Format

Equations

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

Instances For

def Phenomena.Negation.Studies.Rett2026.ENConstruction.isAmbidirectional :

ENConstruction → Bool

Theory-derived: is the construction ambidirectional? Backed by the ambidirectionality theorems in TemporalConnectives and Comparative.

before: ambidirectional on closed intervals (cf. before_ambidirectional in TemporalConnectives.lean)
after: NOT ambidirectional — MAX on complement is different (cf. after_not_ambidirectional)
while: NOT ambidirectional — overlap with B ≠ overlap with Bᶜ (cf. while_not_ambidirectional)
until: ambidirectional — shares endpoint structure with before
comparative: ambidirectional on degree relatives (cf. comparative_boundary in Comparative.lean)
fear: ambidirectional — DERIVED from negative valence in preferential attitude semantics (@cite{villalta-2008}). Fear-type verbs activate both p (content of attitude) and ¬p (content of desire), satisfying @cite{jin-koenig-2021}'s propositional attitude licensing condition (§5.5, 13a). See fear_ambidirectional_from_valence.

Equations

Instances For

def Phenomena.Negation.Studies.Rett2026.ENConstruction.hasEN :

ENConstruction → Bool

Empirically observed: does the construction license EN cross-linguistically? Based on @cite{jin-koenig-2021} 722-language survey (EN attested in 74 languages).

Equations

Instances For

theorem Phenomena.Negation.Studies.Rett2026.rett_generalization (c : ENConstruction) :

c.hasEN = c.isAmbidirectional

Rett's generalization: a construction licenses EN iff it is ambidirectional. Verified exhaustively over all EN-relevant constructions.

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}).

Deriving fear's ambidirectionality #

The fear case of isAmbidirectional is NOT an ad hoc stipulation — it follows from the negative valence of fear-type predicates in preferential attitude semantics (@cite{villalta-2008}).

@cite{jin-koenig-2021} §6.1.1 shows that FEAR triggers entail both Operator₁(p) (content of X's attitude) and Operator₂(¬p) (content of X's desires). This dual-inference property makes the complement ambidirectional: fear p and fear ¬p share the same worry-worthy possibility.

The bridge: negative valence in Preferential.lean corresponds to the propositional attitude licensing condition in @cite{jin-koenig-2021}.

theorem Phenomena.Negation.Studies.Rett2026.fear_licensing_condition :

JinKoenig2021.TriggerSubclass.fear.licensingCondition = JinKoenig2021.LicensingCondition.propositionalAttitude

The FEAR subclass maps to the propositional attitude licensing condition.

theorem Phenomena.Negation.Studies.Rett2026.fear_ambidirectional_from_valence :

JinKoenig2021.negativeValenceEntailsDual Semantics.Attitudes.Preferential.AttitudeValence.negative = true ∧ ENConstruction.fear.isAmbidirectional = true

Fear's ambidirectionality is grounded in negative valence: negative-valence predicates activate dual propositions (p and ¬p), which makes their complements ambidirectional.

This connects three layers:

Preferential.fear has valence = .negative (attitude semantics)
Negative valence → dual inference (@cite{jin-koenig-2021} §5.5)
Dual inference → ambidirectionality (@cite{rett-2026})

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 Phenomena.Negation.Studies.Rett2026.licensesComparativeEN (scaleType : Core.Scale.Boundedness) :

An adjective licenses EN in its comparative iff its scale is non-closed: at least one endpoint is open, so the degree relative has a single shared informative bound.

.open_: both ends open (tall, expensive) → one shared bound ✓
.lowerBounded: min exists, no max (wet) → one shared bound ✓
.upperBounded: max exists, no min (dry) → one shared bound ✓
.closed: both bounds exist (full, empty) → negation can target the other bound → ambidirectionality fails ✗

Equations

Instances For

theorem Phenomena.Negation.Studies.Rett2026.tall_licenses_EN :

licensesComparativeEN Fragments.English.Modifiers.Adjectives.tall.scaleType = true

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

theorem Phenomena.Negation.Studies.Rett2026.full_blocks_EN :

licensesComparativeEN Fragments.English.Modifiers.Adjectives.full.scaleType = false

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

theorem Phenomena.Negation.Studies.Rett2026.expensive_licenses_EN :

licensesComparativeEN Fragments.English.Modifiers.Adjectives.expensive.scaleType = true

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

theorem Phenomena.Negation.Studies.Rett2026.dead_blocks_EN :

licensesComparativeEN Fragments.English.Modifiers.Adjectives.dead.scaleType = false

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

theorem Phenomena.Negation.Studies.Rett2026.licensesComparativeEN_iff_not_closed (b : Core.Scale.Boundedness) :

(decide (licensesComparativeEN b = !b.hasMax) || !b.hasMin) = true

licensesComparativeEN is equivalent to ¬ Boundedness.closed: EN is licensed iff the scale is NOT fully closed. This connects the EN prediction to the existing scale infrastructure.

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

French avant que... ne: "before ¬B" → "well before B" (temporal distance reading; @cite{cepeda-2018}, @cite{krifka-2010b}).
Italian comparative + non: "più alto di quanto non sia" → "much taller than" (evaluative reading; @cite{napoli-nespor-1976}).
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 Phenomena.Negation.Studies.Rett2026.MannerImplicatureDatum :

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

Instances For

def Phenomena.Negation.Studies.Rett2026.instReprMannerImplicatureDatum.repr :

MannerImplicatureDatum → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Negation.Studies.Rett2026.instReprMannerImplicatureDatum :

Repr MannerImplicatureDatum

Equations

Phenomena.Negation.Studies.Rett2026.instReprMannerImplicatureDatum = { reprPrec := Phenomena.Negation.Studies.Rett2026.instReprMannerImplicatureDatum.repr }

def Phenomena.Negation.Studies.Rett2026.frenchBeforeEvaluative :

MannerImplicatureDatum

Equations

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

Instances For

def Phenomena.Negation.Studies.Rett2026.italianComparativeEvaluative :

MannerImplicatureDatum

Equations

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

Instances For

def Phenomena.Negation.Studies.Rett2026.frenchFearAmbivalence :

MannerImplicatureDatum

Equations

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

Instances For

def Phenomena.Negation.Studies.Rett2026.allMannerData :

List MannerImplicatureDatum

Equations

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

Instances For

theorem Phenomena.Negation.Studies.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 Phenomena.Negation.Studies.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

Instances For

theorem Phenomena.Negation.Studies.Rett2026.en_iff_has_host (c : ENConstruction) :

c.hasEN = c.toHostCategory.isSome

Constructions with EN are exactly those with a host category.

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