Thematic Roles — type definitions

Neo-Davidsonian thematic roles as two-place predicates relating entities to events. The Defs partner to Thematic/Basic.lean, which builds the thematic axioms, Davidsonian logical forms, and adverbial modification on top of these types.

Main definitions

• ThematicRel — the core relation type Entity → Event Time → Prop
• EventRel — event-first generalization to non-entity arguments ([Rud25b])
• ThematicFrame — a model's assignment of the role relations

References

• [Dav67], [Par90] (neo-Davidsonian foundations)
• [Rud25b] (EventRel for non-entity arguments)

@[reducible, inline]

abbrev ArgumentStructure.ThematicRel (Entity : Type u_1) (Time : Type u_2) [LinearOrder Time] : Type (max u_1 u_2)

A thematic relation: a two-place predicate relating an entity to an event. The core neo-Davidsonian type. Agent(j, e) means "j is the agent of event e".

Equations

• ArgumentStructure.ThematicRel Entity Time = (Entity → Event Time → Prop)

@[reducible, inline]

abbrev ArgumentStructure.EventRel (Time : Type u_1) (α : Type u_2) [LinearOrder Time] : Type (max u_2 u_1)

A relation between an event and an argument of arbitrary sort. Generalizes ThematicRel past the entity-first restriction: arguments may be propositions, questions, performances, content individuals, or any other ontological category. The argument order is event-first (vs. ThematicRel's entity-first), reflecting the neo-Davidsonian convention for thematic roles vs. the more general event-relation pattern used by content/reenactment relations ([Rud25b], §4.4–4.7).

Equations

• ArgumentStructure.EventRel Time α = (Event Time → α → Prop)

structure ArgumentStructure.ThematicFrame (Entity : Type u_1) (Time : Type u_2) [LinearOrder Time] : Type (max u_1 u_2)

A thematic frame bundles thematic relations for a given model.

Note: holder is a Theory-level role distinct from agent — it selects for states, not actions. The Fragment-layer ThetaRole enum does not include holder since VendlerClass already encodes dynamicity.

• agent : ThematicRel Entity Time

  Agent: volitional causer

• patient : ThematicRel Entity Time

  Patient: affected entity

• theme : ThematicRel Entity Time

  Theme: entity in a state/location

• experiencer : ThematicRel Entity Time

  Experiencer: perceiver/cognizer

• goal : ThematicRel Entity Time

  Goal: recipient/target

• source : ThematicRel Entity Time

  Source: origin

• instrument : ThematicRel Entity Time

  Instrument: means

• stimulus : ThematicRel Entity Time

  Stimulus: cause of experience

• holder : ThematicRel Entity Time

  Holder: entity in a state. Distinct from Agent: selects for states, not actions.