Theory-Neutral Temporal Infrastructure

@cite{allen-1983} @cite{champollion-2015} @cite{fox-hackl-2006} @cite{kamp-reyle-1993} @cite{klein-1994} @cite{kratzer-1989} @cite{rouillard-2026} @cite{zhao-2025} @cite{smith-1991}

Framework-agnostic types for temporal reasoning: intervals, temporal relations, situations (world–time pairs), and concrete time instances.

These definitions are used across truth-conditional semantics, event semantics, dynamic semantics, and intensional semantics. The theory-specific layer (branching time, temporal propositions) remains in Theories/Semantics.Montague/Core/Time.

Key Concepts

1. Times as primitives (intervals or instants)
2. Situations as world-time pairs
3. Temporal relations (precedence, overlap, containment)
4. Atomic distributivity (subinterval property, @cite{zhao-2025})

structure Core.Situation (W : Type u_1) (Time : Type u_2) : Type (max u_1 u_2)

A situation is a part of a world at a time.

Following Kratzer's situation semantics:

• Situations are "slices" of possible worlds
• They have both spatial and temporal extent
• They can be minimal witnesses for propositions

We model situations as world–time pairs, abstracting from spatial extent. This is the most basic composition of ontological primitives.

• world : W

  The world this situation is part of

• time : Time

  The temporal coordinate of the situation

def Core.instReprSituation.repr {W✝ : Type u_1} {Time✝ : Type u_2} [Repr W✝] [Repr Time✝] : Situation W✝ Time✝ → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Core.instReprSituation {W✝ : Type u_1} {Time✝ : Type u_2} [Repr W✝] [Repr Time✝] : Repr (Situation W✝ Time✝)

Equations

• Core.instReprSituation = { reprPrec := Core.instReprSituation.repr }

class Core.Time.TimeStructure (Time : Type u_1) extends LinearOrder Time : Type u_1

Abstract time type.

We keep this polymorphic to allow:

• Discrete times (ℕ, ℤ)
• Dense times (ℚ, ℝ)
• Abstract/opaque times

The key requirement is a linear order for temporal relations.

• le : Time → Time → Prop
• lt : Time → Time → Prop
• le_refl (a : Time) : a ≤ a
• le_trans (a b c : Time) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : Time) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : Time) : a ≤ b → b ≤ a → a = b
• min : Time → Time → Time
• max : Time → Time → Time
• compare : Time → Time → Ordering
• le_total (a b : Time) : a ≤ b ∨ b ≤ a
• toDecidableLE : DecidableLE Time
• toDecidableEq : DecidableEq Time
• toDecidableLT : DecidableLT Time
• min_def (a b : Time) : min a b = if a ≤ b then a else b
• max_def (a b : Time) : max a b = if a ≤ b then b else a
• compare_eq_compareOfLessAndEq (a b : Time) : compare a b = compareOfLessAndEq a b

structure Core.Time.Interval (Time : Type u_1) [LE Time] : Type u_1

Temporal interval: a pair of times [start, end].

Following standard interval semantics.

• start : Time
• finish : Time
• valid : self.start ≤ self.finish

def Core.Time.Interval.point {Time : Type u_1} [LinearOrder Time] (t : Time) : Interval Time

Point interval: start = finish

Equations

• Core.Time.Interval.point t = { start := t, finish := t, valid := ⋯ }

def Core.Time.Interval.contains {Time : Type u_1} [LinearOrder Time] (i : Interval Time) (t : Time) : Prop

Does time t fall within interval i?

Equations

• i.contains t = (i.start ≤ t ∧ t ≤ i.finish)

def Core.Time.Interval.containsB {Time : Type u_1} [LinearOrder Time] [DecidableRel fun (x1 x2 : Time) => x1 ≤ x2] (i : Interval Time) (t : Time) : Bool

Decidable containment for computational use

Equations

• i.containsB t = (decide (i.start ≤ t) && decide (t ≤ i.finish))

def Core.Time.Interval.subinterval {Time : Type u_1} [LinearOrder Time] (i₁ i₂ : Interval Time) : Prop

Interval i₁ is contained in i₂

Equations

• i₁.subinterval i₂ = (i₂.start ≤ i₁.start ∧ i₁.finish ≤ i₂.finish)

def Core.Time.Interval.overlaps {Time : Type u_1} [LinearOrder Time] (i₁ i₂ : Interval Time) : Prop

Intervals overlap

Equations

• i₁.overlaps i₂ = (i₁.start ≤ i₂.finish ∧ i₂.start ≤ i₁.finish)

def Core.Time.Interval.precedes {Time : Type u_1} [LinearOrder Time] (i₁ i₂ : Interval Time) : Prop

i₁ precedes i₂ (no overlap, i₁ entirely before i₂)

Equations

• i₁.precedes i₂ = (i₁.finish < i₂.start)

def Core.Time.Interval.meets {Time : Type u_1} [LinearOrder Time] (i₁ i₂ : Interval Time) : Prop

i₁ meets i₂ (i₁ ends exactly when i₂ starts)

Equations

• i₁.meets i₂ = (i₁.finish = i₂.start)

def Core.Time.Interval.properSubinterval {Time : Type u_1} [LinearOrder Time] (i₁ i₂ : Interval Time) : Prop

Proper subinterval: i₁ ⊆ i₂ with at least one strict boundary. Required for IMPF: reference time PROPERLY inside event runtime.

Equations

• i₁.properSubinterval i₂ = (i₁.subinterval i₂ ∧ (i₂.start < i₁.start ∨ i₁.finish < i₂.finish))

def Core.Time.Interval.isAfter {Time : Type u_1} [LinearOrder Time] (i₁ i₂ : Interval Time) : Prop

i₁ is entirely after i₂ (i₁ starts at or after i₂ finishes).

Equations

• i₁.isAfter i₂ = (i₂.finish ≤ i₁.start)

def Core.Time.Interval.isBefore {Time : Type u_1} [LinearOrder Time] (i₁ i₂ : Interval Time) : Prop

i₁ is entirely before i₂.

Equations

• i₁.isBefore i₂ = (i₁.finish ≤ i₂.start)

theorem Core.Time.Interval.properSub_implies_sub {Time : Type u_1} [LinearOrder Time] (i₁ i₂ : Interval Time) (h : i₁.properSubinterval i₂) : i₁.subinterval i₂

@[simp]

theorem Core.Time.Interval.subinterval_refl {Time : Type u_1} [LinearOrder Time] (i : Interval Time) : i.subinterval i

theorem Core.Time.Interval.properSubinterval_irrefl {Time : Type u_1} [LinearOrder Time] (i : Interval Time) : ¬i.properSubinterval i

No interval is properly contained in itself.

theorem Core.Time.Interval.isAfter_iff_isBefore {Time : Type u_1} [LinearOrder Time] (i₁ i₂ : Interval Time) : i₁.isAfter i₂ ↔ i₂.isBefore i₁

def Core.Time.Interval.finalSubinterval {Time : Type u_1} [LinearOrder Time] (i₁ i₂ : Interval Time) : Prop

Final subinterval: i₁ ⊆ i₂ and they share the same right endpoint. @cite{pancheva-2003}: PTS(i', i) iff i is a final subinterval of i'.

Equations

• i₁.finalSubinterval i₂ = (i₁.subinterval i₂ ∧ i₁.finish = i₂.finish)

def Core.Time.Interval.initialOverlap {Time : Type u_1} [LinearOrder Time] (i₁ i₂ : Interval Time) : Prop

Initial overlap (∂): i₁ and i₂ overlap, and the start of i₂ is in i₁. @cite{pancheva-2003}: i ∂τ(e) — the beginning of the eventuality is included in the reference interval but the end may not be. Used for NEUTRAL viewpoint aspect.

Equations

• i₁.initialOverlap i₂ = (i₁.overlaps i₂ ∧ i₁.contains i₂.start)

theorem Core.Time.Interval.finalSub_implies_sub {Time : Type u_1} [LinearOrder Time] (i₁ i₂ : Interval Time) (h : i₁.finalSubinterval i₂) : i₁.subinterval i₂

Final subinterval implies subinterval.

theorem Core.Time.Interval.finalSubinterval_refl {Time : Type u_1} [LinearOrder Time] (i : Interval Time) : i.finalSubinterval i

Every interval is a final subinterval of itself.

inductive Core.Time.Interval.BoundaryType : Type

Whether an interval's boundary is included (closed) or excluded (open). @cite{rouillard-2026} §2.2.4: the distinction between closed and open times is central to deriving the polarity sensitivity of G-TIAs. Event runtimes are closed; PTSs are open intervals.

• closed : BoundaryType
• open_ : BoundaryType

instance Core.Time.Interval.instDecidableEqBoundaryType : DecidableEq BoundaryType

Equations

• Core.Time.Interval.instDecidableEqBoundaryType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Core.Time.Interval.instReprBoundaryType : Repr BoundaryType

Equations

• Core.Time.Interval.instReprBoundaryType = { reprPrec := Core.Time.Interval.instReprBoundaryType.repr }

def Core.Time.Interval.instReprBoundaryType.repr : BoundaryType → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Core.Time.Interval.instBEqBoundaryType : BEq BoundaryType

Equations

• Core.Time.Interval.instBEqBoundaryType = { beq := Core.Time.Interval.instBEqBoundaryType.beq }

def Core.Time.Interval.instBEqBoundaryType.beq : BoundaryType → BoundaryType → Bool

Equations

• Core.Time.Interval.instBEqBoundaryType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure Core.Time.Interval.GInterval (Time : Type u_2) [LE Time] : Type u_2

A generalized interval with specified boundary types. Extends the basic Interval with open/closed annotations on each end. @cite{rouillard-2026} eq. (14a–b), (99a–b).

• left : Time

  Left endpoint

• right : Time

  Right endpoint

• leftType : BoundaryType

  Left boundary type: closed [m or open]m

• rightType : BoundaryType

  Right boundary type: closed m] or open m[

• valid : self.left ≤ self.right

  The endpoints are ordered

def Core.Time.Interval.GInterval.closed {Time : Type u_2} [LinearOrder Time] (i : Interval Time) : GInterval Time

A closed interval [m₁, m₂]: both endpoints included. @cite{rouillard-2026} eq. (14a): C := {t | min(t) ⊑ᵢ t ∧ max(t) ⊑ᵢ t}.

Equations

• One or more equations did not get rendered due to their size.

def Core.Time.Interval.GInterval.open_ {Time : Type u_2} [LinearOrder Time] (i : Interval Time) : GInterval Time

An open interval]m₁, m₂[: both endpoints excluded. @cite{rouillard-2026} eq. (14b): O := {t | min(t) ⊄ᵢ t ∨ max(t) ⊄ᵢ t}.

Equations

• Core.Time.Interval.GInterval.open_ i = { left := i.start, right := i.finish, leftType := Core.Time.Interval.BoundaryType.open_, rightType := Core.Time.Interval.BoundaryType.open_, valid := ⋯ }

def Core.Time.Interval.GInterval.toOpen {Time : Type u_2} [LinearOrder Time] (gi : GInterval Time) : GInterval Time

The o(t) operation: open counterpart of a time. @cite{rouillard-2026} eq. (99a): if t is open, o(t) = t; if t is closed, o(t) is the open interval with the same endpoints.

Equations

• gi.toOpen = { left := gi.left, right := gi.right, leftType := Core.Time.Interval.BoundaryType.open_, rightType := Core.Time.Interval.BoundaryType.open_, valid := ⋯ }

def Core.Time.Interval.GInterval.toClosed {Time : Type u_2} [LinearOrder Time] (gi : GInterval Time) : GInterval Time

The c(t) operation: closed counterpart of a time. @cite{rouillard-2026} eq. (99b): if t is closed, c(t) = t; if t is open, c(t) adds the endpoints.

Equations

• gi.toClosed = { left := gi.left, right := gi.right, leftType := Core.Time.Interval.BoundaryType.closed, rightType := Core.Time.Interval.BoundaryType.closed, valid := ⋯ }

def Core.Time.Interval.GInterval.isClosed {Time : Type u_2} [LinearOrder Time] (gi : GInterval Time) : Prop

Is this interval closed (both boundaries included)?

Equations

• gi.isClosed = (gi.leftType = Core.Time.Interval.BoundaryType.closed ∧ gi.rightType = Core.Time.Interval.BoundaryType.closed)

def Core.Time.Interval.GInterval.isOpen {Time : Type u_2} [LinearOrder Time] (gi : GInterval Time) : Prop

Is this interval open (both boundaries excluded)?

Equations

• gi.isOpen = (gi.leftType = Core.Time.Interval.BoundaryType.open_ ∧ gi.rightType = Core.Time.Interval.BoundaryType.open_)

def Core.Time.Interval.GInterval.gcontains {Time : Type u_2} [LinearOrder Time] (gi : GInterval Time) (m : Time) : Prop

Containment for generalized intervals: m is in gi. For closed endpoints, ≤ is used; for open endpoints, <.

Equations

• One or more equations did not get rendered due to their size.

def Core.Time.Interval.GInterval.gsubinterval {Time : Type u_2} [LinearOrder Time] (gi₁ gi₂ : GInterval Time) : Prop

Generalized subinterval: gi₁ ⊆ gi₂ (every moment in gi₁ is in gi₂).

Equations

• gi₁.gsubinterval gi₂ = ∀ (m : Time), gi₁.gcontains m → gi₂.gcontains m

def Core.Time.Interval.GInterval.toInterval {Time : Type u_2} [LinearOrder Time] (gi : GInterval Time) : Interval Time

Convert a closed GInterval back to the basic Interval type.

Equations

• gi.toInterval = { start := gi.left, finish := gi.right, valid := ⋯ }

@[simp]

theorem Core.Time.Interval.GInterval.toClosed_isClosed {Time : Type u_2} [LinearOrder Time] (gi : GInterval Time) : gi.toClosed.isClosed

The closed counterpart of an open interval is always closed.

@[simp]

theorem Core.Time.Interval.GInterval.toOpen_isOpen {Time : Type u_2} [LinearOrder Time] (gi : GInterval Time) : gi.toOpen.isOpen

The open counterpart is always open.

@[simp]

theorem Core.Time.Interval.GInterval.toClosed_idempotent {Time : Type u_2} [LinearOrder Time] (gi : GInterval Time) : gi.toClosed.toClosed = gi.toClosed

toClosed is idempotent.

@[simp]

theorem Core.Time.Interval.GInterval.toOpen_idempotent {Time : Type u_2} [LinearOrder Time] (gi : GInterval Time) : gi.toOpen.toOpen = gi.toOpen

toOpen is idempotent.

inductive Core.Time.SituationBoundedness : Type

Aspectual boundedness of a situation.

Whether a situation is conceptualized as having inherent boundaries:

• bounded: telic / perfective / closed (achievements, accomplishments)
• unbounded: atelic / imperfective / open (activities, states)

Cross-cuts Vendler classes and aspectual viewpoint. Used by event semantics (telicity), aspect theory (perfective/imperfective), and temporal discourse interpretation (sequential vs. simultaneous default readings).

• bounded : SituationBoundedness
• unbounded : SituationBoundedness

instance Core.Time.instDecidableEqSituationBoundedness : DecidableEq SituationBoundedness

Equations

• Core.Time.instDecidableEqSituationBoundedness x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Core.Time.instReprSituationBoundedness : Repr SituationBoundedness

Equations

• Core.Time.instReprSituationBoundedness = { reprPrec := Core.Time.instReprSituationBoundedness.repr }

def Core.Time.instReprSituationBoundedness.repr : SituationBoundedness → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Core.Time.instBEqSituationBoundedness.beq : SituationBoundedness → SituationBoundedness → Bool

Equations

• Core.Time.instBEqSituationBoundedness.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Time.instBEqSituationBoundedness : BEq SituationBoundedness

Equations

• Core.Time.instBEqSituationBoundedness = { beq := Core.Time.instBEqSituationBoundedness.beq }

def Core.Time.SituationBoundedness.toMereoTag : SituationBoundedness → Scale.MereoTag

SituationBoundedness → MereoTag: bounded = quantized, unbounded = cumulative. Bounded situations (telic/perfective) are mereologically quantized; unbounded situations (atelic/imperfective) are cumulative.

Equations

• Core.Time.SituationBoundedness.bounded.toMereoTag = Core.Scale.MereoTag.qua
• Core.Time.SituationBoundedness.unbounded.toMereoTag = Core.Scale.MereoTag.cum

instance Core.Time.instLicensingPipelineSituationBoundedness : Scale.LicensingPipeline SituationBoundedness

Equations

• Core.Time.instLicensingPipelineSituationBoundedness = { toBoundedness := fun (s : Core.Time.SituationBoundedness) => s.toMereoTag.toBoundedness }

theorem Core.Time.bounded_licensed : Scale.LicensingPipeline.isLicensed SituationBoundedness.bounded = true

theorem Core.Time.unbounded_blocked : Scale.LicensingPipeline.isLicensed SituationBoundedness.unbounded = false

inductive Core.Time.TemporalRelation : Type

Temporal relation type for tense operators.

These relate two times (typically event time and reference/speech time).

• before : TemporalRelation
• after : TemporalRelation
• overlapping : TemporalRelation
• notAfter : TemporalRelation
• notBefore : TemporalRelation

instance Core.Time.instDecidableEqTemporalRelation : DecidableEq TemporalRelation

Equations

• Core.Time.instDecidableEqTemporalRelation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Time.instReprTemporalRelation.repr : TemporalRelation → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Core.Time.instReprTemporalRelation : Repr TemporalRelation

Equations

• Core.Time.instReprTemporalRelation = { reprPrec := Core.Time.instReprTemporalRelation.repr }

instance Core.Time.instBEqTemporalRelation : BEq TemporalRelation

Equations

• Core.Time.instBEqTemporalRelation = { beq := Core.Time.instBEqTemporalRelation.beq }

def Core.Time.instBEqTemporalRelation.beq : TemporalRelation → TemporalRelation → Bool

Equations

• Core.Time.instBEqTemporalRelation.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Core.Time.TemporalRelation.eval {Time : Type u_1} [LinearOrder Time] : TemporalRelation → Time → Time → Prop

Evaluate a temporal relation on two times

Equations

• Core.Time.TemporalRelation.before.eval x✝¹ x✝ = (x✝¹ < x✝)
• Core.Time.TemporalRelation.after.eval x✝¹ x✝ = (x✝¹ > x✝)
• Core.Time.TemporalRelation.overlapping.eval x✝¹ x✝ = (x✝¹ = x✝)
• Core.Time.TemporalRelation.notAfter.eval x✝¹ x✝ = (x✝¹ ≤ x✝)
• Core.Time.TemporalRelation.notBefore.eval x✝¹ x✝ = (x✝¹ ≥ x✝)

def Core.Time.TemporalRelation.evalB {Time : Type u_1} [LinearOrder Time] [DecidableEq Time] [DecidableRel fun (x1 x2 : Time) => x1 < x2] [DecidableRel fun (x1 x2 : Time) => x1 ≤ x2] : TemporalRelation → Time → Time → Bool

Decidable evaluation

Equations

• Core.Time.TemporalRelation.before.evalB x✝¹ x✝ = decide (x✝¹ < x✝)
• Core.Time.TemporalRelation.after.evalB x✝¹ x✝ = decide (x✝¹ > x✝)
• Core.Time.TemporalRelation.overlapping.evalB x✝¹ x✝ = (x✝¹ == x✝)
• Core.Time.TemporalRelation.notAfter.evalB x✝¹ x✝ = decide (x✝¹ ≤ x✝)
• Core.Time.TemporalRelation.notBefore.evalB x✝¹ x✝ = decide (x✝¹ ≥ x✝)

instance Core.Time.instTimeStructureInt : TimeStructure ℤ

Integer times for concrete examples.

Using ℤ allows both past (negative) and future (positive) times relative to a speech time of 0.

Equations

• Core.Time.instTimeStructureInt = { toLinearOrder := Int.instLinearOrder }

def Core.Time.speechTimeZ : ℤ

Speech time at 0 by convention

Equations

• Core.Time.speechTimeZ = 0

def Core.Time.yesterdayZ : ℤ

Example: yesterday (t = -1)

Equations

• Core.Time.yesterdayZ = -1

def Core.Time.todayZ : ℤ

Example: today (t = 0)

Equations

• Core.Time.todayZ = 0

def Core.Time.tomorrowZ : ℤ

Example: tomorrow (t = 1)

Equations

• Core.Time.tomorrowZ = 1

def Core.Time.Interval.BoundaryType.toBoundedness : BoundaryType → Scale.Boundedness

Interval boundary type maps to scale boundedness. @cite{rouillard-2026}: closed runtimes correspond to closed scales (licensed); open PTSs correspond to open scales (blocked/information collapse). This is the "interval generalization": BoundaryType.closed/.open_ in Core/Time is isomorphic to Boundedness.closed/.open_ in Core/MeasurementScale.

Equations

• Core.Time.Interval.BoundaryType.closed.toBoundedness = Core.Scale.Boundedness.closed
• Core.Time.Interval.BoundaryType.open_.toBoundedness = Core.Scale.Boundedness.open_

theorem Core.Time.closedBoundary_licensed : Interval.BoundaryType.closed.toBoundedness.isLicensed = true

theorem Core.Time.openBoundary_blocked : Interval.BoundaryType.open_.toBoundedness.isLicensed = false

instance Core.Time.instLicensingPipelineBoundaryType : Scale.LicensingPipeline Interval.BoundaryType

Equations

• Core.Time.instLicensingPipelineBoundaryType = { toBoundedness := Core.Time.Interval.BoundaryType.toBoundedness }

@[reducible, inline]

abbrev Core.Time.EvQuant (Event : Type u_1) : Type u_1

An event quantifier: a predicate on event predicates. V(P) holds iff "there is an event satisfying P" according to V's quantificational force.

Equations

• Core.Time.EvQuant Event = ((Event → Prop) → Prop)

def Core.Time.AtomDist {Event : Type u_1} {α : Type u_2} [LinearOrder α] (τ : Event → Interval α) (V : EvQuant Event) : Prop

ATOM-DIST_α (@cite{zhao-2025}, Def. 5.3): an event quantifier V satisfies ATOM-DIST with respect to trace function τ iff for every event predicate P and subinterval i' of τ(e), V also holds for the restriction of P to events whose trace is i'.

Formally: V(P) → ∀ e, P(e) → ∀ i', subinterval(i', τ(e)) → V(λ e'. P(e') ∧ τ(e') = i')

This captures the subinterval property parameterized over any linearly ordered dimension α.

Equations

• Core.Time.AtomDist τ V = ∀ (P : Event → Prop), V P → ∀ (e : Event), P e → ∀ (i' : Core.Time.Interval α), i'.subinterval (τ e) → V fun (e' : Event) => P e' ∧ τ e' = i'

@[reducible, inline]

abbrev Core.Time.AtomDist_t {Event : Type u_1} {Time : Type u_2} [LinearOrder Time] (τ_t : Event → Interval Time) (V : EvQuant Event) : Prop

ATOM-DIST_t: temporal atomic distributivity. Abbreviation for ATOM-DIST with respect to a temporal trace.

Equations

• Core.Time.AtomDist_t τ_t V = Core.Time.AtomDist τ_t V

@[reducible, inline]

abbrev Core.Time.AtomDist_d {Event : Type u_1} {Deg : Type u_2} [LinearOrder Deg] (τ_d : Event → Interval Deg) (V : EvQuant Event) : Prop

ATOM-DIST_d: degree atomic distributivity. Abbreviation for ATOM-DIST with respect to a degree trace.

Equations

• Core.Time.AtomDist_d τ_d V = Core.Time.AtomDist τ_d V

def Core.Time.antiAtomDistLicensed {Event : Type u_1} {α : Type u_2} [LinearOrder α] (τ : Event → Interval α) (V : EvQuant Event) : Prop

NOT-ATOM-DIST_α licensing condition: A particle is licensed by an event quantifier V (w.r.t. trace τ) iff V does NOT satisfy ATOM-DIST_α. This is the presupposition of Mandarin le and mei-you.

Equations

• Core.Time.antiAtomDistLicensed τ V = ¬Core.Time.AtomDist τ V