Negation × Temporal Connective Interaction Data

@cite{giannakidou-2002} @cite{greco-2020} @cite{rett-2026} @cite{jin-koenig-2021}

Theory-neutral empirical data on the interaction between negation and temporal connectives, focusing on:

1. The two-until hypothesis: Greek lexicalizes the distinction between NPI-until (= ¬before) and durative until.

2. Expletive negation: before-clauses license truth- conditionally vacuous negation cross-linguistically, explained by ambidirectionality.

Key Empirical Generalizations

• Greek prin (πριν, 'before') requires subjunctive; mexri (μέχρι, 'until') requires indicative. This mood distinction tracks veridicality.
• Mexri requires imperfective/stative main clause; prin has no aspect restriction. This mirrors Karttunen's durative selectional restriction.
• Expletive negation (EN) in before-clauses is attested in 50 of 74 EN-attesting languages (722 surveyed). EN is NOT attested in after-clauses.
• Italian: prima che non (before + EN), finché non (until + EN). French: avant que ne (before + EN).

inductive Phenomena.TemporalConnectives.NegationData.ActualizationStatus : Type

Whether a temporal connective entails that the main-clause event actually occurred at the boundary time.

• entailment: actualization is part of the assertion — cancellation yields contradiction (@cite{giannakidou-2002}, ex. 38).
• implicature: actualization is a Q-implicature — cancellable (@cite{giannakidou-2002}, ex. 7: "Sure, the princess slept until midnight. In fact she only woke up at 2am.").
• none: no actualization inference at all (@cite{giannakidou-2002}, ex. 72–73: prin/before is compatible with the complement event never occurring).

• entailment : ActualizationStatus
• implicature : ActualizationStatus
• none : ActualizationStatus

instance Phenomena.TemporalConnectives.NegationData.instDecidableEqActualizationStatus : DecidableEq ActualizationStatus

Equations

• Phenomena.TemporalConnectives.NegationData.instDecidableEqActualizationStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.TemporalConnectives.NegationData.instReprActualizationStatus : Repr ActualizationStatus

Equations

• Phenomena.TemporalConnectives.NegationData.instReprActualizationStatus = { reprPrec := Phenomena.TemporalConnectives.NegationData.instReprActualizationStatus.repr }

def Phenomena.TemporalConnectives.NegationData.instReprActualizationStatus.repr : ActualizationStatus → Nat → Std.Format

Equations

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

def Phenomena.TemporalConnectives.NegationData.instBEqActualizationStatus.beq : ActualizationStatus → ActualizationStatus → Bool

Equations

• Phenomena.TemporalConnectives.NegationData.instBEqActualizationStatus.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.TemporalConnectives.NegationData.instBEqActualizationStatus : BEq ActualizationStatus

Equations

• Phenomena.TemporalConnectives.NegationData.instBEqActualizationStatus = { beq := Phenomena.TemporalConnectives.NegationData.instBEqActualizationStatus.beq }

structure Phenomena.TemporalConnectives.NegationData.TwoUntilDatum : Type

A judgment about the two-until distinction, encoding @cite{giannakidou-2002}'s cross-linguistic evidence.

semanticType classifies connectives into three groups:

• before-type (non-veridical, NPI-licensing, no durative restriction)
• endpoint-type (veridical, no NPI-licensing, durative restriction)
• eventive-type (requires anti-veridical trigger, actualization entailment)

Greek lexicalizes all three: prin (before-type), mexri (endpoint-type), para monon (eventive-type). English collapses eventive and before under the single lexeme until, disambiguated by negation context.

• language : String

  Language

• form : String

  Connective form

• semanticType : String

  Semantic type: "before", "endpoint", or "eventive".

• moodRestriction : Option String

  Required mood of complement (if applicable)

• requiresDE : Bool

  Does it require a DE (downward-entailing) licensor?

• complementVeridical : Bool

  Is the complement veridical?

• requiresDurativeMain : Bool

  Does it restrict the main clause to durative aspect?

• licensesNPIs : Bool

  Does it license NPIs in the complement?

• example_ : String

  Example sentence

• actualizationStatus : ActualizationStatus

  Does the connective entail actualization of a change-of-state event at the boundary time? This is the central distinction between NPI-until (entailment) and durative until (implicature).

instance Phenomena.TemporalConnectives.NegationData.instReprTwoUntilDatum : Repr TwoUntilDatum

Equations

• Phenomena.TemporalConnectives.NegationData.instReprTwoUntilDatum = { reprPrec := Phenomena.TemporalConnectives.NegationData.instReprTwoUntilDatum.repr }

def Phenomena.TemporalConnectives.NegationData.instReprTwoUntilDatum.repr : TwoUntilDatum → Nat → Std.Format

Equations

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

def Phenomena.TemporalConnectives.NegationData.greek_prin : TwoUntilDatum

Greek prin (πριν): before-type. Requires subjunctive, does not require DE context (unlike English NPI-until or Greek para monon), non-veridical complement, licenses NPIs. No actualization entailment: prin is compatible with the complement event never occurring (@cite{giannakidou-2002}, §6, ex. (72): "I prigipisa dhen eftase prin apo ta mesanixta" — the princess may or may not have arrived). "Efije prin na erthi o Janis." 'She left before Janis came.'

Equations

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

def Phenomena.TemporalConnectives.NegationData.greek_mexri : TwoUntilDatum

Greek mexri (μέχρι): endpoint-type. Requires indicative, veridical complement, requires imperfective/stative main clause, does NOT license NPIs. Actualization is a conversational implicature, not an entailment. "I Maria perimine mexri irthi o Janis." 'Maria waited until Janis came.'

Equations

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

def Phenomena.TemporalConnectives.NegationData.english_npi_until : TwoUntilDatum

English NPI-until: eventive-type (@cite{giannakidou-2002}). Requires DE licensor (negation). Unlike Greek prin, English collapses both types under the single lexeme until, disambiguated by context.

Classified as "eventive" (not "before") because English NPI-until patterns with Greek para monon on all diagnostics: actualization is an entailment, a DE trigger is required, and there is no durative restriction on the main clause. Karttunen's logical form (NPI-until = ¬before) captures the truth conditions, but the phenomenological classification tracks the same semantic type as para monon.

"The princess didn't wake up until the prince kissed her."

Equations

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

def Phenomena.TemporalConnectives.NegationData.english_dur_until : TwoUntilDatum

English durative until: endpoint-type. No DE requirement, veridical complement, durative main clause required. "John slept until 3pm."

Equations

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

def Phenomena.TemporalConnectives.NegationData.greek_para_monon : TwoUntilDatum

Greek para monon (παρά μονον, lit. 'but only'): eventive-type. The true NPI-until in Greek — lexically distinct from both mexri (durative until) and prin (before). Requires anti-veridical trigger (negation, 'without'). Entails actualization: the main-clause event occurred at the boundary time. Scalar (introduces a scale of contextually relevant times).

@cite{giannakidou-2002}, §3.2: para monon is incompatible with negated perfective eventives (ex. 35: I prigipisa dhen eftase para monon ta mesanixta) but compatible with perfective statives that shift to achievement reading (ex. 37: I prigipisa dhen (apo)kimithike para monon ta mesanixta = 'The princess didn't fall asleep until midnight').

Cancellation of actualization yields contradiction (ex. 38): '#I prigipisa dhen eftase para monon ta mesanixta. Dhen eftase kan ekino to vradi.' ('#The princess didn't arrive until midnight. She didn't even arrive that night.')

Equations

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

theorem Phenomena.TemporalConnectives.NegationData.mood_diagnostic : greek_prin.moodRestriction = some "subjunctive" ∧ greek_mexri.moodRestriction = some "indicative"

The mood diagnostic: NPI-until type takes subjunctive (in languages with the distinction); durative until takes indicative.

theorem Phenomena.TemporalConnectives.NegationData.veridicality_diagnostic : greek_prin.complementVeridical = false ∧ greek_mexri.complementVeridical = true

The veridicality diagnostic: NPI-until is non-veridical; durative until is veridical.

theorem Phenomena.TemporalConnectives.NegationData.aspect_diagnostic : greek_prin.requiresDurativeMain = false ∧ greek_mexri.requiresDurativeMain = true

The aspect diagnostic: durative until requires durative main clause; NPI-until has no such restriction.

theorem Phenomena.TemporalConnectives.NegationData.npi_licensing_diagnostic : greek_prin.licensesNPIs = true ∧ greek_mexri.licensesNPIs = false

The NPI licensing diagnostic: NPI-until (= ¬before) licenses NPIs; durative until does not.

theorem Phenomena.TemporalConnectives.NegationData.diagnostics_aligned : greek_prin.semanticType = "before" ∧ greek_prin.complementVeridical = false ∧ greek_prin.requiresDurativeMain = false ∧ greek_prin.licensesNPIs = true ∧ greek_mexri.semanticType = "endpoint" ∧ greek_mexri.complementVeridical = true ∧ greek_mexri.requiresDurativeMain = true ∧ greek_mexri.licensesNPIs = false

All four diagnostics consistently distinguish the two types.

theorem Phenomena.TemporalConnectives.NegationData.actualization_three_way : greek_para_monon.actualizationStatus = ActualizationStatus.entailment ∧ english_npi_until.actualizationStatus = ActualizationStatus.entailment ∧ greek_mexri.actualizationStatus = ActualizationStatus.implicature ∧ english_dur_until.actualizationStatus = ActualizationStatus.implicature ∧ greek_prin.actualizationStatus = ActualizationStatus.none

The actualization diagnostic: the three-way split.

• para monon / English NPI-until: actualization is an entailment
• mexri / English durative until: actualization is an implicature
• prin: no actualization at all

theorem Phenomena.TemporalConnectives.NegationData.de_requirement_diagnostic : greek_para_monon.requiresDE = true ∧ greek_mexri.requiresDE = false ∧ greek_prin.requiresDE = false

Para monon requires an anti-veridical trigger (negation, 'without'); mexri does not; prin does not. This distinguishes eventive-type from both endpoint-type and before-type.

theorem Phenomena.TemporalConnectives.NegationData.para_monon_matches_english_npi_until : greek_para_monon.actualizationStatus = english_npi_until.actualizationStatus ∧ greek_para_monon.requiresDE = english_npi_until.requiresDE ∧ greek_para_monon.requiresDurativeMain = english_npi_until.requiresDurativeMain

Para monon patterns with English NPI-until on actualization and DE-requirement, confirming it is the Greek lexicalization of Karttunen's punctual until.

theorem Phenomena.TemporalConnectives.NegationData.para_monon_differs_from_prin : greek_para_monon.actualizationStatus ≠ greek_prin.actualizationStatus ∧ greek_para_monon.semanticType ≠ greek_prin.semanticType

Para monon differs from prin on actualization: prin/before has no actualization, para monon entails it. This is the paper's central finding — NPI-until ≠ before on actualization status (@cite{giannakidou-2002}, §6).

theorem Phenomena.TemporalConnectives.NegationData.greek_three_way_lexicalized : greek_prin.semanticType ≠ greek_mexri.semanticType ∧ greek_prin.semanticType ≠ greek_para_monon.semanticType ∧ greek_mexri.semanticType ≠ greek_para_monon.semanticType

The three Greek connectives are pairwise distinct on semantic type.

structure Phenomena.TemporalConnectives.NegationData.ExpletiveNegDatum : Type

An attested instance of expletive negation (EN) in a temporal clause. EN is truth-conditionally vacuous: the sentence has the same truth conditions with or without the negative marker.

• language : String

  Language

• connective : String

  Temporal connective hosting EN

• formWithEN : String

  Surface form with EN

• formWithoutEN : String

  Surface form without EN (same truth conditions)

• obligatory : Bool

  Is EN obligatory in this context?

• mannerImplicature : Bool

  Does EN trigger a manner implicature ("much before")?

• example_ : String

  Example sentence

def Phenomena.TemporalConnectives.NegationData.instReprExpletiveNegDatum.repr : ExpletiveNegDatum → Nat → Std.Format

Equations

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

instance Phenomena.TemporalConnectives.NegationData.instReprExpletiveNegDatum : Repr ExpletiveNegDatum

Equations

• Phenomena.TemporalConnectives.NegationData.instReprExpletiveNegDatum = { reprPrec := Phenomena.TemporalConnectives.NegationData.instReprExpletiveNegDatum.repr }

def Phenomena.TemporalConnectives.NegationData.italian_prima_EN : ExpletiveNegDatum

Italian prima che non — EN in before-clause. "Mario è partito prima che non arrivasse Gianni." 'Mario left before Gianni arrived.' EN is optional; triggers "well before" reading.

Equations

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

def Phenomena.TemporalConnectives.NegationData.italian_finche_EN : ExpletiveNegDatum

Italian finché non — EN in until-clause. "Maria ha aspettato finché non è arrivato Gianni." 'Maria waited until Gianni arrived.' EN is often felt as obligatory in colloquial Italian.

Equations

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

def Phenomena.TemporalConnectives.NegationData.french_avant_EN : ExpletiveNegDatum

French avant que ne — EN in before-clause. "Jean est parti avant que Marie ne soit arrivée." 'Jean left before Marie arrived.' Historically obligatory in formal registers; now optional.

Equations

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

Note: The ambidirectionality↔EN correspondence formalized here is also verified (more comprehensively) in Phenomena.Negation.Studies.Rett2026.rett_generalization over the ENConstruction enum, which covers all six construction types. The ENDistribution entries below provide the same generalization over a subset (temporal connectives only).

structure Phenomena.TemporalConnectives.NegationData.ENDistribution : Type

EN is attested with before and until but NOT with after or when. This follows from ambidirectionality: before is ambidirectional (negating the complement doesn't change truth conditions), so EN is vacuous. After is NOT ambidirectional, so EN would change truth conditions (genuine negation, not expletive).

• connective : String

  Connective

• enAttested : Bool

  Is EN attested cross-linguistically?

• ambidirectional : Bool

  Is the connective ambidirectional?

instance Phenomena.TemporalConnectives.NegationData.instReprENDistribution : Repr ENDistribution

Equations

• Phenomena.TemporalConnectives.NegationData.instReprENDistribution = { reprPrec := Phenomena.TemporalConnectives.NegationData.instReprENDistribution.repr }

def Phenomena.TemporalConnectives.NegationData.instReprENDistribution.repr : ENDistribution → Nat → Std.Format

Equations

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

def Phenomena.TemporalConnectives.NegationData.before_EN : ENDistribution

Equations

• Phenomena.TemporalConnectives.NegationData.before_EN = { connective := "before", enAttested := true, ambidirectional := true }

def Phenomena.TemporalConnectives.NegationData.after_EN : ENDistribution

Equations

• Phenomena.TemporalConnectives.NegationData.after_EN = { connective := "after", enAttested := false, ambidirectional := false }

def Phenomena.TemporalConnectives.NegationData.until_EN : ENDistribution

Equations

• Phenomena.TemporalConnectives.NegationData.until_EN = { connective := "until (NPI type)", enAttested := true, ambidirectional := true }

def Phenomena.TemporalConnectives.NegationData.when_EN : ENDistribution

Equations

• Phenomena.TemporalConnectives.NegationData.when_EN = { connective := "when", enAttested := false, ambidirectional := false }

theorem Phenomena.TemporalConnectives.NegationData.en_iff_ambidirectional : before_EN.enAttested = before_EN.ambidirectional ∧ after_EN.enAttested = after_EN.ambidirectional ∧ until_EN.enAttested = until_EN.ambidirectional ∧ when_EN.enAttested = when_EN.ambidirectional

EN is attested iff the connective is ambidirectional. This is the core empirical generalization: EN is licensed exactly in those environments where negation is truth-conditionally vacuous.

EN survey data (722 languages, 74 with EN, 37 genera) is defined in Phenomena.Negation.Typology.enSurvey to avoid duplication.