The Subinterval Property #
The subinterval property (Bennett & Partee 1972, Dowty 1979) is a fundamental semantic property of event predicates that determines their aspectual class:
- 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]
This property is central to the semantics of temporal adverbials (@cite{rouillard-2026}), NPI licensing in boundary adverbials (@cite{iatridou-zeijlstra-2021}), and the distribution of progressive and imperfective aspect crosslinguistically.
Originally extracted from a Rouillard-2026 substrate file (since deleted in
the 2026-05 rebuild — see Phenomena/TenseAspect/Studies/Rouillard2026.lean)
because it is a general property of event predicates, not specific to any
particular analysis.
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-witness (Bennett-Partee 1972) form of stativity
along the time dimension. The SR_univ decomposition form at
@cite{champollion-2017}'s analogous parameter-space point (dim = τ,
point-interval granularity) is genuinely different math — ∃-decomposition
over P-parts vs ∀-projection over hypothetical witness events. The
quantifier-level cousin (Zhao 2025 Def. 5.36, ATOM-DIST_t) lives in
Core/Time/AtomDist.lean. The three formulations are NOT directly
interderivable; bridging requires explicit witness-existence
assumptions.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Closed subinterval property (CSUB). For any subinterval t of a P-event's runtime, there exists a P-event whose runtime is t. Stronger than SUB: guarantees witnesses exist, not just that predication is preserved.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The subinterval property's consequences at the level of aspect operators. @cite{smith-1997} Ch. 2: states and activities have the subinterval property; accomplishments, achievements, and semelfactives lack it.
`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** (p. 25): IMPF(activity) at I entails
PRFV(activity) at some I' ⊆ I — activities have part-whole homogeneity.
2. **Imperfective paradox** (p. 29): IMPF(accomplishment) does NOT
entail PRFV(accomplishment) — the missing endpoint problem.
3. **IMPF ⊢ PRFV ⟺ CSIP**: the imperfective entails the perfective
if and only if the predicate has the closed subinterval property.
Activity entailment (@cite{smith-1997} p. 25): If an activity predicate P holds at interval I (IMPF reading: I is inside the event's runtime), then P holds at every subinterval of I (PRFV reading: subinterval is contained in the event).
Formally: HasSubintervalProp(P) → IMPF(P)(w)(I) → ∀ I' ⊆ I, ∃e. τ(e) = I' ∧ P(w)(e).
This is the semantic content of "activities entail their own imperfective": "John was running" at I entails "John ran" at every subinterval of I.
Imperfective paradox (@cite{smith-1997} p. 29): The subinterval property fails for accomplishments. 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 hypothesis t₁ < t₂ ensures Time is nontrivial — in a singleton
Time there is only one interval and the SIP holds vacuously for all P.
With two distinct time points, we can construct a "telic" predicate
P that holds only for events spanning the full interval [t₁, t₂]
and fails for proper subintervals like [t₁, t₁].
The central result connecting aspect operators to the subinterval property. For predicates with the closed SIP (states, activities), the imperfective entails the perfective at the same interval:
CSIP(P) → IMPF(P)(w)(t) → PRFV(P)(w)(t)
This is the formal reason the 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 `imperfective_paradox_possible` (which shows that
predicates without the SIP can fail this entailment), this gives
a complete characterization:
IMPF entails PRFV ⟺ the predicate has the subinterval property
The proof:
1. IMPF gives us event e with t ⊂ τ(e) and P(w, e)
2. properSubinterval implies subinterval: t ⊆ τ(e)
3. CSIP 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 CSIP predicates (@cite{smith-1997} Ch. 2). If P has the closed subinterval property, then IMPF(P)(w)(t) entails PRFV(P)(w)(t) — the 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 the CSIP, there exists a running event whose runtime IS exactly t, which satisfies the PRFV containment requirement.
CSIP is necessary for IMPF→PRFV (converse of impf_entails_prfv_of_csip):
if IMPF entails PRFV for ALL predicates, then every predicate has CSIP.
Combined with the forward direction, this gives a complete characterization: (∀ P, IMPF(P) ⊆ PRFV(P)) ⟺ (∀ P, CSIP(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'). 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)