Verb denotation — what a verb does

A verb is, first of all, an operation: applied to its arguments it builds an event predicate. This file is that operation — the DO layer of the Verb API — parallel to how the φ substrate models person features as operations rather than predicates.

For a change-of-state verb the operation is the [BKG20] §1.3.2 decomposition (Verb.CosModel): a root denotes a state predicate and the event predicate is built by become'/cause', dispatched on the root's kinds. The proto-role theta-grid (Verb.subjectRole/objectRole, derived from the effective EntailmentProfiles via EntailmentProfile.toRole) supplies the participant roles.

Main definitions

• Verb.subjectRole / Verb.objectRole — the theta-grid from the proto-role profiles
• Verb.CosModel + inchoative/causative/denote — the change-of-state denotation, dispatched on the root's kinds

Main results

• CosModel.causative_entails_inchoative, denote_result_entails_resultState — the [BKG20] entailments, derived from the root signature

The sublexical again operator and its reading hierarchy live with their anchoring study, Studies/BeaversKoontzGarboden2020.lean.

References

• [Dav67], [Par90] (neo-Davidsonian composition)
• [BKG20] (the change-of-state decomposition)
• [Dow91] (the proto-role profiles that drive the theta-grid)

The theta-grid (derived from the proto-role profiles)

def Verb.subjectRole (v : Verb) : Option ThetaRole

The subject's theta-role, derived from its effective EntailmentProfile (verb override, else Levin-class profile) via EntailmentProfile.toRole.

Equations

• v.subjectRole = v.effectiveSubjectEntailments.bind fun (x : ArgumentStructure.EntailmentProfile) => x.toRole

def Verb.objectRole (v : Verb) : Option ThetaRole

The object's theta-role, derived from its effective EntailmentProfile.

Equations

• v.objectRole = v.effectiveObjectEntailments.bind fun (x : ArgumentStructure.EntailmentProfile) => x.toRole

Change-of-state decomposition ([BKG20] §1.3.2)

For a change-of-state verb the opaque lexical core unpacks into the event-structural decomposition of [BKG20] (22)–(24): a root denotes a state predicate ⟦√V⟧(x,s), and the verb's event predicate is built by the templatic operators become' and cause'. The root's kinds selects which operators apply — .result → become, .cause → cause/effector — so the decomposition is the denotational payoff of the root's kinds.

structure Verb.CosModel (Entity : Type u_1) (State : Type u_2) (Time : Type u_3) [LinearOrder Time] : Type (max (max u_1 u_2) u_3)

The change-of-state model ([BKG20] (22)): the templatic primitives a COS verb's denotation is built from. become/cause/ effector are model primitives here (BKG refine their truth conditions in their §1.6); a Study instantiates them.

• rootState : Verb → Entity → State → Prop

  ⟦√V⟧(x,s) (BKG (22a)): a state s of the root's lexical property holds of x (e.g. flat'(x,s)). The root denotes a state predicate.

• become : State → Event Time → Prop

  become'(s,e) (BKG (22b)): event e gives rise to state s.

• cause : Event Time → Event Time → Prop

  cause'(v,e) (BKG (22c)): event v causes event e.

• effector : Entity → Event Time → Prop

  effector'(y,v) (BKG (22c)): y is the effector of event v.

• manner : Verb → Event Time → Prop

  The bare manner/activity core ⟦√V⟧(e) of a pure-manner root (no change), e.g. jog/run's action specification.

def Verb.CosModel.inchoative {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (M : CosModel Entity State Time) (v : Verb) (x : Entity) : Event Time → Prop

The inchoative denotation ([BKG20] (23c)): λxλe. ∃s. become'(s,e) ∧ ⟦√V⟧(x,s) — an event of change giving rise to a state of the root's property holding of the patient x.

Equations

• M.inchoative v x e = ∃ (s : State), M.become s e ∧ M.rootState v x s

def Verb.CosModel.causative {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (M : CosModel Entity State Time) (v : Verb) (y x : Entity) : Event Time → Prop

The causative denotation ([BKG20] (24c)): the inchoative embedded under an effector and a causing event — λyλxλw. ∃e. effector'(y,w) ∧ cause'(w,e) ∧ inchoative(x)(e).

Equations

• M.causative v y x w = ∃ (e : Event Time), M.effector y w ∧ M.cause w e ∧ M.inchoative v x e

theorem Verb.CosModel.causative_entails_inchoative {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (M : CosModel Entity State Time) (v : Verb) (y x : Entity) (w : Event Time) (h : M.causative v y x w) : ∃ (e : Event Time), M.inchoative v x e

BKG's first prediction ([BKG20] p. 16): the causative entails the inchoative — there is an event satisfying the inchoative, "by simple virtue of" the embedding (∃-projection over the caused event). Holds by construction, not stipulation.

theorem Verb.CosModel.inchoative_entails_resultState {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (M : CosModel Entity State Time) (v : Verb) (x : Entity) (e : Event Time) (h : M.inchoative v x e) : ∃ (s : State), M.become s e ∧ M.rootState v x s

The result-state entailment: the inchoative entails the patient reaches a state of the root's property — ∃s. become'(s,e) ∧ ⟦√V⟧(x,s). The non-cancelable result of a change-of-state root (the break vs hit contrast, [BKG20] (6)); definitional, hence immediate.

theorem Verb.CosModel.causative_entails_resultState {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (M : CosModel Entity State Time) (v : Verb) (y x : Entity) (w : Event Time) (h : M.causative v y x w) : ∃ (e : Event Time) (s : State), M.become s e ∧ M.rootState v x s

Composing the two predictions: a caused change reaches the root state — the causative entails the full result-state condition.

def Verb.CosModel.denote {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (M : CosModel Entity State Time) (v : Verb) (y x : Entity) : Event Time → Prop

The verb's change-of-state denotation, dispatched on its root's kinds (cf. [BKG20] (18)–(19)): .cause → causative, else .result → inchoative, else the bare manner core. The root's kinds select the event template — the denotational payoff of the signature.

Equations

• M.denote v y x = if Verb.LexKind.cause ∈ v.closedKinds then M.causative v y x else if Verb.LexKind.result ∈ v.closedKinds then M.inchoative v x else M.manner v

theorem Verb.CosModel.denote_result_entails_resultState {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (M : CosModel Entity State Time) (v : Verb) (y x : Entity) (e : Event Time) (hres : LexKind.result ∈ v.closedKinds) (h : M.denote v y x e) : ∃ (e' : Event Time) (s : State), M.become s e' ∧ M.rootState v x s

The denotational payoff of a .result root: any verb whose root signature carries result has a denotation entailing the result state — whether the root is causative (.cause) or inchoative. The [BKG20] non-cancelable result, derived from the signature rather than stipulated (and absent for a pure-manner root, whose denote is the manner core).

theorem Verb.CosModel.denote_result_from_template {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (M : CosModel Entity State Time) (v : Verb) (ht : v.root.template.HasResultState) (y x : Entity) (e : Event Time) (h : M.denote v y x e) : ∃ (e' : Event Time) (s : State), M.become s e' ∧ M.rootState v x s

The denotational result entailment is the template diagnostic: a verb whose root's EventStructure.Template embeds a result state has a denotation entailing that result state — denote_result_entails_resultState and Template.HasResultState are one fact, through the closed kind signature ([BKG20]; [RHL98]).