inductive Semantics.Events.EventSort : Type

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

• action : EventSort
• state : EventSort

instance Semantics.Events.instDecidableEqEventSort : DecidableEq EventSort

Equations

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

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

Equations

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

instance Semantics.Events.instReprEventSort : Repr EventSort

Equations

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

instance Semantics.Events.instBEqEventSort : BEq EventSort

Equations

• Semantics.Events.instBEqEventSort = { beq := Semantics.Events.instBEqEventSort.beq }

def Semantics.Events.instBEqEventSort.beq : EventSort → EventSort → Bool

Equations

• Semantics.Events.instBEqEventSort.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Semantics.Events.instInhabitedEventSort.default : EventSort

Equations

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

instance Semantics.Events.instInhabitedEventSort : Inhabited EventSort

Equations

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

structure Semantics.Events.Ev (Time : Type u_1) [LE Time] : Type u_1

An event: a temporal individual with ontological sort. Events have interval-valued runtimes, following @cite{krifka-1989}.

• runtime : Core.Time.Interval Time

  The temporal extent of this event

• sort : EventSort

  Ontological sort: action or state

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

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

Equations

• e.τ = e.runtime

def Semantics.Events.Ev.isAction {Time : Type u_1} [LE Time] (e : Ev Time) : Bool

Is this event an action (dynamic eventuality)?

Equations

• e.isAction = (e.sort == Semantics.Events.EventSort.action)

def Semantics.Events.Ev.isState {Time : Type u_1} [LE Time] (e : Ev Time) : Bool

Is this event a state (stative eventuality)?

Equations

• e.isState = (e.sort == Semantics.Events.EventSort.state)

theorem Semantics.Events.sort_exhaustive (s : EventSort) : s = EventSort.action ∨ s = EventSort.state

Every event is either an action or a state (exhaustivity).

theorem Semantics.Events.sort_exclusive : EventSort.action ≠ EventSort.state

No event is both an action and a state (exclusivity).

theorem Semantics.Events.isAction_iff_not_isState {Time : Type u_1} [LE Time] (e : Ev Time) : e.isAction = true ↔ e.isState = false

isAction and isState are complementary.

theorem Semantics.Events.isState_iff_not_isAction {Time : Type u_1} [LE Time] (e : Ev Time) : e.isState = true ↔ e.isAction = false

isState and isAction are complementary.

def Semantics.Events.EventSort.toDynamicity : EventSort → Tense.Aspect.LexicalAspect.Dynamicity

Map EventSort to Dynamicity (the aspectual feature).

Equations

• Semantics.Events.EventSort.action.toDynamicity = Semantics.Tense.Aspect.LexicalAspect.Dynamicity.dynamic
• Semantics.Events.EventSort.state.toDynamicity = Semantics.Tense.Aspect.LexicalAspect.Dynamicity.stative

def Semantics.Events.dynamicityToEventSort : Tense.Aspect.LexicalAspect.Dynamicity → EventSort

Map Dynamicity back to EventSort.

Equations

• Semantics.Events.dynamicityToEventSort Semantics.Tense.Aspect.LexicalAspect.Dynamicity.dynamic = Semantics.Events.EventSort.action
• Semantics.Events.dynamicityToEventSort Semantics.Tense.Aspect.LexicalAspect.Dynamicity.stative = Semantics.Events.EventSort.state

theorem Semantics.Events.dynamicity_roundtrip (d : Tense.Aspect.LexicalAspect.Dynamicity) : (dynamicityToEventSort d).toDynamicity = d

Roundtrip: toDynamicity ∘ dynamicityToEventSort = id.

theorem Semantics.Events.eventSort_roundtrip (s : EventSort) : dynamicityToEventSort s.toDynamicity = s

Roundtrip: dynamicityToEventSort ∘ toDynamicity = id.

theorem Semantics.Events.vendlerClass_sort_agrees (c : Tense.Aspect.LexicalAspect.VendlerClass) : dynamicityToEventSort c.dynamicity = match c with | Tense.Aspect.LexicalAspect.VendlerClass.state => EventSort.state | Tense.Aspect.LexicalAspect.VendlerClass.activity => EventSort.action | Tense.Aspect.LexicalAspect.VendlerClass.achievement => EventSort.action | Tense.Aspect.LexicalAspect.VendlerClass.accomplishment => EventSort.action

VendlerClass dynamicity agrees with EventSort classification. States map to.state sort; all others map to.action sort.

def Semantics.Events.Ev.toEventuality {Time : Type u_1} [LE Time] (e : Ev Time) : Tense.Aspect.Core.Eventuality Time

Forget the sort: project Ev down to Eventuality.

Equations

• e.toEventuality = { runtime := e.runtime }

def Semantics.Events.eventualityToEv {Time : Type u_1} [LE Time] (ev : Tense.Aspect.Core.Eventuality Time) (s : EventSort) : Ev Time

Lift an Eventuality to Ev with a given sort.

Equations

• Semantics.Events.eventualityToEv ev s = { runtime := ev.runtime, sort := s }

theorem Semantics.Events.toEv_toEventuality_roundtrip {Time : Type u_1} [LE Time] (ev : Tense.Aspect.Core.Eventuality Time) (s : EventSort) : (eventualityToEv ev s).toEventuality = ev

Roundtrip: toEventuality ∘ eventualityToEv forgets the sort (we recover the Eventuality).

theorem Semantics.Events.toEventuality_τ {Time : Type u_1} [LE Time] (e : Ev Time) : e.toEventuality.τ = e.τ

The temporal trace is preserved by the Ev → Eventuality projection.

def Semantics.Events.EventPred.liftToEv {W : Type u_1} {Time : Type u_2} [LE Time] (P : Tense.Aspect.Core.EventPred W Time) : W → Ev Time → Prop

Lift an EventPred (over Eventuality) to a world-indexed predicate over Ev, ignoring the sort.

Equations

• Semantics.Events.EventPred.liftToEv P w e = P w e.toEventuality

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 : Ev Time → Ev Time → Prop

  e₁ is a part of e₂

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

  Part-of is reflexive

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

  Part-of is antisymmetric

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

  Part-of is transitive

• τ_monotone (e₁ e₂ : Ev Time) : partOf e₁ e₂ → e₁.runtime.subinterval e₂.runtime

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

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

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

instance Semantics.Events.eventPreorder (Time : Type u_1) [LinearOrder Time] [m : EventMereology Time] : Preorder (Ev 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 := ⋯ }

@[reducible, inline]

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

A predicate over events (not world-indexed).

Equations

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

@[reducible, inline]

abbrev Semantics.Events.EvPredW (W : Type u_1) (Time : Type u_2) [LE Time] : Type (max u_1 u_2)

A world-indexed predicate over events.

Equations

• Semantics.Events.EvPredW W Time = (W → Semantics.Events.Ev Time → Prop)

def Semantics.Events.existsClosure {Time : Type u_1} [LE 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.Ev Time), P e

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

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

Equations

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

def Semantics.Events.exampleRun : Ev ℤ

Example: a running event from time 1 to 5.

Equations

• Semantics.Events.exampleRun = { runtime := { start := 1, finish := 5, valid := Semantics.Events.exampleRun._proof_2 }, sort := Semantics.Events.EventSort.action }

structure Semantics.Events.Manner (Time : Type u_1) [LE 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}: manners are the ontological category ranged over by how in "How did John run?" and modified by manner adverbs (quickly, carefully). They are to events what properties are to individuals.

Formally, a manner is a predicate on events that picks out a similarity class — all events sharing a characteristic quality. Two events e₁, e₂ have the same manner w.r.t. M iff M(e₁) ∧ M(e₂).

References:

• Dik, S. (1975). The semantic representation of manner adverbials.
• Alexeyenko, S. (2015). The syntax and semantics of manner modification.
• Umbach, C. et al. (2022). Manner reference and similarity.
• Liefke, K. (2024). Natural Language Ontology, §4.3.

• exhibits : Ev Time → Prop

  The characteristic predicate: which events exhibit this manner

def Semantics.Events.mannerOf {Time : Type u_1} [LE Time] (sim : Ev Time → Ev Time → Prop) (e : Ev 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} [LE Time] (m : Manner Time) (e₁ e₂ : Ev Time) : Prop

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

Equations

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

def Semantics.Events.exampleKnow : Ev ℤ

Example: a knowing state from time 0 to 10.

Equations

• Semantics.Events.exampleKnow = { runtime := { start := 0, finish := 10, valid := Semantics.Events.exampleKnow._proof_2 }, sort := Semantics.Events.EventSort.state }

theorem Semantics.Events.exampleRun_isAction : exampleRun.isAction = true

The run event is an action.

theorem Semantics.Events.exampleKnow_isState : exampleKnow.isState = true

The know event is a state.

theorem Semantics.Events.exampleRun_not_state : exampleRun.isState = false

The run event is not a state.

theorem Semantics.Events.exampleKnow_not_action : exampleKnow.isAction = false

The know event is not an action.

theorem Semantics.Events.exampleRun_start : exampleRun.τ.start = 1

The run event starts at 1.

theorem Semantics.Events.exampleRun_finish : exampleRun.τ.finish = 5

The run event ends at 5.

theorem Semantics.Events.exampleKnow_runtime : exampleKnow.τ.start = 0 ∧ exampleKnow.τ.finish = 10

The know event spans 0 to 10.

theorem Semantics.Events.exampleRun_toEventuality_τ : exampleRun.toEventuality.τ = exampleRun.τ

Projecting the run event to Eventuality preserves the runtime.