Documentation

Linglib.Semantics.ArgumentStructure.LevinTheory

Levin Verb Class Theory #

[Lev93] [Dow91] [BKG20]

The LevinClass enum and its classification data (meaningComponents, predictsUnaccusative, isVerbOfCreation) live in Semantics/ArgumentStructure/LevinClass.lean; MeaningComponents in Semantics/ArgumentStructure/MeaningComponents.lean.

This file provides the theoretical content that depends on Root.Kinds: the root signature label, the root–MC comparison enums, and the universal consistency/divergence theorems that ground them. LevinClass is a lossy realization label, not a source of truth (that is Verb.Root.kinds); the theorems below are the non-decorative grounding — each holds for every class and breaks if a table row changes, so per-class rfl spot-checks are not restated.

§ 1. Root entailment label ([BKG20]) #

The rootEntailments signature label and its universal soundness theorem.

§ 2. Root–MC comparison #

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

def ArgumentStructure.LevinClass.rootEntailments :

LevinClass → Verb.Root.Kinds

Root kind signature for each Levin class.

Assignments marked (B&KG) are directly from [BKG20] 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

Table soundness (universal) #

rootEntailments is a lossy realization label, not a source of truth. It earns its place via a theorem that holds for every class and breaks if a row is changed: every assigned signature is well-formed (collocationally closed). Invert any row to an unclosed signature and this fails — the grounding is not decorative. Manner/result complementarity of these signatures is covered by the canonical kinds-layer theory (Roots/Closure.lean, closed_violatesBifurcation_iff), which quantifies over all Root.Kinds, so no per-class MRC spot-check is restated here.

theorem ArgumentStructure.rootEntailments_wellFormed (c : LevinClass) :

c.rootEntailments.WellFormed

Every Levin class is assigned a well-formed (closed) root signature.

Root–MC comparison #

[Lev93]'s meaning components and [BKG20]'s root entailments are two independently-motivated lexical decompositions; they 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

Because B&KG result/manner are coarser than the Levin features, neither table is a function of the other (give carries result but changeOfState = false; hit carries manner but mannerSpec = false), so the two are related by the consistency/divergence theorems below, not by a derivation — a morphism meaningComponents = f rootEntailments is not just absent from the literature but mathematically impossible here, and the manner/result-complementarity dispute ([BKG20] vs the Rappaport Hovav & Levin tradition) is exactly over this independence. The three *Kind enums name the specific divergences, making them grep-able and testable.

inductive ArgumentStructure.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 ([BKG20] Ch. 5; [Lev93] pp. 9–10).

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

Instances For

@[implicit_reducible]

instance ArgumentStructure.instDecidableEqCausationSource :

DecidableEq CausationSource

Equations

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

def ArgumentStructure.instReprCausationSource.repr :

CausationSource → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance ArgumentStructure.instReprCausationSource :

Repr CausationSource

Equations

ArgumentStructure.instReprCausationSource = { reprPrec := ArgumentStructure.instReprCausationSource.repr }

def ArgumentStructure.LevinClass.causationSource (c : LevinClass) :

CausationSource

Derive the causation source from the root signature and meaning components.

Equations

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

Instances For

inductive ArgumentStructure.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) carry result in B&KG but changeOfState = false in Levin.

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

Instances For

@[implicit_reducible]

instance ArgumentStructure.instDecidableEqResultKind :

DecidableEq ResultKind

Equations

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

@[implicit_reducible]

instance ArgumentStructure.instReprResultKind :

Repr ResultKind

Equations

ArgumentStructure.instReprResultKind = { reprPrec := ArgumentStructure.instReprResultKind.repr }

def ArgumentStructure.instReprResultKind.repr :

ResultKind → ℕ → Std.Format

Equations

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

Instances For

def ArgumentStructure.LevinClass.resultKind (c : LevinClass) :

Derive result kind from the root signature and meaning components.

Equations

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

Instances For

inductive ArgumentStructure.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 ArgumentStructure.instDecidableEqMannerKind :

DecidableEq MannerKind

Equations

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

@[implicit_reducible]

instance ArgumentStructure.instReprMannerKind :

Repr MannerKind

Equations

ArgumentStructure.instReprMannerKind = { reprPrec := ArgumentStructure.instReprMannerKind.repr }

def ArgumentStructure.instReprMannerKind.repr :

MannerKind → ℕ → Std.Format

Equations

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

Instances For

def ArgumentStructure.LevinClass.mannerKind (c : LevinClass) :

Derive manner kind from the root signature and meaning components.

Equations

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

Instances For

The causationSource/resultKind/mannerKind classifiers are grounded not by per-class rfl confirmations (which merely restate a row of the def and break in lockstep when the row changes) but by the universal consistency theorems below, which relate them to the root signature and the event template and break under a genuine table change.

Root-structural MC contribution #

def Verb.Root.Kinds.structuralMC (re : Kinds) :

ArgumentStructure.MeaningComponents

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

Equations

re.structuralMC = { changeOfState := decide (Verb.LexKind.result ∈ re), contact := false, motion := false, causation := false, mannerSpec := decide (Verb.LexKind.manner ∈ re) }

Instances For

Universal consistency theorems #

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

theorem ArgumentStructure.levin_spec_implies_bkg_manner (c : LevinClass) :

c.meaningComponents.mannerSpec = true ∨ c.meaningComponents.instrumentSpec = true → Verb.LexKind.manner ∈ c.rootEntailments

Levin spec implies B&KG manner.

theorem ArgumentStructure.causativeResult_always_cos (c : LevinClass) :

c.rootEntailments = Verb.Root.Kinds.causativeResult → c.meaningComponents.changeOfState = true

CausativeResult roots always have changeOfState.

theorem ArgumentStructure.root_cause_accounted_for (c : LevinClass) :

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

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

theorem ArgumentStructure.resultKind_stateChange_imp_template_resultState (c : LevinClass) :

c.resultKind = ResultKind.stateChange → c.eventTemplate.HasResultState

.stateChange resultKind implies RoleList-level result-state.

theorem ArgumentStructure.template_resultState_not_iff_resultKind_stateChange :

∃ (c : LevinClass), c.eventTemplate.HasResultState ∧ c.resultKind ≠ ResultKind.stateChange

The converse fails: aspectual verbs have HasResultState (via the achievement template) but resultKind ≠ .stateChange.

theorem ArgumentStructure.structuralMC_diverges_from_meaningComponents :

∃ (c : LevinClass), c.rootEntailments.structuralMC.changeOfState = true ∧ c.meaningComponents.changeOfState = false

The naive structural prediction structuralMC ∘ rootEntailments is not a refinement of the hand-specified meaningComponents: a class can carry result in its root signature (so structuralMC predicts changeOfState) yet have Levin changeOfState = false — change of possession/location carries result in B&KG but is not a change of state for Levin. This divergence witness is why the bridge enums (ResultKind et al.) exist and meaningComponents is not just structuralMC ∘ rootEntailments.

Root kind signatures determine argument templates — the derivational direction in the argument-realization tradition ([BKG20] roots, [RHL98] event-template linking). The chain runs:

Root.Kinds → RoleList → RoleList → ThetaRole labels

toRoleList formalizes the default derivation. It captures the majority pattern: causative roots produce agent subjects and affected objects; manner-only roots produce agent subjects without causation; result-only roots produce unaccusative subjects; state-only roots produce experiencer subjects.

Two classes of systematic overrides exist:

Psych-causal verbs (amuse): causativeResult roots where the subject is a non-volitional stimulus, not a volitional agent. Override: psychCausal template.
Creation verbs (build): causativeResult roots where the object has dependent existence and incremental theme structure. Override: creation template.

These overrides are documented and verified below.

def ArgumentStructure.toRoleList (re : Verb.Root.Kinds) :

Option RoleList

Derive a default RoleList from a root kind signature.

The derivation follows B&KG's event structure decomposition:

cause: subject is external causer → full agent (V+S+C+M+IE), object undergoes change → CoS+CA
result without cause: internally caused change → unaccusative, sole argument is patient (CoS+CA)
manner without cause/result: activity → agent without causation (V+S+M+IE), no affected object
state only: stative → experiencer subject (S+IE)
no entailments: no default derivation

For cause+manner (fullSpec) vs cause without manner (causativeResult): both produce the same default RoleList. The manner flag restricts HOW the cause proceeds (cutting vs. breaking), not WHETHER there's an agent.

Equations

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

Instances For

For each LevinClass with both rootEntailments and roleList defined, we verify that the derived RoleList either MATCHES the hand-specified one or is a documented override.

theorem ArgumentStructure.roleList_diverges_from_derivation :

∃ (c : LevinClass), c.roleList ≠ toRoleList c.rootEntailments

roleList is not merely toRoleList ∘ rootEntailments: it diverges for the documented overrides (creation, psych-causal). Build witnesses this — its causativeResult root derives resultChange, but the class template is creation (incremental-theme object). A table that always matched the derivation would be redundant with it; this divergence is why roleList exists as a separate label, and §8b documents the overrides.

theorem ArgumentStructure.build_override_creation :

toRoleList LevinClass.build.rootEntailments = some resultChange ∧ LevinClass.build.roleList = some creation

Build-class: causativeResult derives resultChange, but build verbs have a CREATION object (CoS+IT+CA+DE) — the object comes into existence. Dependent existence and incremental theme are additional entailments not captured by root structural features.

theorem ArgumentStructure.amuse_override_psychCausal :

toRoleList LevinClass.amuse.rootEntailments = some resultChange ∧ LevinClass.amuse.roleList = some psychCausal

Amuse-class: causativeResult derives resultChange (agent subject), but psych-causal verbs have a STIMULUS subject (C+IE, no volition) and EXPERIENCER object (S+IE). The nature of causation (volitional vs. stimulus) isn't encoded in root entailments.

theorem ArgumentStructure.eat_has_class_template :

LevinClass.eat.roleList = some consumption

Eat/devour: default from rootEntailments is not defined (minimal), but class-level roleList specifies consumption.

theorem ArgumentStructure.class_templates_override_derivation :

(toRoleList LevinClass.wipe.rootEntailments = some selfMotion ∧ LevinClass.wipe.roleList = some wipeManner) ∧ (toRoleList LevinClass.admire.rootEntailments = some perception ∧ LevinClass.admire.roleList = some psychState) ∧ (toRoleList LevinClass.want.rootEntailments = some perception ∧ LevinClass.want.roleList = some desire) ∧ (toRoleList LevinClass.disappearance.rootEntailments = some unaccusativeCoS ∧ LevinClass.disappearance.roleList = some disappearance) ∧ toRoleList LevinClass.getObtain.rootEntailments = none ∧ LevinClass.getObtain.roleList = some possessionTransfer

The remaining documented overrides, in one place. Root kind signatures are too coarse for these classes: manner roots don't distinguish the wipe class's underspecified-volition subject from full-agent self-motion; state roots don't distinguish sentience-entailed psych states (admire) from bare desire states (want); and result roots don't see the disappearance class's dependent existence.

theorem ArgumentStructure.build_subject_agrees :

resultChange.subjectProfile = creation.subjectProfile

Build-class subject matches the derivation's subject (both are full agent V+S+C+M+IE). The override affects only the object, not the subject.

theorem ArgumentStructure.derived_subjects_wellformed :

((toRoleList Verb.Root.Kinds.causativeResult).elim False fun (x : RoleList) => WellFormedInternal x.subjectProfile) ∧ ((toRoleList Verb.Root.Kinds.pureManner).elim False fun (x : RoleList) => WellFormedInternal x.subjectProfile) ∧ ((toRoleList Verb.Root.Kinds.pureResult).elim False fun (x : RoleList) => WellFormedInternal x.subjectProfile) ∧ (toRoleList Verb.Root.Kinds.propertyConcept).elim False fun (x : RoleList) => WellFormedInternal x.subjectProfile

All canonical root signatures derive well-formed internal constraints (volition → sentience holds for derived subject profiles). The Option.elim False form simultaneously checks that toRoleList succeeds on each input and that the resulting template's subject profile is well-formed.