Giannakidou (2002): UNTIL, Aspect, and Negation

Giannakidou argues for Karttunen's two untils against the one-until analysis of Mittwoch and de Swart, on which negation is an aspectual stativizer. Durative UNTIL asks its description to hold at every subinterval of an interval ending at the until time, which a homogeneous description, one with the subinterval property, supplies and a perfective description of a single event cannot; since the imperfective is homogeneous, Greek, which marks aspect overtly, lets mexri combine with imperfectives and not with negated perfectives, where the polarity item para monon stands in. Under negation the analyses part ways: the wide-scope reading holds when nothing P-like ever happens, whereas eventive UNTIL entails the event and is Karttunen's not until with the actualization his presupposition supplies. The paper's Greek, English, Icelandic and Dutch judgments follow from the fragment entries of the connectives and its classification of the punctual words, and its stativity diagnostics from homogeneity with negation playing no role.

Main statements

• not_durativeUntil_prfv: a perfective description of a single event rules out durative UNTIL.
• wideScope_of_forall_not: the wide-scope reading carries no actualization.
• eventiveUntil_iff: eventive UNTIL is not until with actualization.
• rows_predicted: every judgment on the UNTIL sentences is predicted.
• diagnostics_predicted: the stativity diagnostics follow from homogeneity alone.

Implementation notes

• Descriptions are the interval properties of Aspect; events carry a run time and a perfective description places it within the reference interval, an imperfective one strictly around it. The until interval is required to be nondegenerate, which is what excludes a single event from satisfying the durative condition at both its endpoints.
• Homogeneity is the subinterval property of Aspect/SubintervalProperty.lean, and durative UNTIL is the durative reading Aspect.durative at a nondegenerate span ending at the until time.
• The relation of each connective is read off its fragment entry. Which words are punctual untils, Greek para monon, Icelandic fyrr en and Dutch pas, is the paper's classification (Connective.Punctual). The polarity of the eventive words is read off their polarity-item entries: para monon, fyrr en and English until are negative polarity items and need an antiveridical licenser, Dutch pas is a positive one.
• The oddity of Nancy didn't get married until she died and of its Greek counterpart, which the actualization entailment explains, is pragmatic and is left in prose.

References

• [Gia02]
• [Kar74b]
• [Mit77]
• [dS96]

Durative UNTIL and homogeneity

def Giannakidou2002.durativeUntil {W : Type u_1} {T : Type u_2} [LinearOrder T] (p : W → Set (NonemptyInterval T)) (w : W) (t' : T) : Prop

Durative UNTIL holds when the description holds throughout a nondegenerate interval ending at the until time, at every one of its subintervals.

Equations

• Giannakidou2002.durativeUntil p w t' = ∃ i ∈ Aspect.durative p w, i.toProd.1 < i.toProd.2 ∧ i.toProd.2 = t'

theorem Giannakidou2002.durativeUntil_iff_of_isLowerSet {W : Type u_1} {T : Type u_2} [LinearOrder T] {p : W → Set (NonemptyInterval T)} {w : W} (hp : IsLowerSet (p w)) (t' : T) : durativeUntil p w t' ↔ ∃ i ∈ p w, i.toProd.1 < i.toProd.2 ∧ i.toProd.2 = t'

A homogeneous description need only hold at the until interval itself.

theorem Giannakidou2002.not_durativeUntil_prfv {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {P : W → E → Prop} {w : W} (hP : ∀ (e e' : E), P w e → P w e' → e = e') (t' : T) : ¬durativeUntil (Aspect.PRFV P) w t'

A perfective description of a single event is incompatible with durative UNTIL, since an achievement or accomplishment cannot lie within both endpoints of the until interval.

Negation: wide scope, narrow scope and the eventive UNTIL

def Giannakidou2002.notState {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (P : W → E → Prop) : W → Set (NonemptyInterval T)

The state of not-P-ing, which a stativizing negation would deliver, holds when no P-event overlaps the interval.

Equations

• Giannakidou2002.notState P w = {i : NonemptyInterval T | ∀ (e : E), P w e → ∀ a ∈ Event.τ e, a ∉ i}

theorem Giannakidou2002.isLowerSet_notState {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (P : W → E → Prop) (w : W) : IsLowerSet (notState P w)

def Giannakidou2002.wideScope {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (P : W → E → Prop) (w : W) (t' : T) : Prop

Mittwoch's wide-scope reading is durative UNTIL of the state of not-P-ing.

Equations

• Giannakidou2002.wideScope P w t' = Giannakidou2002.durativeUntil (Giannakidou2002.notState P) w t'

def Giannakidou2002.narrowScope {W : Type u_1} {T : Type u_2} [LinearOrder T] (p : W → Set (NonemptyInterval T)) (w : W) (t' : T) : Prop

External negation denies the durative UNTIL claim.

Equations

• Giannakidou2002.narrowScope p w t' = ¬Giannakidou2002.durativeUntil p w t'

def Giannakidou2002.eventiveUntil {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (P : W → E → Prop) (w : W) (t : T) : Prop

Karttunen's scalar eventive UNTIL holds when a P-event occurs at the until time and none starts earlier.

Equations

• Giannakidou2002.eventiveUntil P w t = ((∃ (e : E), P w e ∧ t ∈ Event.τ e) ∧ ∀ (e : E), P w e → t ≤ (Event.τ e).toProd.1)

theorem Giannakidou2002.eventiveUntil_actualization {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {P : W → E → Prop} {w : W} {t : T} (h : eventiveUntil P w t) : ∃ (e : E), P w e

theorem Giannakidou2002.wideScope_of_forall_not {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {P : W → E → Prop} {w : W} (hP : ∀ (e : E), ¬P w e) {t t' : T} (h : t < t') : wideScope P w t'

The wide-scope reading holds when nothing P-like ever happens, so it carries no actualization.

theorem Giannakidou2002.eventiveUntil_iff {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (P : W → E → Prop) (w : W) (t : T) : eventiveUntil P w t ↔ Karttunen1974.notUntil (Event.τ '' {e : E | P w e}) {NonemptyInterval.pure t} ∧ Heinamaki1974.when_ (Event.τ '' {e : E | P w e}) {NonemptyInterval.pure t}

Eventive UNTIL is Karttunen's not until together with the actualization his presupposition supplies.

theorem Giannakidou2002.eventiveUntil_not_before {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {P : W → E → Prop} {w : W} {t : T} (h : eventiveUntil P w t) : ¬Heinamaki1974.before (Event.τ '' {e : E | P w e}) t

Eventive UNTIL entails not before, one direction of Karttunen's equivalence.

theorem Giannakidou2002.not_before_of_forall_not {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {P : W → E → Prop} {w : W} (hP : ∀ (e : E), ¬P w e) (t : T) : ¬Heinamaki1974.before (Event.τ '' {e : E | P w e}) t

Not before carries no actualization, since it holds when nothing P-like ever happens.

The paper's sentences

inductive Giannakidou2002.Connective : Type

A Connective is one of the UNTIL words or before in the paper's four languages.

• until : Connective
• mexri : Connective
• paraMonon : Connective
• prin : Connective
• til : Connective
• fyrrEn : Connective
• tot : Connective
• pas : Connective

@[instance_reducible]

instance Giannakidou2002.instDecidableEqConnective : DecidableEq Connective

Equations

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

def Giannakidou2002.instReprConnective.repr : Connective → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Giannakidou2002.instReprConnective : Repr Connective

Equations

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

def Giannakidou2002.paraMononEntry : Tense.Connective

The paper's connective entry lists Greek para monon, literally 'but only', as an until word, as in i prigipisa dhen eftase para monon ta mesanixta 'the princess did not arrive until midnight'.

Equations

• Giannakidou2002.paraMononEntry = { form := "para monon", relation := Tense.Connective.Relation.until_ }

def Giannakidou2002.Connective.entry : Connective → Tense.Connective

c.entry is the connective entry of c, the fragment's, or the paper's own for para monon.

Equations

• Giannakidou2002.Connective.until.entry = English.TemporalConnectives.until_
• Giannakidou2002.Connective.mexri.entry = Greek.StandardModern.TemporalConnectives.mexri
• Giannakidou2002.Connective.paraMonon.entry = Giannakidou2002.paraMononEntry
• Giannakidou2002.Connective.prin.entry = Greek.StandardModern.TemporalConnectives.prin
• Giannakidou2002.Connective.til.entry = Icelandic.TemporalConnectives.thangadTil
• Giannakidou2002.Connective.fyrrEn.entry = Icelandic.TemporalConnectives.fyrrEn
• Giannakidou2002.Connective.tot.entry = Dutch.TemporalConnectives.tot
• Giannakidou2002.Connective.pas.entry = Dutch.TemporalConnectives.pas

def Giannakidou2002.Connective.polarityItem : Connective → Option PolarityItem

c.polarityItem is the polarity item that the connective c is or doubles as, for the Greek, Icelandic and Dutch punctual until words, and English until in its eventive use.

Equations

• Giannakidou2002.Connective.until.polarityItem = some English.PolarityItems.until_
• Giannakidou2002.Connective.paraMonon.polarityItem = some Greek.StandardModern.PolarityItems.paraMonon
• Giannakidou2002.Connective.fyrrEn.polarityItem = some Icelandic.PolarityItems.fyrrEn
• Giannakidou2002.Connective.pas.polarityItem = some Dutch.PolarityItems.pas
• x✝.polarityItem = none

def Giannakidou2002.Connective.Punctual (c : Connective) : Prop

The punctual untils, the words the paper takes to lexicalize Karttunen's eventive UNTIL, are Greek para monon, Icelandic fyrr en and Dutch pas.

Equations

• c.Punctual = (c = Giannakidou2002.Connective.paraMonon ∨ c = Giannakidou2002.Connective.fyrrEn ∨ c = Giannakidou2002.Connective.pas)

@[instance_reducible]

instance Giannakidou2002.instDecidablePredConnectivePunctual : DecidablePred Connective.Punctual

Equations

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

@[reducible, inline]

abbrev Giannakidou2002.Connective.Durative (c : Connective) : Prop

A connective is durative UNTIL when it is an until entry that is not punctual.

Equations

• c.Durative = (c.entry.relation = Tense.Connective.Relation.until_ ∧ ¬c.Punctual)

@[reducible, inline]

abbrev Giannakidou2002.Connective.Eventive (c : Connective) : Prop

A connective is eventive UNTIL when it is punctual or an until with a polarity-item use.

Equations

• c.Eventive = (c.Punctual ∨ c.polarityItem.isSome = true)

@[reducible, inline]

abbrev Giannakidou2002.Connective.Before (c : Connective) : Prop

Equations

• c.Before = (c.entry.relation = Tense.Connective.Relation.before)

inductive Giannakidou2002.AspectForm : Type

An AspectForm is the viewpoint of the main clause.

• imperfective : AspectForm
• perfective : AspectForm
• progressive : AspectForm
• perfect : AspectForm
• simplePast : AspectForm

@[instance_reducible]

instance Giannakidou2002.instDecidableEqAspectForm : DecidableEq AspectForm

Equations

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

@[instance_reducible]

instance Giannakidou2002.instReprAspectForm : Repr AspectForm

Equations

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

def Giannakidou2002.instReprAspectForm.repr : AspectForm → ℕ → Std.Format

Equations

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

inductive Giannakidou2002.Eventuality : Type

An Eventuality class separates states and activities from achievements and accomplishments.

• stative : Eventuality
• eventive : Eventuality

@[instance_reducible]

instance Giannakidou2002.instDecidableEqEventuality : DecidableEq Eventuality

Equations

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

@[instance_reducible]

instance Giannakidou2002.instReprEventuality : Repr Eventuality

Equations

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

def Giannakidou2002.instReprEventuality.repr : Eventuality → ℕ → Std.Format

Equations

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

inductive Giannakidou2002.Licenser : Type

A Licenser is what the sentence puts the connective under.

• none : Licenser
• negation : Licenser
• without : Licenser
• nonveridical : Licenser

@[instance_reducible]

instance Giannakidou2002.instDecidableEqLicenser : DecidableEq Licenser

Equations

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

def Giannakidou2002.instReprLicenser.repr : Licenser → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Giannakidou2002.instReprLicenser : Repr Licenser

Equations

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

@[reducible, inline]

abbrev Giannakidou2002.Licenser.Antiveridical (l : Licenser) : Prop

Negation and without are the antiveridical licensers.

Equations

• l.Antiveridical = (l = Giannakidou2002.Licenser.negation ∨ l = Giannakidou2002.Licenser.without)

inductive Giannakidou2002.Test : Type

A Test is what the sentence tests, acceptability, preposing of the UNTIL phrase, or a continuation denying the event.

• plain : Test
• preposed : Test
• noEventContinuation : Test

@[instance_reducible]

instance Giannakidou2002.instDecidableEqTest : DecidableEq Test

Equations

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

@[instance_reducible]

instance Giannakidou2002.instReprTest : Repr Test

Equations

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

def Giannakidou2002.instReprTest.repr : Test → ℕ → Std.Format

Equations

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

structure Giannakidou2002.Row : Type

• connective : Connective
• aspect : AspectForm
• eventuality : Eventuality
• licenser : Licenser
• test : Test
• acceptable : Bool

@[instance_reducible]

instance Giannakidou2002.instDecidableEqRow : DecidableEq Row

Equations

• Giannakidou2002.instDecidableEqRow = Giannakidou2002.instDecidableEqRow.decEq

def Giannakidou2002.instDecidableEqRow.decEq (x✝ x✝¹ : Row) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Giannakidou2002.instReprRow : Repr Row

Equations

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

def Giannakidou2002.instReprRow.repr : Row → ℕ → Std.Format

Equations

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

@[reducible, inline]

abbrev Giannakidou2002.Homog (a : AspectForm) (e : Eventuality) : Prop

A main clause is homogeneous when it has an imperfective, progressive or perfect form, or is stative.

Equations

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

@[reducible, inline]

abbrev Giannakidou2002.WideScopeForm (a : AspectForm) : Prop

The forms that admit the wide-scope reading are the imperfective and the perfect.

Equations

• Giannakidou2002.WideScopeForm a = (a = Giannakidou2002.AspectForm.imperfective ∨ a = Giannakidou2002.AspectForm.perfect)

@[reducible, inline]

abbrev Giannakidou2002.Licensed (c : Connective) (l : Licenser) : Prop

The polarity item of a connective demands an antiveridical licenser for a negative item, none for a positive one.

Equations

• Giannakidou2002.Licensed c l = ∀ i ∈ c.polarityItem, (i.IsNPI → l.Antiveridical) ∧ (i.IsPPI → l = Giannakidou2002.Licenser.none)

def Giannakidou2002.Predicted (r : Row) : Prop

Predicted is the judgment that the two-until analysis predicts for a row.

Equations

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

@[instance_reducible]

instance Giannakidou2002.instDecidablePredRowPredicted : DecidablePred Predicted

Equations

• Giannakidou2002.instDecidablePredRowPredicted x✝ = id inferInstance

def Giannakidou2002.Row.ofDatum (ex : Datum) : Option Row

Equations

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

def Giannakidou2002.rows : List Row

Equations

• Giannakidou2002.rows = List.filterMap Giannakidou2002.Row.ofDatum Giannakidou2002.Examples.all

theorem Giannakidou2002.rows_predicted (r : Row) : r ∈ rows → (r.acceptable = true ↔ Predicted r)

Every judgment on the UNTIL sentences follows from the connective's fragment entry, the homogeneity of the main clause and the licensing of the polarity item.

inductive Giannakidou2002.Diagnostic : Type

A Diagnostic is one of the stativity diagnostics of the fifth section.

• howLong : Diagnostic
• while : Diagnostic
• forAdverbial : Diagnostic
• imperative : Diagnostic

@[instance_reducible]

instance Giannakidou2002.instDecidableEqDiagnostic : DecidableEq Diagnostic

Equations

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

@[instance_reducible]

instance Giannakidou2002.instReprDiagnostic : Repr Diagnostic

Equations

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

def Giannakidou2002.instReprDiagnostic.repr : Diagnostic → ℕ → Std.Format

Equations

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

structure Giannakidou2002.DiagnosticRow : Type

• diagnostic : Diagnostic
• aspect : AspectForm
• eventuality : Eventuality
• licenser : Licenser
• acceptable : Bool

def Giannakidou2002.instDecidableEqDiagnosticRow.decEq (x✝ x✝¹ : DiagnosticRow) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Giannakidou2002.instDecidableEqDiagnosticRow : DecidableEq DiagnosticRow

Equations

• Giannakidou2002.instDecidableEqDiagnosticRow = Giannakidou2002.instDecidableEqDiagnosticRow.decEq

def Giannakidou2002.instReprDiagnosticRow.repr : DiagnosticRow → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Giannakidou2002.instReprDiagnosticRow : Repr DiagnosticRow

Equations

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

def Giannakidou2002.DiagnosticRow.ofDatum (ex : Datum) : Option DiagnosticRow

Equations

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

def Giannakidou2002.diagnostics : List DiagnosticRow

Equations

• Giannakidou2002.diagnostics = List.filterMap Giannakidou2002.DiagnosticRow.ofDatum Giannakidou2002.Examples.all

theorem Giannakidou2002.diagnostics_predicted (r : DiagnosticRow) : r ∈ diagnostics → (r.acceptable = true ↔ (r.diagnostic = Diagnostic.imperative → ¬Homog r.aspect r.eventuality) ∧ (r.diagnostic ≠ Diagnostic.imperative → Homog r.aspect r.eventuality))

The stative diagnostics accept a homogeneous clause and the imperative rejects one, with negation playing no role, so negation is no stativizer.