inductive Semantics.Tense.Aspect.LexicalAspect.Telicity : Type

Telicity: whether an event has a natural endpoint.

• telic : Telicity
• atelic : Telicity

instance Semantics.Tense.Aspect.LexicalAspect.instDecidableEqTelicity : DecidableEq Telicity

Equations

• Semantics.Tense.Aspect.LexicalAspect.instDecidableEqTelicity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Tense.Aspect.LexicalAspect.instReprTelicity : Repr Telicity

Equations

• Semantics.Tense.Aspect.LexicalAspect.instReprTelicity = { reprPrec := Semantics.Tense.Aspect.LexicalAspect.instReprTelicity.repr }

def Semantics.Tense.Aspect.LexicalAspect.instReprTelicity.repr : Telicity → ℕ → Std.Format

Equations

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

def Semantics.Tense.Aspect.LexicalAspect.instBEqTelicity.beq : Telicity → Telicity → Bool

Equations

• Semantics.Tense.Aspect.LexicalAspect.instBEqTelicity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Tense.Aspect.LexicalAspect.instBEqTelicity : BEq Telicity

Equations

• Semantics.Tense.Aspect.LexicalAspect.instBEqTelicity = { beq := Semantics.Tense.Aspect.LexicalAspect.instBEqTelicity.beq }

def Semantics.Tense.Aspect.LexicalAspect.instInhabitedTelicity.default : Telicity

Equations

• Semantics.Tense.Aspect.LexicalAspect.instInhabitedTelicity.default = Semantics.Tense.Aspect.LexicalAspect.Telicity.telic

instance Semantics.Tense.Aspect.LexicalAspect.instInhabitedTelicity : Inhabited Telicity

Equations

• Semantics.Tense.Aspect.LexicalAspect.instInhabitedTelicity = { default := Semantics.Tense.Aspect.LexicalAspect.instInhabitedTelicity.default }

inductive Semantics.Tense.Aspect.LexicalAspect.Duration : Type

Duration: whether an event takes time or is instantaneous.

• durative : Duration
• punctual : Duration

instance Semantics.Tense.Aspect.LexicalAspect.instDecidableEqDuration : DecidableEq Duration

Equations

• Semantics.Tense.Aspect.LexicalAspect.instDecidableEqDuration x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Tense.Aspect.LexicalAspect.instReprDuration : Repr Duration

Equations

• Semantics.Tense.Aspect.LexicalAspect.instReprDuration = { reprPrec := Semantics.Tense.Aspect.LexicalAspect.instReprDuration.repr }

def Semantics.Tense.Aspect.LexicalAspect.instReprDuration.repr : Duration → ℕ → Std.Format

Equations

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

def Semantics.Tense.Aspect.LexicalAspect.instBEqDuration.beq : Duration → Duration → Bool

Equations

• Semantics.Tense.Aspect.LexicalAspect.instBEqDuration.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Tense.Aspect.LexicalAspect.instBEqDuration : BEq Duration

Equations

• Semantics.Tense.Aspect.LexicalAspect.instBEqDuration = { beq := Semantics.Tense.Aspect.LexicalAspect.instBEqDuration.beq }

def Semantics.Tense.Aspect.LexicalAspect.instInhabitedDuration.default : Duration

Equations

• Semantics.Tense.Aspect.LexicalAspect.instInhabitedDuration.default = Semantics.Tense.Aspect.LexicalAspect.Duration.durative

instance Semantics.Tense.Aspect.LexicalAspect.instInhabitedDuration : Inhabited Duration

Equations

• Semantics.Tense.Aspect.LexicalAspect.instInhabitedDuration = { default := Semantics.Tense.Aspect.LexicalAspect.instInhabitedDuration.default }

inductive Semantics.Tense.Aspect.LexicalAspect.Dynamicity : Type

Dynamicity: whether the event involves change.

• dynamic : Dynamicity
• stative : Dynamicity

instance Semantics.Tense.Aspect.LexicalAspect.instDecidableEqDynamicity : DecidableEq Dynamicity

Equations

• Semantics.Tense.Aspect.LexicalAspect.instDecidableEqDynamicity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Tense.Aspect.LexicalAspect.instReprDynamicity.repr : Dynamicity → ℕ → Std.Format

Equations

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

instance Semantics.Tense.Aspect.LexicalAspect.instReprDynamicity : Repr Dynamicity

Equations

• Semantics.Tense.Aspect.LexicalAspect.instReprDynamicity = { reprPrec := Semantics.Tense.Aspect.LexicalAspect.instReprDynamicity.repr }

def Semantics.Tense.Aspect.LexicalAspect.instBEqDynamicity.beq : Dynamicity → Dynamicity → Bool

Equations

• Semantics.Tense.Aspect.LexicalAspect.instBEqDynamicity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Tense.Aspect.LexicalAspect.instBEqDynamicity : BEq Dynamicity

Equations

• Semantics.Tense.Aspect.LexicalAspect.instBEqDynamicity = { beq := Semantics.Tense.Aspect.LexicalAspect.instBEqDynamicity.beq }

def Semantics.Tense.Aspect.LexicalAspect.instInhabitedDynamicity.default : Dynamicity

Equations

• Semantics.Tense.Aspect.LexicalAspect.instInhabitedDynamicity.default = Semantics.Tense.Aspect.LexicalAspect.Dynamicity.dynamic

instance Semantics.Tense.Aspect.LexicalAspect.instInhabitedDynamicity : Inhabited Dynamicity

Equations

• Semantics.Tense.Aspect.LexicalAspect.instInhabitedDynamicity = { default := Semantics.Tense.Aspect.LexicalAspect.instInhabitedDynamicity.default }

def Semantics.Tense.Aspect.LexicalAspect.Telicity.toMereoTag : Telicity → Core.Scale.MereoTag

Telicity → MereoTag: telic = quantized. Telic predicates are QUA (no proper part of a telic event is telic); atelic predicates are CUM (the sum of two atelic events is atelic).

Equations

• Semantics.Tense.Aspect.LexicalAspect.Telicity.telic.toMereoTag = Core.Scale.MereoTag.qua
• Semantics.Tense.Aspect.LexicalAspect.Telicity.atelic.toMereoTag = Core.Scale.MereoTag.cum

inductive Semantics.Tense.Aspect.LexicalAspect.VendlerClass : Type

Vendler's four-way classification of eventualities.

• state : VendlerClass
• activity : VendlerClass
• achievement : VendlerClass
• accomplishment : VendlerClass

instance Semantics.Tense.Aspect.LexicalAspect.instDecidableEqVendlerClass : DecidableEq VendlerClass

Equations

• Semantics.Tense.Aspect.LexicalAspect.instDecidableEqVendlerClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Tense.Aspect.LexicalAspect.instReprVendlerClass.repr : VendlerClass → ℕ → Std.Format

Equations

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

instance Semantics.Tense.Aspect.LexicalAspect.instReprVendlerClass : Repr VendlerClass

Equations

• Semantics.Tense.Aspect.LexicalAspect.instReprVendlerClass = { reprPrec := Semantics.Tense.Aspect.LexicalAspect.instReprVendlerClass.repr }

def Semantics.Tense.Aspect.LexicalAspect.instBEqVendlerClass.beq : VendlerClass → VendlerClass → Bool

Equations

• Semantics.Tense.Aspect.LexicalAspect.instBEqVendlerClass.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Tense.Aspect.LexicalAspect.instBEqVendlerClass : BEq VendlerClass

Equations

• Semantics.Tense.Aspect.LexicalAspect.instBEqVendlerClass = { beq := Semantics.Tense.Aspect.LexicalAspect.instBEqVendlerClass.beq }

instance Semantics.Tense.Aspect.LexicalAspect.instInhabitedVendlerClass : Inhabited VendlerClass

Equations

• Semantics.Tense.Aspect.LexicalAspect.instInhabitedVendlerClass = { default := Semantics.Tense.Aspect.LexicalAspect.instInhabitedVendlerClass.default }

def Semantics.Tense.Aspect.LexicalAspect.instInhabitedVendlerClass.default : VendlerClass

Equations

• Semantics.Tense.Aspect.LexicalAspect.instInhabitedVendlerClass.default = Semantics.Tense.Aspect.LexicalAspect.VendlerClass.state

def Semantics.Tense.Aspect.LexicalAspect.VendlerClass.telicity : VendlerClass → Telicity

Get the telicity of a Vendler class (states treated as atelic).

Equations

• Semantics.Tense.Aspect.LexicalAspect.VendlerClass.state.telicity = Semantics.Tense.Aspect.LexicalAspect.Telicity.atelic
• Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity.telicity = Semantics.Tense.Aspect.LexicalAspect.Telicity.atelic
• Semantics.Tense.Aspect.LexicalAspect.VendlerClass.achievement.telicity = Semantics.Tense.Aspect.LexicalAspect.Telicity.telic
• Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment.telicity = Semantics.Tense.Aspect.LexicalAspect.Telicity.telic

def Semantics.Tense.Aspect.LexicalAspect.VendlerClass.duration : VendlerClass → Duration

Get the duration of a Vendler class.

Equations

• Semantics.Tense.Aspect.LexicalAspect.VendlerClass.state.duration = Semantics.Tense.Aspect.LexicalAspect.Duration.durative
• Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity.duration = Semantics.Tense.Aspect.LexicalAspect.Duration.durative
• Semantics.Tense.Aspect.LexicalAspect.VendlerClass.achievement.duration = Semantics.Tense.Aspect.LexicalAspect.Duration.punctual
• Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment.duration = Semantics.Tense.Aspect.LexicalAspect.Duration.durative

def Semantics.Tense.Aspect.LexicalAspect.VendlerClass.dynamicity : VendlerClass → Dynamicity

Get the dynamicity of a Vendler class.

Equations

• Semantics.Tense.Aspect.LexicalAspect.VendlerClass.state.dynamicity = Semantics.Tense.Aspect.LexicalAspect.Dynamicity.stative
• Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity.dynamicity = Semantics.Tense.Aspect.LexicalAspect.Dynamicity.dynamic
• Semantics.Tense.Aspect.LexicalAspect.VendlerClass.achievement.dynamicity = Semantics.Tense.Aspect.LexicalAspect.Dynamicity.dynamic
• Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment.dynamicity = Semantics.Tense.Aspect.LexicalAspect.Dynamicity.dynamic

theorem Semantics.Tense.Aspect.LexicalAspect.state_is_stative : VendlerClass.state.dynamicity = Dynamicity.stative

States are stative.

theorem Semantics.Tense.Aspect.LexicalAspect.activity_is_atelic : VendlerClass.activity.telicity = Telicity.atelic

Activities are atelic.

theorem Semantics.Tense.Aspect.LexicalAspect.activity_is_durative : VendlerClass.activity.duration = Duration.durative

Activities are durative.

theorem Semantics.Tense.Aspect.LexicalAspect.achievement_is_punctual : VendlerClass.achievement.duration = Duration.punctual

Achievements are punctual.

theorem Semantics.Tense.Aspect.LexicalAspect.achievement_is_telic : VendlerClass.achievement.telicity = Telicity.telic

Achievements are telic.

theorem Semantics.Tense.Aspect.LexicalAspect.accomplishment_is_telic : VendlerClass.accomplishment.telicity = Telicity.telic

Accomplishments are telic.

theorem Semantics.Tense.Aspect.LexicalAspect.accomplishment_is_durative : VendlerClass.accomplishment.duration = Duration.durative

Accomplishments are durative.

theorem Semantics.Tense.Aspect.LexicalAspect.dynamic_classes_are_dynamic (c : VendlerClass) : c ≠ VendlerClass.state → c.dynamicity = Dynamicity.dynamic

All dynamic classes involve change.

theorem Semantics.Tense.Aspect.LexicalAspect.telic_classes (c : VendlerClass) : c.telicity = Telicity.telic ↔ c = VendlerClass.achievement ∨ c = VendlerClass.accomplishment

All telic classes have endpoints.

structure Semantics.Tense.Aspect.LexicalAspect.AspectualProfile : Type

An aspectual profile bundles telicity, duration, and dynamicity.

• telicity : Telicity

  Whether the eventuality has a natural endpoint

• duration : Duration

  Whether the eventuality takes time

• dynamicity : Dynamicity

  Whether the eventuality involves change

instance Semantics.Tense.Aspect.LexicalAspect.instDecidableEqAspectualProfile : DecidableEq AspectualProfile

Equations

• Semantics.Tense.Aspect.LexicalAspect.instDecidableEqAspectualProfile = Semantics.Tense.Aspect.LexicalAspect.instDecidableEqAspectualProfile.decEq

def Semantics.Tense.Aspect.LexicalAspect.instDecidableEqAspectualProfile.decEq (x✝ x✝¹ : AspectualProfile) : Decidable (x✝ = x✝¹)

Equations

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

instance Semantics.Tense.Aspect.LexicalAspect.instReprAspectualProfile : Repr AspectualProfile

Equations

• Semantics.Tense.Aspect.LexicalAspect.instReprAspectualProfile = { reprPrec := Semantics.Tense.Aspect.LexicalAspect.instReprAspectualProfile.repr }

def Semantics.Tense.Aspect.LexicalAspect.instReprAspectualProfile.repr : AspectualProfile → ℕ → Std.Format

Equations

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

def Semantics.Tense.Aspect.LexicalAspect.instBEqAspectualProfile.beq : AspectualProfile → AspectualProfile → Bool

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Tense.Aspect.LexicalAspect.instBEqAspectualProfile.beq x✝¹ x✝ = false

instance Semantics.Tense.Aspect.LexicalAspect.instBEqAspectualProfile : BEq AspectualProfile

Equations

• Semantics.Tense.Aspect.LexicalAspect.instBEqAspectualProfile = { beq := Semantics.Tense.Aspect.LexicalAspect.instBEqAspectualProfile.beq }

def Semantics.Tense.Aspect.LexicalAspect.AspectualProfile.toVendlerClass (p : AspectualProfile) : VendlerClass

Convert an aspectual profile to a Vendler class (semelfactives mapped to activity).

Equations

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

def Semantics.Tense.Aspect.LexicalAspect.VendlerClass.toProfile (c : VendlerClass) : AspectualProfile

Convert a Vendler class to its canonical aspectual profile.

Equations

• c.toProfile = { telicity := c.telicity, duration := c.duration, dynamicity := c.dynamicity }

def Semantics.Tense.Aspect.LexicalAspect.stateProfile : AspectualProfile

Canonical profile for states.

Equations

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

def Semantics.Tense.Aspect.LexicalAspect.activityProfile : AspectualProfile

Canonical profile for activities.

Equations

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

def Semantics.Tense.Aspect.LexicalAspect.achievementProfile : AspectualProfile

Canonical profile for achievements.

Equations

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

def Semantics.Tense.Aspect.LexicalAspect.accomplishmentProfile : AspectualProfile

Canonical profile for accomplishments.

Equations

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

theorem Semantics.Tense.Aspect.LexicalAspect.vendler_profile_roundtrip (c : VendlerClass) : c.toProfile.toVendlerClass = c

Converting a Vendler class to a profile and back is identity.

theorem Semantics.Tense.Aspect.LexicalAspect.stateProfile_toClass : stateProfile.toVendlerClass = VendlerClass.state

The canonical state profile maps to the state class.

theorem Semantics.Tense.Aspect.LexicalAspect.activityProfile_toClass : activityProfile.toVendlerClass = VendlerClass.activity

The canonical activity profile maps to the activity class.

theorem Semantics.Tense.Aspect.LexicalAspect.achievementProfile_toClass : achievementProfile.toVendlerClass = VendlerClass.achievement

The canonical achievement profile maps to the achievement class.

theorem Semantics.Tense.Aspect.LexicalAspect.accomplishmentProfile_toClass : accomplishmentProfile.toVendlerClass = VendlerClass.accomplishment

The canonical accomplishment profile maps to the accomplishment class.

def Semantics.Tense.Aspect.LexicalAspect.AspectualProfile.telicize (p : AspectualProfile) : AspectualProfile

Telicize: add a natural endpoint to an atelic predicate.

Equations

• p.telicize = { telicity := Semantics.Tense.Aspect.LexicalAspect.Telicity.telic, duration := p.duration, dynamicity := p.dynamicity }

def Semantics.Tense.Aspect.LexicalAspect.AspectualProfile.atelicize (p : AspectualProfile) : AspectualProfile

Atelicize: remove the natural endpoint (progressive effect).

Equations

• p.atelicize = { telicity := Semantics.Tense.Aspect.LexicalAspect.Telicity.atelic, duration := p.duration, dynamicity := p.dynamicity }

def Semantics.Tense.Aspect.LexicalAspect.AspectualProfile.duratize (p : AspectualProfile) : AspectualProfile

Duratize: stretch a punctual event over time (iterative).

Equations

• p.duratize = { telicity := p.telicity, duration := Semantics.Tense.Aspect.LexicalAspect.Duration.durative, dynamicity := p.dynamicity }

def Semantics.Tense.Aspect.LexicalAspect.AspectualProfile.statify (p : AspectualProfile) : AspectualProfile

Statify: convert to a stative reading.

Equations

• p.statify = { telicity := p.telicity, duration := p.duration, dynamicity := Semantics.Tense.Aspect.LexicalAspect.Dynamicity.stative }

theorem Semantics.Tense.Aspect.LexicalAspect.telicize_activity : activityProfile.telicize.toVendlerClass = VendlerClass.accomplishment

Telicizing an activity yields an accomplishment.

theorem Semantics.Tense.Aspect.LexicalAspect.atelicize_accomplishment : accomplishmentProfile.atelicize.toVendlerClass = VendlerClass.activity

Atelicizing an accomplishment yields an activity.

theorem Semantics.Tense.Aspect.LexicalAspect.duratize_achievement : achievementProfile.duratize.toVendlerClass = VendlerClass.accomplishment

Duratizing an achievement yields an accomplishment.

theorem Semantics.Tense.Aspect.LexicalAspect.telicize_idempotent (p : AspectualProfile) : p.telicize.telicize = p.telicize

Telicize is idempotent.

theorem Semantics.Tense.Aspect.LexicalAspect.atelicize_idempotent (p : AspectualProfile) : p.atelicize.atelicize = p.atelicize

Atelicize is idempotent.

def Semantics.Tense.Aspect.LexicalAspect.AspectualProfile.isHomogeneous (p : AspectualProfile) : Bool

Whether a predicate is homogeneous (has the subinterval property).

Equations

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

theorem Semantics.Tense.Aspect.LexicalAspect.state_is_homogeneous : stateProfile.isHomogeneous = true

States are homogeneous.

theorem Semantics.Tense.Aspect.LexicalAspect.activity_is_homogeneous : activityProfile.isHomogeneous = true

Activities are homogeneous.

theorem Semantics.Tense.Aspect.LexicalAspect.achievement_not_homogeneous : achievementProfile.isHomogeneous = false

Achievements are not homogeneous.

theorem Semantics.Tense.Aspect.LexicalAspect.accomplishment_not_homogeneous : accomplishmentProfile.isHomogeneous = false

Accomplishments are not homogeneous.

theorem Semantics.Tense.Aspect.LexicalAspect.homogeneous_iff_atelic (p : AspectualProfile) : p.isHomogeneous = true ↔ p.toVendlerClass.telicity = Telicity.atelic

Homogeneous iff atelic.

def Semantics.Tense.Aspect.LexicalAspect.VendlerClass.predictsAtomDist : VendlerClass → Bool

Whether a VendlerClass predicts ATOM-DIST_t (@cite{zhao-2025}, Def. 5.3). States satisfy ATOM-DIST_t (distribute over temporal subintervals); dynamic classes do not. Stricter than isHomogeneous: activities are homogeneous but fail ATOM-DIST_t.

• Zhao, Z. (2025). Cross-Linguistic and Cross-Domain Temporal Expressions. NYU dissertation, Ch. 5.

Equations

• Semantics.Tense.Aspect.LexicalAspect.VendlerClass.state.predictsAtomDist = true
• Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity.predictsAtomDist = false
• Semantics.Tense.Aspect.LexicalAspect.VendlerClass.achievement.predictsAtomDist = false
• Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment.predictsAtomDist = false

theorem Semantics.Tense.Aspect.LexicalAspect.predictsAtomDist_iff_stative (c : VendlerClass) : c.predictsAtomDist = true ↔ c.dynamicity = Dynamicity.stative

ATOM-DIST_t prediction coincides with stative dynamicity.

theorem Semantics.Tense.Aspect.LexicalAspect.state_predictsAtomDist : VendlerClass.state.predictsAtomDist = true

States predict ATOM-DIST_t holds.

theorem Semantics.Tense.Aspect.LexicalAspect.dynamic_predictsAtomDist_false (c : VendlerClass) (h : c.dynamicity = Dynamicity.dynamic) : c.predictsAtomDist = false

All dynamic classes predict ATOM-DIST_t failure.

theorem Semantics.Tense.Aspect.LexicalAspect.atomDist_implies_homogeneous (c : VendlerClass) (h : c.predictsAtomDist = true) : c.toProfile.isHomogeneous = true

ATOM-DIST_t implies homogeneity (but not vice versa). Activities are homogeneous but do NOT satisfy ATOM-DIST_t — this is Zhao's point: ATOM-DIST_t discriminates states from activities, while the classical subinterval property does not.

theorem Semantics.Tense.Aspect.LexicalAspect.predictsAtomDist_iff_not_dynamic (c : VendlerClass) : c.predictsAtomDist = false ↔ c.dynamicity = Dynamicity.dynamic

ATOM-DIST_t prediction is the negation of dynamicity =.dynamic.