Thematic Roles — Davidsonian logical forms + axioms

API on top of Thematic/Defs.lean: thematic axioms (Aktionsart selection + uniqueness), neo-Davidsonian stative logical forms, and adverbial modification (Davidson's key payoff).

Main definitions

• ThematicAxioms — Aktionsart selection + uniqueness constraints
• agent_holder_disjoint — derived from the axioms
• EventModifier + modify + modify_comm + modify_assoc — adverbial modification as predicate conjunction ([Dav67])
• stativeLogicalForm / modifiedStativeLogicalForm / modified_stative_is_pm — stative LFs with holder ([Wel15] §3.2)

References

• [Dav67] (adverbial modification = predicate conjunction)
• [Par90] (thematic roles as separate conjuncts)
• [Wel15] §3.2 (gradable adjectives over states)

Thematic axioms (Aktionsart selection + uniqueness)

class ArgumentStructure.ThematicAxioms (Entity : Type u_1) (Time : Type u_2) [LinearOrder Time] (frame : ThematicFrame Entity Time) : Prop

Semantic constraints on thematic roles.

• agent_selects_action: agents only participate in actions
• holder_selects_state: holders only participate in states
• agent_unique: each event has at most one agent
• patient_unique: each event has at most one patient

• agent_selects_action (x : Entity) (e : Event Time) : frame.agent x e → e.sort = Features.Dynamicity.dynamic

  Agents only participate in actions (dynamic events).

• holder_selects_state (x : Entity) (e : Event Time) : frame.holder x e → e.sort = Features.Dynamicity.stative

  Holders only participate in states.

• agent_unique (x y : Entity) (e : Event Time) : frame.agent x e → frame.agent y e → x = y

  Each event has at most one agent.

• patient_unique (x y : Entity) (e : Event Time) : frame.patient x e → frame.patient y e → x = y

  Each event has at most one patient.

theorem ArgumentStructure.agent_holder_disjoint {Entity : Type u_1} {Time : Type u_2} [LinearOrder Time] {frame : ThematicFrame Entity Time} [ax : ThematicAxioms Entity Time frame] (x : Entity) (e : Event Time) : frame.agent x e → frame.holder x e → False

Agent and holder cannot both hold of the same entity and event, since agents require actions and holders require states.

Adverbial modification (Davidson's key payoff)

@[reducible, inline]

abbrev ArgumentStructure.EventModifier (Time : Type u_1) [LinearOrder Time] : Type u_1

An event modifier: a predicate on events (e.g., "quickly", "in the park").

Equations

• ArgumentStructure.EventModifier Time = (Event Time → Prop)

def ArgumentStructure.modify {Time : Type u_1} [LinearOrder Time] (P : Event Time → Prop) (M : EventModifier Time) : Event Time → Prop

Apply a modifier to an event predicate via conjunction. [Dav67]: adverbial modification is conjunction of event predicates. "John kicked the ball quickly" = ∃e. kick(e) ∧ Agent(j,e) ∧ Patient(b,e) ∧ quickly(e).

Davidson's adverbial modification is the intersective modifier (Semantics.Modification.intersective) at event-predicate type.

Equations

• ArgumentStructure.modify P M = Modifier.intersective P M

theorem ArgumentStructure.modify_comm {Time : Type u_1} [LinearOrder Time] (P : Event Time → Prop) (M₁ M₂ : EventModifier Time) : modify (modify P M₁) M₂ = modify (modify P M₂) M₁

Modification is commutative: "quickly and loudly" = "loudly and quickly".

theorem ArgumentStructure.modify_assoc {Time : Type u_1} [LinearOrder Time] (P : Event Time → Prop) (M₁ M₂ : EventModifier Time) : modify (modify P M₁) M₂ = modify P fun (e : Event Time) => M₁ e ∧ M₂ e

Modification is associative.

Stative logical forms ([Wel15] §3.2)

def ArgumentStructure.stativeLogicalForm {Entity : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : Event Time → Prop) (frame : ThematicFrame Entity Time) (x : Entity) : Prop

"x is happy" ↦ ∃s. P(s) ∧ Holder(x, s). Parallel to intransitiveLogicalForm but using holder instead of agent, reflecting that states select for holders.

Equations

• ArgumentStructure.stativeLogicalForm P frame x = ∃ (s : Event Time), P s ∧ frame.holder x s

def ArgumentStructure.modifiedStativeLogicalForm {Entity : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : Event Time → Prop) (frame : ThematicFrame Entity Time) (x : Entity) (M : EventModifier Time) : Prop

"x is happy in the morning" ↦ ∃s. P(s) ∧ Holder(x, s) ∧ M(s). State modification = event modification applied to states.

Equations

• ArgumentStructure.modifiedStativeLogicalForm P frame x M = ∃ (s : Event Time), P s ∧ frame.holder x s ∧ M s

theorem ArgumentStructure.modified_stative_is_pm {Entity : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : Event Time → Prop) (frame : ThematicFrame Entity Time) (x : Entity) (M : EventModifier Time) : modifiedStativeLogicalForm P frame x M ↔ stativeLogicalForm (modify P M) frame x

Modified stative = stative of modified predicate (Predicate Modification): state modification is an instance of Davidson's conjunction-based event modification.