Root Typology: States and Changes of State ([BEJ+21], B&[BKG20]) [BEJ+21] [BKG20] [Coo19]

[Ara05] [Dix82] [Emb04] [Dow91] [Emb09] [RSN21] [Lev93]

Beavers, Everdell, Jerro, Kauhanen, [BEJ+21] "States and changes of state: A crosslinguistic study of the roots of verbal meaning." Language 97(3), 439–484.

Core contribution

Change-of-state verb roots split into two types:

• Property concept (PC) roots: flat, red, long — underlie deadjectival CoS verbs
• Result roots: crack, break, shatter — underlie non-deadjectival CoS verbs

The key semantic distinction: result roots lexically entail change, while PC roots do not. This refutes the Bifurcation Thesis: contra bifurcation, some roots introduce templatic meaning (change = BECOME).

The deepest theorem

A root's entailment of change determines ALL of its morphosyntactic behavior in a single four-way biconditional (§§3–8):

entailsChange R ↔ ¬hasSimpleStative R ∧ ¬verbalFormIsMarked R ∧ ¬allowsRestitutiveAgain R

This holds crosslinguistically (88-language typological study), ruling out bifurcation as an explanation. The deeper explanation is the Markedness Generalization (eq. 44): morphological markedness reflects semantic mismatch between functional head and root.

Bridges

• EntailmentProfile.changeOfState = result root entailment (ProtoRoles §8)
• TemplateHead.vBecome = the templatic operator that result roots lexicalize
• CoSType.inception = BECOME as ¬P→P transition (ChangeOfState/Theory)
• Template.achievement/.accomplishment = templates containing BECOME (EventStructure)
• Crosslinguistic data validates the correlations (Studies/, e.g. Coon2019, BeaversEtAl2021)

Unified Root (§§15–17)

Extends the file with the RootClassification structure (§16) bundling [Coo19]'s arity dimension (does the root select an internal argument?) with Beavers et al.'s change-entailment dimension. The two axes cross-classify orthogonally (arity_changeType_orthogonal): knowing whether a root selects a theme tells you nothing about whether it entails change, and vice versa.

• Coon, J. (2019). Building verbs in Chuj: Consequences for the nature of roots. Journal of Linguistics 55(1): 35–81.
• Hale, K. & Keyser, S.J. (2002). Prolegomenon to a Theory of Argument Structure. MIT Press.
• Harley, H. (2014). On the identity of roots. Theoretical Linguistics 40, 225–276.

inductive RootType : Type

Two types of change-of-state verb roots ([BEJ+21] §3.1).

Property concept (PC) roots: underlie deadjectival CoS verbs. The root describes a gradable property (dimension, color, value, etc.). Examples: flat, red, long, warm.

Result roots: underlie non-deadjectival CoS verbs. The root describes a specific result state that arises from a particular kind of event (breaking, cooking, killing, etc.). Examples: crack, break, shatter.

• propertyConcept : RootType
• result : RootType

@[implicit_reducible]

instance instDecidableEqRootType : DecidableEq RootType

Equations

• instDecidableEqRootType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def instReprRootType.repr : RootType → ℕ → Std.Format

Equations

• instReprRootType.repr RootType.propertyConcept prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RootType.propertyConcept")).group prec✝
• instReprRootType.repr RootType.result prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RootType.result")).group prec✝

@[implicit_reducible]

instance instReprRootType : Repr RootType

Equations

• instReprRootType = { reprPrec := instReprRootType.repr }

def RootType.entailsChange : RootType → Bool

Whether a root lexically entails prior change ([BEJ+21] §3.6).

PC roots denote simple states that can hold without any prior change event. Result roots denote states that entail a prior change event.

Equations

• RootType.propertyConcept.entailsChange = false
• RootType.result.entailsChange = true

inductive RootDenotationType : Type

The semantic denotation domain of a root ([Coo19], (3); extended by [HKG25]).

• indivStatePred ⟨e, ⟨v,t⟩⟩: individual/state relation (√TV, √ITV; also PC Class 1/3 roots per [HKG25]: λx_e λs_v[P(x)(s)])
• statePred ⟨v,t⟩: predicate of states, no individual argument ([HKG25] Class 2 PC roots: λs_v[P(s)], e.g., √I:YEL 'big' in Wá·šiw)
• measureFn ⟨e, ⟨s,d⟩⟩: entity → event → degree (√POS; [Hen19])
• entityPred ⟨e,t⟩: entity → truth-value, no event (√NOM)

• indivStatePred : RootDenotationType
• statePred : RootDenotationType
• measureFn : RootDenotationType
• entityPred : RootDenotationType

@[implicit_reducible]

instance instDecidableEqRootDenotationType : DecidableEq RootDenotationType

Equations

• instDecidableEqRootDenotationType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def instReprRootDenotationType.repr : RootDenotationType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance instReprRootDenotationType : Repr RootDenotationType

Equations

• instReprRootDenotationType = { reprPrec := instReprRootDenotationType.repr }

def RootDenotationType.hasIndivArg : RootDenotationType → Bool

Whether a root denotation type includes an individual argument.

Types with an individual argument (⟨e, ...⟩) can compose directly with v_become (which requires ⟨e, ⟨v,t⟩⟩). Types without one (⟨v,t⟩) cause a type mismatch and require type-shifting (e.g., ∇) or possessive semantics (v_have) to predicate of individuals. ([HKG25] §5.1)

Equations

• RootDenotationType.indivStatePred.hasIndivArg = true
• RootDenotationType.statePred.hasIndivArg = false
• RootDenotationType.measureFn.hasIndivArg = true
• RootDenotationType.entityPred.hasIndivArg = true

structure RootClassification : Type

Unified root characterization bundling all classification dimensions.

A root is characterized along five independent axes:

1. Arity: does it select an internal argument?
2. Change entailment: does it lexically entail a prior change event?
3. Denotation type ([Coo19], (3)): event predicate, measure function, or entity predicate.
4. Quality dimensions ([SMcN26]): within-class root content
5. Class membership: verb class taxonomy

Axes 1, 2, and 3 cross-classify: Coon's four Chuj root classes are recovered as (arity × denotationType) pairs: √TV = selectsTheme + indivStatePred, √ITV = noTheme + indivStatePred, √POS = noTheme + measureFn, √NOM = noTheme + entityPred.

• arity : Verb.Root.Arity

  Does this root select an internal argument?

• changeType : RootType

  Does this root lexically entail prior change?

• denotationType : Option RootDenotationType

  Semantic denotation domain ([Coo19], (3)). Optional — not all roots have been annotated.

• profile : Verb.Root.Profile

  Within-class quality dimensions ([SMcN26])

• levinClass : Option Semantics.Lexical.LevinClass

  Verb class membership

def instBEqRootClassification.beq : RootClassification → RootClassification → Bool

Equations

• One or more equations did not get rendered due to their size.
• instBEqRootClassification.beq x✝¹ x✝ = false

@[implicit_reducible]

instance instBEqRootClassification : BEq RootClassification

Equations

• instBEqRootClassification = { beq := instBEqRootClassification.beq }

def instReprRootClassification.repr : RootClassification → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance instReprRootClassification : Repr RootClassification

Equations

• instReprRootClassification = { reprPrec := instReprRootClassification.repr }

def RootClassification.entailsChange (r : RootClassification) : Bool

Does this root lexically entail prior change?

Equations

• r.entailsChange = r.changeType.entailsChange

Root change type, and its blindness to the outcome axis

RootType is a projection of a root's entailment signature, derived not stored — Root.changeType is the derived analog of the stored RootClassification.changeType. Crucially it is blind to the [Bha24] outcome axis (Root.outcomes, the orthogonal dimension Root now carries): two roots with the same entailments share a changeType whatever their outcomes — which is precisely why outcome cardinality is a genuinely independent dimension of root content, the one that drives reversative un- where the manner/result typology cannot.

def Verb.Root.changeType (r : Root) : RootType

The change-entailment type of a root, derived from its kind signature: a root entails change iff its signature carries result ([BEJ+21]). The derived analog of RootClassification.changeType.

Equations

• r.changeType = if Verb.LexKind.result ∈ r.kinds then RootType.result else RootType.propertyConcept

theorem Verb.Root.changeType_eq_result_iff (r : Root) : r.changeType = RootType.result ↔ r.HasResult

theorem Verb.Root.changeType_ignores_outcomes {r r' : Root} (h : r.entailments = r'.entailments) : r.changeType = r'.changeType

changeType is blind to outcomes: same entailments ⇒ same changeType, whatever the outcomes. The formal statement of why [Bha24]'s outcome cardinality is an independent axis the manner/result signature cannot see.

inductive PCClass : Type

Property concept root subclasses ([Dix82]; [BEJ+21] ex. 5).

[Dix82] identifies seven semantic categories. [BEJ+21] omits HUMAN PROPENSITY from their Table 2 sample but the category is attested crosslinguistically ([HKG25] Table A1: hungry, afraid, sick, brave, generous, etc. in Wá·šiw).

• dimension : PCClass
• age : PCClass
• value : PCClass
• color : PCClass
• physicalProperty : PCClass
• humanPropensity : PCClass
• speed : PCClass

@[implicit_reducible]

instance instDecidableEqPCClass : DecidableEq PCClass

Equations

• instDecidableEqPCClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance instReprPCClass : Repr PCClass

Equations

• instReprPCClass = { reprPrec := instReprPCClass.repr }

def instReprPCClass.repr : PCClass → ℕ → Std.Format

Equations

• instReprPCClass.repr PCClass.dimension prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PCClass.dimension")).group prec✝
• instReprPCClass.repr PCClass.age prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PCClass.age")).group prec✝
• instReprPCClass.repr PCClass.value prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PCClass.value")).group prec✝
• instReprPCClass.repr PCClass.color prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PCClass.color")).group prec✝
• instReprPCClass.repr PCClass.physicalProperty prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PCClass.physicalProperty")).group prec✝
• instReprPCClass.repr PCClass.humanPropensity prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PCClass.humanPropensity")).group prec✝
• instReprPCClass.repr PCClass.speed prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PCClass.speed")).group prec✝

inductive ResultClass : Type

Result root subclasses ([Lev93]; [BEJ+21] ex. 6).

• entitySpecificCoS : ResultClass
• cooking : ResultClass
• breaking : ResultClass
• bending : ResultClass
• killing : ResultClass
• destroying : ResultClass
• calibratableCoS : ResultClass
• inherentlyDirectedMotion : ResultClass

@[implicit_reducible]

instance instDecidableEqResultClass : DecidableEq ResultClass

Equations

• instDecidableEqResultClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance instReprResultClass : Repr ResultClass

Equations

• instReprResultClass = { reprPrec := instReprResultClass.repr }

def instReprResultClass.repr : ResultClass → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• instReprResultClass.repr ResultClass.entitySpecificCoS prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ResultClass.entitySpecificCoS")).group prec✝
• instReprResultClass.repr ResultClass.cooking prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ResultClass.cooking")).group prec✝
• instReprResultClass.repr ResultClass.breaking prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ResultClass.breaking")).group prec✝
• instReprResultClass.repr ResultClass.bending prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ResultClass.bending")).group prec✝
• instReprResultClass.repr ResultClass.killing prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ResultClass.killing")).group prec✝
• instReprResultClass.repr ResultClass.destroying prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ResultClass.destroying")).group prec✝
• instReprResultClass.repr ResultClass.calibratableCoS prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ResultClass.calibratableCoS")).group prec✝

inductive ChangeRestriction : Type

How a result root's change entailment is restricted (B&[BKG20] §2.4).

Break-type result roots (√CRACK, √SHATTER) entail change of ANY kind — spatial or temporal. A crack can "run from the tree to the house" without a temporal becoming event; the state itself extends spatially.

Cook/kill-type result roots (√COOK, √KILL) entail only TEMPORAL change. Cooking, killing, and melting are necessarily temporal processes. "✱The meat cooked from the oven to the table" is ruled out.

This three-way refinement (PC / break-type / cook-type) is invisible to the binary entailsChange flag but has consequences for spatial predication and the interpretation of directional PPs (B&[BKG20] §2.4).

• anyChange : ChangeRestriction
• temporalOnly : ChangeRestriction

@[implicit_reducible]

instance instDecidableEqChangeRestriction : DecidableEq ChangeRestriction

Equations

• instDecidableEqChangeRestriction x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance instReprChangeRestriction : Repr ChangeRestriction

Equations

• instReprChangeRestriction = { reprPrec := instReprChangeRestriction.repr }

def instReprChangeRestriction.repr : ChangeRestriction → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• instReprChangeRestriction.repr ChangeRestriction.anyChange prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ChangeRestriction.anyChange")).group prec✝

def ResultClass.changeRestriction : ResultClass → ChangeRestriction

Change restriction for each result root subclass. Breaking/bending roots and directed motion allow spatial change descriptions; cooking/killing/destroying/scalar-change roots are temporally restricted.

Equations

• ResultClass.breaking.changeRestriction = ChangeRestriction.anyChange
• ResultClass.bending.changeRestriction = ChangeRestriction.anyChange
• ResultClass.inherentlyDirectedMotion.changeRestriction = ChangeRestriction.anyChange
• ResultClass.entitySpecificCoS.changeRestriction = ChangeRestriction.temporalOnly
• ResultClass.cooking.changeRestriction = ChangeRestriction.temporalOnly
• ResultClass.killing.changeRestriction = ChangeRestriction.temporalOnly
• ResultClass.destroying.changeRestriction = ChangeRestriction.temporalOnly
• ResultClass.calibratableCoS.changeRestriction = ChangeRestriction.temporalOnly

theorem breaking_allows_spatial : ResultClass.breaking.changeRestriction = ChangeRestriction.anyChange

Breaking roots allow spatial change: "The road cracked from the tree to the house."

theorem cooking_temporal_only : ResultClass.cooking.changeRestriction = ChangeRestriction.temporalOnly

Cooking roots restrict to temporal change: "✱The meat cooked from A to B."

def RootType.hasSimpleStative : RootType → Bool

PC roots have simple (unmarked) stative forms; result roots lack them.

Crosslinguistic evidence (§6, Fig. 1): PC median = 95.67% of languages have simple statives; result median = 1.59% (Mann-Whitney U = 1266.5, p < 0.001, n₁ = n₂ = 36).

English: "bright" (PC, simple adj) vs *"shattered" requires prior change.

Equations

• RootType.propertyConcept.hasSimpleStative = true
• RootType.result.hasSimpleStative = false

def RootType.verbalFormIsMarked : RootType → Bool

PC root verbs TEND to be morphologically marked (deadjectival: wid-en, flat-ten); result root verbs tend to be unmarked (break, crack, shatter).

This captures the cross-linguistic DEFAULT pattern, not a universal. [HKG25] §4: Wá·šiw Class 1 PC roots predicate as bare verbs without verbal morphology (zero categorization), deviating from the tendency captured here.

Crosslinguistic evidence (§7, Fig. 5): PC median = 56.01% marked; result median = 15.20% (U = 1291, p < 0.001).

Equations

• RootType.propertyConcept.verbalFormIsMarked = true
• RootType.result.verbalFormIsMarked = false

def RootType.allowsRestitutiveAgain : RootType → Bool

PC roots allow restitutive 'again' (scope over root only); result roots allow only repetitive 'again' (scope over BECOME).

§3.4: "John sharpened the knife again" allows restitutive reading (could be just one sharpening), but "#Chris thawed the meat again" in a restitutive context is unacceptable (necessarily two defrostings).

Under the analysis in §3.6: 'again' can target √ROOT. For PC roots, this yields a restitutive reading (return to prior state without prior change). For result roots, since the root itself entails change, 'again' over the root still entails a prior change event.

Equations

• RootType.propertyConcept.allowsRestitutiveAgain = true
• RootType.result.allowsRestitutiveAgain = false

theorem semantic_determines_morphosyntax (rt : RootType) : rt.entailsChange = true ↔ rt.hasSimpleStative = false ∧ rt.verbalFormIsMarked = false ∧ rt.allowsRestitutiveAgain = false

The main theorem of [BEJ+21].

A root's entailment of change determines ALL of its morphosyntactic behavior in a single four-way biconditional. This is the paper's deepest result: four independently testable properties form a perfect correlation package.

For result roots (entailsChange = true):

• No simple stative forms (§6)
• Unmarked verbal forms (§7)
• No restitutive 'again' — only repetitive (§3.4)

For PC roots (entailsChange = false):

• Simple stative forms exist (§6)
• Marked verbal forms (§7)
• Restitutive 'again' available (§3.4)

This correlation holds crosslinguistically (88 languages, §§4–7) and refutes the Bifurcation Thesis: if roots couldn't introduce templatic meaning (change), there would be NO semantic basis for the morphological and syntactic correlations.

theorem pc_determines_morphosyntax (rt : RootType) : rt.entailsChange = false ↔ rt.hasSimpleStative = true ∧ rt.verbalFormIsMarked = true ∧ rt.allowsRestitutiveAgain = true

The converse: NOT entailing change determines the opposite package.

def bifurcationThesis (rootEntailsChange : RootType → Bool) : Prop

The Bifurcation Thesis for Roots ([Emb09]:1, [Ara05]:79; [BEJ+21] eq. 2):

"If a component of meaning is introduced by a semantic rule that applies to elements in combination [i.e. by templatic operators], then that component of meaning cannot be part of the meaning of a [lexical semantic] root."

Under bifurcation, change (= BECOME) is introduced only by templates, never by roots. Therefore NO root should entail change.

Equations

• bifurcationThesis rootEntailsChange = ∀ (rt : RootType), rootEntailsChange rt = false

theorem bifurcation_fails : ¬bifurcationThesis RootType.entailsChange

[BEJ+21] main result: bifurcation does not hold. Result roots entail change, violating the thesis (§§3.3, 3.6, 9).

theorem result_roots_witness_against_bifurcation : RootType.result.entailsChange = true

Corollary: result roots are a witness to bifurcation failure.

theorem pc_roots_consistent_with_bifurcation : RootType.propertyConcept.entailsChange = false

PC roots are consistent with bifurcation (they don't entail change).

theorem bkg_bifurcation_fails_all_dimensions : Verb.LexKind.result ∈ Verb.Root.Kinds.fullSpec ∧ Verb.LexKind.cause ∈ Verb.Root.Kinds.fullSpec ∧ Verb.LexKind.manner ∈ Verb.Root.Kinds.fullSpec ∧ Verb.LexKind.state ∈ Verb.Root.Kinds.fullSpec

B&[BKG20] strengthened bifurcation failure via Root.Kinds.

[BEJ+21] show roots can entail CHANGE (one templatic notion). B&[BKG20] show roots can entail CHANGE, CAUSATION, and MANNER — ALL notions traditionally reserved for templates. This is a strictly stronger refutation: even if one accepted that change is "special", roots encoding manner+cause (√GUILLOTINE, √HAND) violate bifurcation on three separate dimensions simultaneously.

Witness: Root.Kinds.fullSpec carries all four kinds.

theorem bkg_bifurcation_multiple_witnesses : Verb.LexKind.result ∈ Semantics.Lexical.LevinClass.cut.rootEntailments ∧ Verb.LexKind.manner ∈ Semantics.Lexical.LevinClass.cut.rootEntailments ∧ Verb.LexKind.cause ∈ Semantics.Lexical.LevinClass.give.rootEntailments ∧ Verb.LexKind.manner ∈ Semantics.Lexical.LevinClass.give.rootEntailments

Multiple Levin classes witness the stronger bifurcation failure.

inductive Markedness : Type

Whether a form is morphologically marked (=derived/complex) or unmarked (=basic/simple).

• unmarked : Markedness
• marked : Markedness

@[implicit_reducible]

instance instDecidableEqMarkedness : DecidableEq Markedness

Equations

• instDecidableEqMarkedness x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance instReprMarkedness : Repr Markedness

Equations

• instReprMarkedness = { reprPrec := instReprMarkedness.repr }

def instReprMarkedness.repr : Markedness → ℕ → Std.Format

Equations

• instReprMarkedness.repr Markedness.unmarked prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Markedness.unmarked")).group prec✝
• instReprMarkedness.repr Markedness.marked prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Markedness.marked")).group prec✝

def verbalMarkedness (rt : RootType) : Markedness

The Markedness Generalization ([BEJ+21] eq. 44).

Morphological markedness reflects semantic mismatch between a functional head and its root complement. A form is unmarked when the head's semantic contribution is REDUNDANT with the root's meaning:

(a) Default realization of v_become with complement √ROOT: - If √ROOT entails change → v_become is redundant → UNMARKED verb - If √ROOT does not entail change → v_become adds content → MARKED verb

(b) Default realization of Asp_{S/R} with complement X: - If X does not entail change → already stative → UNMARKED stative - If X entails change → change must be stripped → MARKED stative

This explains three attested language types:

1. English-type: markedness asymmetry realized overtly (-en, -ed)
2. Equipollent: both marked (high-marking languages like Hebrew)
3. Labile: neither marked (low-marking languages like Kinyarwanda)

And rules out the unattested fourth type (where the markedness pattern is the inverse of what the generalization predicts).

Equations

• verbalMarkedness rt = if rt.entailsChange = true then Markedness.unmarked else Markedness.marked

def stativeMarkedness (rt : RootType) : Markedness

Stative markedness is the mirror image of verbal markedness.

Equations

• stativeMarkedness rt = if rt.entailsChange = true then Markedness.marked else Markedness.unmarked

theorem markedness_complementarity (rt : RootType) : verbalMarkedness rt ≠ stativeMarkedness rt

Verbal and stative markedness are always complementary.

theorem result_root_unmarked_verb : verbalMarkedness RootType.result = Markedness.unmarked

Result roots produce unmarked verbs.

theorem pc_root_marked_verb : verbalMarkedness RootType.propertyConcept = Markedness.marked

PC roots produce marked verbs.

theorem result_root_marked_stative : stativeMarkedness RootType.result = Markedness.marked

Result roots produce marked statives.

theorem pc_root_unmarked_stative : stativeMarkedness RootType.propertyConcept = Markedness.unmarked

PC roots produce unmarked statives.

theorem markedness_from_semantics (rt : RootType) : verbalMarkedness rt = Markedness.unmarked ↔ rt.entailsChange = true

The markedness generalization is equivalent to the semantic distinction.

inductive PossessionEntailment : Type

What a ditransitive root entails about possession (B&[BKG20] §3.3). Templates always introduce PROSPECTIVE possession (via ◇ modality). Whether the ROOT adds actual or prospective possession on top determines cancellability: "gave X the ball, #but X never had it" vs. "sent X the ball, but it never arrived" (OK).

• none : PossessionEntailment
• prospective : PossessionEntailment
• actual : PossessionEntailment

@[implicit_reducible]

instance instDecidableEqPossessionEntailment : DecidableEq PossessionEntailment

Equations

• instDecidableEqPossessionEntailment x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance instReprPossessionEntailment : Repr PossessionEntailment

Equations

• instReprPossessionEntailment = { reprPrec := instReprPossessionEntailment.repr }

def instReprPossessionEntailment.repr : PossessionEntailment → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• instReprPossessionEntailment.repr PossessionEntailment.none prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PossessionEntailment.none")).group prec✝

inductive DitransitiveRootClass : Type

Six classes of ditransitive verb roots (B&[BKG20] §3.6). The ditransitive parallel to the PC/result distinction for CoS roots: templates contribute only PROSPECTIVE states; roots can contribute ACTUAL states.

• causedPossession : DitransitiveRootClass
• futureHaving : DitransitiveRootClass
• ballisticMotion : DitransitiveRootClass
• sending : DitransitiveRootClass
• accompaniedMotion : DitransitiveRootClass
• carrying : DitransitiveRootClass

@[implicit_reducible]

instance instDecidableEqDitransitiveRootClass : DecidableEq DitransitiveRootClass

Equations

• instDecidableEqDitransitiveRootClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def instReprDitransitiveRootClass.repr : DitransitiveRootClass → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance instReprDitransitiveRootClass : Repr DitransitiveRootClass

Equations

• instReprDitransitiveRootClass = { reprPrec := instReprDitransitiveRootClass.repr }

structure DitransitiveEntailments : Type

What a ditransitive root entails about the transfer event. Each field is a distinct semantic entailment from the ROOT, independent of what the template provides.

• possession : PossessionEntailment
• causedMotion : Bool
• manner : Bool
• accompaniment : Bool

@[implicit_reducible]

instance instDecidableEqDitransitiveEntailments : DecidableEq DitransitiveEntailments

Equations

• instDecidableEqDitransitiveEntailments = instDecidableEqDitransitiveEntailments.decEq

def instDecidableEqDitransitiveEntailments.decEq (x✝ x✝¹ : DitransitiveEntailments) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance instReprDitransitiveEntailments : Repr DitransitiveEntailments

Equations

• instReprDitransitiveEntailments = { reprPrec := instReprDitransitiveEntailments.repr }

def instReprDitransitiveEntailments.repr : DitransitiveEntailments → ℕ → Std.Format

Equations

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

def DitransitiveRootClass.entailments : DitransitiveRootClass → DitransitiveEntailments

Entailment profile for each ditransitive root class (B&[BKG20] §3.6).

Equations

• DitransitiveRootClass.causedPossession.entailments = { possession := PossessionEntailment.actual, causedMotion := false, manner := false, accompaniment := false }
• DitransitiveRootClass.futureHaving.entailments = { possession := PossessionEntailment.prospective, causedMotion := false, manner := false, accompaniment := false }
• DitransitiveRootClass.ballisticMotion.entailments = { possession := PossessionEntailment.none, causedMotion := true, manner := true, accompaniment := false }
• DitransitiveRootClass.sending.entailments = { possession := PossessionEntailment.none, causedMotion := true, manner := false, accompaniment := false }
• DitransitiveRootClass.accompaniedMotion.entailments = { possession := PossessionEntailment.none, causedMotion := true, manner := false, accompaniment := true }
• DitransitiveRootClass.carrying.entailments = { possession := PossessionEntailment.none, causedMotion := true, manner := true, accompaniment := true }

theorem give_entails_actual_possession : DitransitiveRootClass.causedPossession.entailments.possession = PossessionEntailment.actual

√GIVE entails actual possession — "Kim gave Sandy the ball, #but Sandy never had it" is contradictory (§3.3, ex. 17).

theorem send_no_possession : DitransitiveRootClass.sending.entailments.possession = PossessionEntailment.none

√SEND does NOT entail possession — "Kim sent Sandy the ball, but it never arrived" is felicitous (§3.3, ex. 18).

theorem promise_prospective : DitransitiveRootClass.futureHaving.entailments.possession = PossessionEntailment.prospective

√PROMISE entails only prospective possession.

theorem throw_manner_motion : have e := DitransitiveRootClass.ballisticMotion.entailments; e.possession = PossessionEntailment.none ∧ e.causedMotion = true ∧ e.manner = true

√THROW entails manner + caused motion but not possession.

theorem bring_accompaniment : DitransitiveRootClass.accompaniedMotion.entailments.accompaniment = true

√BRING entails accompaniment — agent travels with theme.

theorem carry_manner_accompaniment : have e := DitransitiveRootClass.carrying.entailments; e.manner = true ∧ e.accompaniment = true ∧ e.possession = PossessionEntailment.none

√CARRY entails manner + accompaniment but not possession.

def Semantics.Lexical.LevinClass.ditransitiveRootClass : LevinClass → Option DitransitiveRootClass

Bridge to LevinClass: ditransitive Levin classes → root classes.

Equations

• Semantics.Lexical.LevinClass.give.ditransitiveRootClass = some DitransitiveRootClass.causedPossession
• Semantics.Lexical.LevinClass.contribute.ditransitiveRootClass = some DitransitiveRootClass.causedPossession
• Semantics.Lexical.LevinClass.exchange.ditransitiveRootClass = some DitransitiveRootClass.causedPossession
• Semantics.Lexical.LevinClass.throw.ditransitiveRootClass = some DitransitiveRootClass.ballisticMotion
• Semantics.Lexical.LevinClass.send.ditransitiveRootClass = some DitransitiveRootClass.sending
• Semantics.Lexical.LevinClass.carry.ditransitiveRootClass = some DitransitiveRootClass.carrying
• x✝.ditransitiveRootClass = none

theorem Semantics.Lexical.give_class_causedPossession : LevinClass.give.ditransitiveRootClass = some DitransitiveRootClass.causedPossession

theorem Semantics.Lexical.throw_class_ballisticMotion : LevinClass.throw.ditransitiveRootClass = some DitransitiveRootClass.ballisticMotion

theorem Semantics.Lexical.send_class_sending : LevinClass.send.ditransitiveRootClass = some DitransitiveRootClass.sending

theorem Semantics.Lexical.carry_class_carrying : LevinClass.carry.ditransitiveRootClass = some DitransitiveRootClass.carrying

inductive MRCDiagnostic : Type

The six MRC diagnostics developed in B&KG (2020 §§4.2–4.3). Three test for result entailment in the root; three test for manner. An MRC violation is a verb that passes diagnostics from BOTH sets.

Result diagnostics (§4.2):

• denialOfResult: "X cut Y, #but Y wasn't separated" — contradictory
• objectDeletion: result verbs resist unspecified object deletion
• restrictedResultatives: result verbs block adding new result XPs

Manner diagnostics (§4.3):

• selectionalRestriction: subject restricted to agents capable of the manner
• denialOfAction: "X cut Y, #but X didn't do anything" — contradictory
• actorParaphrase: paraphrasable as "X did manner to Y" (§4.3)

• denialOfResult : MRCDiagnostic
• objectDeletion : MRCDiagnostic
• restrictedResultatives : MRCDiagnostic
• selectionalRestriction : MRCDiagnostic
• denialOfAction : MRCDiagnostic
• actorParaphrase : MRCDiagnostic

@[implicit_reducible]

instance instDecidableEqMRCDiagnostic : DecidableEq MRCDiagnostic

Equations

• instDecidableEqMRCDiagnostic x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def instReprMRCDiagnostic.repr : MRCDiagnostic → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• instReprMRCDiagnostic.repr MRCDiagnostic.denialOfResult prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "MRCDiagnostic.denialOfResult")).group prec✝
• instReprMRCDiagnostic.repr MRCDiagnostic.objectDeletion prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "MRCDiagnostic.objectDeletion")).group prec✝
• instReprMRCDiagnostic.repr MRCDiagnostic.denialOfAction prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "MRCDiagnostic.denialOfAction")).group prec✝
• instReprMRCDiagnostic.repr MRCDiagnostic.actorParaphrase prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "MRCDiagnostic.actorParaphrase")).group prec✝

@[implicit_reducible]

instance instReprMRCDiagnostic : Repr MRCDiagnostic

Equations

• instReprMRCDiagnostic = { reprPrec := instReprMRCDiagnostic.repr }

def MRCDiagnostic.TestsResult : MRCDiagnostic → Prop

Whether a diagnostic tests for result entailment.

Equations

• MRCDiagnostic.denialOfResult.TestsResult = True
• MRCDiagnostic.objectDeletion.TestsResult = True
• MRCDiagnostic.restrictedResultatives.TestsResult = True
• x✝.TestsResult = False

@[implicit_reducible]

instance instDecidablePredMRCDiagnosticTestsResult : DecidablePred MRCDiagnostic.TestsResult

Equations

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

def MRCDiagnostic.TestsManner : MRCDiagnostic → Prop

Whether a diagnostic tests for manner entailment.

Equations

• MRCDiagnostic.selectionalRestriction.TestsManner = True
• MRCDiagnostic.denialOfAction.TestsManner = True
• MRCDiagnostic.actorParaphrase.TestsManner = True
• x✝.TestsManner = False

@[implicit_reducible]

instance instDecidablePredMRCDiagnosticTestsManner : DecidablePred MRCDiagnostic.TestsManner

Equations

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

theorem diagnostic_exclusive (d : MRCDiagnostic) : d.TestsResult ↔ ¬d.TestsManner

Each diagnostic tests for exactly one of manner or result.

structure MRCDiagnosticProfile : Type

A verb's diagnostic profile: which of the six diagnostics it passes. B&KG (2020 §§4.2–4.3) survey these for each verb class.

• denialOfResult : Bool
• objectDeletion : Bool
• restrictedResultatives : Bool
• selectionalRestriction : Bool
• denialOfAction : Bool
• actorParaphrase : Bool

def instDecidableEqMRCDiagnosticProfile.decEq (x✝ x✝¹ : MRCDiagnosticProfile) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance instDecidableEqMRCDiagnosticProfile : DecidableEq MRCDiagnosticProfile

Equations

• instDecidableEqMRCDiagnosticProfile = instDecidableEqMRCDiagnosticProfile.decEq

def instReprMRCDiagnosticProfile.repr : MRCDiagnosticProfile → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance instReprMRCDiagnosticProfile : Repr MRCDiagnosticProfile

Equations

• instReprMRCDiagnosticProfile = { reprPrec := instReprMRCDiagnosticProfile.repr }

def MRCDiagnosticProfile.showsResult (p : MRCDiagnosticProfile) : Bool

Whether the profile shows result entailment (passes ≥1 result diagnostic).

Equations

• p.showsResult = (p.denialOfResult || p.objectDeletion || p.restrictedResultatives)

def MRCDiagnosticProfile.showsManner (p : MRCDiagnosticProfile) : Bool

Whether the profile shows manner entailment (passes ≥1 manner diagnostic).

Equations

• p.showsManner = (p.selectionalRestriction || p.denialOfAction || p.actorParaphrase)

def MRCDiagnosticProfile.showsMRCViolation (p : MRCDiagnosticProfile) : Bool

An MRC violation is a verb whose diagnostics show BOTH manner and result.

Equations

• p.showsMRCViolation = (p.showsManner && p.showsResult)

def cutDiagnostics : MRCDiagnosticProfile

Cut passes all 6 diagnostics (B&KG §4.4): manner of cutting + separation. "Kim cut the bread, #but the bread wasn't separated" (result) "Kim cut the bread, #but Kim didn't do anything" (manner)

Equations

• cutDiagnostics = { denialOfResult := true, objectDeletion := true, restrictedResultatives := true, selectionalRestriction := true, denialOfAction := true, actorParaphrase := true }

def breakDiagnostics : MRCDiagnosticProfile

Break passes result diagnostics only: pure result (√CRACK), no manner.

Equations

• breakDiagnostics = { denialOfResult := true, objectDeletion := true, restrictedResultatives := true, selectionalRestriction := false, denialOfAction := false, actorParaphrase := false }

def hitDiagnostics : MRCDiagnosticProfile

Hit passes manner diagnostics only: pure manner (impact), no result.

Equations

• hitDiagnostics = { denialOfResult := false, objectDeletion := false, restrictedResultatives := false, selectionalRestriction := true, denialOfAction := true, actorParaphrase := true }

def drownDiagnostics : MRCDiagnosticProfile

Drown passes all 6 (B&KG §4.5): manner of drowning + death result.

Equations

• drownDiagnostics = { denialOfResult := true, objectDeletion := true, restrictedResultatives := true, selectionalRestriction := true, denialOfAction := true, actorParaphrase := true }

theorem cut_MRC_violation : cutDiagnostics.showsMRCViolation = true

theorem break_no_MRC_violation : breakDiagnostics.showsMRCViolation = false

theorem hit_no_MRC_violation : hitDiagnostics.showsMRCViolation = false

theorem drown_MRC_violation : drownDiagnostics.showsMRCViolation = true

theorem cut_diagnostics_match_entailments : cutDiagnostics.showsMRCViolation = true ↔ Semantics.Lexical.LevinClass.cut.rootEntailments.HasMannerAndResult

Cut is MRC-violating by BOTH diagnostics AND kind signature.

theorem break_diagnostics_match_entailments : breakDiagnostics.showsMRCViolation = true ↔ Semantics.Lexical.LevinClass.break_.rootEntailments.HasMannerAndResult

Break is MRC-respecting by BOTH diagnostics AND kind signature.

theorem hit_diagnostics_match_entailments : hitDiagnostics.showsMRCViolation = true ↔ Semantics.Lexical.LevinClass.hit.rootEntailments.HasMannerAndResult

Hit is MRC-respecting by BOTH diagnostics AND kind signature.

def rootTypeFromChangeEntailment (p : ArgumentStructure.EntailmentProfile) : RootType

Dowty's P-Patient entailment (a) "undergoes change of state" is precisely the result root entailment. An object bearing a result root's state predicate has changeOfState = true.

This bridges the root typology to the entailment profile via the shared property.

Equations

• rootTypeFromChangeEntailment p = if p.changeOfState = true then RootType.result else RootType.propertyConcept

theorem result_object_has_changeOfState : rootTypeFromChangeEntailment ArgumentStructure.EntailmentProfile.accomplishmentObjectProfile = RootType.result ∧ rootTypeFromChangeEntailment Features.LevinClassProfiles.contactObject = RootType.propertyConcept

A result verb's object (accomplishment template) has changeOfState = true, so it patterns with result roots. Contact-verb objects (kick: CA+St, no entailed change per [Bea11] eq. (60c)) fall on the other side of the bridge.

theorem die_result_pattern : rootTypeFromChangeEntailment Features.LevinClassProfiles.disappearance.subjectProfile = RootType.result

Die subject undergoes change → result-type pattern.

def RootType.requiresBECOME : RootType → Bool

Result roots MUST combine with a template containing BECOME (achievement or accomplishment), because the root's change entailment is semantically redundant with BECOME.

PC roots CAN combine with any template — with BECOME (achievement/ accomplishment) they get change compositionally; without it (state) they denote simple states.

Equations

• RootType.result.requiresBECOME = true
• RootType.propertyConcept.requiresBECOME = false

theorem result_root_gets_become_template : RootType.result.requiresBECOME = true

Result roots always get templates with BECOME.

def Template.hasBECOME : Semantics.Lexical.EventStructure.Template → Bool

Achievement and accomplishment templates contain BECOME.

Equations

• Template.hasBECOME Semantics.Lexical.EventStructure.Template.achievement = true
• Template.hasBECOME Semantics.Lexical.EventStructure.Template.accomplishment = true
• Template.hasBECOME x✝ = false

theorem result_templates_have_become : Template.hasBECOME Semantics.Lexical.EventStructure.Template.achievement = true ∧ Template.hasBECOME Semantics.Lexical.EventStructure.Template.accomplishment = true

The templates result roots combine with always have BECOME.

theorem state_template_no_become : Template.hasBECOME Semantics.Lexical.EventStructure.Template.state = false

State template lacks BECOME — only available to PC roots.

theorem become_templates_telic : Semantics.Lexical.EventStructure.Template.achievement.vendlerClass = Features.VendlerClass.achievement ∧ Semantics.Lexical.EventStructure.Template.accomplishment.vendlerClass = Features.VendlerClass.accomplishment

Bridge: templates with BECOME map to achievement/accomplishment Vendler classes, both of which are telic (bounded by the result state). This connects the template operator to the existing aspectual profile.

def RootType.stativeAspectualProfile : RootType → Features.AspectualProfile

Aspectual profile for root types in their stative use.

Equations

• RootType.propertyConcept.stativeAspectualProfile = Features.stateProfile
• RootType.result.stativeAspectualProfile = Features.achievementProfile

def RootType.stativeVendlerClass (rt : RootType) : Features.VendlerClass

Result root verbs are typically achievements or accomplishments (they have BECOME in their template). PC root verbs in their inchoative (change-of-state) use are also achievements/accomplishments, but their stative use is a state (derived from profile).

Equations

• rt.stativeVendlerClass = rt.stativeAspectualProfile.toVendlerClass

theorem root_stative_vendler : RootType.propertyConcept.stativeVendlerClass = Features.VendlerClass.state ∧ RootType.result.stativeVendlerClass = Features.VendlerClass.achievement

PC roots in stative use are states; result roots pattern as achievements even in adjectival use (the state entails prior change).

inductive AdjectivalStructure : Type

[Emb04] posits two adjectival structures:

(8a) BASIC STATIVES: [AspP AspS √ROOT] Simple adjective directly combining with stativizer. Only available to PC roots.

(8b) RESULT STATIVES: [AspP AspR [vP DP v_become √ROOT]] Deverbal adjective containing v_become. Available to result roots; superficially also to PC roots.

Under the non-bifurcated analysis, result root adjectives are ALWAYS (8b) because the root requires v_become. PC root adjectives are (8a) by default but can also be (8b).

• basicStative : AdjectivalStructure
• resultStative : AdjectivalStructure

@[implicit_reducible]

instance instDecidableEqAdjectivalStructure : DecidableEq AdjectivalStructure

Equations

• instDecidableEqAdjectivalStructure x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def instReprAdjectivalStructure.repr : AdjectivalStructure → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance instReprAdjectivalStructure : Repr AdjectivalStructure

Equations

• instReprAdjectivalStructure = { reprPrec := instReprAdjectivalStructure.repr }

def RootType.admitsBasicStative : RootType → Bool

PC roots admit both structures; result roots only admit resultStative.

Equations

• RootType.propertyConcept.admitsBasicStative = true
• RootType.result.admitsBasicStative = false

theorem admitsBasicStative_iff_no_change (rt : RootType) : rt.admitsBasicStative = true ↔ rt.entailsChange = false

This is equivalent to NOT entailing change.

inductive AgainReading : Type

Reading-count tabulation of sublexical again by root type ([BKG20] §1.3.2 (25), §2.4 (46)–(47)). again attaches either low (to the root, restitutive) or high (over vbecome, repetitive):

• RESTITUTIVE: presupposes only a prior state — available iff the root is change-free (PC roots, BKG (46));
• REPETITIVE: presupposes a prior change — always available.

A result root's state itself entails change, so its low/restitutive attachment still presupposes change and collapses into the repetitive reading (BKG (47), "result roots never admit truly restitutive readings"). The mechanism — the presuppositional operator and the reading hierarchy — is the canonical Verb.CosModel.again (see result_restitution_entails_change); this enum just records how many distinct readings each RootType admits.

• restitutive : AgainReading
• repetitive : AgainReading

@[implicit_reducible]

instance instDecidableEqAgainReading : DecidableEq AgainReading

Equations

• instDecidableEqAgainReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def instReprAgainReading.repr : AgainReading → ℕ → Std.Format

Equations

• instReprAgainReading.repr AgainReading.restitutive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "AgainReading.restitutive")).group prec✝
• instReprAgainReading.repr AgainReading.repetitive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "AgainReading.repetitive")).group prec✝

@[implicit_reducible]

instance instReprAgainReading : Repr AgainReading

Equations

• instReprAgainReading = { reprPrec := instReprAgainReading.repr }

def RootType.againReadings : RootType → List AgainReading

Which readings of 'again' are available for each root type.

Equations

• RootType.propertyConcept.againReadings = [AgainReading.restitutive, AgainReading.repetitive]
• RootType.result.againReadings = [AgainReading.repetitive]

theorem pc_more_again_readings : RootType.propertyConcept.againReadings.length > RootType.result.againReadings.length

PC roots have strictly more 'again' readings than result roots.

theorem result_no_restitutive : AgainReading.restitutive ∉ RootType.result.againReadings

Result roots lack the restitutive reading.

theorem pc_has_restitutive : AgainReading.restitutive ∈ RootType.propertyConcept.againReadings

PC roots have the restitutive reading.

def DitransitiveRootClass.obligatorilyTelic : DitransitiveRootClass → Bool

Whether a ditransitive verb is obligatorily telic in the IO frame (B&[BKG20] §3.7).

Telicity correlates with whether the root spells out a state in the template. If the root entails actual possession, the template's prospective possession is discharged → definite endpoint → telic.

"Kim gave Sandy balls for an hour" — # (bounded by possession transfer) "Kim sent Sandy balls for an hour" — OK (endpoint only prospective)

Equations

• DitransitiveRootClass.causedPossession.obligatorilyTelic = true
• x✝.obligatorilyTelic = false

theorem telic_iff_actual_possession (c : DitransitiveRootClass) : c.obligatorilyTelic = true ↔ c.entailments.possession = PossessionEntailment.actual

Telicity aligns exactly with actual possession entailment.

def DitransitiveRootClass.againReadings : DitransitiveRootClass → List AgainReading

Predicted again readings for each ditransitive root class.

Equations

• DitransitiveRootClass.causedPossession.againReadings = [AgainReading.repetitive]
• x✝.againReadings = [AgainReading.restitutive, AgainReading.repetitive]

theorem give_one_send_two_again : DitransitiveRootClass.causedPossession.againReadings.length = 1 ∧ DitransitiveRootClass.sending.againReadings.length = 2

Give has one reading (collapse); send has two (distinct).

theorem entails_change_implies_become_template (rt : RootType) (h : rt.entailsChange = true) : rt.requiresBECOME = true

Beavers et al.'s conclusion (§9): accepting that result roots entail change does NOT blunt the predictive power of event structures. It simply means the theory of possible root meanings is richer than bifurcation allows. A verb that entails change should have v_become-type grammatical behavior (argument structure, morphology) even if the change comes from the ROOT rather than the template.

Formally: if a root entails change, then the verb should be associated with a template containing BECOME.

theorem no_become_implies_no_change (rt : RootType) (h : rt.requiresBECOME = false) : rt.entailsChange = false

And conversely: if a root does NOT require BECOME, it doesn't entail change (it can stand alone as a simple stative).

theorem grand_unification (rt : RootType) : (rt.entailsChange = true → rt.hasSimpleStative = false ∧ rt.verbalFormIsMarked = false ∧ rt.allowsRestitutiveAgain = false ∧ rt.requiresBECOME = true ∧ rt.admitsBasicStative = false ∧ verbalMarkedness rt = Markedness.unmarked ∧ stativeMarkedness rt = Markedness.marked) ∧ (rt.entailsChange = false → rt.hasSimpleStative = true ∧ rt.verbalFormIsMarked = true ∧ rt.allowsRestitutiveAgain = true ∧ rt.requiresBECOME = false ∧ rt.admitsBasicStative = true ∧ verbalMarkedness rt = Markedness.marked ∧ stativeMarkedness rt = Markedness.unmarked)

The full correlation package.

Starting from the single Boolean entailsChange, we can derive ALL of the paper's morphosyntactic predictions. This is the formal content of the paper's main contribution: one semantic property (whether the root lexically entails change) is the sole determinant of six independently observable properties.

def RootClassification.verbalMarkedness (r : RootClassification) : Markedness

Predicted verbal markedness from change entailment.

Equations

• r.verbalMarkedness = verbalMarkedness r.changeType

def RootClassification.stativeMarkedness (r : RootClassification) : Markedness

Predicted stative markedness from change entailment.

Equations

• r.stativeMarkedness = stativeMarkedness r.changeType

def RootClassification.break_ : RootClassification

√BREAK: selects theme + entails change (result root, Levin 45.1). "Break X" — the root obligatorily takes a patient that undergoes breaking, and the root lexically entails a prior change event.

Equations

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

def RootClassification.hit : RootClassification

√HIT: selects theme + does not entail change (Levin 18.1). "Hit X" — the root takes a contactee, but hitting does not entail that the patient undergoes a change of state ([Lev93] pp. 5–8). .propertyConcept is used broadly here: the formal content (entailsChange = false) is what matters, not the label.

Equations

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

def RootClassification.die : RootClassification

√DIE: no theme + entails change. "Die" — intransitive; the dying entity is introduced by functional structure (unaccusative vGO/vBE), not selected by the root. Dying lexically entails a prior change event (becoming dead).

Equations

• RootClassification.die = { arity := Verb.Root.Arity.noTheme, changeType := RootType.result, denotationType := some RootDenotationType.indivStatePred }

def RootClassification.sit : RootClassification

√SIT: no theme + does not entail change (positional root). "Sit" — Coon's √POS class: denotes a spatial configuration state. No internal argument, no entailed change.

Equations

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

theorem arity_changeType_orthogonal : (∃ (r : RootClassification), r.arity = Verb.Root.Arity.selectsTheme ∧ r.changeType = RootType.result) ∧ (∃ (r : RootClassification), r.arity = Verb.Root.Arity.selectsTheme ∧ r.changeType = RootType.propertyConcept) ∧ (∃ (r : RootClassification), r.arity = Verb.Root.Arity.noTheme ∧ r.changeType = RootType.result) ∧ ∃ (r : RootClassification), r.arity = Verb.Root.Arity.noTheme ∧ r.changeType = RootType.propertyConcept

Orthogonality of arity and change entailment.

All four cells of the 2×2 cross-classification are inhabited. This proves the two dimensions are genuinely independent: knowing that a root selects a theme tells you nothing about whether it entails change, and vice versa.

theorem change_does_not_determine_arity : (∃ (r : RootClassification), r.entailsChange = true ∧ r.arity = Verb.Root.Arity.selectsTheme) ∧ (∃ (r : RootClassification), r.entailsChange = true ∧ r.arity = Verb.Root.Arity.noTheme) ∧ (∃ (r : RootClassification), r.entailsChange = false ∧ r.arity = Verb.Root.Arity.selectsTheme) ∧ ∃ (r : RootClassification), r.entailsChange = false ∧ r.arity = Verb.Root.Arity.noTheme

Change entailment does not determine arity (and vice versa).

Beavers et al.'s grand unification (§14) shows that entailsChange determines ALL morphosyntactic correlates (markedness, simple stative, again readings, template requirements). But it determines NOTHING about internal argument selection. Coon's arity adds an independent dimension of prediction: whether the root will surface with an internal argument across voice alternations.

theorem theme_persistence (r : RootClassification) (h : r.arity = Verb.Root.Arity.selectsTheme) : r.arity.hasInternalArg = true

Theme persistence ([Coo19] main empirical claim).

If a root selects a theme, the internal argument persists regardless of what v/Voice⁰ head combines with it. In Chuj, √TV roots surface with an internal argument in transitive (Ø), passive (-ch, -j), and antipassive (-w) constructions alike.

This is expressed by design: arity is a field of RootClassification, not of the derived verb. No functional head modifies it.

theorem root_markedness_from_change (r : RootClassification) : r.verbalMarkedness = Markedness.unmarked ↔ r.entailsChange = true

Change entailment determines markedness in the unified Root.

theorem same_change_same_morphosyntax (r₁ r₂ : RootClassification) (h : r₁.changeType = r₂.changeType) : r₁.verbalMarkedness = r₂.verbalMarkedness ∧ r₁.stativeMarkedness = r₂.stativeMarkedness ∧ r₁.entailsChange = r₂.entailsChange

Roots with the same change type have identical morphosyntactic behavior regardless of arity — markedness, stative forms, and again readings are orthogonal to internal argument selection.

structure FullRootSpec : Type

Full root specification: entailment features + structural position. This is [BKG20]'s ch. 5 root typology (display (12)) in full — the 4 binary entailment features × 2 positions give 32 theoretical cells, of which 7 are attested and the rest are principled gaps.

• entailments : Verb.Root.Kinds
• position : Verb.Root.Position

@[implicit_reducible]

instance instDecidableEqFullRootSpec : DecidableEq FullRootSpec

Equations

• instDecidableEqFullRootSpec = instDecidableEqFullRootSpec.decEq

def instDecidableEqFullRootSpec.decEq (x✝ x✝¹ : FullRootSpec) : Decidable (x✝ = x✝¹)

Equations

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

def FullRootSpec.PositionLicensed (s : FullRootSpec) : Prop

Adjoined position requires +manner: a root in adjunct position must specify a manner of action. Without manner, there is nothing to adjoin — the adjunct slot expects an action modifier.

Equations

• s.PositionLicensed = (s.position = Verb.Root.Position.adjoined → Verb.LexKind.manner ∈ s.entailments)

@[implicit_reducible]

instance instDecidablePositionLicensed (s : FullRootSpec) : Decidable s.PositionLicensed

Equations

• instDecidablePositionLicensed s = instDecidablePositionLicensed._aux_1 s

def FullRootSpec.SemanticallyCoherent (s : FullRootSpec) : Prop

+manner +state −result −cause is semantically incoherent (B&KG §5.4.1): the root would specify both a manner of action and a state, but with no result or cause linking them. What would such a verb mean? "Perform manner M while in state S" — with no causal connection.

Equations

• s.SemanticallyCoherent = ¬(Verb.LexKind.manner ∈ s.entailments ∧ Verb.LexKind.state ∈ s.entailments ∧ Verb.LexKind.result ∉ s.entailments ∧ Verb.LexKind.cause ∉ s.entailments)

@[implicit_reducible]

instance instDecidableSemanticallyCoherent (s : FullRootSpec) : Decidable s.SemanticallyCoherent

Equations

• instDecidableSemanticallyCoherent s = instDecidableSemanticallyCoherent._aux_1 s

def FullRootSpec.WellFormed (s : FullRootSpec) : Prop

Full well-formedness: entailment constraints + position licensing + semantic coherence.

Equations

• s.WellFormed = (s.entailments.WellFormed ∧ s.PositionLicensed ∧ s.SemanticallyCoherent)

@[implicit_reducible]

instance instDecidableWellFormed (s : FullRootSpec) : Decidable s.WellFormed

Equations

• instDecidableWellFormed s = instDecidableWellFormed._aux_1 s

Attested cells of Table 12

def FullRootSpec.flat : FullRootSpec

√FLAT: +S −M −R −C, complement. Property concept root.

Equations

• FullRootSpec.flat = { entailments := Verb.Root.Kinds.propertyConcept, position := Verb.Root.Position.complement }

def FullRootSpec.blossom : FullRootSpec

√BLOSSOM: +S −M +R −C, complement. Pure result root.

Equations

• FullRootSpec.blossom = { entailments := Verb.Root.Kinds.pureResult, position := Verb.Root.Position.complement }

def FullRootSpec.crack : FullRootSpec

√CRACK: +S −M +R +C, complement. Causative result root.

Equations

• FullRootSpec.crack = { entailments := Verb.Root.Kinds.causativeResult, position := Verb.Root.Position.complement }

def FullRootSpec.jog : FullRootSpec

√JOG: −S +M −R −C, adjoined. Pure manner root.

Equations

• FullRootSpec.jog = { entailments := Verb.Root.Kinds.pureManner, position := Verb.Root.Position.adjoined }

def FullRootSpec.drown : FullRootSpec

√DROWN: +S +M +R +C, complement. Manner+result in complement position — the manner restricts HOW the state is caused.

Equations

• FullRootSpec.drown = { entailments := Verb.Root.Kinds.fullSpec, position := Verb.Root.Position.complement }

def FullRootSpec.toss : FullRootSpec

√TOSS: +S +M +R +C, adjoined. Manner+result in adjunct position — the manner is the primary event that happens to cause a state change.

Equations

• FullRootSpec.toss = { entailments := Verb.Root.Kinds.fullSpec, position := Verb.Root.Position.adjoined }

@[reducible, inline]

abbrev FullRootSpec.hand : FullRootSpec

√HAND: same entailments + position as √TOSS. The difference is in the ditransitive layer (DitransitiveRootClass.causedPossession vs .ballisticMotion), not in FullRootSpec's 4+1 features.

Equations

• FullRootSpec.hand = FullRootSpec.toss

def FullRootSpec.exist : FullRootSpec

√EXIST: −S −M −R −C, complement. Minimal stative root.

Equations

• FullRootSpec.exist = { entailments := Verb.Root.Kinds.minimal, position := Verb.Root.Position.complement }

theorem flat_wf : FullRootSpec.flat.WellFormed

theorem blossom_wf : FullRootSpec.blossom.WellFormed

theorem crack_wf : FullRootSpec.crack.WellFormed

theorem jog_wf : FullRootSpec.jog.WellFormed

theorem drown_wf : FullRootSpec.drown.WellFormed

theorem toss_wf : FullRootSpec.toss.WellFormed

theorem hand_wf : FullRootSpec.hand.WellFormed

theorem exist_wf : FullRootSpec.exist.WellFormed

theorem drown_toss_same_entailments : FullRootSpec.drown.entailments = FullRootSpec.toss.entailments

√DROWN and √TOSS have identical entailments but different positions.

theorem drown_toss_diff_position : FullRootSpec.drown.position ≠ FullRootSpec.toss.position

inductive TemplateHead : Type

Templatic functional heads in event structure (B&[BKG20] Table 13).

Each root type PREDICTS which templatic heads its verb will entail. If the root's own meaning already includes what a template head provides, that head is "entailed by the root" — its semantic contribution is redundant (though structurally still present).

v_act, v_cause, v_become are verbal heads. P_loc and P_have are prepositional heads specific to ditransitive structures.

• vAct : TemplateHead
• vCause : TemplateHead
• vBecome : TemplateHead
• pLoc : TemplateHead
• pHave : TemplateHead

@[implicit_reducible]

instance instDecidableEqTemplateHead : DecidableEq TemplateHead

Equations

• instDecidableEqTemplateHead x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance instReprTemplateHead : Repr TemplateHead

Equations

• instReprTemplateHead = { reprPrec := instReprTemplateHead.repr }

def instReprTemplateHead.repr : TemplateHead → ℕ → Std.Format

Equations

• instReprTemplateHead.repr TemplateHead.vAct prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TemplateHead.vAct")).group prec✝
• instReprTemplateHead.repr TemplateHead.vCause prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TemplateHead.vCause")).group prec✝
• instReprTemplateHead.repr TemplateHead.vBecome prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TemplateHead.vBecome")).group prec✝
• instReprTemplateHead.repr TemplateHead.pLoc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TemplateHead.pLoc")).group prec✝
• instReprTemplateHead.repr TemplateHead.pHave prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TemplateHead.pHave")).group prec✝

def Verb.Root.Kinds.entailedHeads (s : Kinds) : List TemplateHead

Which template heads a root's entailments make redundant (Table 13).

The mapping is monotone: more root entailments → more heads entailed.

• +result → v_become (root entails the change v_become would provide)
• +cause → v_cause (root entails the causation v_cause would provide)
• +manner ∧ +cause → v_act (manner that causes = activity)
• +manner alone → no v_act (manner without causation doesn't entail activity — √JOG specifies jogging manner but v_act still provides the activity frame)

Equations

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

def DitransitiveRootClass.additionalHeads : DitransitiveRootClass → List TemplateHead

For ditransitive roots, additional prepositional heads beyond the verbal heads predicted by entailedHeads.

Equations

• DitransitiveRootClass.causedPossession.additionalHeads = [TemplateHead.pLoc, TemplateHead.pHave]
• DitransitiveRootClass.ballisticMotion.additionalHeads = [TemplateHead.pLoc]
• DitransitiveRootClass.sending.additionalHeads = [TemplateHead.pLoc]
• DitransitiveRootClass.accompaniedMotion.additionalHeads = [TemplateHead.pLoc]
• DitransitiveRootClass.carrying.additionalHeads = [TemplateHead.pLoc]
• DitransitiveRootClass.futureHaving.additionalHeads = []

Table 13 verification

theorem jog_no_heads : Verb.Root.Kinds.pureManner.entailedHeads = []

√JOG (pureManner): no template heads entailed. The root specifies jogging manner, but v_act still provides the activity frame — the root doesn't make it redundant.

theorem flat_no_heads : Verb.Root.Kinds.propertyConcept.entailedHeads = []

√FLAT (propertyConcept): no template heads entailed. The root names a state, but doesn't entail change or cause.

theorem blossom_heads : Verb.Root.Kinds.pureResult.entailedHeads = [TemplateHead.vBecome]

√BLOSSOM (pureResult): v_become entailed. The root entails change — v_become's contribution is redundant.

theorem crack_heads : Verb.Root.Kinds.causativeResult.entailedHeads = [TemplateHead.vBecome, TemplateHead.vCause]

√CRACK (causativeResult): v_become + v_cause entailed. The root entails change AND causation.

theorem drown_heads : Verb.Root.Kinds.fullSpec.entailedHeads = [TemplateHead.vBecome, TemplateHead.vCause, TemplateHead.vAct]

√DROWN (fullSpec): v_become + v_cause + v_act entailed. The root entails change, causation, AND activity (manner that causes).

theorem toss_heads : Verb.Root.Kinds.fullSpec.entailedHeads ++ DitransitiveRootClass.ballisticMotion.additionalHeads = [TemplateHead.vBecome, TemplateHead.vCause, TemplateHead.vAct, TemplateHead.pLoc]

√TOSS (fullSpec + ballistic): v_become + v_cause + v_act + P_loc. Verbal heads from entailments + P_loc from ditransitive class.

theorem hand_heads : Verb.Root.Kinds.fullSpec.entailedHeads ++ DitransitiveRootClass.causedPossession.additionalHeads = [TemplateHead.vBecome, TemplateHead.vCause, TemplateHead.vAct, TemplateHead.pLoc, TemplateHead.pHave]

√HAND (fullSpec + causedPossession): all 5 heads. Verbal heads from entailments + P_loc + P_have from ditransitive class.

theorem heads_monotone : Verb.Root.Kinds.pureResult.entailedHeads.length ≤ Verb.Root.Kinds.causativeResult.entailedHeads.length ∧ Verb.Root.Kinds.causativeResult.entailedHeads.length ≤ Verb.Root.Kinds.fullSpec.entailedHeads.length

Monotonicity: more root entailments → weakly more heads entailed. Pure result ⊂ causative result ⊂ full spec (by inclusion).

def FullRootSpec.attestedCells : List FullRootSpec

The attested cells of B&KG's Table 12: five complement types (√FLAT, √BLOSSOM, √CRACK, √DROWN, √EXIST) and two adjoined types (√JOG, √TOSS/√HAND).

Equations

• FullRootSpec.attestedCells = [FullRootSpec.flat, FullRootSpec.blossom, FullRootSpec.crack, FullRootSpec.drown, FullRootSpec.exist, FullRootSpec.jog, FullRootSpec.toss]

def FullRootSpec.IsAttestedCell (s : FullRootSpec) : Prop

Whether a FullRootSpec cell is attested in B&KG's Table 12.

Equations

• s.IsAttestedCell = (s.WellFormed ∧ s ∈ FullRootSpec.attestedCells)

@[implicit_reducible]

instance instDecidableIsAttestedCell (s : FullRootSpec) : Decidable s.IsAttestedCell

Equations

• instDecidableIsAttestedCell s = instDecidableIsAttestedCell._aux_1 s

Gap explanations

B&KG (§5.4.1) identify three principled gap types:

1. Adjoined without manner: the adjunct position in event structure hosts manner modifiers. Without +manner, there's nothing to adjoin. This rules out all −manner roots in adjoined position.

2. +manner +state −result −cause: the root would need to encode both a manner of action and a state, with no causal/change connection between them. No known verb has this pattern.

3. Well-formedness violations: +result −state and +cause −result are ruled out by the entailment constraints (result→state, cause→result).

theorem gap_adjoined_no_manner : ¬{ entailments := Verb.Root.Kinds.propertyConcept, position := Verb.Root.Position.adjoined }.PositionLicensed

Gap type 1: adjoined position requires manner.

theorem gap_adjoined_result : ¬{ entailments := Verb.Root.Kinds.pureResult, position := Verb.Root.Position.adjoined }.PositionLicensed

theorem gap_adjoined_causativeResult : ¬{ entailments := Verb.Root.Kinds.causativeResult, position := Verb.Root.Position.adjoined }.PositionLicensed

theorem gap_adjoined_minimal : ¬{ entailments := Verb.Root.Kinds.minimal, position := Verb.Root.Position.adjoined }.PositionLicensed

theorem gap_manner_state_no_result : ¬{ entailments := {Verb.LexKind.state, Verb.LexKind.manner}, position := Verb.Root.Position.complement }.SemanticallyCoherent

Gap type 2: +manner +state −result −cause is incoherent.

theorem gap_manner_state_no_result_adj : ¬{ entailments := {Verb.LexKind.state, Verb.LexKind.manner}, position := Verb.Root.Position.adjoined }.SemanticallyCoherent

theorem gap_result_no_state : ¬{Verb.LexKind.result}.WellFormed

Gap type 3: well-formedness violations.

theorem gap_cause_no_result : ¬{Verb.LexKind.state, Verb.LexKind.cause}.WellFormed

Attested cells are well-formed and recognized

theorem flat_attested : FullRootSpec.flat.IsAttestedCell

theorem blossom_attested : FullRootSpec.blossom.IsAttestedCell

theorem crack_attested : FullRootSpec.crack.IsAttestedCell

theorem jog_attested : FullRootSpec.jog.IsAttestedCell

theorem drown_attested : FullRootSpec.drown.IsAttestedCell

theorem toss_attested : FullRootSpec.toss.IsAttestedCell

theorem exist_attested : FullRootSpec.exist.IsAttestedCell

theorem mannerResult_complement_unattested : ¬{ entailments := Verb.Root.Kinds.mannerResult, position := Verb.Root.Position.complement }.IsAttestedCell

The open question: +S +M +R −C (mannerResult without cause) in complement position. B&KG note this cell may be inhabited by verbs like slide — manner of motion + change of location, without external causation. Left as NOT attested per Table 12, pending further research.

theorem fullSpec_both_positions : FullRootSpec.drown.IsAttestedCell ∧ FullRootSpec.toss.IsAttestedCell ∧ FullRootSpec.drown.entailments = FullRootSpec.toss.entailments

The complement/adjoined split for fullSpec roots is the only case where position differentiates otherwise identical entailments.