[Wur14]: Tense and aspect in English infinitives

[Wur14]

Wurmbrand (Linguistic Inquiry 45(3), 2014) classifies English infinitival complements into three types based on tense-aspect behavior:

1. Future irrealis (decide, want, plan, hope): no independent tense; future orientation comes from a woll-like operator selected by the matrix verb. Example: "Leo decided to read a book" — reading is future of deciding.
2. Propositional (believe, claim): NOW-anchored tense. The embedded event is simultaneous with the matrix attitude. Example: "Leo believes Julia to be a princess" — princess-status at believing time.
3. Restructuring (try, begin): dependent on matrix tense; embedded event in the same temporal domain as the matrix.

Empirical anchors

• (1a) "Leo decided to read a book." — future irrealis
• (1b) "Leo believes Julia to be a princess." — propositional
• (2a) "Leo decided to bring the toys tomorrow." — future-irrealis + episodic adverbial OK
• (2b) "*Leo believed Julia to bring the toys right then." — propositional
  • episodic adverbial blocks bare infinitive (needs progressive)

Lean encoding

The InfinitivalTenseClass type is substrate (Minimalist.ExtendedProjection), shared with Studies/Ostrove2026. Wurmbrand's apparatus — temporal orientation, woll decomposition, episodic predictions, and the verb classification table — is study-local below; the empirical examples are generated from Data/Examples/Wurmbrand2014.json.

Temporal orientation by class

inductive Wurmbrand2014.TemporalOrientation : Type

The temporal orientation of a complement relative to the matrix event.

• futureOriented : TemporalOrientation

  Complement event after the matrix event.

• simultaneous : TemporalOrientation

  Complement event simultaneous with the matrix event.

• dependent : TemporalOrientation

  Complement event's temporal location depends entirely on the matrix.

@[implicit_reducible]

instance Wurmbrand2014.instDecidableEqTemporalOrientation : DecidableEq TemporalOrientation

Equations

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

def Wurmbrand2014.instReprTemporalOrientation.repr : TemporalOrientation → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Wurmbrand2014.instReprTemporalOrientation : Repr TemporalOrientation

Equations

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

def Wurmbrand2014.classOrientation : Minimalist.InfinitivalTenseClass → TemporalOrientation

Each infinitival class's predicted temporal orientation.

Equations

• Wurmbrand2014.classOrientation Minimalist.InfinitivalTenseClass.futureIrrealis = Wurmbrand2014.TemporalOrientation.futureOriented
• Wurmbrand2014.classOrientation Minimalist.InfinitivalTenseClass.propositional = Wurmbrand2014.TemporalOrientation.simultaneous
• Wurmbrand2014.classOrientation Minimalist.InfinitivalTenseClass.restructuring = Wurmbrand2014.TemporalOrientation.dependent

Woll decomposition

structure Wurmbrand2014.WollDecomposition : Type

will = PRES + woll; would = PAST + woll (§2). The tense component undergoes SOT; woll supplies the future orientation.

• tense : Finset Ordering

  The tense component (a Finset Ordering comparison cell).

• hasWoll : Bool

  Whether woll is present (future orientation).

def Wurmbrand2014.instDecidableEqWollDecomposition.decEq (x✝ x✝¹ : WollDecomposition) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Wurmbrand2014.instDecidableEqWollDecomposition : DecidableEq WollDecomposition

Equations

• Wurmbrand2014.instDecidableEqWollDecomposition = Wurmbrand2014.instDecidableEqWollDecomposition.decEq

def Wurmbrand2014.will_ : WollDecomposition

will = present + woll.

Equations

• Wurmbrand2014.will_ = { tense := Tense.present, hasWoll := true }

def Wurmbrand2014.would_ : WollDecomposition

would = past + woll.

Equations

• Wurmbrand2014.would_ = { tense := Tense.past, hasWoll := true }

def Wurmbrand2014.plainPresent : WollDecomposition

Plain present (no woll).

Equations

• Wurmbrand2014.plainPresent = { tense := Tense.present, hasWoll := false }

theorem Wurmbrand2014.will_would_share_woll : will_.hasWoll = would_.hasWoll

will and would share the woll component.

theorem Wurmbrand2014.will_would_tense_differs : will_.tense ≠ would_.tense

will and would differ only in tense.

def Wurmbrand2014.classHasWoll : Minimalist.InfinitivalTenseClass → Bool

Only future-irrealis infinitives contain the future modal woll.

Equations

• Wurmbrand2014.classHasWoll Minimalist.InfinitivalTenseClass.futureIrrealis = true
• Wurmbrand2014.classHasWoll Minimalist.InfinitivalTenseClass.propositional = false
• Wurmbrand2014.classHasWoll Minimalist.InfinitivalTenseClass.restructuring = false

theorem Wurmbrand2014.futureIrrealis_has_woll : classHasWoll Minimalist.InfinitivalTenseClass.futureIrrealis = true

theorem Wurmbrand2014.propositional_no_woll : classHasWoll Minimalist.InfinitivalTenseClass.propositional = false

theorem Wurmbrand2014.restructuring_no_woll : classHasWoll Minimalist.InfinitivalTenseClass.restructuring = false

Episodic interpretation predictions (Table 3)

inductive Wurmbrand2014.EpisodicAvailability : Type

Availability of bare (nonprogressive) episodic interpretations (§4).

• possible : EpisodicAvailability

  Possible: woll supplies an unrestricted future reference time.

• impossible : EpisodicAvailability

  Impossible: the attitude holder's NOW is too short for perfective.

• matrixDependent : EpisodicAvailability

  Matrix-dependent: possible iff the matrix reference time is large enough.

@[implicit_reducible]

instance Wurmbrand2014.instDecidableEqEpisodicAvailability : DecidableEq EpisodicAvailability

Equations

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

@[implicit_reducible]

instance Wurmbrand2014.instReprEpisodicAvailability : Repr EpisodicAvailability

Equations

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

def Wurmbrand2014.instReprEpisodicAvailability.repr : EpisodicAvailability → ℕ → Std.Format

Equations

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

def Wurmbrand2014.classEpisodicPrediction : Minimalist.InfinitivalTenseClass → EpisodicAvailability

Each class's episodic prediction.

Equations

• Wurmbrand2014.classEpisodicPrediction Minimalist.InfinitivalTenseClass.futureIrrealis = Wurmbrand2014.EpisodicAvailability.possible
• Wurmbrand2014.classEpisodicPrediction Minimalist.InfinitivalTenseClass.propositional = Wurmbrand2014.EpisodicAvailability.impossible
• Wurmbrand2014.classEpisodicPrediction Minimalist.InfinitivalTenseClass.restructuring = Wurmbrand2014.EpisodicAvailability.matrixDependent

theorem Wurmbrand2014.propositional_no_episodic : classEpisodicPrediction Minimalist.InfinitivalTenseClass.propositional = EpisodicAvailability.impossible

theorem Wurmbrand2014.restructuring_episodic_matrix_dependent : classEpisodicPrediction Minimalist.InfinitivalTenseClass.restructuring = EpisodicAvailability.matrixDependent

theorem Wurmbrand2014.futureIrrealis_episodic_possible : classEpisodicPrediction Minimalist.InfinitivalTenseClass.futureIrrealis = EpisodicAvailability.possible

Verb classification

structure Wurmbrand2014.InfinitivalVerb : Type

A verb classified by its infinitival tense class (Table 4).

• lemma_ : String

  The verb lemma.

• tenseClass : Minimalist.InfinitivalTenseClass

  Its tense class.

def Wurmbrand2014.instReprInfinitivalVerb.repr : InfinitivalVerb → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Wurmbrand2014.instReprInfinitivalVerb : Repr InfinitivalVerb

Equations

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

def Wurmbrand2014.want : InfinitivalVerb

Equations

• Wurmbrand2014.want = { lemma_ := "want", tenseClass := Minimalist.InfinitivalTenseClass.futureIrrealis }

def Wurmbrand2014.decide : InfinitivalVerb

Equations

• Wurmbrand2014.decide = { lemma_ := "decide", tenseClass := Minimalist.InfinitivalTenseClass.futureIrrealis }

def Wurmbrand2014.plan : InfinitivalVerb

Equations

• Wurmbrand2014.plan = { lemma_ := "plan", tenseClass := Minimalist.InfinitivalTenseClass.futureIrrealis }

def Wurmbrand2014.promise : InfinitivalVerb

Equations

• Wurmbrand2014.promise = { lemma_ := "promise", tenseClass := Minimalist.InfinitivalTenseClass.futureIrrealis }

def Wurmbrand2014.believe : InfinitivalVerb

Equations

• Wurmbrand2014.believe = { lemma_ := "believe", tenseClass := Minimalist.InfinitivalTenseClass.propositional }

def Wurmbrand2014.claim : InfinitivalVerb

Equations

• Wurmbrand2014.claim = { lemma_ := "claim", tenseClass := Minimalist.InfinitivalTenseClass.propositional }

def Wurmbrand2014.try_ : InfinitivalVerb

Equations

• Wurmbrand2014.try_ = { lemma_ := "try", tenseClass := Minimalist.InfinitivalTenseClass.restructuring }

def Wurmbrand2014.begin_ : InfinitivalVerb

Equations

• Wurmbrand2014.begin_ = { lemma_ := "begin", tenseClass := Minimalist.InfinitivalTenseClass.restructuring }

def Wurmbrand2014.manage : InfinitivalVerb

Equations

• Wurmbrand2014.manage = { lemma_ := "manage", tenseClass := Minimalist.InfinitivalTenseClass.restructuring }

structure Wurmbrand2014.AmbiguousVerb : Type

A verb ambiguous between two infinitival tense classes.

• lemma_ : String
• readings : List Minimalist.InfinitivalTenseClass

def Wurmbrand2014.instReprAmbiguousVerb.repr : AmbiguousVerb → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Wurmbrand2014.instReprAmbiguousVerb : Repr AmbiguousVerb

Equations

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

def Wurmbrand2014.expect : AmbiguousVerb

expect is ambiguous between future-irrealis and propositional (§3, §4.3).

Equations

• Wurmbrand2014.expect = { lemma_ := "expect", readings := [Minimalist.InfinitivalTenseClass.futureIrrealis, Minimalist.InfinitivalTenseClass.propositional] }

def Wurmbrand2014.seem : AmbiguousVerb

seem is restructuring, but propositional with an experiencer (§4.4).

Equations

• Wurmbrand2014.seem = { lemma_ := "seem", readings := [Minimalist.InfinitivalTenseClass.restructuring, Minimalist.InfinitivalTenseClass.propositional] }

theorem Wurmbrand2014.expect_is_ambiguous : expect.readings.length > 1

theorem Wurmbrand2014.seem_is_ambiguous : seem.readings.length > 1

Per-class classification theorems

theorem Wurmbrand2014.wurmbrandClassifiesWant : want.tenseClass = Minimalist.InfinitivalTenseClass.futureIrrealis ∧ classOrientation Minimalist.InfinitivalTenseClass.futureIrrealis = TemporalOrientation.futureOriented

want is future-irrealis → future-oriented complement.

theorem Wurmbrand2014.wurmbrandClassifiesBelieve : believe.tenseClass = Minimalist.InfinitivalTenseClass.propositional ∧ classOrientation Minimalist.InfinitivalTenseClass.propositional = TemporalOrientation.simultaneous

believe is propositional → simultaneous complement.

theorem Wurmbrand2014.wurmbrandClassifiesTry : try_.tenseClass = Minimalist.InfinitivalTenseClass.restructuring ∧ classOrientation Minimalist.InfinitivalTenseClass.restructuring = TemporalOrientation.dependent

try is restructuring → dependent on matrix temporal domain.

Derivation theorems

theorem Wurmbrand2014.futureIrrealis_is_future_oriented : classOrientation Minimalist.InfinitivalTenseClass.futureIrrealis = TemporalOrientation.futureOriented

theorem Wurmbrand2014.propositional_now_anchored : classOrientation Minimalist.InfinitivalTenseClass.propositional = TemporalOrientation.simultaneous

theorem Wurmbrand2014.restructuring_dependent : classOrientation Minimalist.InfinitivalTenseClass.restructuring = TemporalOrientation.dependent

theorem Wurmbrand2014.propositional_uses_attitude_eval_time : classOrientation Minimalist.InfinitivalTenseClass.propositional = TemporalOrientation.simultaneous ∧ Tense.standardShift.shiftEvalTime { speechTime := 0, perspectiveTime := 0, referenceTime := 0, eventTime := 5 } = 5

Propositional NOW-anchoring connects to the attitude eval-time shift: standardShift sets the embedded eval time to the matrix event time.

theorem Wurmbrand2014.restructuring_minimal_structure : classOrientation Minimalist.InfinitivalTenseClass.restructuring = TemporalOrientation.dependent ∧ Minimalist.InfinitivalTenseClass.restructuring.toComplementSize = Minimalist.ComplementSize.vP ∧ classHasWoll Minimalist.InfinitivalTenseClass.restructuring = false

Restructuring infinitives lack independent tense: dependent orientation, the smallest complement size (vP), and no woll.

theorem Wurmbrand2014.futureIrrealis_structural_future : classHasWoll Minimalist.InfinitivalTenseClass.futureIrrealis = true ∧ Minimalist.InfinitivalTenseClass.futureIrrealis.toComplementSize = Minimalist.ComplementSize.modP ∧ classOrientation Minimalist.InfinitivalTenseClass.futureIrrealis = TemporalOrientation.futureOriented

Future-oriented complements have woll and project a modal (wollP ≈ ModP).

theorem Wurmbrand2014.woll_iff_future (c : Minimalist.InfinitivalTenseClass) : classHasWoll c = true ↔ classOrientation c = TemporalOrientation.futureOriented

Woll presence correlates exactly with future orientation.

Complement-size hierarchy

Wurmbrand's theory-internal sizing is wollP > TP > vP/AspP. The substrate InfinitivalTenseClass.toComplementSize maps future-irrealis and propositional to the same fseq tier (ModP/TP), so the strict ordering is recorded here via a study-local rank.

def Wurmbrand2014.sizeRank : Minimalist.InfinitivalTenseClass → ℕ

Wurmbrand's complement-size rank: future-irrealis > propositional > restructuring.

Equations

• Wurmbrand2014.sizeRank Minimalist.InfinitivalTenseClass.futureIrrealis = 3
• Wurmbrand2014.sizeRank Minimalist.InfinitivalTenseClass.propositional = 2
• Wurmbrand2014.sizeRank Minimalist.InfinitivalTenseClass.restructuring = 1

theorem Wurmbrand2014.complement_size_hierarchy : sizeRank Minimalist.InfinitivalTenseClass.futureIrrealis > sizeRank Minimalist.InfinitivalTenseClass.propositional ∧ sizeRank Minimalist.InfinitivalTenseClass.propositional > sizeRank Minimalist.InfinitivalTenseClass.restructuring

theorem Wurmbrand2014.episodic_correlates_with_size : classEpisodicPrediction Minimalist.InfinitivalTenseClass.futureIrrealis = EpisodicAvailability.possible ∧ Minimalist.InfinitivalTenseClass.futureIrrealis.toComplementSize = Minimalist.ComplementSize.modP ∧ classEpisodicPrediction Minimalist.InfinitivalTenseClass.propositional = EpisodicAvailability.impossible ∧ Minimalist.InfinitivalTenseClass.propositional.toComplementSize = Minimalist.ComplementSize.tP ∧ classEpisodicPrediction Minimalist.InfinitivalTenseClass.restructuring = EpisodicAvailability.matrixDependent ∧ Minimalist.InfinitivalTenseClass.restructuring.toComplementSize = Minimalist.ComplementSize.vP

Episodic availability tracks complement size: complements with their own temporal elements allow episodic readings; smaller ones are matrix-dependent.