Event Identification

This file defines Event Identification, the composition principle by which Kratzer adds an argument-introducing head to a predicate of events. The head denotes a relation between individuals and events, the predicate a set of events, and the two combine by conjunction at the event, leaving the individual argument open: an agent head and feed the dog yield the relation that holds of an individual and an event when the individual is the agent of the event and the event is a feeding of the dog. Event Identification is meet with the predicate lifted to a relation constant in the individual, so it is the relational counterpart of predicate modification, and repeated applications chain conditions on the same event.

Main definitions

• ArgumentStructure.eventIdentification: the combination of a relation and a predicate.

Main results

• eventIdentification_eq_inf, eventIdentification_eq_comp: Event Identification is meet with the lifted predicate, and predicate modification of each section of the relation.
• eventIdentification_eventIdentification: two applications conjoin the predicates.
• eventIdentification_eq_bot_iff: the result is empty exactly when, for every individual, the relation's events and the predicate's are disjoint.

Implementation notes

Kratzer's rule is partial: it is undefined when the two inputs restrict the event to disjoint sorts, actions and states. Here it is total, and such inputs yield the empty relation (eventIdentification_eq_bot_iff). The carrier is any pair of types, so that the type-driven composition engine, whose events share the domain of individuals, uses the same operation.

References

• [Kra96]

def ArgumentStructure.eventIdentification {α : Type u_1} {β : Type u_2} (f : α → β → Prop) (g : β → Prop) : α → β → Prop

Event Identification conjoins the relation f and the predicate g at the event, leaving the individual argument open.

Equations

• ArgumentStructure.eventIdentification f g x e = (f x e ∧ g e)

@[simp]

theorem ArgumentStructure.eventIdentification_apply {α : Type u_1} {β : Type u_2} {f : α → β → Prop} {g : β → Prop} (x : α) (e : β) : eventIdentification f g x e ↔ f x e ∧ g e

theorem ArgumentStructure.eventIdentification_eq_inf {α : Type u_1} {β : Type u_2} {f : α → β → Prop} {g : β → Prop} : eventIdentification f g = f ⊓ Function.const α g

theorem ArgumentStructure.eventIdentification_eq_comp {α : Type u_1} {β : Type u_2} {f : α → β → Prop} {g : β → Prop} : eventIdentification f g = Modifier.intersective g ∘ f

Event Identification is predicate modification of each of the relation's sections.

theorem ArgumentStructure.eventIdentification_mono {α : Type u_1} {β : Type u_2} {f f' : α → β → Prop} {g g' : β → Prop} (hf : f ≤ f') (hg : g ≤ g') : eventIdentification f g ≤ eventIdentification f' g'

theorem ArgumentStructure.eventIdentification_eventIdentification {α : Type u_1} {β : Type u_2} {f : α → β → Prop} {g : β → Prop} (h : β → Prop) : eventIdentification (eventIdentification f g) h = eventIdentification f (g ⊓ h)

theorem ArgumentStructure.eventIdentification_eq_bot_iff {α : Type u_1} {β : Type u_2} {f : α → β → Prop} {g : β → Prop} : eventIdentification f g = ⊥ ↔ ∀ (x : α), Disjoint (f x) g