Documentation

Linglib.Semantics.Lexical.LevinTheory

Levin Verb Class Theory #

[Lev93] [Dow91] [BKG20]

The LevinClass enum and its classification data (meaningComponents, predictsUnaccusative, isVerbOfCreation) live in Semantics/Lexical/LevinClass.lean; MeaningComponents in Semantics/Lexical/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.

source
def Semantics.Lexical.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.

    source
    theorem Semantics.Lexical.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 conceptLevin conceptRelationship
    resultchangeOfStateB&KG broader: includes location/possession change
    mannermannerSpec ∨ instrumentSpecB&KG broader: includes contact-manner (hit)
    causecausationDistinct: 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.

    source
    inductive Semantics.Lexical.CausationSource :
    Type

    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).

    Instances For
      source
      @[implicit_reducible]
      instance Semantics.Lexical.instDecidableEqCausationSource :
      DecidableEq CausationSource
      Equations
      source
      def Semantics.Lexical.instReprCausationSource.repr :
      CausationSource → ℕ → Std.Format
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[implicit_reducible]
        instance Semantics.Lexical.instReprCausationSource :
        Repr CausationSource
        Equations
        source
        def Semantics.Lexical.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
          source
          inductive Semantics.Lexical.ResultKind :
          Type

          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.

          Instances For
            source
            @[implicit_reducible]
            instance Semantics.Lexical.instDecidableEqResultKind :
            DecidableEq ResultKind
            Equations
            source
            def Semantics.Lexical.instReprResultKind.repr :
            ResultKind → ℕ → Std.Format
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[implicit_reducible]
              instance Semantics.Lexical.instReprResultKind :
              Repr ResultKind
              Equations
              source
              def Semantics.Lexical.LevinClass.resultKind (c : LevinClass) :
              ResultKind

              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
                source
                inductive Semantics.Lexical.MannerKind :
                Type

                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)
                Instances For
                  source
                  @[implicit_reducible]
                  instance Semantics.Lexical.instDecidableEqMannerKind :
                  DecidableEq MannerKind
                  Equations
                  source
                  def Semantics.Lexical.instReprMannerKind.repr :
                  MannerKind → ℕ → Std.Format
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    @[implicit_reducible]
                    instance Semantics.Lexical.instReprMannerKind :
                    Repr MannerKind
                    Equations
                    source
                    def Semantics.Lexical.LevinClass.mannerKind (c : LevinClass) :
                    MannerKind

                    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 #

                      source
                      def Verb.Root.Kinds.structuralMC (re : Kinds) :
                      Semantics.Lexical.MeaningComponents

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

                      Equations
                      Instances For

                        Universal consistency theorems #

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

                        source
                        theorem Semantics.Lexical.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.

                        source
                        theorem Semantics.Lexical.causativeResult_always_cos (c : LevinClass) :
                        c.rootEntailments = Verb.Root.Kinds.causativeResult → c.meaningComponents.changeOfState = true

                        CausativeResult roots always have changeOfState.

                        source
                        theorem Semantics.Lexical.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.

                        source
                        theorem Semantics.Lexical.resultKind_stateChange_imp_template_resultState (c : LevinClass) :
                        c.resultKind = ResultKind.stateChange → c.eventTemplate.HasResultState

                        .stateChange resultKind implies Template-level result-state.

                        source
                        theorem Semantics.Lexical.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.

                        source
                        theorem Semantics.Lexical.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.