Kratzer (1998): More Structural Analogies between Pronouns and Tenses

Kratzer treats tenses as pronouns, after Partee. English has two indexical tenses, a present defined when the context provides an interval including the utterance time and a past defined when it provides one preceding it, and a zero tense with no presupposition that must be bound by the next tense up. A zero tense with a binder index abstracts over the time, so attitude complements denote properties of times, which derives Abusch's constraint from the verbs' selection. What looks like a tense may spell out a tense together with one of Klein's three aspects; since out of the blue only the present is defined and only the perfect places the event before the reference time, a form describes a past event out of the blue just in case it spells out present tense with perfect aspect. The paper's tables assign that combination to the English simple past and the German Perfekt and never to the Präteritum.

Main results

• AspectHead.isAnterior_iff: only the perfect is anterior.
• describesPastOutOfTheBlue_iff: describing a past event out of the blue is spelling out the present perfect.
• rows_outOfTheBlue: the out-of-the-blue judgments of the paper's examples.

Implementation notes

An out-of-the-blue context is the temporal assignment sending every variable to the utterance time, so a tense is defined there iff its cell admits coincidence, by the presupposition of Tense.pronoun. The aspect operators take a reference interval; a tense supplies a point, embedded as NonemptyInterval.pure. The aspects are instances of the library's Aspect.ofRel. The imperfective and the perfective are the library's Aspect.UNBOUNDED and Aspect.PRFV, and the perfect, with strict precedence, is stronger than the perfect viewpoint of Aspect.ViewpointType, which admits an event abutting the reference time (perfect_viewpointType). The zero-pronoun typology of §2–§3 and the locality argument from switch reference are prose. The French table is not entered, since the library has no French tense forms.

References

• [Kra98a]
• [Par73]
• [Abu97]
• [Ogi89]
• [Ogi96]
• [HK98]
• [Kle94]

The tenses (§4–§5)

@[reducible, inline]

abbrev Kratzer1998.tense {W : Type u_1} {T : Type u_2} [LT T] (C : Finset Ordering) (n : ℕ) : Reference.Nominal (Assignment T) W T

The indexical tense with cell C is the variable n presupposing that its reference stands to the utterance time, the time of the index 0, in a position of C. The present and the past are the tenses of the cells present and past.

Equations

• Kratzer1998.tense C n = Tense.pronoun C n 0

@[reducible, inline]

abbrev Kratzer1998.zeroTense {W : Type u_1} {T : Type u_2} [LT T] (n : ℕ) : Reference.Nominal (Assignment T) W T

The zero tense is a variable with no presupposition, bound by the next tense up.

Equations

• Kratzer1998.zeroTense n = Tense.pronoun ⊤ n 0

def Kratzer1998.outOfTheBlue {T : Type u_2} (t₀ : T) : Assignment T

An out-of-the-blue context has no salient time but the utterance time, so every temporal variable resolves to it.

Equations

• Kratzer1998.outOfTheBlue t₀ = Function.const ℕ t₀

theorem Kratzer1998.tense_outOfTheBlue_iff {W : Type u_1} {T : Type u_2} [LinearOrder T] (C : Finset Ordering) (n : ℕ) (t₀ : T) (w : W) : (tense C n).presup (outOfTheBlue t₀) w ↔ Ordering.eq ∈ C

Out of the blue a tense is defined iff its cell admits coincidence with the utterance time, as the present does and the past does not.

theorem Kratzer1998.zeroTense_presup {W : Type u_1} {T : Type u_2} [LinearOrder T] (n : ℕ) (g : Assignment T) (w : W) : (zeroTense n).presup g w

The zero tense has no presupposition.

theorem Kratzer1998.zeroTense_abstract {W : Type u_1} {T : Type u_2} [LT T] (n : ℕ) (g : Assignment T) (t : T) (w : W) : HeimKratzer.lambdaAbsG n (fun (g : Assignment T) => (zeroTense n).selector g w) g t = some t

A zero tense with a binder index makes its clause a property of times, (31). Whatever the assignment, the tense under the abstract denotes the time the abstract is applied to.

theorem Kratzer1998.tense_not_abstracted {W : Type u_1} {T : Type u_2} [LT T] (C : Finset Ordering) {m n : ℕ} (hn : n ≠ m) (g : Assignment T) (t : T) (w : W) : HeimKratzer.lambdaAbsG m (fun (g : Assignment T) => (tense C n).selector g w) g t = some (g n)

An indexical tense cannot be abstracted over by another index. The binder leaves the tense with its own reference, which is why an attitude verb forces a zero tense.

The aspects (§6–§7)

inductive Kratzer1998.AspectHead : Type

An aspect head is imperfective, perfective or perfect. These are the rows of the closing tables.

• imperfective : AspectHead
• perfective : AspectHead
• perfect : AspectHead

@[instance_reducible]

instance Kratzer1998.instDecidableEqAspectHead : DecidableEq AspectHead

Equations

• Kratzer1998.instDecidableEqAspectHead x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Kratzer1998.instReprAspectHead.repr : AspectHead → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Kratzer1998.instReprAspectHead : Repr AspectHead

Equations

• Kratzer1998.instReprAspectHead = { reprPrec := Kratzer1998.instReprAspectHead.repr }

@[instance_reducible]

instance Kratzer1998.instFintypeAspectHead : Fintype AspectHead

Equations

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

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

The operator of (38) turns a property of times into the property of eventualities that holds of e, at any world, iff the property of times holds of the running time of e at every world.

Equations

• Kratzer1998.star P x✝ e = ∀ (w' : W), Event.τ e ∈ P w'

theorem Kratzer1998.star_congr {T : Type u_1} {W : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (P : W → Set (NonemptyInterval T)) (e : E) (w w' : W) : star P w e ↔ star P w' e

The temporal de re is semantically forced, since star P does not depend on the evaluation world.

def Kratzer1998.AspectHead.rel {T : Type u_1} [LinearOrder T] : AspectHead → NonemptyInterval T → NonemptyInterval T → Prop

a.rel r s is the relation of the aspect a between the reference time r and the event time s. The imperfective includes the reference time in the event time, the perfective includes the event time in the reference time, and the perfect has the event over by the reference time.

Equations

• Kratzer1998.AspectHead.imperfective.rel x✝¹ x✝ = (x✝¹ ≤ x✝)
• Kratzer1998.AspectHead.perfective.rel x✝¹ x✝ = (x✝ ≤ x✝¹)
• Kratzer1998.AspectHead.perfect.rel x✝¹ x✝ = x✝.Precedes x✝¹

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

An aspect maps a property of events to the property of times that stand in the aspect's relation to the time of some such event.

Equations

• a.denote P = Aspect.ofRel a.rel P

theorem Kratzer1998.denote_imperfective {T : Type u_1} {W : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (P : W → E → Prop) : AspectHead.imperfective.denote P = Aspect.UNBOUNDED P

theorem Kratzer1998.denote_perfective {T : Type u_1} {W : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (P : W → E → Prop) : AspectHead.perfective.denote P = Aspect.PRFV P

theorem Kratzer1998.perfect_viewpointType {T : Type u_1} {W : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {P : W → E → Prop} {w : W} {r : NonemptyInterval T} : r ∈ AspectHead.perfect.denote P w → r ∈ Aspect.ViewpointType.perfect.denote P w

The perfect entails the perfect viewpoint of the library, whose relation also admits an event that ends exactly when the reference time begins.

def Kratzer1998.AspectHead.IsAnterior (T : Type u_1) [LinearOrder T] (a : AspectHead) : Prop

An anterior aspect places the event time before the reference time.

Equations

• Kratzer1998.AspectHead.IsAnterior T a = ∀ (r s : NonemptyInterval T), a.rel r s → s.Precedes r

theorem Kratzer1998.AspectHead.isAnterior_iff {T : Type u_1} [LinearOrder T] [Nonempty T] (a : AspectHead) : IsAnterior T a ↔ a = perfect

Only the perfect is anterior, since the imperfective and the perfective relate a time to itself.

theorem Kratzer1998.AspectHead.IsAnterior.precedes {T : Type u_1} {W : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {a : AspectHead} (ha : IsAnterior T a) {P : W → E → Prop} {w : W} {r : NonemptyInterval T} (h : r ∈ a.denote P w) : ∃ (e : E), (Event.τ e).Precedes r ∧ P w e

An anterior aspect describes an event that is over by the reference time.

def Kratzer1998.denote {T : Type u_1} {W : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (C : Finset Ordering) (a : AspectHead) (n : ℕ) (P : W → E → Prop) (g : Assignment T) (w : W) : Prop

Tense C on the variable n with aspect a is true of an event property when the tense is defined and the aspect holds of the property at the tense's reference.

Equations

• Kratzer1998.denote C a n P g w = ((Kratzer1998.tense C n).presup g w ∧ NonemptyInterval.pure (HeimKratzer.interpPronoun n g) ∈ a.denote P w)

theorem Kratzer1998.denote_outOfTheBlue_iff {T : Type u_1} {W : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (C : Finset Ordering) (a : AspectHead) (n : ℕ) (P : W → E → Prop) (t₀ : T) (w : W) : denote C a n P (outOfTheBlue t₀) w ↔ Ordering.eq ∈ C ∧ NonemptyInterval.pure t₀ ∈ a.denote P w

Out of the blue a tense with an aspect is true iff the tense admits coincidence with the utterance time and the aspect holds there.

theorem Kratzer1998.denote_present_perfect_outOfTheBlue_iff {T : Type u_1} {W : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (n : ℕ) (P : W → E → Prop) (t₀ : T) (w : W) : denote (Semantics.Denotes.denote Tense.present) AspectHead.perfect n P (outOfTheBlue t₀) w ↔ ∃ (e : E), (Event.τ e).toProd.2 < t₀ ∧ P w e

Present tense with perfect aspect describes an event over by the utterance time, so a past event can be described with no past tense.

What the tense forms spell out (§7)

structure Kratzer1998.Variety : Type

A variety of a language, as the closing tables describe it, is a table of the tense forms with the tenses and aspects they spell out.

• table : List (Tense.Form × Finset Ordering × AspectHead)

  The entries of the table.

def Kratzer1998.english : Variety

In English the progressive forms spell out the imperfective and the simple forms the perfective, and the simple past also spells out the perfect, of the present as of the past.

Equations

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

def Kratzer1998.standardGerman : Variety

In Standard German the synthetic forms spell out the imperfective and the perfective, and their perfects the perfect.

Equations

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

def Kratzer1998.southGerman : Variety

In South German, with the simple past gone, the present perfect also spells out the past with the imperfective and the perfective, and the double perfect the past with the perfect.

Equations

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

theorem Kratzer1998.table_forms : (∀ x ∈ english.table, x.1 ∈ English.Tense.tenseForms) ∧ (∀ x ∈ standardGerman.table, x.1 ∈ German.tenseForms) ∧ ∀ x ∈ southGerman.table, x.1 ∈ German.southernTenseForms

The tables use the tense forms of the Fragments.

def Kratzer1998.Variety.SpellsOut (v : Variety) (f : Tense.Form) (C : Finset Ordering) (a : AspectHead) : Prop

The form f spells out tense C with aspect a.

Equations

• v.SpellsOut f C a = ((f, C, a) ∈ v.table)

@[instance_reducible]

instance Kratzer1998.Variety.instDecidableSpellsOut (v : Variety) (f : Tense.Form) (C : Finset Ordering) (a : AspectHead) : Decidable (v.SpellsOut f C a)

Equations

• v.instDecidableSpellsOut f C a = { decide := decide (List.elem (f, C, a) v.table = true), reflects_decide := ⋯ }

def Kratzer1998.Variety.DescribesPastOutOfTheBlue (v : Variety) (T : Type u_1) [LinearOrder T] (f : Tense.Form) : Prop

A form can describe a past event out of the blue when it spells out a tense defined out of the blue with an anterior aspect.

Equations

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

theorem Kratzer1998.Variety.describesPastOutOfTheBlue_iff (v : Variety) (T : Type u_1) [LinearOrder T] [Nonempty T] (f : Tense.Form) : v.DescribesPastOutOfTheBlue T f ↔ ∃ x ∈ v.table, x.1 = f ∧ Ordering.eq ∈ x.2.1 ∧ x.2.2 = AspectHead.perfect

A form can describe a past event out of the blue iff it spells out, with the perfect, a tense that admits coincidence with the utterance time.

@[instance_reducible]

instance Kratzer1998.Variety.instDecidablePredFormDescribesPastOutOfTheBlueOfNonempty (v : Variety) (T : Type u_1) [LinearOrder T] [Nonempty T] : DecidablePred (v.DescribesPastOutOfTheBlue T)

Equations

• v.instDecidablePredFormDescribesPastOutOfTheBlueOfNonempty T f = decidable_of_iff (∃ x ∈ v.table, x.1 = f ∧ Ordering.eq ∈ x.2.1 ∧ x.2.2 = Kratzer1998.AspectHead.perfect) ⋯

def Kratzer1998.Variety.IsTenseFaithful (v : Variety) : Prop

A table is tense-faithful when a form spells out only the tense its finite verb is inflected for.

Equations

• v.IsTenseFaithful = ∀ x ∈ v.table, x.2.1 = Semantics.Denotes.denote x.1.finite

def Kratzer1998.Variety.IsPerfectCompositional (v : Variety) : Prop

A table is perfect-compositional when the forms that spell out the perfect of a tense are the perfects of the forms that spell out that tense with another aspect.

Equations

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

@[instance_reducible]

instance Kratzer1998.Variety.instDecidableIsTenseFaithful (v : Variety) : Decidable v.IsTenseFaithful

Equations

• v.instDecidableIsTenseFaithful = id inferInstance

@[instance_reducible]

instance Kratzer1998.Variety.instDecidableIsPerfectCompositional (v : Variety) : Decidable v.IsPerfectCompositional

Equations

• v.instDecidableIsPerfectCompositional = id inferInstance

theorem Kratzer1998.standardGerman_transparent : standardGerman.IsTenseFaithful ∧ standardGerman.IsPerfectCompositional

The Standard German table can be read off the make-up of the forms.

theorem Kratzer1998.southGerman_transparent : ¬southGerman.IsTenseFaithful ∧ southGerman.IsPerfectCompositional

South German builds its perfects compositionally, the double perfect on the present perfect as a past, but its present perfect, a present inflection, spells out the past.

theorem Kratzer1998.english_transparent : ¬english.IsTenseFaithful ∧ ¬english.IsPerfectCompositional

English is neither, since the simple past, a past inflection that is the perfect of no form, spells out the present with the perfect.

theorem Kratzer1998.backwardShifted : english.SpellsOut Tense.Form.simplePast (Semantics.Denotes.denote Tense.past) AspectHead.perfect ∧ ¬standardGerman.SpellsOut Tense.Form.simplePast (Semantics.Denotes.denote Tense.past) AspectHead.perfect ∧ standardGerman.SpellsOut Tense.Form.pastPerfect (Semantics.Denotes.denote Tense.past) AspectHead.perfect

The backward-shifted reading of a past under a past, (42), is the past with the perfect, which the English simple past spells out and the German one does not, so that Standard German needs the past perfect.

def Kratzer1998.varieties : List (String × Variety)

The language codes of the example rows name these varieties.

Equations

• Kratzer1998.varieties = [("stan1293", Kratzer1998.english), ("stan1295", Kratzer1998.standardGerman)]

def Kratzer1998.forms : List (String × Tense.Form)

The rows name these tense forms.

Equations

• Kratzer1998.forms = [("simple past", Tense.Form.simplePast), ("Präteritum", Tense.Form.simplePast), ("Perfekt", Tense.Form.presentPerfect)]

theorem Kratzer1998.rows_outOfTheBlue (r : Datum) : r ∈ Examples.all → r.feature? "context" = some "out of the blue" → ∃ v ∈ List.lookup r.language varieties, ∃ f ∈ r.parse? "form" forms, r.judgment = Judgment.acceptable ↔ v.DescribesPastOutOfTheBlue ℤ f

In (40) a form is acceptable out of the blue iff it can describe a past event there. The English simple past and the German present perfect can, and the German simple past cannot.

theorem Kratzer1998.rows_realize (r : Datum) : r ∈ [Examples.ex40b, Examples.ex40c] → ∀ f ∈ German.tenseForms, (∃ ws ∈ German.Verbs.bauen.principalParts.tenseForm f, ws ⊆ r.surfaceTokens) ↔ r.parse? "form" forms = some f

The German rows of (40) are in the form they are labelled with, since of the tense forms of bauen exactly the labelled one has all its words in the row.