Knick and Sharf (2026): On focus and the perfect aspect

Knick and Sharf compose viewpoint aspect, the perfect and tense: an event predicate becomes an interval property under the imperfective or perfective, a set of world-time points under the perfect, and a proposition under a tense. The U-perfect, whose perfect time span has its left boundary in a domain tᵣ, entails its simple present competitor whatever the domain and is equivalent to it under broad focus, where the domain is unrestricted, which is why competition rules it out there. Among the focus alternatives, a domain further in the past is stronger.

Main results

• u_perf_entails_simple_present: the U-perfect entails the simple present.
• broad_focus_equiv: under broad focus the two are equivalent.
• earlier_lb_stronger_impf: an earlier left boundary is stronger under the imperfective.
• earlier_lb_not_weaker_impf: and not conversely.

Implementation notes

• A left boundary is a time point, where the paper's left boundary is a subinterval of tᵣ; the paper's PERF_XN is the perfect over the spans whose left boundary lies in tᵣ.
• later_lb_stronger_prfv, the reversed ordering under the perfective, is not drawn in the paper.

References

• [KS26]

Tense

def KnickSharf2026.evalPres {W : Type u_1} {T : Type u_2} (p : Set (Reference.Index W T)) (tc : T) (w : W) : Prop

The present tense evaluates a set of world-time points at the speech time tc in the world w.

Equations

• KnickSharf2026.evalPres p tc w = ((w, tc) ∈ p)

def KnickSharf2026.evalPast {W : Type u_1} {T : Type u_2} [LinearOrder T] (p : Set (Reference.Index W T)) (tc : T) (w : W) : Prop

The past tense evaluates a set of world-time points at some time before the speech time tc, the quantificational past of Semantics/Tense/Quantificational.lean.

Equations

• KnickSharf2026.evalPast p tc w = ModalLogic.Diamond (Tense.toSetRel (Semantics.Denotes.denote Tense.past)) (fun (t : T) => (w, t) ∈ p) tc

def KnickSharf2026.evalFut {W : Type u_1} {T : Type u_2} [LinearOrder T] (p : Set (Reference.Index W T)) (tc : T) (w : W) : Prop

The future tense evaluates a set of world-time points at some time after the speech time tc.

Equations

• KnickSharf2026.evalFut p tc w = ModalLogic.Diamond (Tense.toSetRel (Semantics.Denotes.denote Tense.future)) (fun (t : T) => (w, t) ∈ p) tc

Composed forms

def KnickSharf2026.simplePresent {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (V : W → E → Prop) (tc : T) (w : W) : Prop

The simple present is PRES(atPoint(IMPF(V))), so John runs holds at speech time when some event e with [tc, tc] ⊂ τ(e) satisfies V.

Equations

• KnickSharf2026.simplePresent V tc w = KnickSharf2026.evalPres (Aspect.atPoint (Aspect.IMPF V)) tc w

def KnickSharf2026.simplePast {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (V : W → E → Prop) (tc : T) (w : W) : Prop

The simple past is PAST(atPoint(PRFV(V))), so John ran holds when some t < tc and some event e with τ(e) ⊆ [t, t] satisfy V.

Equations

• KnickSharf2026.simplePast V tc w = KnickSharf2026.evalPast (Aspect.atPoint (Aspect.PRFV V)) tc w

def KnickSharf2026.presPerfProg {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (V : W → E → Prop) (tc : T) (w : W) : Prop

The present perfect progressive is PRES(PERF(IMPF(V))), so John has been running holds at tc when some perfect time span right-bounded by tc satisfies IMPF(V).

Equations

• KnickSharf2026.presPerfProg V tc w = KnickSharf2026.evalPres (Aspect.PERF (Aspect.IMPF V)) tc w

def KnickSharf2026.presPerfSimple {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (V : W → E → Prop) (tc : T) (w : W) : Prop

The present perfect simple is PRES(PERF(PRFV(V))), so John has run holds at tc when some perfect time span right-bounded by tc satisfies PRFV(V).

Equations

• KnickSharf2026.presPerfSimple V tc w = KnickSharf2026.evalPres (Aspect.PERF (Aspect.PRFV V)) tc w

def KnickSharf2026.presPerfProgXN {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (V : W → E → Prop) (tᵣ : Set T) (tc : T) (w : W) : Prop

The present perfect progressive with Extended Now is PRES(PERF_XN(IMPF(V), tᵣ)), the U-perfect reading of [KS26]; John has been running since Monday restricts the left boundary of the perfect time span to tᵣ.

Equations

• KnickSharf2026.presPerfProgXN V tᵣ tc w = KnickSharf2026.evalPres (Aspect.PERF fun (x : W) => (fun (x : NonemptyInterval T) => x.toProd.1) ⁻¹' tᵣ ∩ Aspect.IMPF V x) tc w

def KnickSharf2026.pastPerfProg {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (V : W → E → Prop) (tc : T) (w : W) : Prop

The past perfect progressive is PAST(PERF(IMPF(V))), so John had been running holds when some t < tc satisfies PERF(IMPF(V)).

Equations

• KnickSharf2026.pastPerfProg V tc w = KnickSharf2026.evalPast (Aspect.PERF (Aspect.IMPF V)) tc w

Unfolding

theorem KnickSharf2026.simplePresent_unfold {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (V : W → E → Prop) (tc : T) (w : W) : simplePresent V tc w ↔ ∃ (e : E), NonemptyInterval.pure tc < Event.τ e ∧ V w e

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

theorem KnickSharf2026.presPerfProgXN_iff {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (V : W → E → Prop) (tᵣ : Set T) (tc : T) (w : W) : presPerfProgXN V tᵣ tc w ↔ ∃ pts ∈ Aspect.IMPF V w, pts.toProd.1 ∈ tᵣ ∧ pts.toProd.2 = tc

The U-perfect under narrow focus, (39b), holds when some perfect time span with its left boundary in tᵣ and its right boundary at tc falls under the imperfective.

Results

theorem KnickSharf2026.u_perf_entails_simple_present {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (V : W → E → Prop) (tᵣ : Set T) (tc : T) (w : W) : presPerfProgXN V tᵣ tc w → simplePresent V tc w

The U-perfect (39b) entails its simple present competitor (39a) whatever the domain tᵣ, since a perfect time span ending at tc inside the run time of an event puts tc itself inside it.

theorem KnickSharf2026.broad_focus_equiv {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (V : W → E → Prop) (tc : T) (w : W) : presPerfProgXN V Set.univ tc w ↔ simplePresent V tc w

Under broad focus, where the domain tᵣ is the whole line, the U-perfect is equivalent to the simple present, the equivalence by which competition rules it out; the converse direction takes the point tc as the perfect time span.

theorem KnickSharf2026.earlier_lb_stronger_impf {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (V : W → E → Prop) (tLB₁ tLB₂ tc : T) (w : W) (h : tLB₁ < tLB₂) (htc : tLB₂ ≤ tc) : presPerfProgXN V {tLB₁} tc w → presPerfProgXN V {tLB₂} tc w

An earlier left boundary is stronger under the imperfective, the ordering of the focus alternatives in (33) and (35), since an event whose run time contains the perfect time span from tLB₁ also contains the shorter one from a later tLB₂.

theorem KnickSharf2026.later_lb_stronger_prfv {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (V : W → E → Prop) (tLB₁ tLB₂ tc : T) (w : W) (h : tLB₁ < tLB₂) : ((w, tc) ∈ Aspect.PERF fun (x : W) => {pts : NonemptyInterval T | pts.toProd.1 = tLB₂} ∩ Aspect.PRFV V x) → (w, tc) ∈ Aspect.PERF fun (x : W) => {pts : NonemptyInterval T | pts.toProd.1 = tLB₁} ∩ Aspect.PRFV V x

A later left boundary is stronger under the perfective (28), since an event fitting inside the shorter span from tLB₂ also fits inside the longer span from an earlier tLB₁.

theorem KnickSharf2026.earlier_lb_not_weaker_impf : ¬∀ (V : Unit → NonemptyInterval ℤ → Prop) (tLB₁ tLB₂ tc : ℤ) (w : Unit), tLB₁ < tLB₂ → presPerfProgXN V {tLB₂} tc w → presPerfProgXN V {tLB₁} tc w

The ordering is strict, as the state s'' of (33) shows, since an event going on since tLB₂ need not have been going on since an earlier tLB₁. The counterexample takes the boundaries 0 and 2, speech time 4, and an event running over [1, 5].