@[reducible, inline]

abbrev Semantics.Events.ThematicRoles.ThematicRel (Entity : Type u_1) (Time : Type u_2) [LE 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

• Semantics.Events.ThematicRoles.ThematicRel Entity Time = (Entity → Semantics.Events.Ev Time → Prop)

structure Semantics.Events.ThematicRoles.ThematicFrame (Entity : Type u_1) (Time : Type u_2) [LE Time] : Type (max u_1 u_2)

A thematic frame bundles thematic relations for a given model. Each field provides the semantic content for one role.

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.

def Semantics.Events.ThematicRoles.ThetaRole.toRel {Entity : Type u_1} {Time : Type u_2} [LE Time] (θ : ThetaRole) (frame : ThematicFrame Entity Time) : ThematicRel Entity Time

Map the Fragment-layer ThetaRole enum to the corresponding ThematicFrame field. This bridges lexical annotations to semantic content.

Equations

• Semantics.Events.ThematicRoles.ThetaRole.toRel ThetaRole.agent frame = frame.agent
• Semantics.Events.ThematicRoles.ThetaRole.toRel ThetaRole.patient frame = frame.patient
• Semantics.Events.ThematicRoles.ThetaRole.toRel ThetaRole.theme frame = frame.theme
• Semantics.Events.ThematicRoles.ThetaRole.toRel ThetaRole.experiencer frame = frame.experiencer
• Semantics.Events.ThematicRoles.ThetaRole.toRel ThetaRole.goal frame = frame.goal
• Semantics.Events.ThematicRoles.ThetaRole.toRel ThetaRole.source frame = frame.source
• Semantics.Events.ThematicRoles.ThetaRole.toRel ThetaRole.instrument frame = frame.instrument
• Semantics.Events.ThematicRoles.ThetaRole.toRel ThetaRole.stimulus frame = frame.stimulus

theorem Semantics.Events.ThematicRoles.agent_toRel {Entity : Type u_1} {Time : Type u_2} [LE Time] (frame : ThematicFrame Entity Time) : ThetaRole.toRel ThetaRole.agent frame = frame.agent

theorem Semantics.Events.ThematicRoles.patient_toRel {Entity : Type u_1} {Time : Type u_2} [LE Time] (frame : ThematicFrame Entity Time) : ThetaRole.toRel ThetaRole.patient frame = frame.patient

theorem Semantics.Events.ThematicRoles.theme_toRel {Entity : Type u_1} {Time : Type u_2} [LE Time] (frame : ThematicFrame Entity Time) : ThetaRole.toRel ThetaRole.theme frame = frame.theme

theorem Semantics.Events.ThematicRoles.experiencer_toRel {Entity : Type u_1} {Time : Type u_2} [LE Time] (frame : ThematicFrame Entity Time) : ThetaRole.toRel ThetaRole.experiencer frame = frame.experiencer

theorem Semantics.Events.ThematicRoles.goal_toRel {Entity : Type u_1} {Time : Type u_2} [LE Time] (frame : ThematicFrame Entity Time) : ThetaRole.toRel ThetaRole.goal frame = frame.goal

theorem Semantics.Events.ThematicRoles.source_toRel {Entity : Type u_1} {Time : Type u_2} [LE Time] (frame : ThematicFrame Entity Time) : ThetaRole.toRel ThetaRole.source frame = frame.source

theorem Semantics.Events.ThematicRoles.instrument_toRel {Entity : Type u_1} {Time : Type u_2} [LE Time] (frame : ThematicFrame Entity Time) : ThetaRole.toRel ThetaRole.instrument frame = frame.instrument

theorem Semantics.Events.ThematicRoles.stimulus_toRel {Entity : Type u_1} {Time : Type u_2} [LE Time] (frame : ThematicFrame Entity Time) : ThetaRole.toRel ThetaRole.stimulus frame = frame.stimulus

class Semantics.Events.ThematicRoles.ThematicAxioms (Entity : Type u_3) (Time : Type u_4) [LE 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 : Ev Time) : frame.agent x e → e.sort = EventSort.action

  Agents only participate in actions (dynamic events).

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

  Holders only participate in states.

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

  Each event has at most one agent.

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

  Each event has at most one patient.

theorem Semantics.Events.ThematicRoles.agent_holder_disjoint {Entity : Type u_3} {Time : Type u_4} [LE Time] {frame : ThematicFrame Entity Time} [ax : ThematicAxioms Entity Time frame] (x : Entity) (e : Ev 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.

def Semantics.Events.ThematicRoles.transitiveLogicalForm {Entity : Type u_3} {Time : Type u_4} [LE Time] (V : EvPred Time) (frame : ThematicFrame Entity Time) (subj obj : Entity) : Prop

Neo-Davidsonian logical form for a transitive sentence: "x V-ed y" ↦ ∃e. V(e) ∧ Agent(x, e) ∧ Patient(y, e)

The key @cite{parsons-1990} insight: thematic roles are separate conjuncts, not part of the verb's argument structure.

Equations

• Semantics.Events.ThematicRoles.transitiveLogicalForm V frame subj obj = ∃ (e : Semantics.Events.Ev Time), V e ∧ frame.agent subj e ∧ frame.patient obj e

def Semantics.Events.ThematicRoles.intransitiveLogicalForm {Entity : Type u_3} {Time : Type u_4} [LE Time] (V : EvPred Time) (frame : ThematicFrame Entity Time) (subj : Entity) : Prop

Neo-Davidsonian logical form for an intransitive sentence: "x V-ed" ↦ ∃e. V(e) ∧ Agent(x, e)

Equations

• Semantics.Events.ThematicRoles.intransitiveLogicalForm V frame subj = ∃ (e : Semantics.Events.Ev Time), V e ∧ frame.agent subj e

def Semantics.Events.ThematicRoles.ditransitiveLogicalForm {Entity : Type u_3} {Time : Type u_4} [LE Time] (V : EvPred Time) (frame : ThematicFrame Entity Time) (subj directObj indirectObj : Entity) : Prop

Neo-Davidsonian logical form for a ditransitive sentence: "x V-ed y z" ↦ ∃e. V(e) ∧ Agent(x, e) ∧ Theme(y, e) ∧ Goal(z, e)

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Semantics.Events.ThematicRoles.EventModifier (Time : Type u_3) [LE Time] : Type u_3

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

Equations

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

def Semantics.Events.ThematicRoles.modify {Time : Type u_3} [LE Time] (P : EvPred Time) (M : EventModifier Time) : EvPred Time

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

Equations

• Semantics.Events.ThematicRoles.modify P M e = (P e ∧ M e)

theorem Semantics.Events.ThematicRoles.modify_comm {Time : Type u_3} [LE Time] (P : 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.Events.ThematicRoles.modify_assoc {Time : Type u_3} [LE Time] (P : EvPred Time) (M₁ M₂ : EventModifier Time) : modify (modify P M₁) M₂ = modify P fun (e : Ev Time) => M₁ e ∧ M₂ e

Modification is associative.

def Semantics.Events.ThematicRoles.stativeLogicalForm {Entity : Type u_3} {Time : Type u_4} [LE Time] (P : EvPred Time) (frame : ThematicFrame Entity Time) (x : Entity) : Prop

Neo-Davidsonian logical form for a stative predicate with a holder: "x is happy" ↦ ∃s. P(s) ∧ Holder(x, s)

Parallel to intransitiveLogicalForm but using holder instead of agent, reflecting that states select for holders, not agents. @cite{wellwood-2015}: gradable adjectives predicate of states with mereological structure.

Note: EventModifier applies to states since states are events (of sort .state).

Equations

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

def Semantics.Events.ThematicRoles.modifiedStativeLogicalForm {Entity : Type u_3} {Time : Type u_4} [LE Time] (P : EvPred Time) (frame : ThematicFrame Entity Time) (x : Entity) (M : EventModifier Time) : Prop

Modified stative logical form: "x is happy in the morning" ↦ ∃s. P(s) ∧ Holder(x, s) ∧ M(s)

State modification is event modification applied to states: the modifier M restricts the state variable via conjunction, exactly as adverbial modifiers restrict event variables in @cite{davidson-1967}.

Equations

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

theorem Semantics.Events.ThematicRoles.modified_stative_is_pm {Entity : Type u_3} {Time : Type u_4} [LE Time] (P : 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): modifiedStativeLogicalForm P frame x M ↔ stativeLogicalForm (modify P M) frame x

This makes explicit that state modification is an instance of Davidson's conjunction-based event modification: modifying the state predicate P by M and then existentially closing is the same as existentially closing P ∧ Holder ∧ M.