Levin (2026): The door pushed open

This file formalizes Levin's analysis of the English intransitive resultative with transitive-only verbs, The door pushed open, The cork pulled free, The valve slammed shut. Outside the resultative these verbs have no intransitive use whose subject is their object, The door pushed. Levin takes the intransitive resultative to be the anticausative variant of the causative alternation and its transitive counterpart the causative variant. The resultative describes a change of state that the verb alone does not, which is what makes the alternation available, and the conditions on the anticausative variant decide when the cause may go unexpressed.

The verbs are verbs of exerting force and verbs of surface contact, manner verbs that do not lexicalize a change (VerbKind). The result adjectives are open, closed, shut, free, loose and flat in the sense that describes a spatial configuration with respect to a reference entity, and not in their other senses, free of shards. The subject must be able to move without the continuous involvement of a cause, as an animate, a machine or a projectile can (Theme.SelfEnergetic), since a change of state properly contained in the causing act requires the cause to be expressed, the Proper Containment Condition of Rappaport Hovav and Levin (CauseRequired). Neither the verb nor the adjective suffices alone, and a sentence of the paper is acceptable exactly when the three conditions meet or the verb alternates by itself (acceptable_iff_licensed). Neo-constructional approaches, on which a verb's lexical properties do not constrain its distribution, expect every verb in every resultative pattern, and must explain why such intransitive resultatives are not more pervasive: The tub scrubbed clean is unacceptable (footnote 7, (16); exists_unacceptable_intransitive_resultative).

Implementation notes

The verb classes are the paper's own lists, not the classes of Levin's 1993 book, from which they differ, fling being there a verb of throwing, as the paper notes (exertingForce_not_all_pushPull). The discourse conditions on the anticausative variant, a cause recoverable from the context or of unknown identity, are conditions of use that no judgment of the paper isolates, and are not modelled; nor are the two intransitive resultatives with other adjectives that the paper offers as possible one-off instances. The kind of the subject is recorded for the rows whose subject the paper discusses.

References

• [Lev26]
• [RHL12]
• [RH14]
• [Lev93]

The proper containment condition

def Levin2026.CauseRequired {T : Type u_1} [LinearOrder T] (act change : NonemptyInterval T) : Prop

The cause must be expressed when the change of state is properly contained within the causing act.

Equations

• Levin2026.CauseRequired act change = (change < act)

theorem Levin2026.not_causeRequired_of_outlasts {T : Type u_1} [LinearOrder T] {act change : NonemptyInterval T} (h : act.toProd.2 < change.toProd.2) : ¬CauseRequired act change

A change that outlasts the causing act, as the swing of a door outlasts the push, is not contained in it, so the cause may go unexpressed.

Verbs, adjectives and subjects

inductive Levin2026.VerbKind : Type

The verbs of the paper's examples are the verbs of exerting force, the two subtypes of verbs of surface contact, the verbs of change of state, which show the causative alternation by themselves, and the other verbs, which are outside the paper's lists.

• exertingForce : VerbKind
• hitting : VerbKind
• wiping : VerbKind
• changeOfState : VerbKind
• other : VerbKind

@[instance_reducible]

instance Levin2026.instDecidableEqVerbKind : DecidableEq VerbKind

Equations

• Levin2026.instDecidableEqVerbKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Levin2026.instReprVerbKind.repr : VerbKind → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Levin2026.instReprVerbKind.repr Levin2026.VerbKind.hitting prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Levin2026.VerbKind.hitting")).group prec✝
• Levin2026.instReprVerbKind.repr Levin2026.VerbKind.wiping prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Levin2026.VerbKind.wiping")).group prec✝
• Levin2026.instReprVerbKind.repr Levin2026.VerbKind.other prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Levin2026.VerbKind.other")).group prec✝

@[instance_reducible]

instance Levin2026.instReprVerbKind : Repr VerbKind

Equations

• Levin2026.instReprVerbKind = { reprPrec := Levin2026.instReprVerbKind.repr }

def Levin2026.VerbKind.AppliesForce (k : VerbKind) : Prop

A verb of exerting force or of surface contact describes the application of a force to an entity.

Equations

• k.AppliesForce = (k = Levin2026.VerbKind.exertingForce ∨ k = Levin2026.VerbKind.hitting ∨ k = Levin2026.VerbKind.wiping)

@[instance_reducible]

instance Levin2026.instDecidablePredVerbKindAppliesForce : DecidablePred VerbKind.AppliesForce

Equations

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

def Levin2026.VerbKind.IsSurfaceContact (k : VerbKind) : Prop

A verb of surface contact describes an entity coming into contact with another through the imparting of a force.

Equations

• k.IsSurfaceContact = (k = Levin2026.VerbKind.hitting ∨ k = Levin2026.VerbKind.wiping)

@[instance_reducible]

instance Levin2026.instDecidablePredVerbKindIsSurfaceContact : DecidablePred VerbKind.IsSurfaceContact

Equations

• Levin2026.instDecidablePredVerbKindIsSurfaceContact x✝ = { decide := decide (x✝ = Levin2026.VerbKind.hitting) || decide (x✝ = Levin2026.VerbKind.wiping), reflects_decide := ⋯ }

def Levin2026.exertingForceVerbs : List String

The attested verbs of exerting force.

Equations

• Levin2026.exertingForceVerbs = ["fling", "jerk", "pull", "push", "shove", "tug", "wrench", "yank"]

def Levin2026.hittingVerbs : List String

The attested verbs of hitting.

Equations

• Levin2026.hittingVerbs = ["bang", "kick", "punch", "slam", "smack", "thrash", "thump"]

def Levin2026.wipingVerbs : List String

The attested verbs of wiping, with wipe itself.

Equations

• Levin2026.wipingVerbs = ["scrape", "sweep", "wipe"]

def Levin2026.VerbKind.labels : List (String × VerbKind)

The verbs by their paperFeatures labels.

Equations

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

inductive Levin2026.Sense : Type

A result adjective is used in its spatially instantiated sense or in another.

• spatial : Sense
• other : Sense

@[instance_reducible]

instance Levin2026.instDecidableEqSense : DecidableEq Sense

Equations

• Levin2026.instDecidableEqSense x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Levin2026.instReprSense : Repr Sense

Equations

• Levin2026.instReprSense = { reprPrec := Levin2026.instReprSense.repr }

def Levin2026.instReprSense.repr : Sense → ℕ → Std.Format

Equations

• Levin2026.instReprSense.repr Levin2026.Sense.spatial prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Levin2026.Sense.spatial")).group prec✝
• Levin2026.instReprSense.repr Levin2026.Sense.other prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Levin2026.Sense.other")).group prec✝

def Levin2026.Sense.labels : List (String × Sense)

The senses by their paperFeatures labels.

Equations

• Levin2026.Sense.labels = [("spatial", Levin2026.Sense.spatial), ("other", Levin2026.Sense.other)]

def Levin2026.adjectiveLabels : List (String × Option Degree.GradableAdjective)

The result adjectives by their paperFeatures labels, with the fragment entry of those the fragment has.

Equations

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

inductive Levin2026.Theme : Type

The kinds of entity a subject denotes.

• animate : Theme
• machine : Theme
• projectile : Theme
• naturalForce : Theme
• manipulated : Theme

@[instance_reducible]

instance Levin2026.instDecidableEqTheme : DecidableEq Theme

Equations

• Levin2026.instDecidableEqTheme x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Levin2026.instReprTheme : Repr Theme

Equations

• Levin2026.instReprTheme = { reprPrec := Levin2026.instReprTheme.repr }

def Levin2026.instReprTheme.repr : Theme → ℕ → Std.Format

Equations

• Levin2026.instReprTheme.repr Levin2026.Theme.animate prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Levin2026.Theme.animate")).group prec✝
• Levin2026.instReprTheme.repr Levin2026.Theme.machine prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Levin2026.Theme.machine")).group prec✝
• Levin2026.instReprTheme.repr Levin2026.Theme.projectile prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Levin2026.Theme.projectile")).group prec✝
• Levin2026.instReprTheme.repr Levin2026.Theme.naturalForce prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Levin2026.Theme.naturalForce")).group prec✝
• Levin2026.instReprTheme.repr Levin2026.Theme.manipulated prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Levin2026.Theme.manipulated")).group prec✝

def Levin2026.Theme.SelfEnergetic (t : Theme) : Prop

A self-energetic entity moves without the continuous involvement of an external cause; an entity that an agent manipulates throughout the event does not.

Equations

• t.SelfEnergetic = (t ≠ Levin2026.Theme.manipulated)

@[instance_reducible]

instance Levin2026.instDecidablePredThemeSelfEnergetic : DecidablePred Theme.SelfEnergetic

Equations

• Levin2026.instDecidablePredThemeSelfEnergetic x✝ = { decide := !decide (x✝ = Levin2026.Theme.manipulated), reflects_decide := ⋯ }

def Levin2026.Theme.labels : List (String × Theme)

The kinds of subject by their paperFeatures labels.

Equations

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

inductive Levin2026.Frame : Type

The frames of the paper's examples.

• transitive : Frame
• intransitive : Frame
• directedMotion : Frame

@[instance_reducible]

instance Levin2026.instDecidableEqFrame : DecidableEq Frame

Equations

• Levin2026.instDecidableEqFrame x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Levin2026.instReprFrame : Repr Frame

Equations

• Levin2026.instReprFrame = { reprPrec := Levin2026.instReprFrame.repr }

def Levin2026.instReprFrame.repr : Frame → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Levin2026.instReprFrame.repr Levin2026.Frame.transitive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Levin2026.Frame.transitive")).group prec✝
• Levin2026.instReprFrame.repr Levin2026.Frame.intransitive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Levin2026.Frame.intransitive")).group prec✝

def Levin2026.Frame.labels : List (String × Frame)

The frames by their paperFeatures labels.

Equations

• Levin2026.Frame.labels = [("transitive", Levin2026.Frame.transitive), ("intransitive", Levin2026.Frame.intransitive), ("directed motion", Levin2026.Frame.directedMotion)]

Licensing

structure Levin2026.Result : Type

A result phrase has an adjective, recorded where the fragment has it, and the sense the adjective is used in.

• adjective : Option Degree.GradableAdjective
• sense : Sense

def Levin2026.Result.IsSpatial (r : Result) : Prop

A result phrase describes a spatially instantiated state when its adjective has a spatial configuration and is used in that sense.

Equations

• r.IsSpatial = (r.sense = Levin2026.Sense.spatial ∧ ∃ a ∈ r.adjective, a.spatialConfigType.isSome = true)

@[instance_reducible]

instance Levin2026.instDecidablePredResultIsSpatial : DecidablePred Result.IsSpatial

Equations

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

structure Levin2026.Row : Type

An example of the paper records the kind of its verb, its result phrase and the kind of its subject, where it has them, its frame and its judgment.

• verb : VerbKind
• result : Option Result
• theme : Option Theme
• frame : Frame
• judgment : Judgment

def Levin2026.Row.Licensed (d : Row) : Prop

An intransitive whose subject is the verb's object is licensed when the verb is a verb of change of state, or when a verb that applies a force combines with a spatially instantiated result predicated of a self-energetic subject.

Equations

• d.Licensed = (d.verb = Levin2026.VerbKind.changeOfState ∨ d.verb.AppliesForce ∧ (∃ r ∈ d.result, r.IsSpatial) ∧ ∃ t ∈ d.theme, t.SelfEnergetic)

@[instance_reducible]

instance Levin2026.instDecidablePredRowLicensed : DecidablePred Row.Licensed

Equations

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

def Levin2026.optional? {α : Type u_1} (e : Datum) (key : String) (table : List (String × α)) : Option (Option α)

An optional feature of an example, read through a table.

Equations

• Levin2026.optional? e key table = match e.feature? key with | none => some none | some v => Option.map some (List.lookup v table)

def Levin2026.result? (e : Datum) : Option (Option Result)

The result phrase of an example, none when the row names no adjective.

Equations

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

def Levin2026.Row.ofDatum (e : Datum) : Option Row

A datum read into its row.

Equations

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

theorem Levin2026.isSome_ofDatum (e : Datum) : e ∈ Examples.all → (Row.ofDatum e).isSome = true

Every example is read.

def Levin2026.data : List Row

The paper's examples.

Equations

• Levin2026.data = List.filterMap Levin2026.Row.ofDatum Levin2026.Examples.all

theorem Levin2026.acceptable_iff_licensed (d : Row) : d ∈ data → d.frame = Frame.intransitive → (d.judgment = Judgment.acceptable ↔ d.Licensed)

An intransitive of the paper, with or without a result phrase, is acceptable exactly when it is licensed.

theorem Levin2026.exists_unacceptable_appliesForce : (∃ d ∈ data, d.verb.AppliesForce ∧ d.frame = Frame.intransitive ∧ d.result = none ∧ d.judgment ≠ Judgment.acceptable) ∧ ∃ d ∈ data, d.verb.AppliesForce ∧ d.frame = Frame.intransitive ∧ d.result.isSome = true ∧ d.judgment ≠ Judgment.acceptable

The verb does not suffice, since a verb that applies a force is unacceptable without a result phrase and with a result that is not spatially instantiated.

theorem Levin2026.exists_unacceptable_spatial : ∃ d ∈ data, d.frame = Frame.intransitive ∧ (∃ r ∈ d.result, r.IsSpatial) ∧ d.judgment ≠ Judgment.acceptable

The adjective does not suffice, since a spatially instantiated result is unacceptable with a verb outside the two classes.

theorem Levin2026.causative_variants (k : VerbKind) : k ∈ [VerbKind.exertingForce, VerbKind.hitting] → (∃ d ∈ data, d.verb = k ∧ d.frame = Frame.transitive ∧ d.result.isSome = true ∧ d.judgment = Judgment.acceptable) ∧ ∃ d ∈ data, d.verb = k ∧ d.frame = Frame.intransitive ∧ d.result.isSome = true ∧ d.judgment = Judgment.acceptable

The verbs of exerting force and the verbs of hitting are attested in both variants, the transitive resultative and the intransitive one.

theorem Levin2026.directedMotion_selfEnergetic (d : Row) : d ∈ data → d.frame = Frame.directedMotion → d.verb.IsSurfaceContact ∧ ∃ t ∈ d.theme, t.SelfEnergetic

The subjects of the directed motion descriptions with verbs of surface contact are self-energetic, as the subjects of the intransitive resultatives are.

theorem Levin2026.not_licensed_of_manipulated {d : Row} (hv : d.verb ≠ VerbKind.changeOfState) (ht : d.theme = some Theme.manipulated) : ¬d.Licensed

An entity that must be manipulated throughout is never the subject of a licensed intransitive resultative with a verb that applies a force.

The construction does not restrict the alternation

theorem Levin2026.participates_causativeInchoative : ¬ArgumentStructure.LevinClass.pushPull.Participates ArgumentStructure.DiathesisAlternation.causativeInchoative ∧ ¬ArgumentStructure.LevinClass.hit.Participates ArgumentStructure.DiathesisAlternation.causativeInchoative ∧ ArgumentStructure.LevinClass.otherChangeOfState.Participates ArgumentStructure.DiathesisAlternation.causativeInchoative

The classes of verbs of exerting force and of hitting lack the causative alternation in [Lev93], and the verbs of change of state have it.

theorem Levin2026.exertingForce_not_all_pushPull : ∃ v ∈ exertingForceVerbs, "fling" = v ∧ v ∉ ArgumentStructure.LevinClass.pushPull.members ∧ v ∈ ArgumentStructure.LevinClass.throw.members

The paper's verbs of exerting force are not all verbs of pushing and pulling in [Lev93]: fling is there a verb of throwing.

theorem Levin2026.exists_unacceptable_intransitive_resultative : ∃ d ∈ data, d.verb = VerbKind.other ∧ d.frame = Frame.intransitive ∧ d.result.isSome = true ∧ d.judgment ≠ Judgment.acceptable

Neo-constructional approaches "do not take a verb's lexical properties to constrain its distribution, so any verb would be expected to appear in all resultative patterns" (footnote 7), but a verb outside the paper's lists is unacceptable in the intransitive resultative, as in (16d) The tub scrubbed clean.