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

This file formalizes the root typology of Beavers and Koontz-Garboden's book and the two theses it refutes. A root carries entailments of four kinds, manner, cause, result and state. The Bifurcation Thesis holds that a root carries only a state or a manner, all eventive content belonging to the verbal template, and Manner/Result Complementarity holds that no root entails both a manner and a result. The root of blossom entails a change and so falsifies the first (bifurcation_thesis_false); the roots of hand and drown entail both a manner and a result and so falsify the second (manner_result_complementarity_false).

The modifier again attaches to the root, to vbecome or to vcause, the three subterms of the causative template, and the entailments among its three readings follow from the subterm order (Template.exists_denote_of_isSubterm). The book's hypothesis about which roots alternate between a causative and an inchoative is compared with the class pages of Levin's English Verb Classes and Alternations (rootHypothesis_matches_profile).

Implementation notes

• The state entailments of the result roots are derived by the collocational closure of the kind signature (Root.closedKinds).
• The thesis predicates are the apparatus of this study alone.

References

• [BKG20]
• [Lev93]
• [Emb09]
• [Ara05]
• [RHL10]
• [vS96]

The two theses, at signature level

def Semantics.Root.Kinds.ontological : Kinds

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

Equations

• Semantics.Root.Kinds.ontological = {Semantics.Root.Kind.state, Semantics.Root.Kind.manner}

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

A signature violates the Bifurcation Thesis when it carries templatic, eventive content, that is, when it is not bounded by ontological.

Equations

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

@[instance_reducible]

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

Equations

• s.instDecidableViolatesBifurcation = { decide := !decide (s ⊆ Semantics.Root.Kinds.ontological), reflects_decide := ⋯ }

theorem Semantics.Root.Kinds.violatesBifurcation_iff (s : Kinds) : s.ViolatesBifurcation ↔ Kind.result ∈ s ∨ Kind.cause ∈ s

Violation is carrying a result or cause kind.

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

Bifurcation violation is monotone, so adding entailments cannot repair a violation.

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

A signature has both manner and result, the configuration that Manner/Result Complementarity claims no root realizes.

Equations

• s.HasMannerAndResult = ({Semantics.Root.Kind.manner, Semantics.Root.Kind.result} ⊆ s)

@[instance_reducible]

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

Equations

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

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

MRC violation is monotone in the signature order.

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

Bifurcation is invariant under collocational closure, since close only adds the state and result kinds forced by cause, never manner.

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

The typology

def Semantics.Root.Kinds.typology : Finset Kinds

The seven rows of the typology (12).

Equations

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

theorem Semantics.Root.Kinds.wellFormed_iff_mem_typology (s : Kinds) : s.WellFormed ↔ s = ∅ ∨ s ∈ typology

The typology (12) is exhaustive, since the signatures respecting the collocational restrictions are its seven rows and ∅.

def Semantics.Root.Kinds.attestedCells : Finset (Kinds × Position)

The filled cells of (12), pairs of a closed signature and a position.

Equations

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

The two theses, at root level

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

A root violates Bifurcation when it itself carries templatic, eventive meaning, a change of state or a cause.

Equations

• r.ViolatesBifurcation = r.kinds.ViolatesBifurcation

@[instance_reducible]

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

Equations

• r.instDecidableViolatesBifurcation = { decide := !decide (r.kinds ⊆ Semantics.Root.Kinds.ontological), reflects_decide := ⋯ }

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

A root respects Bifurcation when it carries only the ontological entailments, state and manner.

Equations

• r.RespectsBifurcation = ¬r.ViolatesBifurcation

@[instance_reducible]

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

Equations

• r.instDecidableRespectsBifurcation = { decide := !decide r.ViolatesBifurcation, reflects_decide := ⋯ }

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

A root respects Bifurcation iff its signature is bounded by the ontological kinds.

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

A root has both manner and result entailments, which Manner/Result Complementarity claims no root does.

Equations

• r.HasMannerAndResult = r.kinds.HasMannerAndResult

@[instance_reducible]

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

Equations

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

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

Negation of HasMannerAndResult.

Equations

• r.RespectsMannerResultComplementarity = ¬r.HasMannerAndResult

@[instance_reducible]

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

Equations

• r.instDecidableRespectsMannerResultComplementarity = { decide := !decide r.HasMannerAndResult, reflects_decide := ⋯ }

Sublexical again and the hierarchy of its readings

Again is a presupposition trigger that can attach at three points in the change-of-state structure, the root, vbecome and vcause (27), which yields the three readings of Mary flattened the rug again (25): the restitutive one, that the rug had been flat, the repetitive one over the change, that it had flattened, and the repetitive one over the causation, that Mary had flattened it. The three points are the subterms state and achievement of the causative template (18c), [y CAUSE [x BECOME P]], and the template itself, causative, whose causing subevent is an eventuality with the causer as effector (Template.denote_cause_effector), and the entry for again is Presupposition.again. The hierarchy of the readings is the subterm order: attached at a template, again presupposes that each of its subterms was realized.

def BeaversKoontzGarboden2020.causative : ArgumentStructure.EventStructure.Template ArgumentStructure.EventStructure.Eventuality.event

The causative change-of-state template (18c), [y CAUSE [x BECOME P]].

Equations

• BeaversKoontzGarboden2020.causative = ArgumentStructure.EventStructure.Template.effector.cause ArgumentStructure.EventStructure.Template.achievement

noncomputable def BeaversKoontzGarboden2020.againAt {Entity : Type u_1} {State Event : Type u} (M : ArgumentStructure.EventStructure.Interpretation Entity State Event) {σ : ArgumentStructure.EventStructure.Eventuality} (t : ArgumentStructure.EventStructure.Template σ) (R : SetRel (ArgumentStructure.EventStructure.Eventuality.Carrier State Event σ) (ArgumentStructure.EventStructure.Eventuality.Carrier State Event σ)) (P : Entity → State → Prop) (y x : Entity) : ArgumentStructure.EventStructure.Eventuality.Carrier State Event σ → SignType

Again attached at the subterm t of the causative template of a root with state predicate P, with R relating an eventuality of the sort of t to the earlier ones. The attachment at state gives the restitutive reading, at achievement the repetitive reading over the change, and at causative the repetitive reading over the causation.

Equations

• BeaversKoontzGarboden2020.againAt M t R P y x = Presupposition.again R (ArgumentStructure.EventStructure.Template.denote M P ⊤ t y x)

theorem BeaversKoontzGarboden2020.exists_denote_of_againAt_ne_zero {Entity : Type u_1} {State Event : Type u} {M : ArgumentStructure.EventStructure.Interpretation Entity State Event} {σ τ : ArgumentStructure.EventStructure.Eventuality} {P : Entity → State → Prop} {y x : Entity} {t : ArgumentStructure.EventStructure.Template σ} {u : ArgumentStructure.EventStructure.Template τ} (hu : u.IsSubterm t) {R : SetRel (ArgumentStructure.EventStructure.Eventuality.Carrier State Event σ) (ArgumentStructure.EventStructure.Eventuality.Carrier State Event σ)} {w : ArgumentStructure.EventStructure.Eventuality.Carrier State Event σ} (h : againAt M t R P y x w ≠ 0) : ∃ (w' : ArgumentStructure.EventStructure.Eventuality.Carrier State Event σ), (w, w') ∈ R ∧ ∃ (y' : Entity) (v : ArgumentStructure.EventStructure.Eventuality.Carrier State Event τ), ArgumentStructure.EventStructure.Template.denote M P ⊤ u y' x v

Again attached at a template presupposes an earlier eventuality of the template, and so the realization of each of its subterms, with the same undergoer, which is the hierarchy of the readings.

theorem BeaversKoontzGarboden2020.exists_become_of_againAt_causative_ne_zero {Entity : Type u_1} {State Event : Type u} {M : ArgumentStructure.EventStructure.Interpretation Entity State Event} {P : Entity → State → Prop} {y x : Entity} {R : SetRel Event Event} {w : Event} (h : againAt M causative R P y x w ≠ 0) : ∃ (w' : Event), (w, w') ∈ R ∧ ∃ (e : Event) (s : State), M.become s e ∧ P x s

End to end, the repetitive reading over the causation presupposes an earlier causing eventuality and a change to the root's state.

theorem BeaversKoontzGarboden2020.exists_become_of_againAt_state_ne_zero {Entity : Type u_1} {State Event : Type u} {M : ArgumentStructure.EventStructure.Interpretation Entity State Event} {P : Entity → State → Prop} {y x : Entity} {R : SetRel State State} {s : State} (hres : M.EntailsChange P) (h : againAt M ArgumentStructure.EventStructure.Template.state R P y x s ≠ 0) : ∃ (s' : State), (s, s') ∈ R ∧ ∃ (e : Event), M.become s' e

For a state predicate that entails change, even the restitutive attachment of again presupposes a change, so result roots never admit a truly restitutive reading.

The six representative roots

def BeaversKoontzGarboden2020.flat : Semantics.Root

√flat is a pure state root.

Equations

• BeaversKoontzGarboden2020.flat = { name := "flat", entailments := {Semantics.Root.Entailment.state "flat"}, position := some Semantics.Root.Position.complement }

def BeaversKoontzGarboden2020.jog : Semantics.Root

√jog is a pure manner-of-motion root.

Equations

• BeaversKoontzGarboden2020.jog = { name := "jog", entailments := {Semantics.Root.Entailment.manner "jogging-gait"}, position := some Semantics.Root.Position.adjoined }

def BeaversKoontzGarboden2020.blossom : Semantics.Root

√blossom is a result root with no specified manner or cause, an internally caused change of state.

Equations

• BeaversKoontzGarboden2020.blossom = { name := "blossom", entailments := {Semantics.Root.Entailment.result "flowering"}, position := some Semantics.Root.Position.complement }

def BeaversKoontzGarboden2020.crack : Semantics.Root

√crack is a caused-result root without a specified manner.

Equations

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

def BeaversKoontzGarboden2020.hand : Semantics.Root

√hand carries manner, cause and result in the adjoined position. The possession result is not cancelable (Mary handed John the book, #but it never came to be on his person), so it is entailed by the root rather than implicated.

Equations

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

def BeaversKoontzGarboden2020.drown : Semantics.Root

√drown is a manner-of-killing root, carrying manner, cause and result in the 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 = {Semantics.Root.Kind.state}

theorem BeaversKoontzGarboden2020.jog_kinds : jog.kinds = {Semantics.Root.Kind.manner}

theorem BeaversKoontzGarboden2020.blossom_kinds : blossom.kinds = {Semantics.Root.Kind.result}

theorem BeaversKoontzGarboden2020.crack_kinds : crack.kinds = {Semantics.Root.Kind.result, Semantics.Root.Kind.cause}

theorem BeaversKoontzGarboden2020.hand_kinds : hand.kinds = {Semantics.Root.Kind.manner, Semantics.Root.Kind.result, Semantics.Root.Kind.cause}

theorem BeaversKoontzGarboden2020.drown_kinds : drown.kinds = {Semantics.Root.Kind.manner, Semantics.Root.Kind.result, Semantics.Root.Kind.cause}

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

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

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

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

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

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

theorem BeaversKoontzGarboden2020.cells_attested (r : Semantics.Root) : r ∈ [flat, jog, blossom, crack, hand, drown] → ∃ (p : Semantics.Root.Position), r.position = some p ∧ (r.closedKinds, p) ∈ Semantics.Root.Kinds.attestedCells

Each of the six roots fills a cell of (12).

theorem BeaversKoontzGarboden2020.hand_drown_differ_in_position : hand.closedKinds = drown.closedKinds ∧ hand.position ≠ drown.position

√hand and √drown share a signature and differ only in position.

Falsifying the Bifurcation Thesis

theorem BeaversKoontzGarboden2020.blossom_violatesBifurcation : blossom.ViolatesBifurcation

√blossom entails a change of state, the templatic content of v_become, in the root, and so falsifies 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 : Semantics.Root), r.ViolatesBifurcation

Some root carries templatic content.

theorem BeaversKoontzGarboden2020.bifurcation_thesis_false : ¬∀ (r : Semantics.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 : Semantics.Root), r.HasMannerAndResult

Some root entails both a manner and a result.

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

The universal closure of Manner/Result Complementarity is false.

Roots respecting each constraint

theorem BeaversKoontzGarboden2020.flat_respectsBifurcation : flat.RespectsBifurcation

√flat, a pure state root, respects Bifurcation, its signature being 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 entailments of the roots in a model

The kinds of a root are meaning postulates on its state predicate (EventStructure.Interpretation.Respects). In an interpretation that respects the signature of √crack, a cracked state arises from a caused change whatever template the root occurs in, while one that respects the signature of √flat may have a flat state that no change gave rise to.

theorem BeaversKoontzGarboden2020.crack_entails_cause {Entity : Type u_1} {State : Type u_2} {Event : Type u_3} {M : ArgumentStructure.EventStructure.Interpretation Entity State Event} {P : Entity → State → Prop} {Q : Event → Prop} {x : Entity} {s : State} (h : M.Respects P Q crack.kinds) (hs : P x s) : ∃ (e : Event) (v : Event), M.become s e ∧ M.cause v e

In a model that respects the signature of √crack, a cracked state arises from a change that some event causes.

theorem BeaversKoontzGarboden2020.drown_entails_manner {Entity : Type u_1} {State : Type u_2} {Event : Type u_3} {M : ArgumentStructure.EventStructure.Interpretation Entity State Event} {P : Entity → State → Prop} {Q : Event → Prop} {x : Entity} {s : State} (h : M.Respects P Q drown.kinds) (hs : P x s) : ∃ (e : Event), M.become s e ∧ ∀ (v : Event), M.cause v e → Q v

In a model that respects the signature of √drown, a drowned state arises from a change whose every cause is an event of the root's manner.

def BeaversKoontzGarboden2020.unchanging : ArgumentStructure.EventStructure.Interpretation Unit Unit Unit

A model without changes.

Equations

• BeaversKoontzGarboden2020.unchanging = { become := fun (x x_1 : Unit) => False, cause := fun (x x_1 : Unit) => False, effector := fun (x x_1 : Unit) => False }

def BeaversKoontzGarboden2020.changing : ArgumentStructure.EventStructure.Interpretation Unit Unit Unit

A model in which every state arises from a caused change.

Equations

• BeaversKoontzGarboden2020.changing = { become := fun (x x_1 : Unit) => True, cause := fun (x x_1 : Unit) => True, effector := fun (x x_1 : Unit) => True }

theorem BeaversKoontzGarboden2020.flat_not_entailsChange : unchanging.Respects (fun (x x_1 : Unit) => True) (fun (x : Unit) => True) flat.kinds ∧ ¬unchanging.EntailsChange fun (x x_1 : Unit) => True

The signature of √flat does not entail change, since the model without changes respects it for a state predicate that holds.

theorem BeaversKoontzGarboden2020.crack_respects : changing.Respects (fun (x x_1 : Unit) => True) (fun (x : Unit) => True) crack.kinds ∧ ¬unchanging.Respects (fun (x x_1 : Unit) => True) (fun (x : Unit) => True) crack.kinds

The signature of √crack is respected for a state predicate that holds, in the model where every state arises from a caused change, and is not respected in the model without changes.

The root hypothesis against Levin's class profiles

def BeaversKoontzGarboden2020.TestedForCausative (c : ArgumentStructure.LevinClass) : Prop

A class Part II of [Lev93] tests for the causative alternation and whose root signature is recorded.

Equations

• BeaversKoontzGarboden2020.TestedForCausative c = (c.rootEntailments.isSome = true ∧ c.Tests ArgumentStructure.DiathesisAlternation.causativeInchoative)

@[instance_reducible]

instance BeaversKoontzGarboden2020.instDecidablePredLevinClassTestedForCausative : DecidablePred TestedForCausative

Equations

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

def BeaversKoontzGarboden2020.rootHypothesisResidue : Finset ArgumentStructure.LevinClass

The tested classes on which the root hypothesis and the class pages disagree. The verbs of creation and the psych causatives have causative-result roots that the hypothesis predicts to alternate although the pages star the alternation. The other classes have pages that attest it without a manner-free causative root, namely the manner-and-result roots, the internally caused result of the grow verbs, and the pure-manner roots of the coil and roll verbs.

Equations

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

theorem BeaversKoontzGarboden2020.rootHypothesis_matches_profile (c : ArgumentStructure.LevinClass) : TestedForCausative c → c ∉ rootHypothesisResidue → (c.RootPredictsCausative ↔ c.Participates ArgumentStructure.DiathesisAlternation.causativeInchoative)

Outside the residue, the root hypothesis agrees with every tested class page.

theorem BeaversKoontzGarboden2020.rootHypothesisResidue_disagrees (c : ArgumentStructure.LevinClass) : c ∈ rootHypothesisResidue → TestedForCausative c ∧ ¬(c.RootPredictsCausative ↔ c.Participates ArgumentStructure.DiathesisAlternation.causativeInchoative)

The residue is exactly the tested classes on which they disagree.