Documentation

Linglib.Theories.Semantics.ArgumentStructure.DiathesisAlternation

Features.DiathesisAlternation #

@cite{levin-1993}

Twenty-five curated diathesis alternations from @cite{levin-1993} Part One, the prediction map from MeaningComponents, the per-class participation profile, and structural theorems characterising how alternation participation interacts with MeaningComponents.fuse.

Provenance #

Moved from Core/Lexical/DiathesisAlternation.lean in the cleanup that dissolved Core/Lexical/. Sibling of LevinClass.lean, MeaningComponents.lean, LevinTheory.lean, LevinClassProfiles.lean — all paper-anchored on @cite{levin-1993} and not theory-neutral substrate.

Selection caveat #

The 25 alternations chosen here are the formaliser's selection of "diagnostically active" alternations from Levin's ~79 in Part One. Levin's monograph lists many narrower alternations as data/prose; the selection here covers what's needed to discriminate the major verb classes per Levin's Introduction. This is NOT Levin's own claim about which alternations are diagnostically active — verify the curation against the empirical needs of any downstream consumer.

UNVERIFIED: Per-alternation section numbers (e.g., §1.1.2.1, §2.1, §7.4) cited from memory throughout. Verify against published @cite{levin-1993} before treating as authoritative.

Sections #

source
inductive Semantics.Lexical.AlternationFamily :
Type

Classification of diathesis alternations by the chapter of @cite{levin-1993} Part One where they are primarily discussed.

Organizational grouping for the curated 25-alternation enum; the remaining ~50 narrow alternations from Part One are documented as data/prose, not as enum constructors.

UNVERIFIED: Chapter assignments cited from memory.

  • transitivity : AlternationFamily

    Ch 1: Transitivity alternations — changes in the number of arguments (causative/inchoative, induced action, middle, conative, object drop).

  • vpInternal : AlternationFamily

    Ch 2: Alternations involving arguments within the VP — rearrangement of internal arguments (dative, benefactive, locative, swarm, etc.).

  • obliqueSubject : AlternationFamily

    Ch 3: Oblique subject alternations — non-agent subjects (instrument subject).

  • passive : AlternationFamily

    Ch 5: Passive — verbal and prepositional passives.

  • postverbalSubject : AlternationFamily

    Ch 6: Alternations involving postverbal subjects — there-insertion, locative inversion (unaccusative diagnostics).

  • otherConstructions : AlternationFamily

    Ch 7: Other constructions — way construction, cognate object, resultative, directional phrase.

Instances For
    source
    @[implicit_reducible]
    instance Semantics.Lexical.instDecidableEqAlternationFamily :
    DecidableEq AlternationFamily
    Equations
    source
    def Semantics.Lexical.instReprAlternationFamily.repr :
    AlternationFamily → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[implicit_reducible]
      instance Semantics.Lexical.instReprAlternationFamily :
      Repr AlternationFamily
      Equations
      source
      inductive Semantics.Lexical.DiathesisAlternation :
      Type

      Curated diathesis alternations from @cite{levin-1993} Part One.

      The first four (causativeInchoative / inducedAction / middle / conative) are the canonical diagnostics from the Introduction; others are from specific chapters. Each is classified by AlternationFamily.

      UNVERIFIED: Per-constructor section numbers cited from memory.

      • causativeInchoative : DiathesisAlternation

        she broke the vase / the vase broke. Diagnoses causation + CoS.

      • inducedAction : DiathesisAlternation

        Bill ran the horse. Causative use of intransitive manner-of-motion verbs.

      • middle : DiathesisAlternation

        the bread cuts easily. Diagnoses change of state.

      • conative : DiathesisAlternation

        I cut at the bread. Diagnoses contact + motion.

      • substanceSource : DiathesisAlternation

        heat radiates from the sun / the sun radiates heat. Substance emission verbs.

      • unspecifiedObject : DiathesisAlternation

        Mike ate the cake / Mike ate. Activity verbs (eat, read, cook, ...). The intransitive has an unexpressed but understood indefinite object.

      • understoodBodyPartObject : DiathesisAlternation

        Bill waved his hand / Bill waved. Body-part verbs where the object names the moved body part.

      • understoodReflexiveObject : DiathesisAlternation

        Bill washed himself / Bill washed. Grooming/body-care verbs where the reflexive object can be dropped.

      • understoodReciprocalObject : DiathesisAlternation

        Anne met Cathy / Anne and Cathy met. Social interaction verbs. Intransitive paraphrasable as transitive with each other.

      • dative : DiathesisAlternation

        give NP NP / give NP to NP. Give/send class.

      • benefactive : DiathesisAlternation

        Martha carved a toy for the baby / Martha carved the baby a toy. Verbs of obtaining and creation.

      • locative : DiathesisAlternation

        spray paint on wall / spray wall with paint. Spray/load class.

      • bodyPartPossessorAscension : DiathesisAlternation

        I hit him on the arm / I hit his arm. Diagnoses contact.

      • swarm : DiathesisAlternation

        Bees swarmed in the garden / The garden swarmed with bees. Intransitive locative alternation for verbs of spatial configuration.

      • materialProduct : DiathesisAlternation

        Martha carved a toy out of wood / Martha carved the wood into a toy. Build/creation verbs.

      • totalTransformation : DiathesisAlternation

        the witch turned the prince into a frog. Complete change of entity type. Turn/convert verbs.

      • instrumentSubject : DiathesisAlternation

        David broke the window with a hammer / the hammer broke the window. Intermediary instruments can become subjects with externally caused verbs.

      • verbalPassive : DiathesisAlternation

        the window was broken (by the boy). Fundamental voice alternation for transitive verbs.

      • prepositionalPassive : DiathesisAlternation

        the bed was slept in. Passive of intransitive + PP, diagnostic for unergative verbs.

      • thereInsertion : DiathesisAlternation

        a problem developed / there developed a problem. Unaccusative diagnostic: existence/appearance verbs.

      • locativeInversion : DiathesisAlternation

        an old woman lives in the woods / in the woods lives an old woman. Unaccusative diagnostic: existence/spatial configuration verbs.

      • cognateObject : DiathesisAlternation

        she laughed a bitter laugh. Unergative diagnostic: agentive intransitives can take cognate objects.

      • wayConstruction : DiathesisAlternation

        she elbowed her way through the crowd. Manner-of-motion and body-motion verbs.

      • resultative : DiathesisAlternation

        hammer the metal flat. Available to manner verbs.

      • directionalPhrase : DiathesisAlternation

        she ran to the store. Manner-of-motion verbs with directional PPs (Talmy's satellite-framing).

      Instances For
        source
        @[implicit_reducible]
        instance Semantics.Lexical.instDecidableEqDiathesisAlternation :
        DecidableEq DiathesisAlternation
        Equations
        source
        @[implicit_reducible]
        instance Semantics.Lexical.instReprDiathesisAlternation :
        Repr DiathesisAlternation
        Equations
        source
        def Semantics.Lexical.instReprDiathesisAlternation.repr :
        DiathesisAlternation → ℕ → Std.Format
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Semantics.Lexical.DiathesisAlternation.family :
          DiathesisAlternation → AlternationFamily

          Which family of @cite{levin-1993} Part One each alternation belongs to. Classifies the 25 curated alternations into 6 families matching the chapter structure of Part One.

          Equations
          Instances For
            source
            def Semantics.Lexical.MeaningComponents.predictedAlternation :
            MeaningComponents → DiathesisAlternation → Bool

            Predicted alternation participation derived from meaning components.

            The core claim of @cite{levin-1993}: meaning components — diagnosed by alternation participation — form the bridge between verb semantics and verb syntax. Each diagnostic alternation corresponds to a specific configuration of meaning components:

            AlternationRequired components
            Causative/inchoativechangeOfState ∧ causation ∧ ¬instrumentSpec
            MiddlechangeOfState
            Conativecontact ∧ motion
            Body-part possessor ascensioncontact
            Instrument subjectcausation ∧ ¬instrumentSpec
            ResultativechangeOfState ∧ ¬instrumentSpec (manner verbs)

            The remaining alternations are class-specific rather than component-derived.

            Equations
            Instances For

              These theorems characterize how MeaningComponents.fuse (componentwise OR) interacts with predictedAlternation. They are stated purely over MeaningComponents — no reference to specific constructions, verb classes, or empirical data. Construction grammar modules use these as lemmas.

              Note: fuse is componentwise OR; the substrate's design choice. NOT to be attributed to Goldberg 1995 specifically (Goldberg's actual constructional unification is more structured than disjunctive feature OR).

              source
              theorem Semantics.Lexical.fuse_cos_caus_enables (v c : MeaningComponents) (hCoS : c.changeOfState = true) (hCaus : c.causation = true) (hInstV : v.instrumentSpec = false) (hInstC : c.instrumentSpec = false) :
              have f := v.fuse c; f.predictedAlternation DiathesisAlternation.causativeInchoative = true ∧ f.predictedAlternation DiathesisAlternation.middle = true ∧ f.predictedAlternation DiathesisAlternation.instrumentSubject = true ∧ f.predictedAlternation DiathesisAlternation.resultative = true

              Enabling via CoS + causation: fusing any verb (without instrumentSpec) with any meaning components contributing CoS + causation (without instrumentSpec) enables all four instrument-sensitive alternations.

              source
              theorem Semantics.Lexical.fuse_cos_only_partial (v c : MeaningComponents) (hCoS : c.changeOfState = true) (hNoCaus : c.causation = false) (hNoCausV : v.causation = false) (hInstV : v.instrumentSpec = false) (hInstC : c.instrumentSpec = false) :
              have f := v.fuse c; f.predictedAlternation DiathesisAlternation.middle = true ∧ f.predictedAlternation DiathesisAlternation.resultative = true ∧ f.predictedAlternation DiathesisAlternation.causativeInchoative = false ∧ f.predictedAlternation DiathesisAlternation.instrumentSubject = false

              Partial enabling via CoS only: fusing a verb (without instrumentSpec or causation) with meaning components contributing CoS but NOT causation enables middle and resultative alternation, but NOT causativeInchoative or instrumentSubject.

              source
              theorem Semantics.Lexical.instrumentSpec_blocks (mc : MeaningComponents) (h : mc.instrumentSpec = true) :
              mc.predictedAlternation DiathesisAlternation.causativeInchoative = false ∧ mc.predictedAlternation DiathesisAlternation.instrumentSubject = false ∧ mc.predictedAlternation DiathesisAlternation.resultative = false

              instrumentSpec blocks unconditionally: any meaning components with instrumentSpec = true are blocked from causativeInchoative, instrumentSubject, and resultative.

              source
              theorem Semantics.Lexical.instrumentSpec_blocks_after_fuse (v c : MeaningComponents) (h : v.instrumentSpec = true) :
              (v.fuse c).predictedAlternation DiathesisAlternation.causativeInchoative = false ∧ (v.fuse c).predictedAlternation DiathesisAlternation.instrumentSubject = false ∧ (v.fuse c).predictedAlternation DiathesisAlternation.resultative = false

              Corollary: instrumentSpec blocks after ANY fusion, since v.instrumentSpec = true → (v.fuse c).instrumentSpec = true.

              source
              theorem Semantics.Lexical.fuse_alternation_monotone (v c : MeaningComponents) (alt : DiathesisAlternation) (h_no_inst : c.instrumentSpec = false) (h_bare : v.predictedAlternation alt = true) :
              (v.fuse c).predictedAlternation alt = true

              Monotonicity: an instrument-free fusion never removes an alternation.

              source
              theorem Semantics.Lexical.instrumentSpec_persists (v c : MeaningComponents) (h : v.instrumentSpec = true) :
              (v.fuse c).instrumentSpec = true

              instrumentSpec persists through fusion: once a verb has instrument specificity, no fusion can remove it (true || b = true).

              source
              theorem Semantics.Lexical.fuse_not_generally_monotone :
              ∃ (v : MeaningComponents) (c : MeaningComponents) (alt : DiathesisAlternation), v.predictedAlternation alt = true ∧ (v.fuse c).predictedAlternation alt = false

              Fusion is NOT generally monotone: when instrumentSpec is added, it CAN block an alternation the verb had alone.

              source
              theorem Semantics.Lexical.fuse_blocks_only_via_instrumentSpec (v c : MeaningComponents) (alt : DiathesisAlternation) (h_bare : v.predictedAlternation alt = true) (h_fused : (v.fuse c).predictedAlternation alt = false) :
              (v.fuse c).instrumentSpec = true

              instrumentSpec is the sole blocker: if a verb participates alone but NOT after fusion, instrumentSpec must have been introduced.

              source
              def Semantics.Lexical.LevinClass.participatesIn (c : LevinClass) (alt : DiathesisAlternation) :
              Bool

              Full alternation profile for a Levin class, combining component-derived predictions with class-specific overrides.

              Component-derived: causativeInchoative, middle, conative, bodyPartPossessorAscension, instrumentSubject, resultative.

              Class-specific overrides below; these are the formaliser's reading of @cite{levin-1993} Part I verb lists and Part II class descriptions. UNVERIFIED: Per-class participation rows cited from memory; verify against the published monograph.

              Instances For

                The four verbs break, cut, hit, touch are distinguished by exactly their pattern of alternation participation (per @cite{levin-1993} Introduction).

                source
                theorem Semantics.Lexical.break_alternations :
                LevinClass.break_.participatesIn DiathesisAlternation.causativeInchoative = true ∧ LevinClass.break_.participatesIn DiathesisAlternation.middle = true ∧ LevinClass.break_.participatesIn DiathesisAlternation.conative = false ∧ LevinClass.break_.participatesIn DiathesisAlternation.bodyPartPossessorAscension = false

                Break participates in causative/inchoative and middle (CoS + causation).

                source
                theorem Semantics.Lexical.cut_alternations :
                LevinClass.cut.participatesIn DiathesisAlternation.causativeInchoative = false ∧ LevinClass.cut.participatesIn DiathesisAlternation.middle = true ∧ LevinClass.cut.participatesIn DiathesisAlternation.conative = true ∧ LevinClass.cut.participatesIn DiathesisAlternation.bodyPartPossessorAscension = true

                Cut participates in middle, conative, and BPPA but NOT causative/inchoative. Instrument specification blocks the inchoative ("*The string cut"). Because cut inherently specifies an instrument, it requires an agent.

                source
                theorem Semantics.Lexical.hit_alternations :
                LevinClass.hit.participatesIn DiathesisAlternation.causativeInchoative = false ∧ LevinClass.hit.participatesIn DiathesisAlternation.middle = false ∧ LevinClass.hit.participatesIn DiathesisAlternation.conative = true ∧ LevinClass.hit.participatesIn DiathesisAlternation.bodyPartPossessorAscension = true

                Hit participates in conative and body-part ascension (contact + motion, no CoS).

                source
                theorem Semantics.Lexical.touch_alternations :
                LevinClass.touch.participatesIn DiathesisAlternation.causativeInchoative = false ∧ LevinClass.touch.participatesIn DiathesisAlternation.middle = false ∧ LevinClass.touch.participatesIn DiathesisAlternation.conative = false ∧ LevinClass.touch.participatesIn DiathesisAlternation.bodyPartPossessorAscension = true

                Touch participates only in body-part ascension (contact only).

                source
                theorem Semantics.Lexical.MeaningComponents.instrumentSpec_blocks_ci (mc : MeaningComponents) (h : mc.instrumentSpec = true) :
                mc.predictedAlternation DiathesisAlternation.causativeInchoative = false

                Instrument specification blocks the causative/inchoative alternation.

                source
                theorem Semantics.Lexical.MeaningComponents.instrumentSpec_blocks_resultative (mc : MeaningComponents) (h : mc.instrumentSpec = true) :
                mc.predictedAlternation DiathesisAlternation.resultative = false

                Corollary: instrument specification also blocks the resultative.

                Cross-class predictions #

                source
                theorem Semantics.Lexical.cos_classes_causative :
                LevinClass.break_.participatesIn DiathesisAlternation.causativeInchoative = true ∧ LevinClass.bend.participatesIn DiathesisAlternation.causativeInchoative = true ∧ LevinClass.cooking.participatesIn DiathesisAlternation.causativeInchoative = true ∧ LevinClass.otherCoS.participatesIn DiathesisAlternation.causativeInchoative = true

                All CoS classes participate in the causative/inchoative alternation.

                source
                theorem Semantics.Lexical.sprayLoad_locative :
                LevinClass.sprayLoad.participatesIn DiathesisAlternation.locative = true

                Spray/load participates in the locative alternation.

                source
                theorem Semantics.Lexical.give_dative :
                LevinClass.give.participatesIn DiathesisAlternation.dative = true

                Give class participates in the dative alternation.

                source
                theorem Semantics.Lexical.motion_no_causative :
                LevinClass.mannerOfMotion.participatesIn DiathesisAlternation.causativeInchoative = false ∧ LevinClass.inherentlyDirectedMotion.participatesIn DiathesisAlternation.causativeInchoative = false

                Motion verbs don't participate in causative alternation (no causation component).

                source
                theorem Semantics.Lexical.contact_motion_conative :
                LevinClass.hit.participatesIn DiathesisAlternation.conative = true ∧ LevinClass.swat.participatesIn DiathesisAlternation.conative = true ∧ LevinClass.poke.participatesIn DiathesisAlternation.conative = true ∧ LevinClass.cut.participatesIn DiathesisAlternation.conative = true

                Contact verbs predict conative alternation participation.

                source
                theorem Semantics.Lexical.touch_no_conative :
                LevinClass.touch.participatesIn DiathesisAlternation.conative = false

                Touch verbs lack motion → no conative despite having contact.

                source
                theorem Semantics.Lexical.cut_no_resultative_break_resultative :
                LevinClass.cut.participatesIn DiathesisAlternation.resultative = false ∧ LevinClass.break_.participatesIn DiathesisAlternation.resultative = true

                Cut blocked from resultative; break participates (no instrumentSpec).

                source
                theorem Semantics.Lexical.causativeInchoative_implies_unaccusative :
                LevinClass.break_.participatesIn DiathesisAlternation.causativeInchoative = true ∧ LevinClass.break_.PredictsUnaccusative ∧ LevinClass.otherCoS.participatesIn DiathesisAlternation.causativeInchoative = true ∧ LevinClass.otherCoS.PredictsUnaccusative

                The causative/inchoative alternation implies the existence of an unaccusative variant.

                Family classification theorems #

                source
                theorem Semantics.Lexical.canonical_diagnostics_families :
                DiathesisAlternation.causativeInchoative.family = AlternationFamily.transitivity ∧ DiathesisAlternation.middle.family = AlternationFamily.transitivity ∧ DiathesisAlternation.conative.family = AlternationFamily.transitivity ∧ DiathesisAlternation.bodyPartPossessorAscension.family = AlternationFamily.vpInternal

                The canonical diagnostics all belong to the transitivity or VP-internal families.

                source
                theorem Semantics.Lexical.passive_family :
                DiathesisAlternation.verbalPassive.family = AlternationFamily.passive ∧ DiathesisAlternation.prepositionalPassive.family = AlternationFamily.passive

                Passive alternations form their own family.

                Class-specific alternation predictions #

                source
                theorem Semantics.Lexical.build_benefactive_materialProduct :
                LevinClass.build.participatesIn DiathesisAlternation.benefactive = true ∧ LevinClass.build.participatesIn DiathesisAlternation.materialProduct = true

                Build verbs participate in both benefactive and material/product alternations.

                source
                theorem Semantics.Lexical.substanceEmission_substanceSource :
                LevinClass.substanceEmission.participatesIn DiathesisAlternation.substanceSource = true

                Substance emission verbs participate in the substance/source alternation.

                source
                theorem Semantics.Lexical.eat_unspecifiedObject_devour_blocked :
                LevinClass.eat.participatesIn DiathesisAlternation.unspecifiedObject = true ∧ LevinClass.devour.participatesIn DiathesisAlternation.unspecifiedObject = false

                Eat verbs participate in the unspecified object alternation. Devour verbs do NOT — they require an expressed object.

                source
                theorem Semantics.Lexical.socialInteraction_reciprocal :
                LevinClass.socialInteraction.participatesIn DiathesisAlternation.understoodReciprocalObject = true

                Social interaction verbs show the understood reciprocal object alternation.

                source
                theorem Semantics.Lexical.existence_thereInsertion :
                LevinClass.exist.participatesIn DiathesisAlternation.thereInsertion = true ∧ LevinClass.appear.participatesIn DiathesisAlternation.thereInsertion = true

                Existence and appearance verbs participate in there-insertion.

                source
                theorem Semantics.Lexical.existence_locativeInversion :
                LevinClass.exist.participatesIn DiathesisAlternation.locativeInversion = true ∧ LevinClass.mannerOfMotion.participatesIn DiathesisAlternation.locativeInversion = true

                Existence and manner-of-motion verbs participate in locative inversion.

                source
                theorem Semantics.Lexical.unaccusative_diagnostics_align :
                LevinClass.exist.PredictsUnaccusative ∧ LevinClass.exist.participatesIn DiathesisAlternation.thereInsertion = true ∧ LevinClass.exist.participatesIn DiathesisAlternation.locativeInversion = true ∧ LevinClass.appear.PredictsUnaccusative ∧ LevinClass.appear.participatesIn DiathesisAlternation.thereInsertion = true ∧ LevinClass.appear.participatesIn DiathesisAlternation.locativeInversion = true

                There-insertion and locative inversion align with unaccusativity.

                source
                theorem Semantics.Lexical.break_instrumentSubject_cut_blocked :
                LevinClass.break_.participatesIn DiathesisAlternation.instrumentSubject = true ∧ LevinClass.cut.participatesIn DiathesisAlternation.instrumentSubject = false

                Instrument subject alternation is predicted by external causation.

                source
                theorem Semantics.Lexical.instrumentSpec_blocks_ci_and_instrumentSubject (mc : MeaningComponents) (h : mc.instrumentSpec = true) :
                mc.predictedAlternation DiathesisAlternation.causativeInchoative = false ∧ mc.predictedAlternation DiathesisAlternation.instrumentSubject = false

                Instrument specification blocks both causative/inchoative and instrument subject alternations.

                Per-alternation predictions #

                source
                theorem Semantics.Lexical.mannerOfMotion_inducedAction :
                LevinClass.mannerOfMotion.participatesIn DiathesisAlternation.inducedAction = true

                Manner-of-motion verbs participate in the induced action alternation.

                source
                theorem Semantics.Lexical.dress_understoodReflexive :
                LevinClass.dress.participatesIn DiathesisAlternation.understoodReflexiveObject = true

                Grooming verbs participate in the understood reflexive object alternation.

                source
                theorem Semantics.Lexical.bodyProcess_understoodBodyPart :
                LevinClass.bodyProcess.participatesIn DiathesisAlternation.understoodBodyPartObject = true

                Body process verbs participate in the understood body-part object alternation.

                source
                theorem Semantics.Lexical.turn_totalTransformation :
                LevinClass.turn.participatesIn DiathesisAlternation.totalTransformation = true

                Turn/convert verbs participate in the total transformation alternation.

                source
                theorem Semantics.Lexical.mannerOfMotion_wayConstruction :
                LevinClass.mannerOfMotion.participatesIn DiathesisAlternation.wayConstruction = true

                Manner-of-motion verbs participate in the way construction.

                source
                theorem Semantics.Lexical.mannerOfMotion_directionalPhrase :
                LevinClass.mannerOfMotion.participatesIn DiathesisAlternation.directionalPhrase = true

                Manner-of-motion verbs participate in the directional phrase alternation.

                source
                theorem Semantics.Lexical.unergative_diagnostics :
                LevinClass.mannerOfMotion.participatesIn DiathesisAlternation.cognateObject = true ∧ LevinClass.mannerOfMotion.participatesIn DiathesisAlternation.prepositionalPassive = true

                Unergative diagnostics: manner-of-motion verbs participate in cognate object and prepositional passive.

                source
                theorem Semantics.Lexical.mannerOfMotion_breadth :
                LevinClass.mannerOfMotion.participatesIn DiathesisAlternation.inducedAction = true ∧ LevinClass.mannerOfMotion.participatesIn DiathesisAlternation.wayConstruction = true ∧ LevinClass.mannerOfMotion.participatesIn DiathesisAlternation.directionalPhrase = true ∧ LevinClass.mannerOfMotion.participatesIn DiathesisAlternation.cognateObject = true ∧ LevinClass.mannerOfMotion.participatesIn DiathesisAlternation.prepositionalPassive = true ∧ LevinClass.mannerOfMotion.participatesIn DiathesisAlternation.locativeInversion = true

                Manner-of-motion verbs are diagnostic workhorses: 6 alternations from 4 different families.

                Verbal passive coverage #

                source
                theorem Semantics.Lexical.verbalPassive_coverage :
                LevinClass.break_.participatesIn DiathesisAlternation.verbalPassive = true ∧ LevinClass.hit.participatesIn DiathesisAlternation.verbalPassive = true ∧ LevinClass.put.participatesIn DiathesisAlternation.verbalPassive = true ∧ LevinClass.give.participatesIn DiathesisAlternation.verbalPassive = true ∧ LevinClass.build.participatesIn DiathesisAlternation.verbalPassive = true ∧ LevinClass.murder.participatesIn DiathesisAlternation.verbalPassive = true ∧ LevinClass.see.participatesIn DiathesisAlternation.verbalPassive = true ∧ LevinClass.amuse.participatesIn DiathesisAlternation.verbalPassive = true

                Verbal passive is available across all major transitive class families.

                source
                theorem Semantics.Lexical.measure_no_verbalPassive :
                LevinClass.measure.participatesIn DiathesisAlternation.verbalPassive = false

                Measure verbs do NOT participate in verbal passive.

                source
                theorem Semantics.Lexical.weather_no_verbalPassive :
                LevinClass.weather.participatesIn DiathesisAlternation.verbalPassive = false

                Weather verbs do NOT participate in verbal passive (no object to promote).

                Prepositional passive and swarm coverage #

                source
                theorem Semantics.Lexical.prepositionalPassive_unergatives :
                LevinClass.mannerOfMotion.participatesIn DiathesisAlternation.prepositionalPassive = true ∧ LevinClass.bodyProcess.participatesIn DiathesisAlternation.prepositionalPassive = true ∧ LevinClass.mannerOfSpeaking.participatesIn DiathesisAlternation.prepositionalPassive = true ∧ LevinClass.assumePosition.participatesIn DiathesisAlternation.prepositionalPassive = true

                Prepositional passive aligns with unergativity.

                source
                theorem Semantics.Lexical.swarm_classes :
                LevinClass.exist.participatesIn DiathesisAlternation.swarm = true ∧ LevinClass.mannerOfMotion.participatesIn DiathesisAlternation.swarm = true ∧ LevinClass.bodyInternalMotion.participatesIn DiathesisAlternation.swarm = true

                The swarm alternation applies to existence and manner-of-motion verbs.