Root entailments of the Levin classes

The root-entailment signature of [BKG20] that each class of [Lev93] realizes, for the classes the literature has analysed; none for the rest. LevinClass.RootEntails reads a single entailment off the signature, and LevinClass.RootPredictsCausative is the root hypothesis for the causative alternation, read off the signature.

References

• [BKG20]
• [Lev93]

def ArgumentStructure.LevinClass.rootEntailments : LevinClass → Option Semantics.Root.Kinds

The root signature a class realizes, where one has been established: manner roots for the activity classes, causative-result roots for the externally caused changes of state, pure result roots for the internally caused ones, property concepts for the statives, the empty signature for roots with no structural entailment.

def ArgumentStructure.LevinClass.RootEntails (c : LevinClass) (k : Semantics.Root.Kind) : Prop

The class's root carries the entailment.

Equations

• c.RootEntails k = match c.rootEntailments with | some s => k ∈ s | none => False

@[instance_reducible]

instance ArgumentStructure.instDecidableRootEntails (c : LevinClass) (k : Semantics.Root.Kind) : Decidable (c.RootEntails k)

Equations

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

theorem ArgumentStructure.LevinClass.rootEntailments_wellFormed (c : LevinClass) (s : Semantics.Root.Kinds) (h : c.rootEntailments = some s) : s.WellFormed

Every recorded signature is well-formed.

The root hypothesis for the causative alternation

def ArgumentStructure.LevinClass.causativeExceptions : Finset LevinClass

The classes whose root entails its causer, so that no inchoative variant exists although the root entails a caused change: the destroy and murder verbs of [BKG20].

Equations

• ArgumentStructure.LevinClass.causativeExceptions = {ArgumentStructure.LevinClass.destroy, ArgumentStructure.LevinClass.murder}

def ArgumentStructure.LevinClass.RootPredictsCausative (c : LevinClass) : Prop

The root hypothesis: a class alternates between causative and inchoative when its root entails a caused change and no manner, unless the root entails its causer (causativeExceptions). A hypothesis to be measured against Part II of [Lev93], not data.

Equations

• c.RootPredictsCausative = ((∃ s ∈ c.rootEntailments, Semantics.Root.Kind.cause ∈ s ∧ Semantics.Root.Kind.manner ∉ s) ∧ c ∉ ArgumentStructure.LevinClass.causativeExceptions)

@[instance_reducible]

instance ArgumentStructure.instDecidableRootPredictsCausative (c : LevinClass) : Decidable c.RootPredictsCausative

Equations

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