Documentation

Linglib.Studies.Zhao2025

Zhao 2025: Cross-Linguistic and Cross-Domain Temporal Expressions #

Two results from [Zha25]: the VendlerClass ↔ Mandarin-particle licensing bridge, and the ⌈then⌉-present puzzle.

Mandarin particle licensing #

Lexical facts about three Mandarin particles' anti-AtomDist requirements (from Fragments/Mandarin/AspectComparison.lean). Composed with Aktionsart's dynamicity projection — which assigns .stative to exactly the .state VendlerClass — these yield the licensing pattern of [Zha25]: le and meiyou are licensed by the dynamic classes (activity / achievement / accomplishment / semelfactive); guo is licensed by every class including state.

The cross-domain bridge is the composition of two independently-decidable facts (the lexical requirement here + the dynamicity projection in Aktionsart), not a single theorem.

le.requiresAntiAtomDist = true is the Fragment-level encoding of [Zha25] Def. 5.36 (p. 165) ATOM-DIST_t at the verb-quantifier level. The substrate-side treatment lives in Core/Time/AtomDist.lean (AtomDist τ V, with EvQuant.ofPred bridging from event predicates to event quantifiers); for the witness-universal subinterval form on event predicates, see HasSubintervalProp in Semantics/Aspect/SubintervalProperty.lean. The unification: Zhao 2025's particle-licensing condition is the quantifier-level atomic-granularity stativity test along the time dimension. Bridging Fragment Bool fields to substrate Props for specific Mandarin verbs requires per-verb denotations (theory-hub denotation discipline; follow-up).

The ⌈then⌉-present puzzle #

Temporal ⌈then⌉ is cross-linguistically incompatible with the present tense: ⌈then⌉ presupposes a reference disjoint from the temporal perspective π (Tense.Perspective.thenPresup), PRES presupposes overlap with π (ReichenbachFrame.isPresent in the point approximation), and the temporal assertion ("during then") forces the PRES reference inside the ⌈then⌉ reference — so no reference satisfies both (then_present_root_clash). Deleted (SOT) tense escapes: it contributes no perspectival presupposition, and ⌈then⌉'s own presupposition is satisfiable on any nontrivial timeline (Tense.Perspective.thenPresup_satisfiable).

The attested ⌈then⌉ adverbs (thenAdverbs, from the Fragment lexicons): English then, Japanese 当時 tōji, Greek τότε tóte, Russian тогда togda, Hebrew אז az — root-clause ⌈then⌉ + PRES is ungrammatical in each. (English ⌈then⌉ with an embedded present under future is variably acceptable, an exception the paper leaves open.)

Mandarin particle licensing #

source
theorem Zhao2025.le_requires_anti_atomDist :
Mandarin.AspectComparison.le.requiresAntiAtomDist = true

le requires anti-AtomDist (a lexical-entry fact).

source
theorem Zhao2025.meiyou_requires_anti_atomDist :
Mandarin.AspectComparison.meiyou.requiresAntiAtomDist = true

meiyou requires anti-AtomDist (a lexical-entry fact).

source
theorem Zhao2025.guo_compatible_with_all :
Mandarin.AspectComparison.guo.requiresAntiAtomDist = false

guo imposes no ATOM-DIST restriction; compatible with all VendlerClasses including states.

The ⌈then⌉-present puzzle #

source
def Zhao2025.thenAdverbs :
List Tense.Perspective.ThenAdverb

The ⌈then⌉ adverbs of [Zha25]'s language sample, from the Fragment lexicons.

Equations
Instances For
    source
    theorem Zhao2025.then_present_root_clash {Time : Type u_1} [LinearOrder Time] (f : _root_.Time.ReichenbachFrame Time) (hSimple : f.isSimpleCase) (hPres : f.isPresent) :
    ¬∃ (thenRef : Time), f.referenceTime = thenRef ∧ Tense.Perspective.thenPresup thenRef f.speechTime

    Root clause ("Mary is feeling sick (*then)"): π = S, so a present-tensed clause admits no ⌈then⌉ restriction — no reference satisfies both the "during then" containment and ⌈then⌉'s disjointness from π.