Beavers & Koontz-Garboden (2020): The Roots of Verbal Meaning

[BKG20]

The six representative roots of the book's root typology (ch. 5), and the falsification of the Bifurcation Thesis of Roots ([Emb09]; [Ara05]) and of Manner/Result Complementarity ([RHL10]).

Root	manner	cause	result	state	position
√flat				✓	complement
√blossom			✓	✓	complement
√crack		✓	✓	✓	complement
√jog	✓				adjoined
√hand	✓	✓	✓	✓	adjoined
√drown	✓	✓	✓	✓	complement

The +state cells of √blossom, √crack, √hand, √drown are derived: the book's typology values are the collocational closures (Root.closedKinds) of the base atom kinds, and each closed signature is one of the canonical typology rows (Root.Kinds.pureResult, causativeResult, fullSpec). √blossom falsifies Bifurcation on its own, since change of state is templatic (v_become) content. √hand and √drown additionally falsify Manner/Result Complementarity; they differ only in root position (adjoined vs complement), the contrast carrying the book's account of which root types are attested.

Main declarations

• Root.Kinds.ViolatesBifurcation, Root.HasMannerAndResult and relatives — the two thesis predicates, at signature and root level
• flat, jog, blossom, crack, hand, drown
• exists_violatesBifurcation, bifurcation_thesis_false
• exists_hasMannerAndResult, manner_result_complementarity_false
• Verb.CosModel.again and the (25)–(27) reading hierarchy

The thesis predicates and the sublexical again operator are carried here as single-consumer apparatus (this study is their only consumer); they graduate back to the theory layer when a second study lands.

The two theses, at signature level

def Verb.Root.Kinds.ontological : Kinds

The ontological kinds — all the Bifurcation Thesis allows a root to carry.

Equations

• Verb.Root.Kinds.ontological = {Verb.LexKind.state, Verb.LexKind.manner}

def Verb.Root.Kinds.ViolatesBifurcation (s : Kinds) : Prop

A signature violates the Bifurcation Thesis ([Emb09]; the assumption of [Ara05]) iff it carries templatic (eventive) content — it is not bounded by ontological.

Equations

• s.ViolatesBifurcation = ¬s ⊆ Verb.Root.Kinds.ontological

@[instance_reducible]

instance Verb.Root.Kinds.instDecidableViolatesBifurcation (s : Kinds) : Decidable s.ViolatesBifurcation

Equations

• s.instDecidableViolatesBifurcation = Verb.Root.Kinds.instDecidableViolatesBifurcation._aux_1 s

theorem Verb.Root.Kinds.violatesBifurcation_iff (s : Kinds) : s.ViolatesBifurcation ↔ LexKind.result ∈ s ∨ LexKind.cause ∈ s

Violation is carrying a result or cause kind.

theorem Verb.Root.Kinds.violatesBifurcation_mono {s t : Kinds} : s ⊆ t → s.ViolatesBifurcation → t.ViolatesBifurcation

Bifurcation violation is monotone: adding entailments cannot repair a violation.

def Verb.Root.Kinds.HasMannerAndResult (s : Kinds) : Prop

A signature has both manner and result — the configuration Manner/Result Complementarity ([RHL10]) claims no root realizes.

Equations

• s.HasMannerAndResult = ({Verb.LexKind.manner, Verb.LexKind.result} ⊆ s)

@[instance_reducible]

instance Verb.Root.Kinds.instDecidableHasMannerAndResult (s : Kinds) : Decidable s.HasMannerAndResult

Equations

• s.instDecidableHasMannerAndResult = Verb.Root.Kinds.instDecidableHasMannerAndResult._aux_1 s

theorem Verb.Root.Kinds.hasMannerAndResult_mono {s t : Kinds} : s ⊆ t → s.HasMannerAndResult → t.HasMannerAndResult

MRC violation is monotone in the signature order.

theorem Verb.Root.Kinds.violatesBifurcation_close_iff (s : Kinds) : s.close.ViolatesBifurcation ↔ s.ViolatesBifurcation

Bifurcation is invariant under collocational closure: close only adds state/result kinds forced by cause, never manner.

theorem Verb.Root.Kinds.hasMannerAndResult_close_iff (s : Kinds) : s.close.HasMannerAndResult ↔ s.HasMannerAndResult ∨ LexKind.manner ∈ s ∧ LexKind.cause ∈ s

The two theses, at root level

def Verb.Root.ViolatesBifurcation (r : Root) : Prop

A root violates Bifurcation iff it itself carries templatic (eventive) meaning — change of state or cause (Root.Kinds.violatesBifurcation_iff).

Equations

• r.ViolatesBifurcation = r.kinds.ViolatesBifurcation

@[instance_reducible]

instance Verb.Root.instDecidableViolatesBifurcation (r : Root) : Decidable r.ViolatesBifurcation

Equations

• r.instDecidableViolatesBifurcation = Verb.Root.instDecidableViolatesBifurcation._aux_1 r

def Verb.Root.RespectsBifurcation (r : Root) : Prop

Negation of ViolatesBifurcation: the root carries only ontological entailments (state, manner).

Equations

• r.RespectsBifurcation = ¬r.ViolatesBifurcation

@[instance_reducible]

instance Verb.Root.instDecidableRespectsBifurcation (r : Root) : Decidable r.RespectsBifurcation

Equations

• r.instDecidableRespectsBifurcation = Verb.Root.instDecidableRespectsBifurcation._aux_1 r

theorem Verb.Root.respectsBifurcation_iff_le {r : Root} : r.RespectsBifurcation ↔ r.kinds ⊆ Kinds.ontological

The thesis as an order statement: a root respects Bifurcation iff its signature is bounded by the ontological kinds.

def Verb.Root.HasMannerAndResult (r : Root) : Prop

A root has both manner and result entailments — Manner/Result Complementarity ([RHL10]) is the universal claim that no root does.

Equations

• r.HasMannerAndResult = r.kinds.HasMannerAndResult

@[instance_reducible]

instance Verb.Root.instDecidableHasMannerAndResult (r : Root) : Decidable r.HasMannerAndResult

Equations

• r.instDecidableHasMannerAndResult = Verb.Root.instDecidableHasMannerAndResult._aux_1 r

def Verb.Root.RespectsMannerResultComplementarity (r : Root) : Prop

Negation of HasMannerAndResult.

Equations

• r.RespectsMannerResultComplementarity = ¬r.HasMannerAndResult

@[instance_reducible]

instance Verb.Root.instDecidableRespectsMannerResultComplementarity (r : Root) : Decidable r.RespectsMannerResultComplementarity

Equations

• r.instDecidableRespectsMannerResultComplementarity = Verb.Root.instDecidableRespectsMannerResultComplementarity._aux_1 r

Sublexical again — the restitutive/repetitive hierarchy (§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 (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). (26) (a simplified [vS96]) defines ⟦again⟧ = λPλe. P(e) ∧ ∂∃e′[e′ ≪ e ∧ P(e′)]. The reading hierarchy (25c) ⊨ (25b) ⊨ (25a) and the result-root collapse (§2.4, exs (43)/(45)) fall out of the change-of-state entailments of Verb.CosModel.

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

(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′. The ∂ operator is not analysed 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 ((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

(27a): again attached low, to the root √V. The asserted/presupposed predicate is the root state — 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

(27b): again attached to vbecomeP — 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

(27c): again attached high, to vcauseP — 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

(25) hierarchy, upper step: the repetitive-causation presupposition (25c) entails the repetitive-change presupposition (25b) — the earlier causing event is an earlier change, by causative_entails_inchoative.

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

(25) hierarchy, lower step: the repetitive-change presupposition (25b) entails the restitutive presupposition (25a) — 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

(25) hierarchy, end to end: "Mary had flattened it before" ⊨ "it had been flat before", 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

§2.4 (45): for a result root the root state itself entails a prior change, so even the low/restitutive attachment of again carries a change entailment — the restitutive reading collapses into the repetitive one ("result roots never admit truly restitutive readings").

The six representative roots

def BeaversKoontzGarboden2020.flat : Verb.Root

√flat — pure state.

Equations

• BeaversKoontzGarboden2020.flat = { name := "flat", entailments := {Verb.LexEntailment.hasState "flat"} }

def BeaversKoontzGarboden2020.jog : Verb.Root

√jog — pure manner of motion.

Equations

• BeaversKoontzGarboden2020.jog = { name := "jog", entailments := {Verb.LexEntailment.hasManner "jogging-gait"} }

def BeaversKoontzGarboden2020.blossom : Verb.Root

√blossom — result with no specified manner or cause (an internally caused change of state).

Equations

• BeaversKoontzGarboden2020.blossom = { name := "blossom", entailments := {Verb.LexEntailment.becomesState "flowering"} }

def BeaversKoontzGarboden2020.crack : Verb.Root

√crack — caused result without specified manner.

Equations

• BeaversKoontzGarboden2020.crack = { name := "crack", entailments := {Verb.LexEntailment.becomesState "fissured", Verb.LexEntailment.hasCause} }

def BeaversKoontzGarboden2020.hand : Verb.Root

√hand — manner + cause + result, adjoined position. The possession result is non-cancelable ("#Mary handed John the book, but he never got it"), so it is root-entailed rather than implicated ([BKG20] ch. 3).

Equations

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

def BeaversKoontzGarboden2020.drown : Verb.Root

√drown — manner of killing (Levin 1993's crucify, drown, hang, electrocute class; [BKG20] ch. 4): manner + cause + result, complement position.

Equations

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

Kind signatures

Base signatures record the atom kinds; closed signatures are their collocational closures, and coincide with the canonical rows of the book's typology.

theorem BeaversKoontzGarboden2020.flat_kinds : flat.kinds = {Verb.LexKind.state}

theorem BeaversKoontzGarboden2020.jog_kinds : jog.kinds = {Verb.LexKind.manner}

theorem BeaversKoontzGarboden2020.blossom_kinds : blossom.kinds = {Verb.LexKind.result}

theorem BeaversKoontzGarboden2020.crack_kinds : crack.kinds = {Verb.LexKind.result, Verb.LexKind.cause}

theorem BeaversKoontzGarboden2020.hand_kinds : hand.kinds = {Verb.LexKind.manner, Verb.LexKind.result, Verb.LexKind.cause}

theorem BeaversKoontzGarboden2020.drown_kinds : drown.kinds = {Verb.LexKind.manner, Verb.LexKind.result, Verb.LexKind.cause}

theorem BeaversKoontzGarboden2020.flat_closedKinds : flat.closedKinds = Verb.Root.Kinds.propertyConcept

theorem BeaversKoontzGarboden2020.jog_closedKinds : jog.closedKinds = Verb.Root.Kinds.pureManner

theorem BeaversKoontzGarboden2020.blossom_closedKinds : blossom.closedKinds = Verb.Root.Kinds.pureResult

theorem BeaversKoontzGarboden2020.crack_closedKinds : crack.closedKinds = Verb.Root.Kinds.causativeResult

theorem BeaversKoontzGarboden2020.hand_closedKinds : hand.closedKinds = Verb.Root.Kinds.fullSpec

theorem BeaversKoontzGarboden2020.drown_closedKinds : drown.closedKinds = Verb.Root.Kinds.fullSpec

Falsifying the Bifurcation Thesis

theorem BeaversKoontzGarboden2020.blossom_violatesBifurcation : blossom.ViolatesBifurcation

√blossom entails change of state — templatic (v_become) content in the root — falsifying Bifurcation without any manner or cause entailment.

theorem BeaversKoontzGarboden2020.crack_violatesBifurcation : crack.ViolatesBifurcation

theorem BeaversKoontzGarboden2020.hand_violatesBifurcation : hand.ViolatesBifurcation

theorem BeaversKoontzGarboden2020.drown_violatesBifurcation : drown.ViolatesBifurcation

theorem BeaversKoontzGarboden2020.exists_violatesBifurcation : ∃ (r : Verb.Root), r.ViolatesBifurcation

Some root carries templatic content.

theorem BeaversKoontzGarboden2020.bifurcation_thesis_false : ¬∀ (r : Verb.Root), r.RespectsBifurcation

The universal closure of the Bifurcation Thesis is false.

Falsifying Manner/Result Complementarity

theorem BeaversKoontzGarboden2020.hand_hasMannerAndResult : hand.HasMannerAndResult

√hand entails both a manner (by-hand transfer) and a result (recipient possession).

theorem BeaversKoontzGarboden2020.drown_hasMannerAndResult : drown.HasMannerAndResult

√drown entails both a manner (submersion) and a result (death); it differs from √hand in root position.

theorem BeaversKoontzGarboden2020.exists_hasMannerAndResult : ∃ (r : Verb.Root), r.HasMannerAndResult

Some root entails both a manner and a result.

theorem BeaversKoontzGarboden2020.manner_result_complementarity_false : ¬∀ (r : Verb.Root), r.RespectsMannerResultComplementarity

The universal closure of Manner/Result Complementarity is false.

Roots respecting each constraint

theorem BeaversKoontzGarboden2020.flat_respectsBifurcation : flat.RespectsBifurcation

√flat (pure state) respects Bifurcation: its signature is bounded by the ontological kinds.

theorem BeaversKoontzGarboden2020.jog_respectsBifurcation : jog.RespectsBifurcation

√jog (pure manner) respects Bifurcation.

theorem BeaversKoontzGarboden2020.crack_respectsMannerResultComplementarity : crack.RespectsMannerResultComplementarity

√crack (cause + result, no manner) respects Manner/Result Complementarity.

The roots cash out denotationally ([BKG20] §1.3.2)

Threading the roots through the change-of-state denotation (Verb.CosModel): a verb's denotation is dispatched on its root's kinds, so the kinds proven above select the event template and the result entailment of (6) follows from the signature. √crack (+cause+result) entails a result state in any model; √jog (pure manner) does not — the break/hit contrast.

def BeaversKoontzGarboden2020.crackV : Verb

crack the change-of-state verb (Mary cracked the vase).

Equations

• BeaversKoontzGarboden2020.crackV = { frames := [Frame.np], root := BeaversKoontzGarboden2020.crack, form := "crack" }

def BeaversKoontzGarboden2020.jogV : Verb

jog the pure-manner activity verb (Mary jogged).

Equations

• BeaversKoontzGarboden2020.jogV = { frames := [], root := BeaversKoontzGarboden2020.jog, form := "jog" }

theorem BeaversKoontzGarboden2020.crack_denote_entails_result {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (M : Verb.CosModel Entity State Time) (y x : Entity) (e : Event Time) (h : M.denote crackV y x e) : ∃ (e' : Event Time) (s : State), M.become s e' ∧ M.rootState crackV x s

√crack carries .result, so in any model its denotation entails the result state — the non-cancelable result of [BKG20] (6), derived from crack's signature rather than stipulated.

theorem BeaversKoontzGarboden2020.jog_denote_eq_manner {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (M : Verb.CosModel Entity State Time) (y x : Entity) : M.denote jogV y x = M.manner jogV

√jog has no .result (nor .cause), so its denotation is the bare manner core — no become, no result state. Only the change-of-state root entails a result.

The same contrast at the template level ([RHL98])

Verb.Root.template reads the event-structure template off a root's collocational closure; the kinds proven above fix it, and HasResultState reduces to carrying result (Verb.Root.template_hasResultState_iff). So the denotational result entailment (√crack) and the template result diagnostic are one fact seen through kinds.

theorem BeaversKoontzGarboden2020.flat_template : flat.template = ArgumentStructure.EventStructure.Template.state

theorem BeaversKoontzGarboden2020.jog_template : jog.template = ArgumentStructure.EventStructure.Template.activity

theorem BeaversKoontzGarboden2020.blossom_template : blossom.template = ArgumentStructure.EventStructure.Template.achievement

theorem BeaversKoontzGarboden2020.crack_template : crack.template = ArgumentStructure.EventStructure.Template.accomplishment

theorem BeaversKoontzGarboden2020.crack_template_hasResultState : crack.template.HasResultState

√crack's template embeds a result state (it carries result); √jog's does not — the break/hit contrast, now at the template layer and provably the same signature fact as crack_denote_entails_result.

theorem BeaversKoontzGarboden2020.jog_template_no_resultState : ¬jog.template.HasResultState

theorem BeaversKoontzGarboden2020.crack_template_forces_denote_result {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (M : Verb.CosModel Entity State Time) (y x : Entity) (e : Event Time) (h : M.denote crackV y x e) : ∃ (e' : Event Time) (s : State), M.become s e' ∧ M.rootState crackV x s

√crack's template embeds a result state, so by denote_result_from_template its denotation entails the result state in any model — the template diagnostic and the denotational entailment are one fact through crack's kinds.