Thematic Roles — Davidsonian logical forms + axioms

API on top of ArgumentStructure/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 (@cite{davidson-1967})
• stativeLogicalForm / modifiedStativeLogicalForm / modified_stative_is_pm — stative LFs with holder (@cite{wellwood-2015} §3.2)

References

• @cite{davidson-1967} (adverbial modification = predicate conjunction)
• @cite{parsons-1990} (thematic roles as separate conjuncts)
• @cite{wellwood-2015} §3.2 (gradable adjectives over states)

Thematic axioms (Aktionsart selection + uniqueness)

class Semantics.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 : Events.Event Time) : frame.agent x e → e.sort = Events.EventSort.action

  Agents only participate in actions (dynamic events).

• holder_selects_state (x : Entity) (e : Events.Event Time) : frame.holder x e → e.sort = Events.EventSort.state

  Holders only participate in states.

• agent_unique (x y : Entity) (e : Events.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 : Events.Event Time) : frame.patient x e → frame.patient y e → x = y

  Each event has at most one patient.

theorem Semantics.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 : Events.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 Semantics.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

• Semantics.ArgumentStructure.EventModifier Time = Semantics.Events.EvPred Time

def Semantics.ArgumentStructure.modify {Time : Type u_1} [LinearOrder Time] (P : Events.EvPred Time) (M : EventModifier Time) : Events.EvPred Time

Apply a modifier to an event predicate via conjunction. @cite{davidson-1967}: adverbial modification is conjunction of event predicates. "John kicked the ball quickly" = ∃e. kick(e) ∧ Agent(j,e) ∧ Patient(b,e) ∧ quickly(e).

Equations

• Semantics.ArgumentStructure.modify P M e = (P e ∧ M e)

theorem Semantics.ArgumentStructure.modify_comm {Time : Type u_1} [LinearOrder Time] (P : Events.EvPred Time) (M₁ M₂ : EventModifier Time) : modify (modify P M₁) M₂ = modify (modify P M₂) M₁

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

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

Modification is associative.

Stative logical forms (@cite{wellwood-2015} §3.2)

def Semantics.ArgumentStructure.stativeLogicalForm {Entity : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : Events.EvPred Time) (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

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

def Semantics.ArgumentStructure.modifiedStativeLogicalForm {Entity : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : Events.EvPred Time) (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

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

theorem Semantics.ArgumentStructure.modified_stative_is_pm {Entity : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : Events.EvPred Time) (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.