Evaluate a point predicate at speech time (PRESENT). PRES: p holds at tc in world w.
Equations
- Semantics.TenseAspectComposition.evalPres p tc w = p { world := w, time := tc }
Instances For
Evaluate a point predicate with existential past (PAST). PAST: ∃t < tc, p(w)(t).
Equations
- Semantics.TenseAspectComposition.evalPast p tc w = ∃ t < tc, p { world := w, time := t }
Instances For
Evaluate a point predicate with existential future (FUTURE). FUT: ∃t > tc, p(w)(t).
Equations
- Semantics.TenseAspectComposition.evalFut p tc w = ∃ t > tc, p { world := w, time := t }
Instances For
Simple present: PRES(IMPF(V).atPoint). "John runs" = at speech time, ∃e with tc ⊂ τ(e) and V(e). Since atPoint evaluates at [tc, tc], this gives: ∃e, [tc,tc] ⊂ τ(e) ∧ V(e).
Equations
Instances For
Simple past: PAST(PRFV(V).atPoint). "John ran" = ∃t < tc, ∃e with τ(e) ⊆ [t,t] and V(e).
Equations
Instances For
Present perfect progressive: PRES(PERF(IMPF(V))). "John has been running" = at tc, ∃PTS with RB(PTS, tc) and IMPF(V)(PTS).
Equations
Instances For
Present perfect simple: PRES(PERF(PRFV(V))). "John has run" = at tc, ∃PTS with RB(PTS, tc) and PRFV(V)(PTS).
Equations
Instances For
Present perfect progressive with Extended Now: PRES(PERF_XN(IMPF(V), tᵣ)). @cite{knick-sharf-2026} eq. 39b: the U-perf reading. "John has been running (since Monday)" with domain restriction tᵣ on LB.
Equations
Instances For
Past perfect progressive: PAST(PERF(IMPF(V))). "John had been running" = ∃t < tc, PERF(IMPF(V))(w)(t).
Equations
Instances For
Simple present unfolds to: ∃e, [tc,tc] ⊂ τ(e) ∧ V(w)(e).
Present perfect progressive with XN unfolds to K&S eq. 39b: ∃PTS, ∃tLB ∈ tᵣ, LB(tLB, PTS) ∧ RB(PTS, tc) ∧ IMPF(V)(w)(PTS).
Theorem 3 (@cite{knick-sharf-2026}): U-perf(tᵣ) entails simple present.
For any domain restriction tᵣ, the present perfect progressive with Extended Now entails the simple present. Intuitively: if there is a PTS ending at tc containing the reference time inside an ongoing event, then tc itself is inside that event.
Proof sketch: Given PERF_XN(IMPF(V), tᵣ)(w)(tc), we have PTS with RB(PTS, tc) and ∃e with PTS ⊂ τ(e). Since [tc,tc] ⊆ PTS (because tc = PTS.finish) and PTS ⊂ τ(e), we get [tc,tc] ⊂ τ(e).
Theorem 4 (@cite{knick-sharf-2026}): U-perf with maximal domain ↔ simple present.
Under broad focus (tᵣ = Set.univ), the U-perf reading is equivalent to the simple present. This is the "degenerate" case where no LB constraint is imposed.
Proof sketch: (→) by Theorem 3. (←) Given simplePresent, we have ∃e with [tc,tc] ⊂ τ(e). Construct PTS = [e.τ.start, tc]. Then LB(e.τ.start, PTS) ∈ Set.univ, RB(PTS, tc), and PTS ⊆ τ(e) with PTS ⊂ τ(e) (since tc < e.τ.finish by properSubinterval).
Theorem 5 (@cite{knick-sharf-2026}): Earlier LB is stronger under IMPF.
If tLB₁ < tLB₂, then PERF_XN(IMPF(V), {tLB₁}) entails PERF_XN(IMPF(V), {tLB₂}).
Under IMPF, the event must contain the entire PTS. A PTS starting earlier (at tLB₁) requires a longer event runtime, which also contains a PTS starting later (at tLB₂) — because IMPF gives the subinterval property.
Proof sketch: Given PTS₁ = [tLB₁, tc] with e.τ ⊃ PTS₁ and V(e), construct PTS₂ = [tLB₂, tc]. Since tLB₁ < tLB₂ ≤ tc, PTS₂ is valid. PTS₂ ⊆ PTS₁ ⊆ τ(e), and PTS₂ ⊂ τ(e) follows from PTS₁ ⊂ τ(e).
Theorem 6 (@cite{knick-sharf-2026}): Later LB is stronger under PRFV.
If tLB₁ < tLB₂, then PERF_XN(PRFV(V), {tLB₂}) entails PERF_XN(PRFV(V), {tLB₁}).
Under PRFV, the event must be contained within the PTS. A PTS starting later (at tLB₂) is shorter, imposing a tighter constraint on event placement. But a PTS starting earlier (at tLB₁) is longer, so any event fitting in [tLB₂, tc] also fits in [tLB₁, tc].
Proof sketch: Given PTS₂ = [tLB₂, tc] with τ(e) ⊆ PTS₂, construct PTS₁ = [tLB₁, tc]. Since tLB₁ < tLB₂, PTS₂ ⊆ PTS₁, so τ(e) ⊆ PTS₁.
Theorem 7 (@cite{knick-sharf-2026}): Converse of Theorem 5 is FALSE.
PERF_XN(IMPF(V), {tLB₂}) does NOT entail PERF_XN(IMPF(V), {tLB₁}) when tLB₁ < tLB₂. An event that has been going on since tLB₂ need not have been going on since the earlier tLB₁.
Counterexample: Let tLB₁ = 0, tLB₂ = 2, tc = 4. An event with runtime [1, 5] satisfies IMPF for PTS = [2, 4] (since [2,4] ⊂ [1,5]), but does NOT satisfy IMPF for PTS = [0, 4] (since [0,4] ⊄ [1,5]: the event hadn't started at time 0).