Zhao (2025): Cross-Linguistic and Cross-Domain Temporal Expressions

Zhao's dissertation analyzes the Mandarin particles le, méi-yǒu and guò, which occur both with verbs, locating an event in time, and in comparatives, locating a degree on a scale. Temporal le rejects a stative predicate unless it has a duration argument, degree le rejects a comparative unless it has a measure phrase, and méi-yǒu mirrors both. Verbal projections denote quantifiers over events, an event has a trace on the timeline or on a degree scale, and the licensing condition is Atomic Distributivity: whenever the quantifier applies to the events with a trace, it applies to those with any subinterval of it as trace. Le is defined only of a quantifier that fails Atomic Distributivity, so the bare stative and the bare comparative are presupposition failures, which a duration or a measure phrase repairs.

Main definitions

• EvQuant: a quantifier over events.
• AtomDist: Atomic Distributivity.
• le: the particle le.
• meiyou: the particle méi-yǒu.

Main results

• hasSubintervalProperty_iff_forall_atomDist: for an existential quantifier, Atomic Distributivity over time is the subinterval property.
• not_atomDist_ofPred: a description without point traces fails Atomic Distributivity.
• not_le_dom_of_le: the bare stative is a presupposition failure of le.
• le_dom_of_length: a duration argument or a measure phrase licenses le.
• meiyou_dom_of_surpasses: guò licenses méi-yǒu.

Implementation notes

Times and degrees are the points of a linear order, traces its closed intervals, and a point is the interval NonemptyInterval.pure; the dissertation also admits non-convex sums of points, which its analyses do not use. The norm of (4.2.2) is defined only on proper intervals, so a duration argument is a positive NonemptyInterval.length. The particles take the measurement μ_α(a) of their evaluation argument as a point. Le is commonly called a perfective marker; the dissertation strips its temporal content down to precedence, which is the relation Aspect assigns to the perfect, le_get_iff_perfect. The first part of the dissertation, the ⌈then⌉-present puzzle, is joint work with Tsilia, formalized in Studies/TsiliaZhao2026.lean.

The library takes states and activities alike to have the subinterval property; here an activity fails it because of its minimal parts, (5.41), which is what lets le attach to activities.

References

• [Zha25]
• [Cha15]
• [BP72]
• [TZ26]

Atomic Distributivity (chapter 5)

@[reducible, inline]

abbrev Zhao2025.EvQuant (E : Type u_3) : Type u_3

A verbal projection denotes a quantifier over events, as in [Cha15].

Equations

• Zhao2025.EvQuant E = ((E → Prop) → Prop)

def Zhao2025.EvQuant.ofPred {E : Type u_1} (P : E → Prop) : EvQuant E

EvQuant.ofPred P is the existential quantifier over the events of P, the shape of (5.37).

Equations

• Zhao2025.EvQuant.ofPred P f = ∃ (e : E), P e ∧ f e

def Zhao2025.AtomDist {E : Type u_1} {α : Type u_2} [Preorder α] (τ : E → NonemptyInterval α) (V : EvQuant E) : Prop

Atomic Distributivity along the trace τ, (5.83), holds when, whenever the quantifier applies to the events with trace i, it applies to the events with trace i' for each subinterval i' of i.

Equations

• Zhao2025.AtomDist τ V = ∀ (i : NonemptyInterval α), (V fun (x : E) => τ x = i) → ∀ i' ≤ i, V fun (x : E) => τ x = i'

theorem Zhao2025.atomDist_ofPred_iff {E : Type u_1} {α : Type u_2} [Preorder α] {τ : E → NonemptyInterval α} {P : E → Prop} : AtomDist τ (EvQuant.ofPred P) ↔ IsLowerSet (τ '' {e : E | P e})

An existential quantifier is atomically distributive exactly when the traces of the described events form a lower set.

theorem Zhao2025.atomDist_ofPred_mem {E : Type u_1} {α : Type u_2} [Preorder α] {τ : E → NonemptyInterval α} (hτ : Function.Surjective τ) {S : Set (NonemptyInterval α)} (hS : IsLowerSet S) : AtomDist τ (EvQuant.ofPred fun (x : E) => τ x ∈ S)

Where every interval is a trace, a description by a lower set of traces is atomically distributive.

theorem Zhao2025.atomDist_ofPred_le {E : Type u_1} {α : Type u_2} [Preorder α] {τ : E → NonemptyInterval α} (hτ : Function.Surjective τ) (I : NonemptyInterval α) : AtomDist τ (EvQuant.ofPred fun (x : E) => τ x ≤ I)

A state that holds throughout I holds at every subinterval of I, (5.38).

theorem Zhao2025.atomDist_ofPred_lt_fst {E : Type u_1} {α : Type u_2} [Preorder α] {τ : E → NonemptyInterval α} (hτ : Function.Surjective τ) (m : α) : AtomDist τ (EvQuant.ofPred fun (e : E) => m < (τ e).toProd.1)

The degree events above a standard m, as in the bare comparative bǐ Yángjiǎn gāo 'taller than Yangjian', are atomically distributive, (5.53).

theorem Zhao2025.not_atomDist_ofPred {E : Type u_1} {α : Type u_2} [Preorder α] {τ : E → NonemptyInterval α} {P : E → Prop} (hne : ∃ (e : E), P e) (hP : ∀ (e : E), P e → ¬(τ e).IsPoint) : ¬AtomDist τ (EvQuant.ofPred P)

A description with an event, none of whose events has a point trace, is not atomically distributive, as for the non-stative classes of (5.39)–(5.41).

def Zhao2025.Surpasses {E : Type u_1} {α : Type u_2} [Preorder α] (τ : E → NonemptyInterval α) (θ : E → α) (e : E) : Prop

An event surpasses when its trace properly contains the measurement of its theme, (6.45).

Equations

• Zhao2025.Surpasses τ θ e = ((τ e).toProd.1 < θ e ∧ θ e < (τ e).toProd.2)

theorem Zhao2025.not_atomDist_ofPred_surpasses {E : Type u_1} {α : Type u_2} [Preorder α] {τ : E → NonemptyInterval α} {P : E → Prop} {θ : E → α} (hne : ∃ (e : E), P e) (hP : ∀ (e : E), P e → Surpasses τ θ e) : ¬AtomDist τ (EvQuant.ofPred P)

The quantifier over surpassing events that guò introduces, (6.44), is never atomically distributive.

theorem Zhao2025.hasSubintervalProperty_iff_forall_atomDist {E : Type u_1} {W : Type u_3} {T : Type u_4} [LinearOrder T] [Event.TemporalTrace E T] {P : W → E → Prop} : Aspect.HasSubintervalProperty P ↔ ∀ (w : W), AtomDist Event.τ (EvQuant.ofPred (P w))

A predicate of events in time has the subinterval property exactly when its existential quantifier is atomically distributive over time at every world.

theorem Zhao2025.not_atomDist_ofPred_length {E : Type u_1} {α : Type u_2} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {τ : E → NonemptyInterval α} {P : E → Prop} {d : α} (hd : 0 < d) (hne : ∃ (e : E), P e ∧ (τ e).length = d) : ¬AtomDist τ (EvQuant.ofPred fun (e : E) => P e ∧ (τ e).length = d)

A duration argument or a measure phrase gives the trace a positive length, so the description is not atomically distributive, (5.44), (5.57).

Le and méi-yǒu (chapter 6)

def Zhao2025.le {E : Type u_1} {α : Type u_2} [Preorder α] (τ : E → NonemptyInterval α) (V : EvQuant E) (p : α) : Part Prop

Le, (6.3), is defined only of a quantifier that is not atomically distributive, and asserts that it applies to the events whose trace precedes p, the measurement of the evaluation argument.

Equations

• Zhao2025.le τ V p = { Dom := ¬Zhao2025.AtomDist τ V, get := fun (x : ¬Zhao2025.AtomDist τ V) => V fun (e : E) => (τ e).IsBefore (NonemptyInterval.pure p) }

def Zhao2025.meiyou {E : Type u_1} {α : Type u_2} [Preorder α] (τ : E → NonemptyInterval α) (V : EvQuant E) (p : α) : Part Prop

Méi-yǒu, (6.18), is the negation of le, with the same presupposition.

Equations

• Zhao2025.meiyou τ V p = Part.map Not (Zhao2025.le τ V p)

@[simp]

theorem Zhao2025.le_dom {E : Type u_1} {α : Type u_2} [Preorder α] {τ : E → NonemptyInterval α} {V : EvQuant E} {p : α} : (le τ V p).Dom ↔ ¬AtomDist τ V

@[simp]

theorem Zhao2025.meiyou_dom {E : Type u_1} {α : Type u_2} [Preorder α] {τ : E → NonemptyInterval α} {V : EvQuant E} {p : α} : (meiyou τ V p).Dom ↔ ¬AtomDist τ V

@[simp]

theorem Zhao2025.le_get {E : Type u_1} {α : Type u_2} [Preorder α] {τ : E → NonemptyInterval α} {V : EvQuant E} {p : α} (h : (le τ V p).Dom) : (le τ V p).get h ↔ V fun (e : E) => (τ e).IsBefore (NonemptyInterval.pure p)

@[simp]

theorem Zhao2025.meiyou_get {E : Type u_1} {α : Type u_2} [Preorder α] {τ : E → NonemptyInterval α} {V : EvQuant E} {p : α} (h : (meiyou τ V p).Dom) : (meiyou τ V p).get h ↔ ¬(le τ V p).get h

theorem Zhao2025.not_le_dom_of_le {E : Type u_1} {α : Type u_2} [Preorder α] {τ : E → NonemptyInterval α} {p : α} (hτ : Function.Surjective τ) (I : NonemptyInterval α) : ¬(le τ (EvQuant.ofPred fun (x : E) => τ x ≤ I) p).Dom

The bare stative is a presupposition failure of le, (3.40).

theorem Zhao2025.not_le_dom_of_lt_fst {E : Type u_1} {α : Type u_2} [Preorder α] {τ : E → NonemptyInterval α} {p : α} (hτ : Function.Surjective τ) (m : α) : ¬(le τ (EvQuant.ofPred fun (e : E) => m < (τ e).toProd.1) p).Dom

The bare comparative is a presupposition failure of le, (5.46).

theorem Zhao2025.meiyou_dom_of_surpasses {E : Type u_1} {α : Type u_2} [Preorder α] {τ : E → NonemptyInterval α} {P : E → Prop} {p : α} {θ : E → α} (hne : ∃ (e : E), P e) (hP : ∀ (e : E), P e → Surpasses τ θ e) : (meiyou τ (EvQuant.ofPred P) p).Dom

Guò licenses méi-yǒu, whatever the description of the surpassing events, (6.73), (6.74).

theorem Zhao2025.le_dom_of_length {E : Type u_1} {α : Type u_2} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {τ : E → NonemptyInterval α} {P : E → Prop} {d p : α} (hd : 0 < d) (hne : ∃ (e : E), P e ∧ (τ e).length = d) : (le τ (EvQuant.ofPred fun (e : E) => P e ∧ (τ e).length = d) p).Dom

A duration argument or a measure phrase licenses le, (6.4), (6.5).

theorem Zhao2025.le_get_iff_perfect {E : Type u_1} {T : Type u_3} [LinearOrder T] {τ : E → NonemptyInterval T} {V : EvQuant E} {p : T} (h : (le τ V p).Dom) : (le τ V p).get h ↔ V fun (e : E) => Aspect.ViewpointType.perfect.ttTSitRelation (NonemptyInterval.pure p) (τ e)

The temporal content of le is precedence, the relation of the perfect between a topic time p and the time of the event.