Event Mereology

@cite{bach-1986} @cite{champollion-2017}

Event-specific mereological infrastructure built on top of the generic Core.Mereology definitions. Specializes CUM, QUA, IsSumHom, etc. to event structures with EventCEM, thematic role homomorphisms, and Vendler class bridges.

Generic mereological definitions (CUM, DIV, QUA, Atom, AlgClosure, IsSumHom, Overlap, ExtMeasure, QMOD) live in Core.Mereology.

Sections

1. Event CEM (Classical Extensional Mereology enrichment)
2. Lexical Cumulativity
3. Role Homomorphism (θ preserves ⊕)
4. τ Homomorphism (runtime preserves ⊕)
5. Bridges to existing types

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

Classical Extensional Mereology for events: enriches EventMereology with binary sum (⊔) via SemilatticeSup (Ev Time). @cite{champollion-2017} Ch. 2: event domain forms a join semilattice.

• partOf : Ev Time → Ev Time → Prop
• refl (e : Ev Time) : partOf e e
• antisymm (e₁ e₂ : Ev Time) : partOf e₁ e₂ → partOf e₂ e₁ → e₁ = e₂
• trans (e₁ e₂ e₃ : Ev Time) : partOf e₁ e₂ → partOf e₂ e₃ → partOf e₁ e₃
• τ_monotone (e₁ e₂ : Ev Time) : partOf e₁ e₂ → e₁.runtime.subinterval e₂.runtime
• sort_preserved (e₁ e₂ : Ev Time) : partOf e₁ e₂ → e₁.sort = e₂.sort
• evSemilatticeSup : SemilatticeSup (Ev Time)

  Events form a join semilattice (binary sum ⊕ exists).

• le_eq_partOf (e₁ e₂ : Ev Time) : e₁ ≤ e₂ ↔ EventMereology.partOf e₁ e₂

  ≤ from SemilatticeSup agrees with partOf.

• intervalSemilatticeSup : SemilatticeSup (Core.Time.Interval Time)

  Intervals form a join semilattice (for τ homomorphism).

• τ_hom (e₁ e₂ : Ev Time) : (SemilatticeSup.sup e₁ e₂).runtime = SemilatticeSup.sup e₁.runtime e₂.runtime

  τ is a sum homomorphism: τ(e₁ ⊕ e₂) = τ(e₁) ⊕ τ(e₂). @cite{champollion-2017} §2.5.1.

noncomputable instance Semantics.Events.Mereology.eventCEMSemilatticeSup (Time : Type u_1) [LinearOrder Time] [cem : EventCEM Time] : SemilatticeSup (Ev Time)

Equations

• Semantics.Events.Mereology.eventCEMSemilatticeSup Time = Semantics.Events.Mereology.EventCEM.evSemilatticeSup

def Semantics.Events.Mereology.LexCum (Time : Type u_1) [LinearOrder Time] [cem : EventCEM Time] (P : EvPred Time) : Prop

Lexical cumulativity for event predicates: the event-specific instantiation of CUM. A verb predicate V is lexically cumulative iff for any two V-events, their sum is also a V-event. @cite{champollion-2017} §3.2: activities and states are lexically cumulative.

Equations

• Semantics.Events.Mereology.LexCum Time P = ∀ (e₁ e₂ : Semantics.Events.Ev Time), P e₁ → P e₂ → P (SemilatticeSup.sup e₁ e₂)

theorem Semantics.Events.Mereology.cum_iff_lexCum (Time : Type u_1) [LinearOrder Time] [cem : EventCEM Time] (P : EvPred Time) : CUM P ↔ LexCum Time P

LexCum is exactly CUM specialized to EvPred. This bridges the abstract and event-specific formulations.

class Semantics.Events.Mereology.RoleHom (Entity : Type u_1) (Time : Type u_2) [LinearOrder Time] [cem : EventCEM Time] [SemilatticeSup Entity] : Type (max u_1 u_2)

A thematic-role sum homomorphism: the function mapping each event to its θ-role filler preserves ⊕. @cite{champollion-2017} §2.5.1 eq. 34–35: Agent(e₁ ⊕ e₂) = Agent(e₁) ⊕ Agent(e₂).

This is stated as: given a function θ : Ev Time → Entity extracting the unique role-filler, θ is a sum homomorphism.

• agentOf : Ev Time → Entity

  Agent extraction function (partial: only defined for events with agents).

• agent_hom : IsSumHom agentOf

  Agent extraction preserves ⊕.

• patientOf : Ev Time → Entity

  Patient extraction function.

• patient_hom : IsSumHom patientOf

  Patient extraction preserves ⊕.

• themeOf : Ev Time → Entity

  Theme extraction function.

• theme_hom : IsSumHom themeOf

  Theme extraction preserves ⊕.

theorem Semantics.Events.Mereology.τ_is_sum_hom (Time : Type u_1) [LinearOrder Time] [cem : EventCEM Time] (e₁ e₂ : Ev Time) : (SemilatticeSup.sup e₁ e₂).runtime = SemilatticeSup.sup e₁.runtime e₂.runtime

τ is a sum homomorphism: follows directly from EventCEM.τ_hom. τ(e₁ ⊕ e₂) = τ(e₁) ⊕ τ(e₂). @cite{champollion-2017} §2.5.1: the runtime function preserves sums.

instance Semantics.Events.Mereology.instIsSumHomRuntime (Time : Type u_1) [LinearOrder Time] [cem : EventCEM Time] : IsSumHom fun (e : Ev Time) => e.runtime

τ (runtime extraction) as an IsSumHom instance, derived from EventCEM.τ_hom. Enables cum_pullback to work automatically for τ without manually threading the sum-homomorphism proof.

theorem Semantics.Events.Mereology.vendlerClass_atelic_implies_cum_intent (c : Tense.Aspect.LexicalAspect.VendlerClass) (h : c.telicity = Tense.Aspect.LexicalAspect.Telicity.atelic) : c = Tense.Aspect.LexicalAspect.VendlerClass.state ∨ c = Tense.Aspect.LexicalAspect.VendlerClass.activity

Atelic Vendler classes yield predicates that are naturally cumulative. States and activities have the subinterval property, which entails CUM for their event predicates.

theorem Semantics.Events.Mereology.vendlerClass_telic_implies_qua_intent (c : Tense.Aspect.LexicalAspect.VendlerClass) (h : c.telicity = Tense.Aspect.LexicalAspect.Telicity.telic) : c = Tense.Aspect.LexicalAspect.VendlerClass.achievement ∨ c = Tense.Aspect.LexicalAspect.VendlerClass.accomplishment

Telic Vendler classes yield predicates that are naturally quantized. Achievements and accomplishments lack the subinterval property, corresponding to QUA.