Neo-Davidsonian Event Semantics — type definitions

Foundational types for neo-Davidsonian event semantics (@cite{davidson-1967}, @cite{parsons-1990}). Verbs denote predicates of events; thematic roles are independent two-place predicates (see ThematicRoles.lean).

This file is the Defs partner to Basic.lean: pure type/structure declarations and one foundational typeclass + instance, no API. Files that only need to talk about events (taking Event Time as an argument, parameterizing by [EventMereology Time]) can import this file alone; files that need sort predicates, dynamicity bridges, or Davidsonian existential closure import Basic.lean.

Main definitions

• EventSort — binary action/state ontological sort (@cite{bach-1986})
• Event — the unified event type: a runtime interval + sort
• Event.τ — temporal trace function
• EventMereology — part-of typeclass with τ-monotonicity + sort-preservation
• eventPreorder — Preorder instance derived from EventMereology
• EvPred / EventPred — predicate / world-indexed-predicate types
• existsClosure / existsClosureW — Davidsonian existential closure
• Manner — manner ontology (@cite{liefke-2024} §4.3)

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 — @cite{champollion-2017} and @cite{zhao-2025} 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 .action.

References

• @cite{davidson-1967}, @cite{parsons-1990} (neo-Davidsonian foundations)
• @cite{bach-1986} (action/state ontology)
• @cite{krifka-1989} (interval-valued runtimes)
• @cite{champollion-2017}, @cite{zhao-2025} (event-as-generic)
• @cite{liefke-2024} §4.3 (manner ontology)

inductive Semantics.Events.EventSort : Type

Binary ontological sort for events. Actions involve change; states do not.

• action : EventSort
• state : EventSort

@[implicit_reducible]

instance Semantics.Events.instDecidableEqEventSort : DecidableEq EventSort

Equations

• Semantics.Events.instDecidableEqEventSort x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.Events.instReprEventSort : Repr EventSort

Equations

• Semantics.Events.instReprEventSort = { reprPrec := Semantics.Events.instReprEventSort.repr }

def Semantics.Events.instReprEventSort.repr : EventSort → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Events.instInhabitedEventSort : Inhabited EventSort

Equations

• Semantics.Events.instInhabitedEventSort = { default := Semantics.Events.instInhabitedEventSort.default }

def Semantics.Events.instInhabitedEventSort.default : EventSort

Equations

• Semantics.Events.instInhabitedEventSort.default = Semantics.Events.EventSort.action

structure Semantics.Events.Event (Time : Type u_1) [LinearOrder Time] : Type u_1

An event: a temporal individual with ontological sort.

• runtime : Core.Time.Interval Time

  The temporal extent of this event

• sort : EventSort

  Ontological sort: action or state

def Semantics.Events.Event.τ {Time : Type u_1} [LinearOrder Time] (e : Event Time) : Core.Time.Interval Time

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

Equations

• e.τ = e.runtime

@[reducible, inline]

abbrev Semantics.Events.EvPred (Time : Type u_1) [LinearOrder Time] : Type u_1

A predicate over events (not world-indexed).

Equations

• Semantics.Events.EvPred Time = (Semantics.Events.Event Time → Prop)

@[reducible, inline]

abbrev Semantics.Events.EventPred (W : Type u_1) (Time : Type u_2) [LinearOrder Time] : Type (max u_1 u_2)

A world-indexed predicate over events. The standard type for verb / VP denotations in tense-aspect composition.

Equations

• Semantics.Events.EventPred W Time = (W → Semantics.Events.Event Time → Prop)

def Semantics.Events.existsClosure {Time : Type u_1} [LinearOrder Time] (P : EvPred Time) : Prop

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

Equations

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

def Semantics.Events.existsClosureW {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : EventPred W Time) : W → Prop

World-indexed existential closure: λw. ∃e. P(w)(e).

Equations

• Semantics.Events.existsClosureW P w = ∃ (e : Semantics.Events.Event Time), P w e

class Semantics.Events.EventMereology (Time : Type u_1) [LinearOrder Time] : Type u_1

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.subinterval 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 Semantics.Events.eventPreorder (Time : Type u_1) [LinearOrder Time] [m : EventMereology Time] : Preorder (Event Time)

Event mereology induces a Preorder.

Equations

• Semantics.Events.eventPreorder Time = { le := Semantics.Events.EventMereology.partOf, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

structure Semantics.Events.Manner (Time : Type u_1) [LinearOrder Time] : Type u_1

A manner: the "how" of an event, individuated as an equivalence class of events under a similarity relation (@cite{liefke-2024} §4.3). Manners are to events what properties are to individuals.

• exhibits : Event Time → Prop

  The characteristic predicate: which events exhibit this manner

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

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

Equations

• Semantics.Events.mannerOf sim e = { exhibits := sim e }

def Semantics.Events.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₂)