Thematic-Role Properties on θ

[Kri98] [Dow91] [Ten94] [Car84]

The mereological properties a thematic relation θ : Object → Event → Prop can have. These properties — uniqueness of participants/events, cumulativity, mapping to objects/events/strict-sub-objects/strict-sub-events — are the foundation of mereological event semantics. Each property formalizes a structural correspondence between the part-mereology of objects and the part-mereology of events under a thematic role.

Topic-named (not paper-named): defines the deep substrate that [Kri98] §3.2 (eq. 43-50) develops, but also the substrate that [Dow91] proto-roles, [Ten94] aspectual roles, [Car84] thematic-role-as-relation theory, and any modern incremental-theme account uses. Specific paper replications import this file and instantiate the predicates on paper-specific data.

def ArgumentStructure.UP {α : Type u_1} {β : Type u_2} (θ : α → β → Prop) : Prop

Uniqueness of Participant (UP): each event has at most one θ-filler. [Kri98] eq. 43: θ(x,e) ∧ θ(y,e) → x = y.

Equations

• ArgumentStructure.UP θ = ∀ (x y : α) (e : β), θ x e → θ y e → x = y

def ArgumentStructure.CumTheta {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (θ : α → β → Prop) : Prop

Cumulative theta (CumTheta): θ preserves sums. [Kri98] eq. 44: θ(x,e) ∧ θ(y,e') → θ(x⊕y, e⊕e'). This is the relational analog of IsSumHom.

Equations

• ArgumentStructure.CumTheta θ = ∀ (x y : α) (e e' : β), θ x e → θ y e' → θ (x ⊔ y) (e ⊔ e')

def ArgumentStructure.ME {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (θ : α → β → Prop) : Prop

Mapping to Events (ME): object parts map to event parts. [Kri98] eq. 45: θ(x,e) ∧ y ≤ x → ∃e'. e' ≤ e ∧ θ(y,e').

Equations

• ArgumentStructure.ME θ = ∀ (x : α) (e : β) (y : α), θ x e → y ≤ x → ∃ e' ≤ e, θ y e'

def ArgumentStructure.MSE {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (θ : α → β → Prop) : Prop

Mapping to Strict subEvents (MSE): proper object parts map to proper subevents. [Kri98] eq. 46: θ(x,e) ∧ y < x → ∃e'. e' < e ∧ θ(y,e').

Equations

• ArgumentStructure.MSE θ = ∀ (x : α) (e : β) (y : α), θ x e → y < x → ∃ e' < e, θ y e'

def ArgumentStructure.UE {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (θ : α → β → Prop) : Prop

Uniqueness of Events (UE): each object part maps to a unique event part. [Kri98] eq. 47: θ(x,e) ∧ y ≤ x → ∃!e'. e' ≤ e ∧ θ(y,e').

Equations

• ArgumentStructure.UE θ = ∀ (x : α) (e : β) (y : α), θ x e → y ≤ x → ∃ e' ≤ e, θ y e' ∧ ∀ e'' ≤ e, θ y e'' → e'' = e'

def ArgumentStructure.MO {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (θ : α → β → Prop) : Prop

Mapping to Objects (MO): event parts map to object parts. [Kri98] eq. 48: θ(x,e) ∧ e' ≤ e → ∃y. y ≤ x ∧ θ(y,e').

Equations

• ArgumentStructure.MO θ = ∀ (x : α) (e e' : β), θ x e → e' ≤ e → ∃ y ≤ x, θ y e'

def ArgumentStructure.MSO {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (θ : α → β → Prop) : Prop

Mapping to Strict subObjects (MSO): proper subevents map to proper object parts. [Kri98] eq. 49: θ(x,e) ∧ e' < e → ∃y. y < x ∧ θ(y,e').

Equations

• ArgumentStructure.MSO θ = ∀ (x : α) (e e' : β), θ x e → e' < e → ∃ y < x, θ y e'

def ArgumentStructure.UO {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (θ : α → β → Prop) : Prop

Uniqueness of Objects (UO): each event part maps to a unique object part. [Kri98] eq. 50: θ(x,e) ∧ e' ≤ e → ∃!y. y ≤ x ∧ θ(y,e').

Equations

• ArgumentStructure.UO θ = ∀ (x : α) (e e' : β), θ x e → e' ≤ e → ∃ y ≤ x, θ y e' ∧ ∀ z ≤ x, θ z e' → z = y

def ArgumentStructure.GUE {α : Type u_1} {β : Type u_2} (θ : α → β → Prop) : Prop

Generalized Uniqueness of Events (GUE): each object participates in at most one event. [Kri98] eq. 52: θ(x,e) ∧ θ(x,e') → e = e'.

Equations

• ArgumentStructure.GUE θ = ∀ (x : α) (e e' : β), θ x e → θ x e' → e = e'

theorem ArgumentStructure.roleHom_implies_cumTheta {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {f : β → α} (hf : Mereology.IsSumHom f) : CumTheta fun (x : α) (e : β) => f e = x

Bridge: a sum-homomorphism f : β → α (functional θ from Mereology.lean) induces a CumTheta relation λ x e, f e = x. This connects the functional view (θ as projection function) to the relational view (θ as binary predicate) at the cumulativity level.

IsCumThetaVerb — typeclass for cumulative-θ verbs

class ArgumentStructure.IsCumThetaVerb {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (θ : α → β → Prop) : Prop

A thematic relation θ has cumulative theta (mathlib-discipline typeclass form of CumTheta for synthesis).

The weakest verb-class typeclass: every K98 verb class (strictly incremental, incremental, cumulative-only) satisfies CumTheta and hence IsCumThetaVerb. The stronger classes (IsSincVerb in Aspect/Incremental.lean, IsIncVerb in Aspect/Incremental.lean) register upward instances providing IsCumThetaVerb automatically.

Note: this typeclass is content-driven — its only field is CumTheta, satisfied by ALL K98 verb classes. The "cumOnly" empirical class (cumulative and non-incremental) is a separate sub-classification not captured here; per [Kri98] §3.2 (page 12-13), push (the cart), pull, carry — transitive activities with theme arguments where mereological structure does NOT transfer to events. K98 does not classify stative experiencer verbs (love, know) under CumTheta; statives are treated separately (page 13: see the picture, touch a cup are "peculiar" cases violating UP).

• cumTheta : CumTheta θ

  Cumulative theta: θ preserves sums (K98 eq. 44).