Tense Evaluation Operators

def Tense.TenseAspectComposition.evalPres {W : Type u_1} {Time : Type u_2} (p : Semantics.Aspect.PointPred W Time) (tc : Time) (w : W) : Prop

Evaluate a point predicate at speech time (PRESENT). PRES: p holds at tc in world w.

Equations

• Tense.TenseAspectComposition.evalPres p tc w = p { world := w, time := tc }

def Tense.TenseAspectComposition.evalRel {W : Type u_1} {Time : Type u_2} (rel : Time → Time → Prop) (p : Semantics.Aspect.PointPred W Time) (tc : Time) (w : W) : Prop

Existential tense evaluation: the GQ some (Quantification.some_sem) over times rel-related to the evaluation time tc, scope p at ⟨w, ·⟩. evalPast/evalFut are the </> instances.

Equations

• Tense.TenseAspectComposition.evalRel rel p tc w = Quantification.some_sem (fun (t : Time) => rel t tc) fun (t : Time) => p { world := w, time := t }

theorem Tense.TenseAspectComposition.evalRel_mono {W : Type u_1} {Time : Type u_2} {rel : Time → Time → Prop} {p q : Semantics.Aspect.PointPred W Time} (h : ∀ (x : Intensional.WorldTimeIndex W Time), p x → q x) {tc : Time} {w : W} : evalRel rel p tc w → evalRel rel q tc w

Monotone in the body predicate — inherited from some_scope_up, not reproved.

def Tense.TenseAspectComposition.evalPast {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (p : Semantics.Aspect.PointPred W Time) (tc : Time) (w : W) : Prop

Evaluate a point predicate with existential past (PAST): ∃ t < tc, p(w)(t).

Equations

• Tense.TenseAspectComposition.evalPast p tc w = Tense.TenseAspectComposition.evalRel (fun (x1 x2 : Time) => x1 < x2) p tc w

def Tense.TenseAspectComposition.evalFut {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (p : Semantics.Aspect.PointPred W Time) (tc : Time) (w : W) : Prop

Evaluate a point predicate with existential future (FUTURE): ∃ t > tc, p(w)(t).

Equations

• Tense.TenseAspectComposition.evalFut p tc w = Tense.TenseAspectComposition.evalRel (fun (x1 x2 : Time) => x1 > x2) p tc w

theorem Tense.TenseAspectComposition.evalPast_iff_quantificationalPast {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (p : Semantics.Aspect.PointPred W Time) (tc : Time) (w : W) : evalPast p tc w ↔ quantificationalPast Set.univ (fun (t : Time) => p { world := w, time := t }) tc

The pipeline's existential past is [Sha14]'s quantificational past with trivial restrictor: evalPast = quantificationalPast over Set.univ. Together with pronominalLookup_eq_some_iff_tensePronoun (in LexicalType.lean), this places both of Sharvit's tense lexical types over the operators the rest of the codebase already uses.

Composed Tense–Aspect Forms

def Tense.TenseAspectComposition.simplePresent {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (V : W → Event Time → Prop) (tc : Time) (w : W) : Prop

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

• Tense.TenseAspectComposition.simplePresent V tc w = Tense.TenseAspectComposition.evalPres (Semantics.Aspect.IMPF V).atPoint tc w

def Tense.TenseAspectComposition.simplePast {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (V : W → Event Time → Prop) (tc : Time) (w : W) : Prop

Simple past: PAST(PRFV(V).atPoint). "John ran" = ∃t < tc, ∃e with τ(e) ⊆ [t,t] and V(e).

Equations

• Tense.TenseAspectComposition.simplePast V tc w = Tense.TenseAspectComposition.evalPast (Semantics.Aspect.PRFV V).atPoint tc w

def Tense.TenseAspectComposition.presPerfProg {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (V : W → Event Time → Prop) (tc : Time) (w : W) : Prop

Present perfect progressive: PRES(PERF(IMPF(V))). "John has been running" = at tc, ∃PTS with RB(PTS, tc) and IMPF(V)(PTS).

Equations

• Tense.TenseAspectComposition.presPerfProg V tc w = Tense.TenseAspectComposition.evalPres (Semantics.Aspect.PERF (Semantics.Aspect.IMPF V)) tc w

def Tense.TenseAspectComposition.presPerfSimple {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (V : W → Event Time → Prop) (tc : Time) (w : W) : Prop

Present perfect simple: PRES(PERF(PRFV(V))). "John has run" = at tc, ∃PTS with RB(PTS, tc) and PRFV(V)(PTS).

Equations

• Tense.TenseAspectComposition.presPerfSimple V tc w = Tense.TenseAspectComposition.evalPres (Semantics.Aspect.PERF (Semantics.Aspect.PRFV V)) tc w

def Tense.TenseAspectComposition.presPerfProgXN {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (V : W → Event Time → Prop) (tᵣ : Set Time) (tc : Time) (w : W) : Prop

Present perfect progressive with Extended Now: PRES(PERF_XN(IMPF(V), tᵣ)). [KS26] eq. 39b: the U-perf reading. "John has been running (since Monday)" with domain restriction tᵣ on LB.

Equations

• Tense.TenseAspectComposition.presPerfProgXN V tᵣ tc w = Tense.TenseAspectComposition.evalPres (Semantics.Aspect.PERF_XN (Semantics.Aspect.IMPF V) tᵣ) tc w

def Tense.TenseAspectComposition.pastPerfProg {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (V : W → Event Time → Prop) (tc : Time) (w : W) : Prop

Past perfect progressive: PAST(PERF(IMPF(V))). "John had been running" = ∃t < tc, PERF(IMPF(V))(w)(t).

Equations

• Tense.TenseAspectComposition.pastPerfProg V tc w = Tense.TenseAspectComposition.evalPast (Semantics.Aspect.PERF (Semantics.Aspect.IMPF V)) tc w

Unfold Theorems

theorem Tense.TenseAspectComposition.simplePresent_unfold {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (V : W → Event Time → Prop) (tc : Time) (w : W) : simplePresent V tc w ↔ ∃ (e : Event Time), NonemptyInterval.pure tc < e.τ ∧ V w e

Simple present unfolds to: ∃e, [tc,tc] ⊂ τ(e) ∧ V(w)(e).

theorem Tense.TenseAspectComposition.presPerfProgXN_unfold {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (V : W → Event Time → Prop) (tᵣ : Set Time) (tc : Time) (w : W) : presPerfProgXN V tᵣ tc w ↔ ∃ (pts : NonemptyInterval Time), ∃ tLB ∈ tᵣ, Semantics.Aspect.LB tLB pts ∧ Semantics.Aspect.RB pts tc ∧ Semantics.Aspect.IMPF V w pts

Present perfect progressive with XN unfolds to K&S eq. 39b: ∃PTS, ∃tLB ∈ tᵣ, LB(tLB, PTS) ∧ RB(PTS, tc) ∧ IMPF(V)(w)(PTS).

[KS26] Core Results

theorem Tense.TenseAspectComposition.u_perf_entails_simple_present {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (V : W → Event Time → Prop) (tᵣ : Set Time) (tc : Time) (w : W) : presPerfProgXN V tᵣ tc w → simplePresent V tc w

Theorem 3 ([KS26]): 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.snd) and PTS ⊂ τ(e), we get [tc,tc] ⊂ τ(e).

theorem Tense.TenseAspectComposition.broad_focus_equiv {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (V : W → Event Time → Prop) (tc : Time) (w : W) : presPerfProgXN V Set.univ tc w ↔ simplePresent V tc w

Theorem 4 ([KS26]): 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.τ.fst, tc]. Then LB(e.τ.fst, PTS) ∈ Set.univ, RB(PTS, tc), and PTS ⊆ τ(e) with PTS ⊂ τ(e) (since tc < e.τ.snd by properSubinterval).

theorem Tense.TenseAspectComposition.earlier_lb_stronger_impf {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (V : W → Event Time → Prop) (tLB₁ tLB₂ tc : Time) (w : W) (h : tLB₁ < tLB₂) (htc : tLB₂ ≤ tc) : Semantics.Aspect.PERF_XN (Semantics.Aspect.IMPF V) {tLB₁} { world := w, time := tc } → Semantics.Aspect.PERF_XN (Semantics.Aspect.IMPF V) {tLB₂} { world := w, time := tc }

Theorem 5 ([KS26]): 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 Tense.TenseAspectComposition.later_lb_stronger_prfv {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (V : W → Event Time → Prop) (tLB₁ tLB₂ tc : Time) (w : W) (h : tLB₁ < tLB₂) : Semantics.Aspect.PERF_XN (Semantics.Aspect.PRFV V) {tLB₂} { world := w, time := tc } → Semantics.Aspect.PERF_XN (Semantics.Aspect.PRFV V) {tLB₁} { world := w, time := tc }

Theorem 6 ([KS26]): 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 Tense.TenseAspectComposition.earlier_lb_not_weaker_impf : ¬∀ (V : Unit → Event ℤ → Prop) (tLB₁ tLB₂ tc : ℤ) (w : Unit), tLB₁ < tLB₂ → Semantics.Aspect.PERF_XN (Semantics.Aspect.IMPF V) {tLB₂} { world := w, time := tc } → Semantics.Aspect.PERF_XN (Semantics.Aspect.IMPF V) {tLB₁} { world := w, time := tc }

Theorem 7 ([KS26]): 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).