Wurmbrand (2014): Tense and Aspect in English Infinitives

This file formalizes [Wur14]'s account of the temporal composition of English infinitival complements. Three classes are distinguished by whether a bare, nonprogressive verb phrase can be episodic: future infinitives allow it, propositional attitude infinitives never do, and tenseless simultaneous infinitives allow it depending on the matrix tense (InfinitivalTenseClass). The distribution is derived from viewpoint aspect. Perfective aspect includes the event time in the reference time and imperfective the reverse (Perfective), and an episodic eventive predicate occupies an extended interval, so perfective fails whenever the reference time is an instant (not_perfective_of_isPoint). Each class fixes the embedded reference time (ReferenceTime): the future modal woll shifts it to an unrestricted interval after the evaluation time, a propositional attitude imposes the holder's NOW, an instant, and a tenseless simultaneous infinitive inherits the matrix reference time, an instant under present tense and an extended interval under past. The three rows of the paper's table follow (Episodic), and a verb ambiguous between classes, like seem, is episodic exactly when one of its classes is (Verb.Episodic).

Future infinitives are tenseless: finite will is present tense plus woll and would is past plus woll (Composition), so finite future is absolute while infinitival future is relative to the matrix event (infinitival_relative), and infinitives are invisible to the sequence-of-tense rule, whose local tense feature skips them (localTense): a past under an infinitive under past deletes, a past under will does not, and a silent would in the infinitive would wrongly license deletion under a will matrix (silent_would_wrong).

Implementation notes

Times are the nonempty intervals of a linear order; an instant is an interval whose endpoints coincide. The evaluation time of woll and the attitude holder's NOW are one instant parameter, and adverbials that restrict a reference time to an instant fall under the same lemma as the NOW. The obligatory deletion of would's past is taken as the paper does, as a lexical requirement.

References

• [Wur14]
• [Ogi96]
• [Abu88]
• [Wur01]
• [Lan00a]

inductive Wurmbrand2014.InfinitivalTenseClass : Type

The three classes of infinitival complement by tense behaviour. Future irrealis infinitives, decide, want and plan, are tenseless with woll and future-oriented; propositional infinitives, believe and claim, are anchored to the attitude holder's now; restructuring infinitives, try, begin and seem, have no attitude holder and take the matrix reference time.

• futureIrrealis : InfinitivalTenseClass
• propositional : InfinitivalTenseClass
• restructuring : InfinitivalTenseClass

@[instance_reducible]

instance Wurmbrand2014.instDecidableEqInfinitivalTenseClass : DecidableEq InfinitivalTenseClass

Equations

• Wurmbrand2014.instDecidableEqInfinitivalTenseClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Wurmbrand2014.instReprInfinitivalTenseClass.repr : InfinitivalTenseClass → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Wurmbrand2014.instReprInfinitivalTenseClass : Repr InfinitivalTenseClass

Equations

• Wurmbrand2014.instReprInfinitivalTenseClass = { reprPrec := Wurmbrand2014.instReprInfinitivalTenseClass.repr }

@[instance_reducible]

instance Wurmbrand2014.instInhabitedInfinitivalTenseClass : Inhabited InfinitivalTenseClass

Equations

• Wurmbrand2014.instInhabitedInfinitivalTenseClass = { default := Wurmbrand2014.instInhabitedInfinitivalTenseClass.default }

def Wurmbrand2014.InfinitivalTenseClass.complementSize : InfinitivalTenseClass → Minimalist.ComplementSize

The structural size of each class, the modal layer of woll for a future irrealis infinitive, a TP for a propositional one and a bare vP for a restructuring one, the modal and tense layers sharing a level of the functional sequence.

Equations

• Wurmbrand2014.InfinitivalTenseClass.futureIrrealis.complementSize = Minimalist.ComplementSize.modP
• Wurmbrand2014.InfinitivalTenseClass.propositional.complementSize = Minimalist.ComplementSize.tP
• Wurmbrand2014.InfinitivalTenseClass.restructuring.complementSize = Minimalist.ComplementSize.vP

Viewpoint aspect

def Wurmbrand2014.Perfective {T : Type u_1} [LinearOrder T] (e r : NonemptyInterval T) : Prop

Perfective aspect includes the event time in the reference time.

Equations

• Wurmbrand2014.Perfective e r = (e ≤ r)

def Wurmbrand2014.Imperfective {T : Type u_1} [LinearOrder T] (e r : NonemptyInterval T) : Prop

Imperfective aspect includes the reference time in the event time.

Equations

• Wurmbrand2014.Imperfective e r = (r ≤ e)

theorem Wurmbrand2014.not_perfective_of_isPoint {T : Type u_1} [LinearOrder T] {e r : NonemptyInterval T} (he : ¬e.IsPoint) (hr : r.IsPoint) : ¬Perfective e r

An extended event time cannot be included in an instant: perfective aspect fails at a point reference time, the present, an attitude holder's NOW, or a reference time an adverbial restricts to an instant.

theorem Wurmbrand2014.imperfective_pure_of_mem {T : Type u_1} [LinearOrder T] {e : NonemptyInterval T} {t : T} (h : t ∈ e) : Imperfective e (NonemptyInterval.pure t)

Imperfective aspect, the progressive, is available at any instant within the event.

The reference time of an infinitive

def Wurmbrand2014.ReferenceTime {T : Type u_1} [LinearOrder T] (matrixR : NonemptyInterval T) (now : T) : InfinitivalTenseClass → NonemptyInterval T → Prop

The reference time each class assigns the embedded aspect, given the matrix reference time and the evaluation instant: after woll, any interval after the evaluation time; under a propositional attitude, the holder's NOW; in a tenseless simultaneous infinitive, the matrix reference time.

Equations

• Wurmbrand2014.ReferenceTime matrixR now Wurmbrand2014.InfinitivalTenseClass.futureIrrealis x✝ = (now < x✝.toProd.1)
• Wurmbrand2014.ReferenceTime matrixR now Wurmbrand2014.InfinitivalTenseClass.propositional x✝ = (x✝ = NonemptyInterval.pure now)
• Wurmbrand2014.ReferenceTime matrixR now Wurmbrand2014.InfinitivalTenseClass.restructuring x✝ = (x✝ = matrixR)

def Wurmbrand2014.Episodic {T : Type u_1} [LinearOrder T] (matrixR : NonemptyInterval T) (now : T) (c : InfinitivalTenseClass) : Prop

A bare episodic verb phrase is available when some reference time of the class includes an extended event time.

Equations

• Wurmbrand2014.Episodic matrixR now c = ∃ (r : NonemptyInterval T), Wurmbrand2014.ReferenceTime matrixR now c r ∧ ∃ (e : NonemptyInterval T), ¬e.IsPoint ∧ Wurmbrand2014.Perfective e r

theorem Wurmbrand2014.episodic_futureIrrealis {T : Type u_1} [LinearOrder T] (matrixR : NonemptyInterval T) (now : T) [NoMaxOrder T] : Episodic matrixR now InfinitivalTenseClass.futureIrrealis

A future infinitive always has an episodic reading: woll supplies an unrestricted interval.

theorem Wurmbrand2014.not_episodic_propositional {T : Type u_1} [LinearOrder T] (matrixR : NonemptyInterval T) (now : T) : ¬Episodic matrixR now InfinitivalTenseClass.propositional

A propositional attitude infinitive never has one: the holder's NOW is an instant.

theorem Wurmbrand2014.episodic_restructuring_iff {T : Type u_1} [LinearOrder T] (matrixR : NonemptyInterval T) (now : T) : Episodic matrixR now InfinitivalTenseClass.restructuring ↔ ¬matrixR.IsPoint

A tenseless simultaneous infinitive has one exactly when the matrix reference time is extended: under past tense, but not under present, nor under an adverbial restricting it to an instant.

Verbs

inductive Wurmbrand2014.Verb : Type

The infinitive-taking verbs of the paper's table.

• decide : Verb
• want : Verb
• promise : Verb
• expect : Verb
• claim : Verb
• believe : Verb
• try_ : Verb
• begin_ : Verb
• manage : Verb
• seem : Verb

@[instance_reducible]

instance Wurmbrand2014.instDecidableEqVerb : DecidableEq Verb

Equations

• Wurmbrand2014.instDecidableEqVerb x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Wurmbrand2014.instReprVerb.repr : Verb → ℕ → Std.Format

Equations

• Wurmbrand2014.instReprVerb.repr Wurmbrand2014.Verb.decide prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Wurmbrand2014.Verb.decide")).group prec✝
• Wurmbrand2014.instReprVerb.repr Wurmbrand2014.Verb.want prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Wurmbrand2014.Verb.want")).group prec✝
• Wurmbrand2014.instReprVerb.repr Wurmbrand2014.Verb.promise prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Wurmbrand2014.Verb.promise")).group prec✝
• Wurmbrand2014.instReprVerb.repr Wurmbrand2014.Verb.expect prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Wurmbrand2014.Verb.expect")).group prec✝
• Wurmbrand2014.instReprVerb.repr Wurmbrand2014.Verb.claim prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Wurmbrand2014.Verb.claim")).group prec✝
• Wurmbrand2014.instReprVerb.repr Wurmbrand2014.Verb.believe prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Wurmbrand2014.Verb.believe")).group prec✝
• Wurmbrand2014.instReprVerb.repr Wurmbrand2014.Verb.try_ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Wurmbrand2014.Verb.try_")).group prec✝
• Wurmbrand2014.instReprVerb.repr Wurmbrand2014.Verb.begin_ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Wurmbrand2014.Verb.begin_")).group prec✝
• Wurmbrand2014.instReprVerb.repr Wurmbrand2014.Verb.manage prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Wurmbrand2014.Verb.manage")).group prec✝
• Wurmbrand2014.instReprVerb.repr Wurmbrand2014.Verb.seem prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Wurmbrand2014.Verb.seem")).group prec✝

@[instance_reducible]

instance Wurmbrand2014.instReprVerb : Repr Verb

Equations

• Wurmbrand2014.instReprVerb = { reprPrec := Wurmbrand2014.instReprVerb.repr }

def Wurmbrand2014.Verb.classes : Verb → List InfinitivalTenseClass

The classes a verb's infinitive may belong to. Expect is future or, as a belief, propositional; seem is tenseless simultaneous or, with an attitude holder, propositional.

Equations

• Wurmbrand2014.Verb.decide.classes = [Wurmbrand2014.InfinitivalTenseClass.futureIrrealis]
• Wurmbrand2014.Verb.want.classes = [Wurmbrand2014.InfinitivalTenseClass.futureIrrealis]
• Wurmbrand2014.Verb.promise.classes = [Wurmbrand2014.InfinitivalTenseClass.futureIrrealis]
• Wurmbrand2014.Verb.expect.classes = [Wurmbrand2014.InfinitivalTenseClass.futureIrrealis, Wurmbrand2014.InfinitivalTenseClass.propositional]
• Wurmbrand2014.Verb.claim.classes = [Wurmbrand2014.InfinitivalTenseClass.propositional]
• Wurmbrand2014.Verb.believe.classes = [Wurmbrand2014.InfinitivalTenseClass.propositional]
• Wurmbrand2014.Verb.try_.classes = [Wurmbrand2014.InfinitivalTenseClass.restructuring]
• Wurmbrand2014.Verb.begin_.classes = [Wurmbrand2014.InfinitivalTenseClass.restructuring]
• Wurmbrand2014.Verb.manage.classes = [Wurmbrand2014.InfinitivalTenseClass.restructuring]
• Wurmbrand2014.Verb.seem.classes = [Wurmbrand2014.InfinitivalTenseClass.restructuring, Wurmbrand2014.InfinitivalTenseClass.propositional]

def Wurmbrand2014.Verb.Episodic {T : Type u_1} [LinearOrder T] (matrixR : NonemptyInterval T) (now : T) (v : Verb) : Prop

A verb's infinitive has an episodic reading when one of its classes does.

Equations

• Wurmbrand2014.Verb.Episodic matrixR now v = ∃ c ∈ v.classes, Wurmbrand2014.Episodic matrixR now c

theorem Wurmbrand2014.believe_not_episodic {T : Type u_1} [LinearOrder T] (matrixR : NonemptyInterval T) (now : T) : ¬Verb.Episodic matrixR now Verb.believe

believe never allows a bare episodic complement.

theorem Wurmbrand2014.seem_episodic_iff {T : Type u_1} [LinearOrder T] (matrixR : NonemptyInterval T) (now : T) : Verb.Episodic matrixR now Verb.seem ↔ ¬matrixR.IsPoint

seem allows one exactly when the matrix reference time is extended: its propositional option adds nothing.

theorem Wurmbrand2014.decide_episodic {T : Type u_1} [LinearOrder T] (matrixR : NonemptyInterval T) (now : T) [NoMaxOrder T] : Verb.Episodic matrixR now Verb.decide

decide always allows one.

Temporal composition

structure Wurmbrand2014.Composition : Type

The temporal composition of a clause is an optional tense feature together with whether the future modal woll is present.

• tense : Option (Finset Ordering)
• woll : Bool

def Wurmbrand2014.instDecidableEqComposition.decEq (x✝ x✝¹ : Composition) : Decidable (x✝ = x✝¹)

Equations

• Wurmbrand2014.instDecidableEqComposition.decEq { tense := a, woll := a_1 } { tense := b, woll := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Wurmbrand2014.instDecidableEqComposition : DecidableEq Composition

Equations

• Wurmbrand2014.instDecidableEqComposition = Wurmbrand2014.instDecidableEqComposition.decEq

def Wurmbrand2014.will : Composition

Finite will is present tense plus woll.

Equations

• Wurmbrand2014.will = { tense := some (Semantics.Denotes.denote Tense.present), woll := true }

def Wurmbrand2014.would : Composition

Finite would is past tense plus woll.

Equations

• Wurmbrand2014.would = { tense := some (Semantics.Denotes.denote Tense.past), woll := true }

def Wurmbrand2014.infinitive (woll : Bool) : Composition

An infinitive has no tense, with or without woll.

Equations

• Wurmbrand2014.infinitive woll = { tense := none, woll := woll }

def Wurmbrand2014.composition : InfinitivalTenseClass → Composition

The composition of each class is tenseless, with woll in the future class only.

Equations

• Wurmbrand2014.composition Wurmbrand2014.InfinitivalTenseClass.futureIrrealis = Wurmbrand2014.infinitive true
• Wurmbrand2014.composition Wurmbrand2014.InfinitivalTenseClass.propositional = Wurmbrand2014.infinitive false
• Wurmbrand2014.composition Wurmbrand2014.InfinitivalTenseClass.restructuring = Wurmbrand2014.infinitive false

theorem Wurmbrand2014.woll_iff_modP (c : InfinitivalTenseClass) : (composition c).woll = true ↔ c.complementSize = Minimalist.ComplementSize.modP

woll projects the modal layer: a class has woll exactly when its complement is a ModP.

def Wurmbrand2014.Composition.Locates {T : Type u_1} [LinearOrder T] (c : Composition) (utterance eval e : T) : Prop

A composition with woll locates its event after the utterance time when present tense is present and after the evaluation time otherwise.

Equations

• c.Locates utterance eval e = (c.woll = true ∧ if c.tense = some (Semantics.Denotes.denote Tense.present) then utterance < e else eval < e)

theorem Wurmbrand2014.will_absolute {T : Type u_1} [LinearOrder T] {utterance eval e : T} (h : will.Locates utterance eval e) : utterance < e

Finite future is absolute: the event follows the utterance time.

theorem Wurmbrand2014.infinitival_relative {T : Type u_1} [LinearOrder T] [DenselyOrdered T] {utterance eval : T} (h : eval < utterance) : ∃ (e : T), (infinitive true).Locates utterance eval e ∧ e < utterance

Infinitival future is relative: the event may precede the utterance time so long as it follows the matrix evaluation time.

Sequence of tense

def Wurmbrand2014.localTense : List (Option (Finset Ordering)) → Option (Finset Ordering)

The local tense feature of an embedded tense is the nearest tense feature above it, infinitives contributing none.

Equations

• Wurmbrand2014.localTense [] = none
• Wurmbrand2014.localTense (some f :: tail) = some f
• Wurmbrand2014.localTense (none :: rest) = Wurmbrand2014.localTense rest

def Wurmbrand2014.sotApplies (above : List (Option (Finset Ordering))) (embedded : Finset Ordering) : Bool

Ogihara's rule lets an embedded tense delete when its local tense feature is the same feature.

Equations

• Wurmbrand2014.sotApplies above embedded = match Wurmbrand2014.localTense above with | some m => decide (m = embedded) | none => false

theorem Wurmbrand2014.sot_will_blocks : sotApplies [will.tense, some (Semantics.Denotes.denote Tense.past)] (Semantics.Denotes.denote Tense.past) = false

The present of will intervenes between two pasts, blocking deletion.

theorem Wurmbrand2014.sot_infinitive_transparent : sotApplies [(infinitive true).tense, some (Semantics.Denotes.denote Tense.past)] (Semantics.Denotes.denote Tense.past) = true

A tenseless infinitive does not intervene, so the lower past deletes.

theorem Wurmbrand2014.sot_would : sotApplies [would.tense, some (Semantics.Denotes.denote Tense.past)] (Semantics.Denotes.denote Tense.past) = true

The past of would licenses deletion below it.

theorem Wurmbrand2014.sot_will_infinitive : sotApplies [(infinitive true).tense, will.tense] (Semantics.Denotes.denote Tense.past) = false

Under a will matrix, a past below an infinitive finds no past above it.

theorem Wurmbrand2014.silent_would_wrong : sotApplies [would.tense, will.tense] (Semantics.Denotes.denote Tense.past) = true

A silent would in the infinitive would license deletion under a will matrix, contrary to the judgment.

def Wurmbrand2014.WouldLicensed (above : List (Option (Finset Ordering))) : Prop

would's past must delete: it is licensed only below a past.

Equations

• Wurmbrand2014.WouldLicensed above = (Wurmbrand2014.sotApplies above (Semantics.Denotes.denote Tense.past) = true)

@[instance_reducible]

instance Wurmbrand2014.instDecidablePredListOptionFinsetOrderingWouldLicensed : DecidablePred WouldLicensed

Equations

• Wurmbrand2014.instDecidablePredListOptionFinsetOrderingWouldLicensed x✝ = Wurmbrand2014.instDecidablePredListOptionFinsetOrderingWouldLicensed._aux_1 x✝

theorem Wurmbrand2014.would_licensing : ¬WouldLicensed [will.tense] ∧ WouldLicensed [some (Semantics.Denotes.denote Tense.past)]

Temporal would under will is out, under a past matrix in.