Documentation

Linglib.Theories.Semantics.Lexical.LevinTheory

Levin Verb Class Theory #

@cite{levin-1993} @cite{dowty-1991} @cite{beavers-koontz-garboden-2020}

The LevinClass enum and its classification data (MeaningComponents, meaningComponents, predictsUnaccusative, isVerbOfCreation) are defined in Core/Lexical/VerbClass.lean.

This file provides the theoretical content that depends on RootEntailments: root entailment mapping, root–MC bridge enums, and universal consistency theorems.

§ 1. Root entailment mapping (@cite{beavers-koontz-garboden-2020}) #

Root structural entailments, well-formedness verification, and MRC tests.

§ 2. Root–MC bridge #

Classification enums (CausationSource, ResultKind, MannerKind) naming the systematic divergences between B&KG root features and Levin meaning components, plus universal consistency theorems.

def Semantics.Lexical.LevinClass.rootEntailments :

LevinClass → Roots.RootEntailments

Root structural entailments for each Levin class.

Assignments marked (B&KG) are directly from @cite{beavers-koontz-garboden-2020} Table 12 and Chapters 2–5. Others are inferred from class semantics following B&KG's framework:

Externally caused CoS → causativeResult (√CRACK pattern)
Internally caused CoS → pureResult (√BLOSSOM pattern)
Action/manner verbs → pureManner (√JOG pattern)
MRC violators → fullSpec (√HAND/√DROWN pattern)
Stative/psychological → propertyConcept (√FLAT pattern)

Classes marked (default) use minimal as a conservative placeholder pending detailed study under B&KG's framework.

Equations

Instances For

Well-formedness verification #

theorem Semantics.Lexical.break_root_wf :

LevinClass.break_.rootEntailments.WellFormed

theorem Semantics.Lexical.cut_root_wf :

LevinClass.cut.rootEntailments.WellFormed

theorem Semantics.Lexical.hit_root_wf :

LevinClass.hit.rootEntailments.WellFormed

theorem Semantics.Lexical.touch_root_wf :

LevinClass.touch.rootEntailments.WellFormed

theorem Semantics.Lexical.give_root_wf :

LevinClass.give.rootEntailments.WellFormed

theorem Semantics.Lexical.destroy_root_wf :

LevinClass.destroy.rootEntailments.WellFormed

theorem Semantics.Lexical.murder_root_wf :

LevinClass.murder.rootEntailments.WellFormed

theorem Semantics.Lexical.poison_root_wf :

LevinClass.poison.rootEntailments.WellFormed

MRC violation verification #

theorem Semantics.Lexical.cut_violates_MRC :

LevinClass.cut.rootEntailments.ViolatesMRC

theorem Semantics.Lexical.cooking_violates_MRC :

LevinClass.cooking.rootEntailments.ViolatesMRC

theorem Semantics.Lexical.poison_violates_MRC :

LevinClass.poison.rootEntailments.ViolatesMRC

theorem Semantics.Lexical.break_respects_MRC :

¬LevinClass.break_.rootEntailments.ViolatesMRC

theorem Semantics.Lexical.hit_respects_MRC :

¬LevinClass.hit.rootEntailments.ViolatesMRC

VOC–root entailment theorems #

theorem Semantics.Lexical.build_class_causative :

LevinClass.build.rootEntailments = Roots.RootEntailments.causativeResult

Core creation classes have causativeResult root entailments.

theorem Semantics.Lexical.create_class_causative :

LevinClass.create.rootEntailments = Roots.RootEntailments.causativeResult

Root–MC correspondence (2026 consensus) #

The 2026 consensus in lexical semantics (@cite{beavers-koontz-garboden-2020}, @cite{rappaport-hovav-levin-2024}) treats root entailments as primary: verb behavior at the Levin diagnostic level is determined by root content plus semantic field membership plus template structure.

But the B&KG root features and the Levin meaning components are NOT isomorphic — they conceptualize different levels of granularity:

B&KG concept	Levin concept	Relationship
`result`	`changeOfState`	B&KG broader: includes location/possession change
`manner`	`mannerSpec` ∨ `instrumentSpec`	B&KG broader: includes contact-manner (hit)
`cause`	`causation`	Distinct: root-level vs event-level causation

The three *Kind enums below name the specific cases where the two frameworks diverge, making the divergences grep-able and testable.

inductive Semantics.Lexical.CausationSource :

Where a verb class's event-level causation originates.

B&KG's root-level cause and Levin's event-level causation are distinct concepts (@cite{beavers-koontz-garboden-2020} Ch. 5; @cite{levin-1993} pp. 9–10).

rootExternal : CausationSource
rootNonDetachable : CausationSource
template : CausationSource
none : CausationSource

Instances For

@[implicit_reducible]

instance Semantics.Lexical.instDecidableEqCausationSource :

DecidableEq CausationSource

Equations

Semantics.Lexical.instDecidableEqCausationSource x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.Lexical.instReprCausationSource :

Repr CausationSource

Equations

Semantics.Lexical.instReprCausationSource = { reprPrec := Semantics.Lexical.instReprCausationSource.repr }

def Semantics.Lexical.instReprCausationSource.repr :

CausationSource → ℕ → Std.Format

Equations

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

Instances For

def Semantics.Lexical.LevinClass.causationSource (c : LevinClass) :

CausationSource

Derive the causation source from root entailments and meaning components.

Equations

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

Instances For

inductive Semantics.Lexical.ResultKind :

What kind of result the root entails (refines B&KG result).

Levin's changeOfState corresponds to stateChange only — change of location (throw, arrive) and change of possession (give) have result = true in B&KG but changeOfState = false in Levin.

stateChange : ResultKind
locationChange : ResultKind
possessionChange : ResultKind
none : ResultKind

Instances For

@[implicit_reducible]

instance Semantics.Lexical.instDecidableEqResultKind :

DecidableEq ResultKind

Equations

Semantics.Lexical.instDecidableEqResultKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Lexical.instReprResultKind.repr :

ResultKind → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Semantics.Lexical.instReprResultKind :

Repr ResultKind

Equations

Semantics.Lexical.instReprResultKind = { reprPrec := Semantics.Lexical.instReprResultKind.repr }

def Semantics.Lexical.LevinClass.resultKind (c : LevinClass) :

Derive result kind from root entailments and meaning components.

Equations

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

Instances For

inductive Semantics.Lexical.MannerKind :

How root manner maps to Levin's MC spec features.

B&KG's manner subsumes three Levin-level distinctions:

mannerSpec: how the action proceeds (cooking, running)
instrumentSpec: what tool is used (cutting, poking)
unspecified: manner verb without a Levin spec flag (hit, push)

mannerSpec : MannerKind
instrumentSpec : MannerKind
unspecified : MannerKind
none : MannerKind

Instances For

@[implicit_reducible]

instance Semantics.Lexical.instDecidableEqMannerKind :

DecidableEq MannerKind

Equations

Semantics.Lexical.instDecidableEqMannerKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Lexical.instReprMannerKind.repr :

MannerKind → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Semantics.Lexical.instReprMannerKind :

Repr MannerKind

Equations

Semantics.Lexical.instReprMannerKind = { reprPrec := Semantics.Lexical.instReprMannerKind.repr }

def Semantics.Lexical.LevinClass.mannerKind (c : LevinClass) :

Derive manner kind from root entailments and meaning components.

Equations

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

Instances For

Causation source verification #

theorem Semantics.Lexical.break_causation_rootExternal :

LevinClass.break_.causationSource = CausationSource.rootExternal

theorem Semantics.Lexical.destroy_causation_rootExternal :

LevinClass.destroy.causationSource = CausationSource.rootExternal

theorem Semantics.Lexical.murder_causation_rootExternal :

LevinClass.murder.causationSource = CausationSource.rootExternal

theorem Semantics.Lexical.eat_causation_rootNonDetachable :

LevinClass.eat.causationSource = CausationSource.rootNonDetachable

theorem Semantics.Lexical.devour_causation_rootNonDetachable :

LevinClass.devour.causationSource = CausationSource.rootNonDetachable

theorem Semantics.Lexical.put_causation_template :

LevinClass.put.causationSource = CausationSource.template

theorem Semantics.Lexical.send_causation_template :

LevinClass.send.causationSource = CausationSource.template

theorem Semantics.Lexical.grow_causation_template :

LevinClass.grow.causationSource = CausationSource.template

theorem Semantics.Lexical.hit_causation_none :

LevinClass.hit.causationSource = CausationSource.none

theorem Semantics.Lexical.mannerOfMotion_causation_none :

LevinClass.mannerOfMotion.causationSource = CausationSource.none

Result kind verification #

theorem Semantics.Lexical.break_result_stateChange :

LevinClass.break_.resultKind = ResultKind.stateChange

theorem Semantics.Lexical.destroy_result_stateChange :

LevinClass.destroy.resultKind = ResultKind.stateChange

theorem Semantics.Lexical.throw_result_locationChange :

LevinClass.throw.resultKind = ResultKind.locationChange

theorem Semantics.Lexical.inherentlyDirectedMotion_result_locationChange :

LevinClass.inherentlyDirectedMotion.resultKind = ResultKind.locationChange

theorem Semantics.Lexical.leave_result_locationChange :

LevinClass.leave.resultKind = ResultKind.locationChange

theorem Semantics.Lexical.give_result_possessionChange :

LevinClass.give.resultKind = ResultKind.possessionChange

theorem Semantics.Lexical.hit_result_none :

LevinClass.hit.resultKind = ResultKind.none

Manner kind verification #

theorem Semantics.Lexical.cooking_manner_mannerSpec :

LevinClass.cooking.mannerKind = MannerKind.mannerSpec

theorem Semantics.Lexical.mannerOfMotion_manner_mannerSpec :

LevinClass.mannerOfMotion.mannerKind = MannerKind.mannerSpec

theorem Semantics.Lexical.cut_manner_instrumentSpec :

LevinClass.cut.mannerKind = MannerKind.instrumentSpec

theorem Semantics.Lexical.poke_manner_instrumentSpec :

LevinClass.poke.mannerKind = MannerKind.instrumentSpec

theorem Semantics.Lexical.hit_manner_unspecified :

LevinClass.hit.mannerKind = MannerKind.unspecified

theorem Semantics.Lexical.pushPull_manner_unspecified :

LevinClass.pushPull.mannerKind = MannerKind.unspecified

theorem Semantics.Lexical.break_manner_none :

LevinClass.break_.mannerKind = MannerKind.none

Root-structural MC contribution #

def Semantics.Lexical.RootEntailments.structuralMC (re : Roots.RootEntailments) :

MeaningComponents

Root structural contribution to meaning components. Maps result → changeOfState and manner → mannerSpec.

Equations

Semantics.Lexical.RootEntailments.structuralMC re = { changeOfState := re.result, contact := false, motion := false, causation := false, mannerSpec := re.manner }

Instances For

Universal consistency theorems #

These hold for ALL 78 LevinClass constructors and are proved by exhaustive case analysis.

theorem Semantics.Lexical.levin_spec_implies_bkg_manner (c : LevinClass) :

c.meaningComponents.mannerSpec = true ∨ c.meaningComponents.instrumentSpec = true → c.rootEntailments.manner = true

Levin spec implies B&KG manner.

theorem Semantics.Lexical.causativeResult_always_cos (c : LevinClass) :

c.rootEntailments = Roots.RootEntailments.causativeResult → c.meaningComponents.changeOfState = true

CausativeResult roots always have changeOfState.

theorem Semantics.Lexical.root_cause_accounted_for (c : LevinClass) :

c.rootEntailments.cause = true → c.meaningComponents.causation = true ∨ c.causationSource = CausationSource.rootNonDetachable

Root cause implies either event causation or non-detachable causation.