Interpretations of the event-structure primitives

This file defines the interpretations of the primitives of event-structural decomposition. An interpretation gives the three relations that the verbal heads introduce: an eventuality gives rise to a state, an eventuality causes another, and an individual is the effector of an eventuality. In the vocabulary of model theory it is a structure for the signature with these three relation symbols, over the sorts of individuals, states and eventualities. The heads themselves are operators on predicates. vBecome turns a state predicate into the predicate of the events that give rise to such a state, and vCause turns an event predicate into the predicate of the events that cause such an event.

A state predicate may itself entail a change, a cause of the change, or a manner of the causing event. These are the meaning postulates that Beavers and Koontz-Garboden attach to the state predicate of a root, one for each kind of entailment. The postulates of a kind signature form a theory, and an interpretation Respects the signature for a predicate when it is a model of that theory. An entailment is then a statement about every interpretation, and a failure of entailment is witnessed by one.

Main definitions

• EventStructure.Interpretation: the relations become, cause and effector.
• Interpretation.vBecome, Interpretation.vCause: the two heads.
• Interpretation.EntailsChange, EntailsCause, EntailsManner: the postulates on a state predicate.
• Interpretation.Respects: the interpretation is a model of the postulates of a signature.

Main results

• Interpretation.Entails.anti: the postulates are downward closed along the order on kinds.
• Interpretation.respects_close: a signature and its collocational closure have the same models.

Implementation notes

The sorts are type parameters, so a relation cannot be applied to an argument of the wrong sort. mathlib's first-order structures are single-sorted; a view of an interpretation as such a structure, with the postulates as sentences, is not yet defined.

References

• [BKG20]

structure ArgumentStructure.EventStructure.Interpretation (Entity : Type u_1) (State : Type u_2) (Event : Type u_3) : Type (max (max u_1 u_2) u_3)

An interpretation of the event-structure primitives, the relations that the verbal heads introduce.

• become : State → Event → Prop

  The eventuality gives rise to the state.

• cause : Event → Event → Prop

  The first eventuality causes the second.

• effector : Entity → Event → Prop

  The individual is the effector of the eventuality.

def ArgumentStructure.EventStructure.Interpretation.vBecome {Entity : Type u_1} {State : Type u_2} {Event : Type u_3} (M : Interpretation Entity State Event) (P : Entity → State → Prop) (x : Entity) (e : Event) : Prop

The change-of-state head vBecome P x holds of the events that give rise to a state of which P x holds.

Equations

• M.vBecome P x e = ∃ (s : State), M.become s e ∧ P x s

def ArgumentStructure.EventStructure.Interpretation.vCause {Entity : Type u_1} {State : Type u_2} {Event : Type u_3} (M : Interpretation Entity State Event) (Q : Event → Prop) (y : Entity) (v : Event) : Prop

The causative head vCause Q y holds of the events whose effector is y and which cause an event of which Q holds.

Equations

• M.vCause Q y v = ∃ (e : Event), M.effector y v ∧ M.cause v e ∧ Q e

theorem ArgumentStructure.EventStructure.Interpretation.vBecome_mono {Entity : Type u_1} {State : Type u_2} {Event : Type u_3} {M : Interpretation Entity State Event} {P P' : Entity → State → Prop} (h : P ≤ P') : M.vBecome P ≤ M.vBecome P'

theorem ArgumentStructure.EventStructure.Interpretation.vCause_mono {Entity : Type u_1} {State : Type u_2} {Event : Type u_3} {M : Interpretation Entity State Event} {Q Q' : Event → Prop} (h : Q ≤ Q') : M.vCause Q ≤ M.vCause Q'

theorem ArgumentStructure.EventStructure.Interpretation.exists_state_of_vBecome {Entity : Type u_1} {State : Type u_2} {Event : Type u_3} {M : Interpretation Entity State Event} {P : Entity → State → Prop} {x : Entity} {e : Event} (h : M.vBecome P x e) : ∃ (s : State), M.become s e ∧ P x s

A change gives rise to a state of the predicate.

theorem ArgumentStructure.EventStructure.Interpretation.exists_of_vCause {Entity : Type u_1} {State : Type u_2} {Event : Type u_3} {M : Interpretation Entity State Event} {Q : Event → Prop} {y : Entity} {e : Event} (h : M.vCause Q y e) : ∃ (e' : Event), Q e'

A causing event has a caused event of the embedded predicate.

Meaning postulates on a state predicate

def ArgumentStructure.EventStructure.Interpretation.EntailsChange {Entity : Type u_1} {State : Type u_2} {Event : Type u_3} (M : Interpretation Entity State Event) (P : Entity → State → Prop) : Prop

The state predicate P entails change when every state of which it holds arises from a change.

Equations

• M.EntailsChange P = ∀ (x : Entity) (s : State), P x s → ∃ (e : Event), M.become s e

def ArgumentStructure.EventStructure.Interpretation.EntailsCause {Entity : Type u_1} {State : Type u_2} {Event : Type u_3} (M : Interpretation Entity State Event) (P : Entity → State → Prop) : Prop

The state predicate P entails a cause when every state of which it holds arises from a change that some event causes.

Equations

• M.EntailsCause P = ∀ (x : Entity) (s : State), P x s → ∃ (e : Event) (v : Event), M.become s e ∧ M.cause v e

def ArgumentStructure.EventStructure.Interpretation.EntailsManner {Entity : Type u_1} {State : Type u_2} {Event : Type u_3} (M : Interpretation Entity State Event) (P : Entity → State → Prop) (Q : Event → Prop) : Prop

The state predicate P entails the manner Q when every state of which it holds arises from a change whose every cause is a Q-event.

Equations

• M.EntailsManner P Q = ∀ (x : Entity) (s : State), P x s → ∃ (e : Event), M.become s e ∧ ∀ (v : Event), M.cause v e → Q v

def ArgumentStructure.EventStructure.Interpretation.Entails {Entity : Type u_1} {State : Type u_2} {Event : Type u_3} (M : Interpretation Entity State Event) (P : Entity → State → Prop) (Q : Event → Prop) : Semantics.Root.Kind → Prop

The meaning postulate of a kind of root entailment for the state predicate P, with Q the manner. A state imposes nothing beyond the predicate itself.

Equations

• M.Entails P Q Semantics.Root.Kind.state = True
• M.Entails P Q Semantics.Root.Kind.result = M.EntailsChange P
• M.Entails P Q Semantics.Root.Kind.cause = M.EntailsCause P
• M.Entails P Q Semantics.Root.Kind.manner = M.EntailsManner P Q

def ArgumentStructure.EventStructure.Interpretation.Respects {Entity : Type u_1} {State : Type u_2} {Event : Type u_3} (M : Interpretation Entity State Event) (P : Entity → State → Prop) (Q : Event → Prop) (ks : Semantics.Root.Kinds) : Prop

The interpretation respects the kind signature ks for P and Q when it is a model of the postulates of its kinds.

Equations

• M.Respects P Q ks = ∀ k ∈ ks, M.Entails P Q k

theorem ArgumentStructure.EventStructure.Interpretation.EntailsCause.entailsChange {Entity : Type u_1} {State : Type u_2} {Event : Type u_3} {M : Interpretation Entity State Event} {P : Entity → State → Prop} (h : M.EntailsCause P) : M.EntailsChange P

theorem ArgumentStructure.EventStructure.Interpretation.EntailsManner.entailsChange {Entity : Type u_1} {State : Type u_2} {Event : Type u_3} {M : Interpretation Entity State Event} {P : Entity → State → Prop} {Q : Event → Prop} (h : M.EntailsManner P Q) : M.EntailsChange P

theorem ArgumentStructure.EventStructure.Interpretation.Entails.anti {Entity : Type u_1} {State : Type u_2} {Event : Type u_3} {M : Interpretation Entity State Event} {P : Entity → State → Prop} {Q : Event → Prop} {j k : Semantics.Root.Kind} (hkj : k ≤ j) (h : M.Entails P Q j) : M.Entails P Q k

The postulates are downward closed along the collocational order on kinds, since a cause entails a change and both entail a state.

theorem ArgumentStructure.EventStructure.Interpretation.Respects.mono {Entity : Type u_1} {State : Type u_2} {Event : Type u_3} {M : Interpretation Entity State Event} {P : Entity → State → Prop} {Q : Event → Prop} {ks ks' : Semantics.Root.Kinds} (hks : ks ⊆ ks') (h : M.Respects P Q ks') : M.Respects P Q ks

@[simp]

theorem ArgumentStructure.EventStructure.Interpretation.respects_close {Entity : Type u_1} {State : Type u_2} {Event : Type u_3} {M : Interpretation Entity State Event} {P : Entity → State → Prop} {Q : Event → Prop} {ks : Semantics.Root.Kinds} : M.Respects P Q ks.close ↔ M.Respects P Q ks

A signature is respected iff its collocational closure is.

theorem ArgumentStructure.EventStructure.Interpretation.Respects.entailsChange {Entity : Type u_1} {State : Type u_2} {Event : Type u_3} {M : Interpretation Entity State Event} {P : Entity → State → Prop} {Q : Event → Prop} {ks : Semantics.Root.Kinds} (h : M.Respects P Q ks) (hr : Semantics.Root.Kind.result ∈ ks.close) : M.EntailsChange P

An interpretation that respects a signature whose closure has a result satisfies the postulate of change.