Neo-Davidsonian Event Semantics

Foundational types and basic API for neo-Davidsonian event semantics ([Dav67], [Par90]). Verbs denote predicates of events; thematic roles are independent two-place predicates (ArgumentStructure.ThematicRel).

Main definitions

• Event — the unified event type: a runtime interval + Features.Dynamicity sort
• Event.τ — temporal trace function
• Event.isAction / Event.isState — decidable Prop sort predicates (the dynamic / stative poles of Features.Dynamicity)
• Event.isPunctual / Event.isDurative — decidable Prop duration predicates
• Event.existsClosure — Davidsonian existential closure
• Event.Mereology — part-of typeclass with τ-monotonicity + sort-preservation
• Event.partialOrder — PartialOrder instance derived from Event.Mereology
• Event.Manner — manner ontology ([Lie24] §4.3)
• exampleRun / exampleKnow — concrete Event ℤ instances

Naming note

Event is the unified type for linguistic events. The Bach 1981/1986 distinction between "eventuality" (genus, sortless) and "event" (narrow sense, non-state) has largely collapsed in current practice — [Cha17] and [Zha25] both use "event" generically with sort/aktionsart as an inherent attribute. Tense-aspect code that doesn't care about sort simply doesn't reference .sort; sortless construction sites default to .dynamic.

References

• [Dav67], [Par90] (neo-Davidsonian foundations)
• [Bac86] (action/state ontology)
• [Kri89] (interval-valued runtimes)
• [Cha17], [Zha25] (event-as-generic)
• [Lie24] §4.3 (manner ontology)

structure Event (Time : Type u_1) [LinearOrder Time] : Type u_1

An event: a temporal individual with ontological sort.

• runtime : NonemptyInterval Time

  The temporal extent of this event

• sort : Features.Dynamicity

  Ontological sort (aktionsart): dynamic or stative ([Bac86]). This is the Features.Dynamicity feature — the action/state distinction at the event-token level.

Temporal trace

def Event.τ {Time : Type u_1} [LinearOrder Time] (e : Event Time) : NonemptyInterval Time

Temporal trace function τ(e) = the runtime interval of event e.

Equations

• e.τ = e.runtime

Sort predicates

def Event.isAction {Time : Type u_1} [LinearOrder Time] (e : Event Time) : Prop

Is this event an action (dynamic event)?

Equations

• e.isAction = (e.sort = Features.Dynamicity.dynamic)

def Event.isState {Time : Type u_1} [LinearOrder Time] (e : Event Time) : Prop

Is this event a state (stative event)?

Equations

• e.isState = (e.sort = Features.Dynamicity.stative)

@[implicit_reducible]

instance Event.instDecidablePredIsAction {Time : Type u_1} [LinearOrder Time] : DecidablePred isAction

Equations

• e.instDecidablePredIsAction = decEq e.sort Features.Dynamicity.dynamic

@[implicit_reducible]

instance Event.instDecidablePredIsState {Time : Type u_1} [LinearOrder Time] : DecidablePred isState

Equations

• e.instDecidablePredIsState = decEq e.sort Features.Dynamicity.stative

theorem Event.isAction_iff_not_isState {Time : Type u_1} [LinearOrder Time] (e : Event Time) : e.isAction ↔ ¬e.isState

isAction and isState are complementary.

theorem Event.isState_iff_not_isAction {Time : Type u_1} [LinearOrder Time] (e : Event Time) : e.isState ↔ ¬e.isAction

isState and isAction are complementary.

Duration predicates

def Event.isPunctual {Time : Type u_1} [LinearOrder Time] (e : Event Time) : Prop

Is this event punctual (instantaneous)? Its runtime is a single point. The temporal-extent counterpart of the dynamicity sort; derived from the runtime via NonemptyInterval.IsPoint.

Equations

• e.isPunctual = e.τ.IsPoint

def Event.isDurative {Time : Type u_1} [LinearOrder Time] (e : Event Time) : Prop

Is this event durative (temporally extended)?

Equations

• e.isDurative = ¬e.isPunctual

@[implicit_reducible]

instance Event.instDecidablePredIsPunctual {Time : Type u_1} [LinearOrder Time] : DecidablePred isPunctual

Equations

• e.instDecidablePredIsPunctual = id (id inferInstance)

@[implicit_reducible]

instance Event.instDecidablePredIsDurative {Time : Type u_1} [LinearOrder Time] : DecidablePred isDurative

Equations

• e.instDecidablePredIsDurative = id inferInstance

theorem Event.isDurative_iff_not_isPunctual {Time : Type u_1} [LinearOrder Time] (e : Event Time) : e.isDurative ↔ ¬e.isPunctual

isDurative and isPunctual are complementary.

Existential closure

def Event.existsClosure {Time : Type u_1} [LinearOrder Time] (P : Event Time → Prop) : Prop

Existential closure: ∃e. P(e). The fundamental step from event semantics to truth conditions.

Equations

• Event.existsClosure P = ∃ (e : Event Time), P e

Mereology

class Event.Mereology (Time : Type u_2) [LinearOrder Time] : Type u_2

Axioms for event part-of structure. Part-of is a partial order on events with temporal and sort constraints.

• partOf : Event Time → Event Time → Prop

  e₁ is a part of e₂

• refl (e : Event Time) : partOf e e

  Part-of is reflexive

• antisymm (e₁ e₂ : Event Time) : partOf e₁ e₂ → partOf e₂ e₁ → e₁ = e₂

  Part-of is antisymmetric

• trans (e₁ e₂ e₃ : Event Time) : partOf e₁ e₂ → partOf e₂ e₃ → partOf e₁ e₃

  Part-of is transitive

• τ_monotone (e₁ e₂ : Event Time) : partOf e₁ e₂ → e₁.runtime ≤ e₂.runtime

  τ is monotone: if e₁ ⊑ e₂ then τ(e₁) ⊆ τ(e₂)

• sort_preserved (e₁ e₂ : Event Time) : partOf e₁ e₂ → e₁.sort = e₂.sort

  Sort is preserved under part-of: parts of actions are actions, parts of states are states

@[implicit_reducible]

instance Event.partialOrder (Time : Type u_2) [LinearOrder Time] [m : Mereology Time] : PartialOrder (Event Time)

Event mereology induces a PartialOrder: parthood is reflexive, transitive, and antisymmetric.

Equations

• Event.partialOrder Time = { le := Event.Mereology.partOf, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

Manner

structure Event.Manner (Time : Type u_2) [LinearOrder Time] : Type u_2

A manner: the "how" of an event, individuated as an equivalence class of events under a similarity relation ([Lie24] §4.3). Manners are to events what properties are to individuals.

• exhibits : Event Time → Prop

  The characteristic predicate: which events exhibit this manner

def Event.manner {Time : Type u_1} [LinearOrder Time] (e : Event Time) (sim : Event Time → Event Time → Prop) : Manner Time

The manner of an event under a similarity criterion. e.manner sim gives the manner class of e under sim.

Equations

• e.manner sim = { exhibits := sim e }

def Event.Manner.sharedBy {Time : Type u_1} [LinearOrder Time] (m : Manner Time) (e₁ e₂ : Event Time) : Prop

Two events share a manner iff both satisfy the manner predicate.

Equations

• m.sharedBy e₁ e₂ = (m.exhibits e₁ ∧ m.exhibits e₂)

Run-time projection (event predicate → interval set)

The event→interval projection: the set of run-time intervals of the events satisfying P, i.e. the image of P under the temporal trace τ ([Kri89], [Kri98]). This is neutral event substrate — the upper rung of the projection ladder whose tense-specific lower rungs (timeTrace, the canonical denotation patterns) live in Semantics/Tense/TemporalConnectives/. It is homed here, upstream of all aspect/tense theories, so that subinterval/homogeneity properties can be stated as order-theoretic facts about it (see Semantics/Aspect/SubintervalProperty.lean).

def eventDenotation {Time : Type u_1} [LinearOrder Time] (P : Event Time → Prop) : Set (NonemptyInterval Time)

The event→interval projection: the set of run-time intervals of events satisfying P, i.e. the image of P under the temporal trace τ. Every event-level temporal theory projects to the interval level through this map.

Equations

• eventDenotation P = Event.τ '' {e : Event Time | P e}

@[simp]

theorem mem_eventDenotation {Time : Type u_1} [LinearOrder Time] {P : Event Time → Prop} {i : NonemptyInterval Time} : i ∈ eventDenotation P ↔ ∃ (e : Event Time), P e ∧ e.τ = i

Membership in eventDenotation: an interval is a run-time of some P-event.

theorem eventDenotation_eq_empty {Time : Type u_1} [LinearOrder Time] {P : Event Time → Prop} : eventDenotation P = ∅ ↔ ∀ (e : Event Time), ¬P e

No events satisfy P ↔ the denotation is empty.

theorem mem_eventDenotation_of {Time : Type u_1} [LinearOrder Time] {P : Event Time → Prop} {e : Event Time} (he : P e) : e.τ ∈ eventDenotation P

The run-time of any P-event is in the denotation.

Concrete examples (ℤ-time events)

def exampleRun : Event ℤ

Example: a running event from time 1 to 5.

Equations

• exampleRun = { runtime := { fst := 1, snd := 5, fst_le_snd := exampleRun._proof_2 }, sort := Features.Dynamicity.dynamic }

def exampleKnow : Event ℤ

Example: a knowing state from time 0 to 10.

Equations

• exampleKnow = { runtime := { fst := 0, snd := 10, fst_le_snd := exampleKnow._proof_2 }, sort := Features.Dynamicity.stative }

theorem exampleRun_isAction : exampleRun.isAction

The run event is an action.

theorem exampleKnow_isState : exampleKnow.isState

The know event is a state.

theorem exampleRun_not_state : ¬exampleRun.isState

The run event is not a state.

theorem exampleKnow_not_action : ¬exampleKnow.isAction

The know event is not an action.

theorem exampleRun_isDurative : exampleRun.isDurative

The run event is durative.

theorem exampleRun_start : exampleRun.τ.toProd.1 = 1

The run event starts at 1.

theorem exampleRun_finish : exampleRun.τ.toProd.2 = 5

The run event ends at 5.

theorem exampleKnow_runtime : exampleKnow.τ.toProd.1 = 0 ∧ exampleKnow.τ.toProd.2 = 10

The know event spans 0 to 10.