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
• CosModel.again + againRestitutive/againRepetitiveBecome/againRepetitiveCause — the sublexical again operator and its three attachment readings

Main results

• CosModel.causative_entails_inchoative, denote_result_entails_resultState — the [BKG20] entailments, derived from the root signature
• CosModel.againPresup_cause_entails_state, result_restitution_entails_change — the [BKG20] (25) reading hierarchy and the result-root restitutive collapse, derived from the change-of-state entailments

References

• [Dav67], [Par90] (neo-Davidsonian composition)
• [BKG20] (the change-of-state decomposition; sublexical again)
• [vS96] (the again presupposition analysis adopted in BKG (26))
• [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]).

Sublexical again — the restitutive/repetitive hierarchy

([beavers-koontz-garboden-2020] §1.3.2, exs (25)–(27))

again is a presupposition trigger that can attach at three points in the change-of-state structure — the root, vbecome, or vcause — yielding the three readings of Mary flattened the rug again in BKG (25): restitutive ("it had been flat", a prior state), repetitive over the change ("it had flattened", a prior become event), and repetitive over the causation ("Mary had flattened it", a prior cause event). BKG (26) (a simplified [vS96]) defines ⟦again⟧ = λPλe. P(e) ∧ ∂∃e′[e′ ≪ e ∧ P(e′)]: P of the eventuality, plus the presupposition (∂) of a strictly earlier P-eventuality (e′ ≪ e). The reading hierarchy (25c) ⊨ (25b) ⊨ (25a) and the result-root collapse (§2.4, exs (43)/(45): a result root's state entails its own change, so even root-scope again is repetitive) fall out of the change-of-state entailments above.

def Verb.CosModel.again {ι : Type u_4} (lt : ι → ι → Prop) (P : ι → Prop) (e : ι) : Prop

BKG (26): the sublexical modifier again. Given a precedence ≪ (lt) on an eventuality type ι and a predicate P, again asserts P e and presupposes a strictly earlier e′ ≪ e with P e′. Following BKG we do not analyse the ∂ operator further — the earlier-eventuality conjunct is the presupposition (againPresup).

Equations

• Verb.CosModel.again lt P e = (P e ∧ ∃ (e' : ι), lt e' e ∧ P e')

def Verb.CosModel.againPresup {ι : Type u_4} (lt : ι → ι → Prop) (P : ι → Prop) (e : ι) : Prop

The presupposition again contributes (BKG (26), the ∂-marked conjunct): a strictly earlier eventuality also satisfying P.

Equations

• Verb.CosModel.againPresup lt P e = ∃ (e' : ι), lt e' e ∧ P e'

theorem Verb.CosModel.again_iff {ι : Type u_4} (lt : ι → ι → Prop) (P : ι → Prop) (e : ι) : again lt P e ↔ P e ∧ againPresup lt P e

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

BKG (27a): again attached low, to the root √V. The asserted/presupposed predicate is the root state, so the presupposition is of a strictly earlier root-state of the patient — the restitutive reading.

Equations

• M.againRestitutive ltS v x s = Verb.CosModel.again ltS (M.rootState v x) s

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

BKG (27b): again attached to vbecomeP. The predicate is the inchoative change event, so the presupposition is of a strictly earlier change — the repetitive-over-change reading.

Equations

• M.againRepetitiveBecome ltE v x e = Verb.CosModel.again ltE (M.inchoative v x) e

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

BKG (27c): again attached high, to vcauseP. The predicate is the causative causing event, so the presupposition is of a strictly earlier causation — the repetitive-over-causation reading.

Equations

• M.againRepetitiveCause ltE v y x w = Verb.CosModel.again ltE (M.causative v y x) w

theorem Verb.CosModel.againPresup_cause_entails_become {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (M : CosModel Entity State Time) (lt : Event Time → Event Time → Prop) (v : Verb) (y x : Entity) (w : Event Time) (h : againPresup lt (M.causative v y x) w) : ∃ (w' : Event Time), lt w' w ∧ ∃ (e : Event Time), M.inchoative v x e

BKG (25) hierarchy, upper step: the repetitive-causation presupposition (25c, "Mary had flattened it before") entails the repetitive-change presupposition (25b, "it had flattened before") — the earlier causing event is an earlier change, by causative_entails_inchoative. The ≪-witness is carried through.

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

BKG (25) hierarchy, lower step: the repetitive-change presupposition (25b, "it had flattened before") entails the restitutive presupposition (25a, "it had been flat before") — the earlier change gives rise to an earlier root state, by inchoative_entails_resultState.

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

BKG (25) hierarchy, end to end: the repetitive-causation presupposition (25c) entails the restitutive presupposition (25a) — "Mary had flattened it before" ⊨ "it had been flat before". The two steps composed through the change-of-state decomposition (causative_entails_resultState).

theorem Verb.CosModel.result_restitution_entails_change {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (M : CosModel Entity State Time) (ltS : State → State → Prop) (v : Verb) (x : Entity) (s : State) (hres : ∀ (s : State), M.rootState v x s → ∃ (e : Event Time), M.become s e) (h : againPresup ltS (M.rootState v x) s) : ∃ (s' : State), ltS s' s ∧ ∃ (e : Event Time), M.become s' e

BKG §2.4 (45): for a result root the root state itself entails a prior change (∃ become), so even the low/restitutive attachment of again over the root carries a change entailment — the restitutive reading collapses into the repetitive one ([BKG20]: "result roots never admit truly restitutive readings"). Formally, the restitutive presupposition (an earlier state) already delivers an earlier change. The premise hres is BKG (45a)'s meaning, realized by a root whose closedKinds contain .result (cf. denote_result_entails_resultState).