English Temporal Expressions Fragment

@cite{alstott-aravind-2026} @cite{heinamaki-1974} @cite{rett-2020} @cite{karttunen-1974} @cite{ogihara-steinert-threlkeld-2024}

Lexical entries for temporal expressions: subordinating connectives (before, after, while, until, when, since, till) and adverbial modifiers (within, at, by), unified under a single TemporalExprEntry type.

The connective/modifier distinction is captured by the ComplementType field (clausal vs nominal), but the semantic fields — order, licensesNPI, complementVeridical — are shared, enabling uniform pattern theorems across both categories. This matters because by has the same temporal-ordering semantics as before (weakened to ≤) and should participate in the veridicality and NPI-licensing generalizations.

inductive Fragments.English.TemporalExpressions.TemporalOrder : Type

Temporal ordering relation encoded by a connective or modifier.

• before : TemporalOrder
• after : TemporalOrder
• while_ : TemporalOrder
• when_ : TemporalOrder
• until_ : TemporalOrder
• since_ : TemporalOrder
• by_ : TemporalOrder
• whenever : TemporalOrder

instance Fragments.English.TemporalExpressions.instDecidableEqTemporalOrder : DecidableEq TemporalOrder

Equations

• Fragments.English.TemporalExpressions.instDecidableEqTemporalOrder x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Fragments.English.TemporalExpressions.instReprTemporalOrder : Repr TemporalOrder

Equations

• Fragments.English.TemporalExpressions.instReprTemporalOrder = { reprPrec := Fragments.English.TemporalExpressions.instReprTemporalOrder.repr }

def Fragments.English.TemporalExpressions.instReprTemporalOrder.repr : TemporalOrder → ℕ → Std.Format

Equations

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

instance Fragments.English.TemporalExpressions.instBEqTemporalOrder : BEq TemporalOrder

Equations

• Fragments.English.TemporalExpressions.instBEqTemporalOrder = { beq := Fragments.English.TemporalExpressions.instBEqTemporalOrder.beq }

def Fragments.English.TemporalExpressions.instBEqTemporalOrder.beq : TemporalOrder → TemporalOrder → Bool

Equations

• Fragments.English.TemporalExpressions.instBEqTemporalOrder.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.English.TemporalExpressions.instInhabitedTemporalOrder : Inhabited TemporalOrder

Equations

• Fragments.English.TemporalExpressions.instInhabitedTemporalOrder = { default := Fragments.English.TemporalExpressions.instInhabitedTemporalOrder.default }

def Fragments.English.TemporalExpressions.instInhabitedTemporalOrder.default : TemporalOrder

Equations

• Fragments.English.TemporalExpressions.instInhabitedTemporalOrder.default = Fragments.English.TemporalExpressions.TemporalOrder.before

inductive Fragments.English.TemporalExpressions.Reading : Type

Available readings for a temporal clause or modified VP. "Start" = initial point of embedded eventuality; "finish" = final point.

• beforeStart : Reading
• beforeFinish : Reading
• afterStart : Reading
• afterFinish : Reading
• durative : Reading

instance Fragments.English.TemporalExpressions.instDecidableEqReading : DecidableEq Reading

Equations

• Fragments.English.TemporalExpressions.instDecidableEqReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Fragments.English.TemporalExpressions.instReprReading.repr : Reading → ℕ → Std.Format

Equations

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

instance Fragments.English.TemporalExpressions.instReprReading : Repr Reading

Equations

• Fragments.English.TemporalExpressions.instReprReading = { reprPrec := Fragments.English.TemporalExpressions.instReprReading.repr }

instance Fragments.English.TemporalExpressions.instBEqReading : BEq Reading

Equations

• Fragments.English.TemporalExpressions.instBEqReading = { beq := Fragments.English.TemporalExpressions.instBEqReading.beq }

def Fragments.English.TemporalExpressions.instBEqReading.beq : Reading → Reading → Bool

Equations

• Fragments.English.TemporalExpressions.instBEqReading.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Fragments.English.TemporalExpressions.instInhabitedReading.default : Reading

Equations

• Fragments.English.TemporalExpressions.instInhabitedReading.default = Fragments.English.TemporalExpressions.Reading.beforeStart

instance Fragments.English.TemporalExpressions.instInhabitedReading : Inhabited Reading

Equations

• Fragments.English.TemporalExpressions.instInhabitedReading = { default := Fragments.English.TemporalExpressions.instInhabitedReading.default }

inductive Fragments.English.TemporalExpressions.ComplementType : Type

Syntactic complement type: clausal (before she arrived) vs nominal (by 3pm, within an hour).

• clausal : ComplementType
• nominal : ComplementType

instance Fragments.English.TemporalExpressions.instDecidableEqComplementType : DecidableEq ComplementType

Equations

• Fragments.English.TemporalExpressions.instDecidableEqComplementType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Fragments.English.TemporalExpressions.instReprComplementType : Repr ComplementType

Equations

• Fragments.English.TemporalExpressions.instReprComplementType = { reprPrec := Fragments.English.TemporalExpressions.instReprComplementType.repr }

def Fragments.English.TemporalExpressions.instReprComplementType.repr : ComplementType → ℕ → Std.Format

Equations

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

def Fragments.English.TemporalExpressions.instBEqComplementType.beq : ComplementType → ComplementType → Bool

Equations

• Fragments.English.TemporalExpressions.instBEqComplementType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.English.TemporalExpressions.instBEqComplementType : BEq ComplementType

Equations

• Fragments.English.TemporalExpressions.instBEqComplementType = { beq := Fragments.English.TemporalExpressions.instBEqComplementType.beq }

instance Fragments.English.TemporalExpressions.instInhabitedComplementType : Inhabited ComplementType

Equations

• Fragments.English.TemporalExpressions.instInhabitedComplementType = { default := Fragments.English.TemporalExpressions.instInhabitedComplementType.default }

def Fragments.English.TemporalExpressions.instInhabitedComplementType.default : ComplementType

Equations

• Fragments.English.TemporalExpressions.instInhabitedComplementType.default = Fragments.English.TemporalExpressions.ComplementType.clausal

structure Fragments.English.TemporalExpressions.TemporalExprEntry : Type

Lexical entry for any temporal expression — subordinating connective or adverbial modifier. Unifies the semantic fields (ordering direction, NPI licensing, veridicality) that @cite{heinamaki-1974} shows are shared across both syntactic categories.

The complementType field records the syntactic distinction (clausal vs nominal complement) without splitting the semantic properties into separate types.

• form : String

  Surface form

• complementType : ComplementType

  Syntactic complement type

• order : TemporalOrder

  Temporal ordering direction

• licensesNPI : Bool

  Does this expression license NPIs in its complement?

• defaultReading : Reading

  Reading obtained without coercion (Rett's strong default)

• coercedReading : Option Reading

  Reading requiring aspectual coercion (INCHOAT or COMPLET)

• embeddedTelicityEffect : Bool

  Does telicity of the embedded clause affect interpretation?

• crossLinguisticBasic : Bool

  Attested in all 17 languages of @cite{rett-2020}'s typological survey

• complementVeridical : Bool

  Does the expression entail the truth of its complement? after is veridical: "He left after she arrived" entails she arrived. before is non-veridical: "He left before she arrived" is compatible with her not arriving.

• forcesPunctual : Bool

  Does this expression force a punctual (point-like) reading?

• triggeredCoercion : Option String

  Which coercion operator is mandatorily triggered (if any). some "INCHOAT" or some "COMPLET" for modifiers that force coercion (e.g. within, at). none for connectives like before/after where coercion is optional — those use coercedReading to record the alternative reading available through voluntary coercion.

def Fragments.English.TemporalExpressions.instReprTemporalExprEntry.repr : TemporalExprEntry → ℕ → Std.Format

Equations

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

instance Fragments.English.TemporalExpressions.instReprTemporalExprEntry : Repr TemporalExprEntry

Equations

• Fragments.English.TemporalExpressions.instReprTemporalExprEntry = { reprPrec := Fragments.English.TemporalExpressions.instReprTemporalExprEntry.repr }

instance Fragments.English.TemporalExpressions.instBEqTemporalExprEntry : BEq TemporalExprEntry

Equations

• Fragments.English.TemporalExpressions.instBEqTemporalExprEntry = { beq := Fragments.English.TemporalExpressions.instBEqTemporalExprEntry.beq }

def Fragments.English.TemporalExpressions.instBEqTemporalExprEntry.beq : TemporalExprEntry → TemporalExprEntry → Bool

Equations

• One or more equations did not get rendered due to their size.
• Fragments.English.TemporalExpressions.instBEqTemporalExprEntry.beq x✝¹ x✝ = false

def Fragments.English.TemporalExpressions.before_ : TemporalExprEntry

before: licenses NPIs; default = before-start; coerced = before-finish (requires COMPLET to extract telos of telic EE).

Equations

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

def Fragments.English.TemporalExpressions.after_ : TemporalExprEntry

after: no NPIs; default = after-finish; coerced = after-start (requires INCHOAT to extract onset of atelic EE).

Equations

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

def Fragments.English.TemporalExpressions.while_conn : TemporalExprEntry

while: durative overlap, no coercion, no telicity sensitivity.

Equations

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

def Fragments.English.TemporalExpressions.until_ : TemporalExprEntry

until: durative persistence up to complement time. Has two uses:

• Durative: "John slept until 3pm" — main clause is stative, until marks minimum extent. Truth-conditionally = temporal overlap.
• Punctual (with negation): "He didn't wake up until 3pm" — logical form = NOT(A BEFORE T). Licenses NPIs in this use.

We encode the durative reading as default, with the punctual reading arising compositionally via negation + the before semantics.

Equations

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

def Fragments.English.TemporalExpressions.when_conn : TemporalExprEntry

when: temporal coincidence, no coercion. Veridical complement. "John arrived when Mary left" — the two events overlap in time. Symmetric: "A when B" ↔ "B when A".

Equations

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

def Fragments.English.TemporalExpressions.since_conn : TemporalExprEntry

since: starting-point connective. Veridical complement. "He's been happy since she arrived" entails she arrived. Requires durative (stative/activity) main clause, like until. Does not license NPIs.

Equations

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

def Fragments.English.TemporalExpressions.till_conn : TemporalExprEntry

till: dialectal variant of until. Identical semantic properties to until. Dialectally restricted: not universal across English varieties.

Equations

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

def Fragments.English.TemporalExpressions.within_ : TemporalExprEntry

within + duration: relevant to INCHOAT debate. Alstott & Aravind Exps 1a, 3: "within an hour" + activity verb. Alstott & Aravind found no INCHOAT cost here.

Equations

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

def Fragments.English.TemporalExpressions.at_punct : TemporalExprEntry

at + time point: relevant to COMPLET debate. Alstott & Aravind Exp 1b: "at 7 o'clock" + accomplishment. Forces punctual reading → COMPLET required for telic events.

Equations

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

def Fragments.English.TemporalExpressions.by_deadline : TemporalExprEntry

by + time point: deadline semantics. "He arrived by 3pm" = at or before 3pm. Weaker than before (allows coincidence). Does not force punctual reading: "He had finished the book by Tuesday" is fine with an accomplishment.

Equations

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

def Fragments.English.TemporalExpressions.asLongAs : TemporalExprEntry

as long as: temporal containment, synonymous with while. "I'll stay as long as you need me." Same ∀-containment semantics as while. Carries an additional conditional flavor in many uses ("As long as it rains, we stay inside"), but truth-conditionally equivalent to while.

Equations

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

def Fragments.English.TemporalExpressions.whenever_conn : TemporalExprEntry

whenever: universally quantified temporal overlap. "Whenever it rains, I carry an umbrella." Every occasion of B has a corresponding occurrence of A. Truth-conditionally ∀t∈B, t∈A (= while with arguments swapped). Implies habitual/generic interpretation. Veridical for both clauses (given nonempty B).

Equations

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

def Fragments.English.TemporalExpressions.asSoonAs : TemporalExprEntry

as soon as: strengthened after with temporal proximity implicature. "He left as soon as she arrived." Truth-conditionally equivalent to after (∃∃ ordering), but pragmatically implies minimal temporal gap between the two events. Veridical complement.

Equations

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

def Fragments.English.TemporalExpressions.allEntries : List TemporalExprEntry

Equations

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

def Fragments.English.TemporalExpressions.allConnectives : List TemporalExprEntry

Connective entries only (clausal complement).

Equations

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

def Fragments.English.TemporalExpressions.allModifiers : List TemporalExprEntry

Modifier entries only (nominal complement).

Equations

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

theorem Fragments.English.TemporalExpressions.before_form_agrees : before_.form = FunctionWords.before.form

theorem Fragments.English.TemporalExpressions.after_form_agrees : after_.form = FunctionWords.after.form

theorem Fragments.English.TemporalExpressions.all_orders_covered : before_.order = TemporalOrder.before ∧ after_.order = TemporalOrder.after ∧ while_conn.order = TemporalOrder.while_ ∧ until_.order = TemporalOrder.until_ ∧ when_conn.order = TemporalOrder.when_ ∧ since_conn.order = TemporalOrder.since_ ∧ by_deadline.order = TemporalOrder.by_ ∧ whenever_conn.order = TemporalOrder.whenever

All eight temporal orders in the enum have corresponding entries.

theorem Fragments.English.TemporalExpressions.only_before_nonveridical : before_.complementVeridical = false ∧ after_.complementVeridical = true ∧ while_conn.complementVeridical = true ∧ until_.complementVeridical = true ∧ when_conn.complementVeridical = true ∧ since_conn.complementVeridical = true ∧ till_conn.complementVeridical = true ∧ asLongAs.complementVeridical = true ∧ whenever_conn.complementVeridical = true ∧ asSoonAs.complementVeridical = true ∧ by_deadline.complementVeridical = true ∧ within_.complementVeridical = true ∧ at_punct.complementVeridical = true

Veridicality pattern: before is the only non-veridical expression. This holds across both connectives and modifiers.

theorem Fragments.English.TemporalExpressions.npi_pattern : before_.licensesNPI = true ∧ until_.licensesNPI = true ∧ till_conn.licensesNPI = true ∧ after_.licensesNPI = false ∧ while_conn.licensesNPI = false ∧ when_conn.licensesNPI = false ∧ since_conn.licensesNPI = false ∧ asLongAs.licensesNPI = false ∧ whenever_conn.licensesNPI = false ∧ asSoonAs.licensesNPI = false ∧ by_deadline.licensesNPI = false ∧ within_.licensesNPI = false ∧ at_punct.licensesNPI = false

NPI licensing pattern: only before, until, and till license NPIs. For before, this follows from downward entailment of the complement. For until/till, this arises in the punctual (not...until) construction, which is truth-conditionally ¬before. No modifiers license NPIs.

theorem Fragments.English.TemporalExpressions.till_matches_until : till_conn.order = until_.order ∧ till_conn.licensesNPI = until_.licensesNPI ∧ till_conn.defaultReading = until_.defaultReading ∧ till_conn.complementVeridical = until_.complementVeridical

Till and until agree on all semantic properties.

theorem Fragments.English.TemporalExpressions.complement_type_classification : before_.complementType = ComplementType.clausal ∧ after_.complementType = ComplementType.clausal ∧ while_conn.complementType = ComplementType.clausal ∧ until_.complementType = ComplementType.clausal ∧ when_conn.complementType = ComplementType.clausal ∧ since_conn.complementType = ComplementType.clausal ∧ till_conn.complementType = ComplementType.clausal ∧ by_deadline.complementType = ComplementType.nominal ∧ within_.complementType = ComplementType.nominal ∧ at_punct.complementType = ComplementType.nominal

The complement-type field correctly classifies all entries.

theorem Fragments.English.TemporalExpressions.asLongAs_matches_while : asLongAs.order = while_conn.order ∧ asLongAs.licensesNPI = while_conn.licensesNPI ∧ asLongAs.defaultReading = while_conn.defaultReading ∧ asLongAs.complementVeridical = while_conn.complementVeridical

As long as agrees with while on all semantic properties.

theorem Fragments.English.TemporalExpressions.asSoonAs_matches_after : asSoonAs.order = after_.order ∧ asSoonAs.licensesNPI = after_.licensesNPI ∧ asSoonAs.defaultReading = after_.defaultReading ∧ asSoonAs.complementVeridical = after_.complementVeridical

As soon as agrees with after on ordering and veridicality.