The Subinterval Property #
The subinterval property ([BP72], [Dow79]) is a fundamental semantic property of event predicates that diagnoses the atelic/telic (homogeneous/non-homogeneous) division of aspectual classes:
- Statives and activities have it: if John is sleeping for [1pm, 3pm], he is sleeping at every subinterval
- Accomplishments and achievements lack it: if John built a house in [Jan, Dec], he did not build a house in [Jan, Feb]
It does not by itself fix the full four-way Vendler class (state vs. activity and accomplishment vs. achievement need stativity/punctuality diagnostics); it draws only the homogeneous/non-homogeneous line.
This property underlies the semantics of temporal adverbials ([Rou26]) and interacts with the aspectual sensitivity of boundary adverbials ([IZ21]) and the distribution of progressive and imperfective aspect crosslinguistically.
This is general event-predicate substrate, not specific to any particular
analysis — consumed by Studies/Rouillard2026.lean,
Studies/IatridouZeijlstra2021.lean,
Studies/OgiharaSteinertThrelkeld2024.lean, and the run-time projection in
Semantics/Tense/TemporalConnectives/Projection.lean.
Subinterval property for event predicates (mereological version). SUB(P) iff every subinterval of a P-event's runtime that is also the runtime of some event is the runtime of a P-event. States and activities have this property; accomplishments/achievements lack it.
This is the universal-over-witnesses form: it constrains only those
subintervals that already happen to be some event's runtime. It is
therefore vacuously satisfiable when the event ontology is sparse
(no event has runtime exactly t ⇒ the inner ∀ e₂ is empty). The
contentful, witness-producing form is HasClosedSubintervalProp
(CSUB) below, which every operator-level theorem in this file consumes;
plain SUB is the weaker conditional and does not on its own express
Bennett-Partee/Dowty homogeneity.
The Stratified.SubintervalReference decomposition form at
[Cha17]'s analogous parameter-space point (dim = τ,
point-interval granularity) is genuinely different math — ∃-decomposition
over P-parts vs ∀-projection over hypothetical witness events; the
distinctness is backed by the counterexamples in
Semantics/Aspect/Stratified.lean. The quantifier-level cousin
([Zha25] ATOM-DIST_t) lives in Semantics/Aspect/AtomDist.lean. The
three formulations are NOT directly interderivable; bridging requires
explicit witness-existence assumptions.
Equations
- Semantics.Aspect.SubintervalProperty.HasSubintervalProp P = ∀ (e₁ : Event Time) (w : W), P w e₁ → ∀ t ≤ e₁.τ, ∀ (e₂ : Event Time), e₂.τ = t → P w e₂
Instances For
Closed subinterval property (CSUB): P's run-times form a lower set.
This is the contentful homogeneity property — eventDenotation (P w ·)
(the run-time image, Semantics/Events/Basic.lean) is downward-closed in
NonemptyInterval Time at every world. Equivalently, for any subinterval
t of a P-event's runtime there exists a P-event whose runtime is t
(the witness form — see hasClosedSubintervalProp_iff_witnesses).
CSUB is exactly Krifka divisivity of the run-time image: DIV
([Cha17]; Semantics/Mereology.lean) is by definition
IsLowerSet, so HasClosedSubintervalProp P ↔ ∀ w, DIV (eventDenotation (P w ·))
holds definitionally. Stating CSUB directly on mathlib's IsLowerSet
collapses three former encodings of the same concept — the bespoke
∀∀∃ witness predicate, Mereology.DIV, and the lower-set fact proved
ad hoc in Tense/TemporalConnectives/Projection.lean — onto one carrier.
Stronger than HasSubintervalProp (SUB): SUB only constrains witnesses
that already exist and is vacuous under a sparse event ontology; CSUB
produces a witness at every subinterval, which is what every
operator-level theorem below consumes.
Equations
- Semantics.Aspect.SubintervalProperty.HasClosedSubintervalProp P = ∀ (w : W), IsLowerSet (eventDenotation fun (e : Event Time) => P w e)
Instances For
CSUB ⟺ the witness form. Unfolds the lower-set definition to the classic Bennett-Partee/Dowty statement: every subinterval of a P-event's runtime is itself the runtime of some P-event. Operator-level theorems consume CSUB through this characterization.
The subinterval property's consequences at the level of aspect operators. The atelic/telic homogeneity generalization is canonically [Dow79] / [BP72]; [Smi97] supplies the viewpoint-classification framing (states and activities have the subinterval property; accomplishments, achievements, and semelfactives lack it).
**Caveat — these are *extensional* results.** `IMPF`/`PRFV` here
existentially quantify over a *completed* event in the evaluation world
(`Basic.lean`). The genuine imperfective paradox — "John was building a
house" can be true with no house ever completed — is *intensional* and
requires a modal PROG over inertia/continuation worlds ([dowty-1979];
Landman 1992; Portner 1998), which this file does NOT model. What is
proved below is the homogeneity half: for subinterval-closed predicates
the extensional imperfective entails the perfective, and for telic ones
it need not.
`Features/Aktionsart.lean` carries the VendlerClass enum used to
state the consumer-side facts (`c = .state ∨ c = .activity` for
SUB-having classes). Here we prove the operator-level consequences:
1. **Activity entailment**: for CSUB predicates, holding at `e₁` yields a
P-event at every subinterval of `e₁`'s runtime — part-whole homogeneity.
2. **Telic non-homogeneity**: not every predicate is subinterval-closed
(the missing-endpoint predicate is a witness).
3. **IMPF ⊢ PRFV ⟺ CSUB**: the extensional imperfective entails the
perfective iff the predicate has the closed subinterval property.
Activity entailment ([Dow79]; [BP72]):
if an activity predicate P has the closed subinterval property and
holds of event e₁, then every subinterval t of e₁'s runtime is
itself the runtime of a P-event.
Formally: HasClosedSubintervalProp P → P w e₁ → t ≤ e₁.τ → ∃ e₂, e₂.τ = t ∧ P w e₂.
This is the part-whole homogeneity behind "activities entail their own
imperfective" — "John was running" entails "John ran" at every
subinterval. It is the witness form of CSUB
(hasClosedSubintervalProp_iff_witnesses).
Telic non-homogeneity (the extensional core of the imperfective paradox, [Dow79]): the subinterval property is not universal — some predicates fail it. This is why "John was building a house" does not entail "John built a house": proper subintervals of a house-building event are not themselves house-building events (the result state is missing). (The full paradox — truth without any completed event — is intensional and modeled elsewhere; see the section caveat above. This theorem only exhibits a non-subinterval-closed predicate.)
The hypothesis t₁ < t₂ ensures Time is nontrivial — in a singleton
Time there is only one interval and SUB holds vacuously for all P.
With two distinct time points, we construct a "telic" predicate
P that holds only for events finishing at t₂ and fails for proper
subintervals like [t₁, t₁].
The central result connecting aspect operators to the subinterval property. For predicates with the closed subinterval property (CSUB — states, activities), the extensional imperfective entails the perfective at the same interval:
CSUB(P) → IMPF(P)(w)(t) → PRFV(P)(w)(t)
This is the formal reason the (extensional) imperfective paradox does NOT
arise for homogeneous predicates. "Mary was running" (IMPF) entails
"Mary ran" (PRFV) because any subinterval of a running event is
itself a running event — so the reference time t, which is inside
the event's runtime, is itself the runtime of a running event.
Combined with `csub_necessary_for_impf_prfv` (the converse), this gives
a complete characterization:
(∀ P, IMPF(P) ⊆ PRFV(P)) ⟺ (∀ P, CSUB(P))
The proof:
1. IMPF gives us event e with t ⊂ τ(e) and P(w, e)
2. proper containment implies containment: t ≤ τ(e)
3. CSUB with e, w, t yields witness e₂ with τ(e₂) = t and P(w, e₂)
4. Since τ(e₂) = t ≤ t (reflexive), PRFV holds with witness e₂
IMPF entails PRFV for CSUB predicates ([Dow79]; [Smi97]). If P has the closed subinterval property, then IMPF(P)(w)(t) entails PRFV(P)(w)(t) — the (extensional) imperfective entails the perfective at the same reference interval.
This is why "Mary was running" entails "Mary ran": the reference time t is properly inside the running event's runtime, and since running has CSUB, there exists a running event whose runtime IS exactly t, which satisfies the PRFV containment requirement.
CSUB is necessary for IMPF→PRFV (converse of impf_entails_prfv_of_csub):
if IMPF entails PRFV for ALL predicates, then every predicate has CSUB.
Combined with the forward direction, this gives a complete characterization: (∀ P, IMPF(P) ⊆ PRFV(P)) ⟺ (∀ P, CSUB(P))
The proof uses the refined predicate trick: given P, e, w, t with
P(w,e) and t ⊆ τ(e), we apply the hypothesis not to P directly but
to Q(w', e') := P(w', e') ∧ t ⊆ τ(e'). The case split on e.τ = t is
load-bearing: IMPF requires strict containment t < e.τ, so the
equality case must be discharged by e itself. Then:
- PRFV gives τ(e₂) ⊆ t (event contained in reference time)
- Q gives t ⊆ τ(e₂) (from the predicate's second conjunct)
- Mutual containment gives τ(e₂) = t (closing the ⊆ → = gap)