Giannakidou (2002): UNTIL, Aspect, and Negation

[Gia02] [Kar74] [Kle94] [dS96] [dSM99]

A Novel Argument for Two Untils. Semantics and Linguistic Theory 12, 84–103.

Central Argument

Viewpoint aspect determines negation scope with until:

• Imperfective main clause: homogeneous (subinterval property), satisfying durative until's selectional restriction. Both wide-scope and narrow-scope negation are available.

• Perfective main clause: not homogeneous. Only narrow-scope negation (= Karttunen's ¬before) is available.

This provides a novel argument for [Kar74]'s two-until hypothesis: the scope readings are logically independent, so the restriction to narrow scope under PRFV is a genuine empirical constraint, not a logical consequence.

A secondary contribution (§6) refines [Kar74]'s identity NPI-until = ¬before: while truth-conditionally valid, para monon (NPI-until) and prin (before) differ on actualization — NPI-until entails the main-clause event occurred, before does not — and on scope interaction with imperfective aspect.

Architecture

Uses Aspect.Core.UNBOUNDED (= non-strict IMPF, [Pan03]) projected to SentDenotation for the imperfective denotation:

Unit → Event Time → Prop ──[UNBOUNDED]──▷ IntervalPred ──[fix w=()]──▷ SentDenotation

The key property — subinterval-closure — holds for both UNBOUNDED (⊆) and IMPF (⊂); we use UNBOUNDED because the argument doesn't depend on the strict/non-strict distinction and the non-strict version connects cleanly to stativeDenotation in Basic.lean.

Key Results

1. impfDen_subinterval_closed: IMPF gives homogeneity
2. prfvDen_not_subinterval_closed: PRFV does not
3. scope_readings_distinct/scope_readings_independent: logically independent
4. impfDen_homogeneous/prfvDen_not_always_homogeneous: wide scope derived
5. wideScopeNotUntil_compatible_with_empty_main: wide scope lacks actualization
6. eventiveUntil_entails_actualization: NPI-until entails actualization
7. negBefore_lacks_actualization: ¬before compatible with no main-clause event
8. before_not_equiv_eventiveUntil: ¬before ≠ NPI-until on actualization (§6)
9. stativizer_all_wrong: all five diagnostics refute [dS96] (§5)

@[reducible, inline]

abbrev Giannakidou2002.impfDen {Time : Type u_1} [LinearOrder Time] (P : Unit → Event Time → Prop) : Tense.TemporalConnectives.SentDenotation Time

IMPF denotation: project Aspect.Core.UNBOUNDED to SentDenotation. Each interval in the denotation is a subinterval of some event runtime ([Kle94]: TT ⊆ TSit). Uses UNBOUNDED ([Pan03]) rather than IMPF (which requires strict ⊂) because the homogeneity argument is identical and the non-strict version connects cleanly to stativeDenotation.

Equations

• Giannakidou2002.impfDen P = {i : NonemptyInterval Time | Semantics.Aspect.UNBOUNDED P () i}

def Giannakidou2002.prfvDen {Time : Type u_1} [LinearOrder Time] (P : Unit → Event Time → Prop) : Tense.TemporalConnectives.SentDenotation Time

PRFV denotation: the set of exact event runtimes — the eventDenotation τ-image (Projection.lean) of P (). Unlike the Aspect.Core.PRFV operator (whose intervals CONTAIN the runtime: TSit ⊆ TT), this gives the runtime itself, directly characterizing the event's temporal extent.

Equations

• Giannakidou2002.prfvDen P = eventDenotation (P ())

A sentence denotation is homogeneous (subinterval-closed) when membership is preserved under subintervals — Karttunen's selectional restriction for durative until. This is exactly mathlib's IsLowerSet over the interval ≤ (subinterval containment), so we state homogeneity directly as IsLowerSet below.

theorem Giannakidou2002.impfDen_subinterval_closed {Time : Type u_1} [LinearOrder Time] (P : Unit → Event Time → Prop) (t : NonemptyInterval Time) (ht : t ∈ impfDen P) (t' : NonemptyInterval Time) (ht' : t' ≤ t) : t' ∈ impfDen P

IMPF denotation satisfies the subinterval property.

This is exactly the homogeneity property that [Kar74] requires of the main clause of durative until. The imperfective viewpoint provides this automatically: since the event extends beyond any reference interval, every sub-window into the event is equally valid.

theorem Giannakidou2002.impfDen_contains_runtime {Time : Type u_1} [LinearOrder Time] (P : Unit → Event Time → Prop) (e : Event Time) (hP : P () e) : e.τ ∈ impfDen P

IMPF denotation contains the event runtime itself (the maximal interval).

theorem Giannakidou2002.prfvDen_not_subinterval_closed : ¬∀ (P : Unit → Event ℤ → Prop), ∀ t ∈ prfvDen P, ∀ t' ≤ t, t' ∈ prfvDen P

PRFV denotation does NOT have the subinterval property.

Counterexample: An event with runtime [0, 5]. The interval [0, 5] is in the denotation, but [1, 3] (a strict subinterval) is not — PRFV only includes the exact runtime.

This is why perfective clauses cannot be main clauses of durative until: they lack the homogeneity that until requires.

theorem Giannakidou2002.impfDen_homogeneous {Time : Type u_1} [LinearOrder Time] (P : Unit → Event Time → Prop) : IsLowerSet (impfDen P)

IMPF denotation is homogeneous (a lower set / subinterval-closed) — wide scope is available.

theorem Giannakidou2002.prfvDen_not_always_homogeneous : ¬∀ (P : Unit → Event ℤ → Prop), IsLowerSet (prfvDen P)

PRFV denotation is not always homogeneous — wide scope is not always available. This is derived from the subinterval-closure failure, not stipulated as a Bool field.

theorem Giannakidou2002.scope_pattern_derived {Time : Type u_1} [LinearOrder Time] : (∀ (P : Unit → Event Time → Prop), IsLowerSet (impfDen P)) ∧ ¬∀ (P : Unit → Event ℤ → Prop), IsLowerSet (prfvDen P)

[Gia02]'s scope generalization, derived from homogeneity: wide-scope negation requires a homogeneous main clause, which IMPF provides and PRFV does not. The restriction to narrow scope under PRFV follows from PRFV's failure of subinterval-closure, not from a stipulated constraint.

theorem Giannakidou2002.impfDen_singleton_eq_stativeDenotation {Time : Type u_1} [LinearOrder Time] (i : NonemptyInterval Time) : (impfDen fun (x : Unit) (e : Event Time) => e.τ = i) = Tense.TemporalConnectives.stativeDenotation i

For a single event with runtime i, the IMPF denotation is exactly the stative denotation of i (all subintervals). This connects the aspect bridge to the existing temporal connective infrastructure in Basic.lean.

theorem Giannakidou2002.prfvDen_singleton_eq_accomplishmentDenotation {Time : Type u_1} [LinearOrder Time] (i : NonemptyInterval Time) : (prfvDen fun (x : Unit) (e : Event Time) => e.τ = i) = Tense.TemporalConnectives.accomplishmentDenotation i

For a single event, the PRFV denotation is exactly the accomplishment denotation (singleton containing just the runtime).

theorem Giannakidou2002.timeTrace_impf_eq_prfv {Time : Type u_1} [LinearOrder Time] (P : Unit → Event Time → Prop) : Tense.TemporalConnectives.timeTrace (impfDen P) = Tense.TemporalConnectives.timeTrace (prfvDen P)

The time traces of IMPF and PRFV denotations are identical: both equal the set of times contained in some event runtime.

This is why Karttunen's Level 1 (point-set) definitions cannot distinguish imperfective from perfective clauses — the difference is only visible at Level 2 (interval sets).

def Giannakidou2002.wideScopeNotUntil {Time : Type u_1} [LinearOrder Time] (A : Unit → Event Time → Prop) (B : Tense.TemporalConnectives.SentDenotation Time) : Prop

Wide-scope negation over imperfective until:

¬∃t [t ∈ timeTrace(IMPF(A)) ∧ t ∈ timeTrace(B)]

"It's not the case that A was ongoing up to the time of B."

Available when A is imperfective: the main clause denotes a homogeneous interval set via IMPF, so until can take it as an argument. Negation scopes over the entire until-clause.

Equations

• Giannakidou2002.wideScopeNotUntil A B = ¬Tense.TemporalConnectives.Karttunen.when_ (Giannakidou2002.impfDen A) B

def Giannakidou2002.narrowScopeNotUntil {Time : Type u_1} [LinearOrder Time] (A : Unit → Event Time → Prop) (B : Tense.TemporalConnectives.SentDenotation Time) : Prop

Narrow-scope negation under until (= Karttunen's ¬before):

¬(A BEFORE B)

"A didn't happen before B" — the event occurred, but not prior to B.

This is the only reading available with perfective main clauses: since PRFV gives a bounded event, until reduces to temporal ordering and negation gives Karttunen's notUntil = ¬before.

Equations

• Giannakidou2002.narrowScopeNotUntil A B = Tense.TemporalConnectives.Karttunen.notUntil (Giannakidou2002.prfvDen A) B

theorem Giannakidou2002.narrowScope_eq_not_before {Time : Type u_1} [LinearOrder Time] (A : Unit → Event Time → Prop) (B : Tense.TemporalConnectives.SentDenotation Time) : narrowScopeNotUntil A B ↔ ¬Tense.TemporalConnectives.Anscombe.before (prfvDen A) B

Narrow-scope ¬until is exactly ¬before (by definition). This is [Kar74]'s identity, now made explicit in the aspectual decomposition.

theorem Giannakidou2002.scope_readings_distinct : ∃ (A : Unit → Event ℤ → Prop) (B : Tense.TemporalConnectives.SentDenotation ℤ), wideScopeNotUntil A B ∧ ¬narrowScopeNotUntil A B

The two scope readings are semantically distinct: there exist A, B where wide-scope holds but narrow-scope fails.

Counterexample: event A with runtime [0, 5], B at time 7.

• Wide scope: ¬(any A-time overlaps with time 7). TRUE — 7 ∉ [0, 5].
• Narrow scope: ¬(A happened before B). FALSE — time 0 < 7, so A precedes B and Anscombe.before holds.

theorem Giannakidou2002.scope_readings_independent : ∃ (A : Unit → Event ℤ → Prop) (B : Tense.TemporalConnectives.SentDenotation ℤ), ¬wideScopeNotUntil A B ∧ narrowScopeNotUntil A B

The reverse also holds: there exist A, B where narrow-scope holds but wide-scope fails. This confirms the two readings are genuinely independent.

def Giannakidou2002.eventiveUntil {Time : Type u_1} [LinearOrder Time] (A B : Tense.TemporalConnectives.SentDenotation Time) : Prop

Eventive UNTIL: the semantics of Greek para monon and Karttunen's punctual until. Combines temporal coincidence (A overlaps B) with lateness (A does not precede B):

⟦dhen P para monon Q⟧ = (∃t. t∈A ∧ t∈B) ∧ ¬(A before B)

This builds actualization into the assertion, unlike Karttunen.notUntil (= ¬before alone) which holds vacuously when A is empty.

This is a simplified version of the full ex. (39), which additionally includes a contextual restriction C over the scale of relevant times: ¬∃t'∃e' [t'∈C ∧ t'<t ∧ P(e',t')]. The scalar/contextual component is abstracted away here; the core truth-conditional difference (overlap + lateness vs. lateness alone) is preserved.

Equations

• Giannakidou2002.eventiveUntil A B = ((∃ t ∈ Tense.TemporalConnectives.timeTrace A, t ∈ Tense.TemporalConnectives.timeTrace B) ∧ ¬Tense.TemporalConnectives.Anscombe.before A B)

theorem Giannakidou2002.eventiveUntil_entails_actualization {Time : Type u_1} [LinearOrder Time] (A B : Tense.TemporalConnectives.SentDenotation Time) : eventiveUntil A B → ∃ (t : Time), t ∈ Tense.TemporalConnectives.timeTrace A

Eventive UNTIL entails main-clause actualization: A must have occurred. This is the actualization entailment that [Gia02] identifies as the hallmark of NPI-until (para monon), absent from durative until (mexri) and before (prin).

theorem Giannakidou2002.eventiveUntil_entails_complement {Time : Type u_1} [LinearOrder Time] (A B : Tense.TemporalConnectives.SentDenotation Time) : eventiveUntil A B → ∃ (t : Time), t ∈ Tense.TemporalConnectives.timeTrace B

Eventive UNTIL entails complement actualization: B must have occurred.

theorem Giannakidou2002.eventiveUntil_entails_notBefore {Time : Type u_1} [LinearOrder Time] (A B : Tense.TemporalConnectives.SentDenotation Time) : eventiveUntil A B → Tense.TemporalConnectives.Karttunen.notUntil A B

Eventive UNTIL entails ¬before: A didn't happen prior to B.

theorem Giannakidou2002.eventiveUntil_entails_when {Time : Type u_1} [LinearOrder Time] (A B : Tense.TemporalConnectives.SentDenotation Time) : eventiveUntil A B → Tense.TemporalConnectives.Karttunen.when_ A B

Eventive UNTIL entails temporal coincidence (when): A and B overlap.

theorem Giannakidou2002.notUntil_not_implies_eventiveUntil : ∃ (A : Tense.TemporalConnectives.SentDenotation ℤ) (B : Tense.TemporalConnectives.SentDenotation ℤ), Tense.TemporalConnectives.Karttunen.notUntil A B ∧ ¬eventiveUntil A B

Karttunen's notUntil does NOT entail eventive UNTIL: ¬(A before B) holds vacuously when A is empty (no actualization).

theorem Giannakidou2002.wideScopeNotUntil_compatible_with_empty_main : ∃ (A : Unit → Event ℤ → Prop) (B : Tense.TemporalConnectives.SentDenotation ℤ), wideScopeNotUntil A B ∧ ¬∃ (t : ℤ), t ∈ Tense.TemporalConnectives.timeTrace (impfDen A)

Wide-scope negation does NOT entail actualization.

This is the key asymmetry with eventive UNTIL (§8 above): NPI-until (para monon) entails actualization, but the Mittwoch reading (wide-scope negation over durative until) does not.

Proved by construction: an event A with runtime [0, 5] and complement B at time 3. Wide-scope negation holds (the state of not-A extends beyond B), but A DID occur — the non-actualization is shown by the fact that wide-scope is COMPATIBLE with either actualization or non-actualization, unlike eventive UNTIL which requires it.

This formalizes the contrast between [Gia02]'s ex. (51) (imperfective mexri + continuation asserting no event) and ex. (57) (perfective para monon + contradictory continuation).

theorem Giannakidou2002.durative_compatible_with_before : ∃ (A : Tense.TemporalConnectives.SentDenotation ℤ) (B : Tense.TemporalConnectives.SentDenotation ℤ), Tense.TemporalConnectives.Karttunen.until A B ∧ Tense.TemporalConnectives.Anscombe.before A B

Durative until is compatible with A preceding B: the main clause state can extend well before the complement time.

This is the formal correlate of [Gia02]'s ex. (7): "Sure, the princess slept until midnight. In fact she only woke up at 2am." — the state extends past the boundary, and the change-of-state is not entailed.

theorem Giannakidou2002.eventiveUntil_strictly_stronger : (∀ (A B : Tense.TemporalConnectives.SentDenotation ℤ), eventiveUntil A B → Tense.TemporalConnectives.Karttunen.notUntil A B) ∧ ∃ (A : Tense.TemporalConnectives.SentDenotation ℤ) (B : Tense.TemporalConnectives.SentDenotation ℤ), Tense.TemporalConnectives.Karttunen.notUntil A B ∧ ¬eventiveUntil A B

Eventive UNTIL is strictly stronger than Karttunen's notUntil.

• eventiveUntil → notUntil (actualization + lateness → lateness)
• notUntil ↛ eventiveUntil (lateness alone lacks actualization)

This is the formal content of [Gia02]'s central claim: the two readings are not truth-conditionally equivalent under negation.

inductive Giannakidou2002.UntilType : Type

Giannakidou's three-way semantic typology of until-type connectives: before-type (prin), endpoint-type (durative until, mexri), and eventive-type (NPI-until, para monon).

• before : UntilType
• endpoint : UntilType
• eventive : UntilType

@[implicit_reducible]

instance Giannakidou2002.instDecidableEqUntilType : DecidableEq UntilType

Equations

• Giannakidou2002.instDecidableEqUntilType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Giannakidou2002.instReprUntilType.repr : UntilType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Giannakidou2002.instReprUntilType : Repr UntilType

Equations

• Giannakidou2002.instReprUntilType = { reprPrec := Giannakidou2002.instReprUntilType.repr }

inductive Giannakidou2002.ActualizationStatus : Type

Whether a connective entails that the main-clause event actually occurred at the boundary time: an entailment (cancellation yields contradiction, ex. 38), a cancellable Q-implicature (ex. 7), or absent entirely (exx. 72–73).

• entailment : ActualizationStatus
• implicature : ActualizationStatus
• absent : ActualizationStatus

@[implicit_reducible]

instance Giannakidou2002.instDecidableEqActualizationStatus : DecidableEq ActualizationStatus

Equations

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

def Giannakidou2002.instReprActualizationStatus.repr : ActualizationStatus → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Giannakidou2002.instReprActualizationStatus : Repr ActualizationStatus

Equations

• Giannakidou2002.instReprActualizationStatus = { reprPrec := Giannakidou2002.instReprActualizationStatus.repr }

def Giannakidou2002.untilTypeOf (row : Data.Examples.LinguisticExample) : Option UntilType

The row's semantic_type feature as an UntilType.

Equations

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

def Giannakidou2002.actualizationOf (row : Data.Examples.LinguisticExample) : Option ActualizationStatus

The row's actualization feature as an ActualizationStatus.

Equations

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

def Giannakidou2002.UntilType.actualization : UntilType → ActualizationStatus

The actualization status each semantic type carries, matching the formal operators: eventive = eventiveUntil (the overlap conjunct entails actualization), endpoint = Karttunen.until (boundary change-of-state only implicated), before = Karttunen.notUntil under negation (lateness alone, cf. negBefore_lacks_actualization).

Equations

• Giannakidou2002.UntilType.before.actualization = Giannakidou2002.ActualizationStatus.absent
• Giannakidou2002.UntilType.endpoint.actualization = Giannakidou2002.ActualizationStatus.implicature
• Giannakidou2002.UntilType.eventive.actualization = Giannakidou2002.ActualizationStatus.entailment

theorem Giannakidou2002.actualization_determined_by_type (row : Data.Examples.LinguisticExample) : row ∈ Examples.all → actualizationOf row = Option.map UntilType.actualization (untilTypeOf row)

Every row's actualization annotation is determined by its semantic type — the three-way split that is the paper's central claim.

theorem Giannakidou2002.veridical_iff_endpoint (row : Data.Examples.LinguisticExample) : row ∈ Examples.all → (row.feature? "complement_veridical" = some "true" ↔ untilTypeOf row = some UntilType.endpoint)

Endpoint-type rows are exactly the veridical ones: durative until presupposes its complement, while before-type and eventive-type connectives are nonveridical.

theorem Giannakidou2002.durative_main_iff_endpoint (row : Data.Examples.LinguisticExample) : row ∈ Examples.all → (row.feature? "requires_durative_main" = some "true" ↔ untilTypeOf row = some UntilType.endpoint)

Endpoint-type rows are exactly the ones with the durative main-clause restriction. The formal correlate: wide scope requires homogeneity (impfDen_homogeneous), which only durative/imperfective main clauses provide; narrow scope (narrowScopeNotUntil) does not.

theorem Giannakidou2002.requires_de_iff_eventive (row : Data.Examples.LinguisticExample) : row ∈ Examples.all → (row.feature? "requires_de" = some "true" ↔ untilTypeOf row = some UntilType.eventive)

Eventive-type rows are exactly the ones requiring an anti-veridical (DE) trigger — the licensing condition on para monon and English NPI-until.

theorem Giannakidou2002.npi_licensing_by_type (row : Data.Examples.LinguisticExample) : row ∈ Examples.all → (untilTypeOf row = some UntilType.before → row.feature? "licenses_npis" = some "true") ∧ (untilTypeOf row = some UntilType.endpoint → row.feature? "licenses_npis" = some "false")

Before-type rows license NPIs; endpoint-type rows do not. (Eventive rows split: English NPI-until hosts NPIs, para monon does not.)

theorem Giannakidou2002.greek_lexicalizes_three_types (ty : UntilType) : ∃ row ∈ Examples.all, row.language = "mode1248" ∧ untilTypeOf row = some ty

Greek lexicalizes all three semantic types as distinct connectives: prin (before), mexri (endpoint), para monon (eventive).

def Giannakidou2002.UntilType.greekMood : UntilType → Option String

The mood restriction each semantic type imposes in Greek.

Equations

• Giannakidou2002.UntilType.before.greekMood = some "subjunctive"
• Giannakidou2002.UntilType.endpoint.greekMood = some "indicative"
• Giannakidou2002.UntilType.eventive.greekMood = none

theorem Giannakidou2002.greek_mood_tracks_type (row : Data.Examples.LinguisticExample) : row ∈ Examples.all → row.language = "mode1248" → row.feature? "mood" = (untilTypeOf row).bind UntilType.greekMood

Greek mood tracks the semantic type: subjunctive for before-type, indicative for endpoint-type, no mood restriction for eventive-type. The mood split is the morphological reflex of (non)veridicality.

theorem Giannakidou2002.greek_three_way_maps_to_operators : Greek.StandardModern.TemporalConnectives.mexri.order = English.TemporalExpressions.TemporalOrder.until_ ∧ Greek.StandardModern.TemporalConnectives.mexri.complementVeridical = true ∧ Greek.StandardModern.TemporalConnectives.paraMonon.order = English.TemporalExpressions.TemporalOrder.until_ ∧ Greek.StandardModern.TemporalConnectives.paraMonon.complementVeridical = false ∧ Greek.StandardModern.TemporalConnectives.paraMonon.forcesPunctual = true ∧ Greek.StandardModern.TemporalConnectives.prin.order = English.TemporalExpressions.TemporalOrder.before ∧ Greek.StandardModern.TemporalConnectives.prin.complementVeridical = false

Greek lexicalizes the three semantic types as distinct lexemes: mexri (durative), para monon (eventive NPI), prin (before). Each maps to a different temporal connective operator:

• mexri → Karttunen.until (= when_, overlap)
• para monon → eventiveUntil (overlap + lateness)
• prin → Anscombe.before (ordering)

theorem Giannakidou2002.veridicality_split : Greek.StandardModern.TemporalConnectives.mexri.complementVeridical = true ∧ Greek.StandardModern.TemporalConnectives.paraMonon.complementVeridical = false ∧ Greek.StandardModern.TemporalConnectives.prin.complementVeridical = false

The veridicality split between mexri (veridical) and para monon (non-veridical) corresponds to the formal difference: durative until presupposes the complement, while eventive until asserts both overlap and non-precedence.

[Gia02] refutes the analysis of negation as an aspectual operator that converts eventive predicates into stative ones ([dS96], [dSM99]). On that account, negation takes an eventuality description P and yields a maximal state s such that no event of type P is contained in s. If this were correct, negated perfectives should behave like statives — but they don't: Greek negated perfectives still reject durative until (mexri), reject how long, reject while, and accept imperatives.

theorem Giannakidou2002.stativizer_false_for_perfective : ¬∀ (P : Unit → Event ℤ → Prop), IsLowerSet (prfvDen P)

[dS96]'s stativizer hypothesis: negation converts events into maximal states, so ALL negated predicates (including perfectives) should be homogeneous (subinterval-closed), just like true statives.

The formal refutation: if this were correct, then PRFV denotations would always be homogeneous. But we proved in §2 that PRFV is NOT always homogeneous (prfvDen_not_subinterval_closed).

inductive Giannakidou2002.StativizerDiagnostic : Type

The five stativizer diagnostics and their results for negated perfective forms ([Gia02], §5, ex. 67–71):

Diagnostic	True stative	Neg+PRFV	Stativizer predicts
how long	✓	✗	✓ (WRONG)
while	✓	✗	✓ (WRONG)
for adv	✓	✗	✓ (WRONG)
imperative	✗	✓	✗ (WRONG)
mexri	✓	✗	✓ (WRONG)

All five diagnostics give results inconsistent with stativehood for negated perfectives.

• howLong : StativizerDiagnostic
• while_ : StativizerDiagnostic
• forAdverb : StativizerDiagnostic
• imperative : StativizerDiagnostic
• mexri : StativizerDiagnostic

@[implicit_reducible]

instance Giannakidou2002.instDecidableEqStativizerDiagnostic : DecidableEq StativizerDiagnostic

Equations

• Giannakidou2002.instDecidableEqStativizerDiagnostic x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Giannakidou2002.instReprStativizerDiagnostic : Repr StativizerDiagnostic

Equations

• Giannakidou2002.instReprStativizerDiagnostic = { reprPrec := Giannakidou2002.instReprStativizerDiagnostic.repr }

def Giannakidou2002.instReprStativizerDiagnostic.repr : StativizerDiagnostic → ℕ → Std.Format

Equations

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

structure Giannakidou2002.DiagnosticResult : Type

Result of applying a stativizer diagnostic.

• diagnostic : StativizerDiagnostic
• trueStativeResult : Bool

  Is this compatible with true statives?

• negPerfResult : Bool

  Is this compatible with negated perfectives?

• stativizerPredicts : Bool

  What does the stativizer predict for negated perfectives?

def Giannakidou2002.instReprDiagnosticResult.repr : DiagnosticResult → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Giannakidou2002.instReprDiagnosticResult : Repr DiagnosticResult

Equations

• Giannakidou2002.instReprDiagnosticResult = { reprPrec := Giannakidou2002.instReprDiagnosticResult.repr }

def Giannakidou2002.diagnosticResults : List DiagnosticResult

Equations

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

theorem Giannakidou2002.stativizer_all_wrong (d : DiagnosticResult) : d ∈ diagnosticResults → d.negPerfResult ≠ d.stativizerPredicts

The stativizer gets every diagnostic wrong: its prediction never matches the actual negated-perfective result.

theorem Giannakidou2002.english_past_perfective_default : (¬∀ (P : Unit → Event ℤ → Prop), IsLowerSet (prfvDen P)) ∧ ∀ (P : Unit → Event ℤ → Prop), IsLowerSet (impfDen P)

[Gia02]'s argument that the English simple past has a perfective default value: English past-tense statives with until pattern with Greek PERFECTIVE, not imperfective.

Evidence: "The princess didn't sleep until midnight" lacks the Mittwoch reading (no wide-scope until), entails actualization (she fell asleep at midnight), and disallows preposing ("*Until midnight, the princess didn't sleep"). These are exactly the properties of Greek negated perfective + mexri, not Greek negated imperfective + mexri.

Formalized as: the scope pattern for English simple past follows from PRFV (not IMPF), which is why wide-scope is unavailable.

[Gia02]'s §6 refines [Kar74]'s identity NPI-until = ¬before: while truth-conditionally valid at the level of temporal ordering, the two connectives differ on actualization.

- *Prin/before*: no actualization. "I prigipisa dhen eftase prin apo ta
  mesanixta" (ex. 72) is compatible with "she arrived later or didn't
  arrive at all."
- *Para monon*/NPI-*until*: actualization is an entailment. "I prigipisa
  dhen eftase para monon ta mesanixta" (ex. 38) is contradicted by
  "she didn't arrive that night."

Additionally, the Mittwoch reading (wide scope) is NOT available with
*prin* + imperfective stative (ex. 76): "I prigipisa dhen kimotane prin
apo ta mesanixta" gives only a habitual reading ("there was a period
during which she had the habit of not going to bed before midnight"),
not a stative reading. This contrasts with *mexri* + IMPF (ex. 74)
which does give the stative/Mittwoch reading. 

theorem Giannakidou2002.negBefore_lacks_actualization : ∃ (A : Tense.TemporalConnectives.SentDenotation ℤ) (B : Tense.TemporalConnectives.SentDenotation ℤ), Tense.TemporalConnectives.Karttunen.notUntil A B ∧ ¬∃ (t : ℤ), t ∈ Tense.TemporalConnectives.timeTrace A

¬before (= [Kar74]'s notUntil) is compatible with the main-clause event never occurring: when A = ∅, ¬(A before B) holds vacuously since Anscombe.before ∅ B is always false.

[Gia02], §6, ex. (72): "I prigipisa dhen eftase prin apo ta mesanixta" — the princess may or may not have arrived. Prin/before with negation does not entail actualization of the arriving event.

Contrast with eventiveUntil, which requires main-clause actualization (the overlap conjunct forces a witness in A).

theorem Giannakidou2002.before_not_equiv_eventiveUntil {Time : Type u_1} [LinearOrder Time] : (∀ (A B : Tense.TemporalConnectives.SentDenotation Time), eventiveUntil A B → ∃ (t : Time), t ∈ Tense.TemporalConnectives.timeTrace A) ∧ ∃ (A : Tense.TemporalConnectives.SentDenotation ℤ) (B : Tense.TemporalConnectives.SentDenotation ℤ), Tense.TemporalConnectives.Karttunen.notUntil A B ∧ ¬∃ (t : ℤ), t ∈ Tense.TemporalConnectives.timeTrace A

NPI-until ≠ ¬before on actualization ([Gia02], §6).

• eventiveUntil A B entails main-clause actualization (∃t ∈ A)
• ¬(A before B) is compatible with main-clause non-actualization (A = ∅)

This is the formal content of [Gia02]'s central §6 claim: [Kar74]'s truth-conditional identity (NPI-until = ¬before) holds at the level of temporal ordering, but the two connective types are not interchangeable — NPI-until additionally requires actualization. The impression of equivalence is a by-product of scalarity, a feature common to both prin/before and until/para monon.

Per-language strategy entries for the durative/eventive until distinction. The UntilStrategy enum + UntilTypologyEntry schema (consolidated from the former Typology/TemporalConnectives.lean) plus the per-language data + Fragment grounding theorems are all paper-anchored here.

inductive Giannakidou2002.UntilStrategy : Type

How a language handles the durative/eventive until distinction ([Gia02]).

• threeWay : UntilStrategy

  Three distinct lexemes: before, durative until, eventive NPI-until. Greek: prin, mexri, para monon.

• twoWay : UntilStrategy

  Two distinct lexemes: durative until and eventive NPI-until. Icelandic: flanga til, fyrr en. Finnish: kunnes, ennenkuin.

• ambiguous : UntilStrategy

  Single ambiguous lexeme, disambiguated by negation context. English: until.

• ppiReplacement : UntilStrategy

  Durative until blocked under negation; PPI replaces NPI-until. Dutch: tot, pas. German: bis, erst.

@[implicit_reducible]

instance Giannakidou2002.instDecidableEqUntilStrategy : DecidableEq UntilStrategy

Equations

• Giannakidou2002.instDecidableEqUntilStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Giannakidou2002.instReprUntilStrategy.repr : UntilStrategy → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Giannakidou2002.instReprUntilStrategy : Repr UntilStrategy

Equations

• Giannakidou2002.instReprUntilStrategy = { reprPrec := Giannakidou2002.instReprUntilStrategy.repr }

structure Giannakidou2002.UntilTypologyEntry : Type

A language's strategy for the two-until distinction.

• language : String
• strategy : UntilStrategy
• durativeForm : String

  Surface form for durative until.

• eventiveForm : String

  Surface form for eventive until (NPI or PPI).

• eventiveMorphBeforeBased : Bool

  Is the eventive form morphologically built on before? ([Kar74]'s identity NPI-until = ¬before.)

• hasOvertAspect : Bool

  Does the language have overt perfective/imperfective marking? Orthogonal to the lexicalization choice.

@[implicit_reducible]

instance Giannakidou2002.instReprUntilTypologyEntry : Repr UntilTypologyEntry

Equations

• Giannakidou2002.instReprUntilTypologyEntry = { reprPrec := Giannakidou2002.instReprUntilTypologyEntry.repr }

def Giannakidou2002.instReprUntilTypologyEntry.repr : UntilTypologyEntry → ℕ → Std.Format

Equations

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

def Giannakidou2002.greek : UntilTypologyEntry

Equations

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

def Giannakidou2002.icelandic : UntilTypologyEntry

Equations

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

def Giannakidou2002.finnish : UntilTypologyEntry

Equations

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

def Giannakidou2002.english : UntilTypologyEntry

Equations

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

def Giannakidou2002.dutch : UntilTypologyEntry

Equations

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

def Giannakidou2002.german : UntilTypologyEntry

Equations

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

def Giannakidou2002.typology : List UntilTypologyEntry

The full typological sample (6 languages, 4 strategies).

Equations

• Giannakidou2002.typology = [Giannakidou2002.greek, Giannakidou2002.icelandic, Giannakidou2002.finnish, Giannakidou2002.english, Giannakidou2002.dutch, Giannakidou2002.german]

theorem Giannakidou2002.all_distinguish_durative_eventive (e : UntilTypologyEntry) : e ∈ typology → e.durativeForm ≠ e.eventiveForm

Every language in the sample uses distinct surface forms for durative and eventive until (even the ambiguous strategy uses the same form in different syntactic contexts, disambiguated by negation).

theorem Giannakidou2002.before_morphology_attested : icelandic.eventiveMorphBeforeBased = true ∧ finnish.eventiveMorphBeforeBased = true

The two-way and three-way strategies both have morphologically before-based eventive forms in at least one language, confirming [Kar74]'s identity NPI-until = ¬before.

theorem Giannakidou2002.aspect_not_required : icelandic.hasOvertAspect = false ∧ icelandic.strategy = UntilStrategy.twoWay ∧ finnish.hasOvertAspect = false ∧ finnish.strategy = UntilStrategy.twoWay

Overt aspect marking is NOT required for lexicalization of the two-until distinction. Icelandic and Finnish lack overt verbal aspect but still lexicalize two untils.

theorem Giannakidou2002.greek_confirmed : Greek.StandardModern.TemporalConnectives.mexri.form ≠ Greek.StandardModern.TemporalConnectives.paraMonon.form ∧ Greek.StandardModern.TemporalConnectives.mexri.form ≠ Greek.StandardModern.TemporalConnectives.prin.form ∧ Greek.StandardModern.TemporalConnectives.paraMonon.form ≠ Greek.StandardModern.TemporalConnectives.prin.form

Greek strategy confirmed by fragment: three distinct forms.

theorem Giannakidou2002.icelandic_confirmed : Icelandic.TemporalConnectives.flangaTil.form ≠ Icelandic.TemporalConnectives.fyrrEn.form ∧ Icelandic.TemporalConnectives.flangaTil.complementVeridical = true ∧ Icelandic.TemporalConnectives.fyrrEn.complementVeridical = false

Icelandic strategy confirmed by fragment: two distinct forms with veridicality split.

theorem Giannakidou2002.dutch_confirmed : Dutch.TemporalConnectives.tot.form ≠ Dutch.TemporalConnectives.pas.form ∧ Dutch.TemporalConnectives.tot.complementVeridical = true ∧ Dutch.TemporalConnectives.pas.complementVeridical = false

Dutch strategy confirmed by fragment: two distinct forms with veridicality split.

theorem Giannakidou2002.eventive_attested_crosslinguistically : (∃ row ∈ Examples.all, row.language = "stan1293" ∧ untilTypeOf row = some UntilType.eventive) ∧ ∃ row ∈ Examples.all, row.language = "mode1248" ∧ untilTypeOf row = some UntilType.eventive

The eventive type is attested in both English (NPI-until) and Greek (para monon): the lexicalization strategies differ, but the semantic type — and with it the actualization entailment (actualization_determined_by_type) — is preserved.