Giannakidou (2002): UNTIL, Aspect, and Negation #
@cite{giannakidou-2002} @cite{karttunen-1974} @cite{klein-1994} @cite{de-swart-1996} @cite{de-swart-molendijk-1999}
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 @cite{karttunen-1974}'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 @cite{karttunen-1974}'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, @cite{pancheva-2003}) projected
to SentDenotation for the imperfective denotation:
EventPred Unit Time ──[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 #
impfDen_subinterval_closed: IMPF gives homogeneityprfvDen_not_subinterval_closed: PRFV does notscope_readings_distinct/scope_readings_independent: logically independentimpfDen_homogeneous/prfvDen_not_always_homogeneous: wide scope derivedwideScopeNotUntil_compatible_with_empty_main: wide scope lacks actualizationeventiveUntil_entails_actualization: NPI-until entails actualizationnegBefore_lacks_actualization: ¬before compatible with no main-clause eventbefore_not_equiv_eventiveUntil: ¬before ≠ NPI-until on actualization (§6)stativizer_all_wrong: all five diagnostics refute @cite{de-swart-1996} (§5)
IMPF denotation: project Aspect.Core.UNBOUNDED to SentDenotation.
Each interval in the denotation is a subinterval of some event runtime
(@cite{klein-1994}: TT ⊆ TSit). Uses UNBOUNDED (@cite{pancheva-2003})
rather than IMPF (which requires strict ⊂) because the homogeneity
argument is identical and the non-strict version connects cleanly to
stativeDenotation.
Equations
Instances For
PRFV denotation: the set of exact event runtimes.
Unlike the Aspect.Core.PRFV operator (which gives intervals CONTAINING
the runtime: TSit ⊆ TT), this gives the τ-image {τ(e) | P(e)} — the
interval set that directly characterizes the event's temporal extent.
This matches the eventDenotation pattern from EventBridge.lean.
Equations
- Phenomena.TemporalConnectives.Studies.Giannakidou2002.prfvDen P = {i : Core.Time.Interval Time | ∃ (e : Semantics.Tense.Aspect.Core.Eventuality Time), P () e ∧ e.τ = i}
Instances For
A sentence denotation is homogeneous (subinterval-closed) when membership is preserved under subintervals. This is Karttunen's selectional restriction for durative until: the main clause must be homogeneous.
Equations
- Phenomena.TemporalConnectives.Studies.Giannakidou2002.IsHomogeneous D = ∀ t ∈ D, ∀ (t' : Core.Time.Interval Time), t'.subinterval t → t' ∈ D
Instances For
IMPF denotation satisfies the subinterval property.
This is exactly the homogeneity property that @cite{karttunen-1974} 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.
IMPF denotation contains the event runtime itself (the maximal interval).
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.
IMPF denotation is homogeneous — wide scope is available.
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.
@cite{giannakidou-2002}'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.
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.
For a single event, the PRFV denotation is exactly the accomplishment denotation (singleton containing just the runtime).
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).
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
- One or more equations did not get rendered due to their size.
Instances For
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
- One or more equations did not get rendered due to their size.
Instances For
Narrow-scope ¬until is exactly ¬before (by definition). This is @cite{karttunen-1974}'s identity, now made explicit in the aspectual decomposition.
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.beforeholds.
The reverse also holds: there exist A, B where narrow-scope holds but wide-scope fails. This confirms the two readings are genuinely independent.
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
- One or more equations did not get rendered due to their size.
Instances For
Eventive UNTIL entails main-clause actualization: A must have occurred. This is the actualization entailment that @cite{giannakidou-2002} identifies as the hallmark of NPI-until (para monon), absent from durative until (mexri) and before (prin).
Eventive UNTIL entails complement actualization: B must have occurred.
Eventive UNTIL entails ¬before: A didn't happen prior to B.
Eventive UNTIL entails temporal coincidence (when): A and B overlap.
Karttunen's notUntil does NOT entail eventive UNTIL:
¬(A before B) holds vacuously when A is empty (no actualization).
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 @cite{giannakidou-2002}'s ex. (51) (imperfective mexri + continuation asserting no event) and ex. (57) (perfective para monon + contradictory continuation).
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 @cite{giannakidou-2002}'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.
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 @cite{giannakidou-2002}'s central claim: the two readings are not truth-conditionally equivalent under negation.
The NegationData actualization three-way split aligns with the formal
semantics: eventive-type (entailment) corresponds to eventiveUntil
(overlap + lateness), endpoint-type (implicature) to Karttunen.until
(overlap alone), and before-type (none) to Karttunen.notUntil
(lateness alone).
The aspect diagnostic from NegationData: durative until (mexri) requires imperfective main clause; NPI-until (para monon) does not. This matches the formal result: wide-scope requires homogeneity (= imperfective), narrow-scope does not.
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)
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.
@cite{giannakidou-2002} refutes the analysis of negation as an aspectual operator that converts eventive predicates into stative ones (@cite{de-swart-1996}, @cite{de-swart-molendijk-1999}). 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.
@cite{de-swart-1996}'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).
The five stativizer diagnostics and their results for negated perfective forms (@cite{giannakidou-2002}, §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
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
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?
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
The stativizer gets every diagnostic wrong: its prediction never matches the actual negated-perfective result.
@cite{giannakidou-2002}'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.
@cite{giannakidou-2002}'s §6 refines @cite{karttunen-1974}'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.
¬before (= @cite{karttunen-1974}'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.
@cite{giannakidou-2002}, §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).
NPI-until ≠ ¬before on actualization (@cite{giannakidou-2002}, §6).
eventiveUntil A Bentails main-clause actualization (∃t ∈ A)¬(A before B)is compatible with main-clause non-actualization (A = ∅)
This is the formal content of @cite{giannakidou-2002}'s central §6 claim: @cite{karttunen-1974}'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.