Root classification: change type, denotation type, and cross-classification

The cross-linguistic classification dimensions a change-of-state verb root is typed by: whether it lexically entails change (ChangeType), its semantic denotation domain (DenotationType), Dixon's property-concept categories (PCClass), Levin's result-verb categories (ResultClass), and the bundled Classification cross-classifying arity against change entailment.

Anchoring and provenance

• ChangeType — the property-concept vs. result split of [Lev93]'s deadjectival typology. The reading that result roots lexically entail change (entailsChange, allowsRestitutiveAgain) is the [BEJ+21]/[BKG20] account and is contested by the Distributed-Morphology camp, for whom change is templatic; the split itself is theory-neutral.
• DenotationType — the four denotation domains of [Coo19]'s Chuj root classes (3), extended by [HKG25]. A single-account type earning substrate status by consumer count (Chuj fragment, Coon 2019, Hanink & Koontz-Garboden 2025).
• PCClass — [Dix82]'s seven property-concept categories (consensus).
• ResultClass — [Lev93]'s result-verb categories (consensus), except inherentlyDirectedMotion, a formaliser addition not on Levin's list.

Main definitions

• ChangeType, ChangeType.entailsChange, ChangeType.allowsRestitutiveAgain
• DenotationType, DenotationType.hasIndivArg
• PCClass, ResultClass
• Classification bundling arity × change entailment × denotation type

Main results

• arity_changeType_orthogonal, change_does_not_determine_arity — the arity and change-entailment dimensions are independent (all four cells inhabited).
• theme_persistence — a theme-selecting root keeps its internal argument regardless of the functional head ([Coo19]).

inductive Verb.Root.ChangeType : 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 (flat, red, long, warm). Result roots underlie non-deadjectival CoS verbs: the root describes a specific result state arising from a particular event (crack, break, shatter).

• propertyConcept : ChangeType
• result : ChangeType

@[implicit_reducible]

instance Verb.Root.instDecidableEqChangeType : DecidableEq ChangeType

Equations

• Verb.Root.instDecidableEqChangeType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Verb.Root.instReprChangeType : Repr ChangeType

Equations

• Verb.Root.instReprChangeType = { reprPrec := Verb.Root.instReprChangeType.repr }

def Verb.Root.instReprChangeType.repr : ChangeType → ℕ → Std.Format

Equations

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

def Verb.Root.ChangeType.entailsChange : ChangeType → Bool

Whether a root lexically entails prior change ([BEJ+21] §3.6). PC roots denote simple states holding without prior change; result roots denote states entailing a prior change event. The entailment reading is the B&KG account, contested by the DM camp.

Equations

• Verb.Root.ChangeType.propertyConcept.entailsChange = false
• Verb.Root.ChangeType.result.entailsChange = true

def Verb.Root.ChangeType.allowsRestitutiveAgain : ChangeType → Bool

PC roots allow restitutive again (scope over root only); result roots allow only repetitive again (scope over BECOME) ([BEJ+21] §3.4). Since a result root's state itself entails change, again over the root still entails a prior change event, collapsing into the repetitive reading.

Equations

• Verb.Root.ChangeType.propertyConcept.allowsRestitutiveAgain = true
• Verb.Root.ChangeType.result.allowsRestitutiveAgain = false

inductive Verb.Root.DenotationType : 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])
• statePred ⟨v,t⟩: predicate of states, no individual argument (PC Class 2)
• measureFn ⟨e, ⟨s,d⟩⟩: entity → event → degree (√POS in [Coo19] (3), following [Hen19]'s measure functions)
• entityPred ⟨e,t⟩: entity → truth-value, no event (√NOM)

• indivStatePred : DenotationType
• statePred : DenotationType
• measureFn : DenotationType
• entityPred : DenotationType

@[implicit_reducible]

instance Verb.Root.instDecidableEqDenotationType : DecidableEq DenotationType

Equations

• Verb.Root.instDecidableEqDenotationType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Verb.Root.instReprDenotationType.repr : DenotationType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Verb.Root.instReprDenotationType : Repr DenotationType

Equations

• Verb.Root.instReprDenotationType = { reprPrec := Verb.Root.instReprDenotationType.repr }

def Verb.Root.DenotationType.hasIndivArg : DenotationType → Bool

Whether a root denotation type includes an individual argument.

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

Equations

• Verb.Root.DenotationType.indivStatePred.hasIndivArg = true
• Verb.Root.DenotationType.statePred.hasIndivArg = false
• Verb.Root.DenotationType.measureFn.hasIndivArg = true
• Verb.Root.DenotationType.entityPred.hasIndivArg = true

inductive Verb.Root.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).

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

@[implicit_reducible]

instance Verb.Root.instDecidableEqPCClass : DecidableEq PCClass

Equations

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

@[implicit_reducible]

instance Verb.Root.instReprPCClass : Repr PCClass

Equations

• Verb.Root.instReprPCClass = { reprPrec := Verb.Root.instReprPCClass.repr }

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

Equations

• One or more equations did not get rendered due to their size.
• Verb.Root.instReprPCClass.repr Verb.Root.PCClass.dimension prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Verb.Root.PCClass.dimension")).group prec✝
• Verb.Root.instReprPCClass.repr Verb.Root.PCClass.age prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Verb.Root.PCClass.age")).group prec✝
• Verb.Root.instReprPCClass.repr Verb.Root.PCClass.value prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Verb.Root.PCClass.value")).group prec✝
• Verb.Root.instReprPCClass.repr Verb.Root.PCClass.color prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Verb.Root.PCClass.color")).group prec✝
• Verb.Root.instReprPCClass.repr Verb.Root.PCClass.speed prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Verb.Root.PCClass.speed")).group prec✝

inductive Verb.Root.ResultClass : Type

Result root subclasses ([Lev93]; [BEJ+21] ex. 6). inherentlyDirectedMotion is a formaliser addition, not on Levin's list.

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

@[implicit_reducible]

instance Verb.Root.instDecidableEqResultClass : DecidableEq ResultClass

Equations

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

@[implicit_reducible]

instance Verb.Root.instReprResultClass : Repr ResultClass

Equations

• Verb.Root.instReprResultClass = { reprPrec := Verb.Root.instReprResultClass.repr }

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

Equations

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

structure Verb.Root.Classification : Type

Unified root characterization bundling the classification dimensions.

A root is characterized along independent axes: arity (does it select an internal argument?), change entailment (does it lexically entail prior change?), denotation type ([Coo19] (3)), within-class quality dimensions, and verb-class membership. Arity, change entailment, and denotation type cross-classify: [Coo19]'s four Chuj root classes are recovered as (arity × denotationType) pairs — √TV = selectsTheme + indivStatePred, √ITV = noTheme + indivStatePred, √POS = noTheme + measureFn, √NOM = noTheme + entityPred.

• arity : Arity

  Does this root select an internal argument?

• changeType : ChangeType

  Does this root lexically entail prior change?

• denotationType : Option DenotationType

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

• profile : Profile

  Within-class quality dimensions ([SMcN26]).

• levinClass : Option ArgumentStructure.LevinClass

  Verb class membership.

@[implicit_reducible]

instance Verb.Root.instBEqClassification : BEq Classification

Equations

• Verb.Root.instBEqClassification = { beq := Verb.Root.instBEqClassification.beq }

def Verb.Root.instBEqClassification.beq : Classification → Classification → Bool

Equations

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

@[implicit_reducible]

instance Verb.Root.instReprClassification : Repr Classification

Equations

• Verb.Root.instReprClassification = { reprPrec := Verb.Root.instReprClassification.repr }

def Verb.Root.instReprClassification.repr : Classification → ℕ → Std.Format

Equations

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

def Verb.Root.Classification.entailsChange (r : Classification) : Bool

Does this root lexically entail prior change?

Equations

• r.entailsChange = r.changeType.entailsChange

Cross-classification: arity × change entailment

def Verb.Root.Classification.break_ : Classification

√BREAK: selects theme + entails change (result root, [Lev93] 45.1).

Equations

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

def Verb.Root.Classification.hit : Classification

√HIT: selects theme + does not entail change ([Lev93] 18.1). .propertyConcept is used broadly: 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 Verb.Root.Classification.die : Classification

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

Equations

• Verb.Root.Classification.die = { arity := Verb.Root.Arity.noTheme, changeType := Verb.Root.ChangeType.result, denotationType := some Verb.Root.DenotationType.indivStatePred }

def Verb.Root.Classification.sit : Classification

√SIT: no theme + does not entail change (positional root, Coon's √POS class). Denotes a measure function ⟨e,⟨s,d⟩⟩ ([Coo19] (3), following [Hen19]).

Equations

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

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

Orthogonality of arity and change entailment. All four cells of the 2×2 cross-classification are inhabited: knowing that a root selects a theme tells you nothing about whether it entails change, and vice versa.

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

Change entailment does not determine arity (and vice versa). Change entailment fixes all morphosyntactic correlates (markedness, simple stative, again readings) but nothing about internal argument selection — [Coo19]'s arity is an independent dimension.

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

Theme persistence ([Coo19] main empirical claim). If a root selects a theme, the internal argument persists regardless of the v/Voice⁰ head. In Chuj, √TV roots surface with an internal argument in transitive, passive, and antipassive constructions alike. Expressed by design: arity is a field of Classification, not of the derived verb.