B&K-G Typology, Bifurcation, and Manner/Result Complementarity #

@cite{beavers-koontz-garboden-2020} @cite{rappaport-hovav-levin-2010}

The four-feature typology of @cite{beavers-koontz-garboden-2020} (±state, ±manner, ±result, ±cause) classifies roots by which kinds of atomic entailments they carry. Crucially, this classification is derived from Root.entailments — not stipulated as a separate enum.

Two long-standing conjectures restrict which feature combinations are allowed:

Bifurcation Thesis of Roots: roots only carry "ontological" entailments (state, manner). Eventive structure (result, cause) is contributed by templatic heads, never by roots.
Manner/Result Complementarity (@cite{rappaport-hovav-levin-2010}): a single root entails manner or result, never both.

@cite{beavers-koontz-garboden-2020} argue both fail. Here we encode them as Boolean predicates on roots and provide witnesses (in BeaversKoontzGarboden2020.lean) that falsify the universal closures.

source

structure Semantics.Lexical.Roots.FeatureSignature :

Type

The four-feature classification of a root (@cite{beavers-koontz-garboden-2020} table 13). All four features are derived from Root.entailments, so the 16-cell typology falls out of which kinds of atoms a root carries.

state : Bool
manner : Bool
result : Bool
cause : Bool

Instances For

source

def Semantics.Lexical.Roots.instDecidableEqFeatureSignature.decEq (x✝ x✝¹ : FeatureSignature) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

source

@[implicit_reducible]

instance Semantics.Lexical.Roots.instDecidableEqFeatureSignature :

DecidableEq FeatureSignature

Equations

Semantics.Lexical.Roots.instDecidableEqFeatureSignature = Semantics.Lexical.Roots.instDecidableEqFeatureSignature.decEq

source

@[implicit_reducible]

instance Semantics.Lexical.Roots.instReprFeatureSignature :

Repr FeatureSignature

Equations

Semantics.Lexical.Roots.instReprFeatureSignature = { reprPrec := Semantics.Lexical.Roots.instReprFeatureSignature.repr }

source

def Semantics.Lexical.Roots.instReprFeatureSignature.repr :

FeatureSignature → Nat → Std.Format

Equations

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

Instances For

source

def Semantics.Lexical.Roots.Root.featureSignature (r : Root) :

FeatureSignature

The B&K-G feature signature of a root, derived from its entailment list.

Equations

r.featureSignature = { state := r.hasState, manner := r.hasManner, result := r.hasResult, cause := r.hasCause }

Instances For

source

def Semantics.Lexical.Roots.Root.ViolatesBifurcation (r : Root) :

Prop

A root violates Bifurcation iff it carries both an ontological entailment (state or manner) and an eventive one (result or cause). The Bifurcation Thesis (@cite{beavers-koontz-garboden-2020}) is the universal claim that no root violates this.

Equations

r.ViolatesBifurcation = ((r.hasState = true ∨ r.hasManner = true) ∧ (r.hasResult = true ∨ r.hasCause = true))

Instances For

source

@[implicit_reducible]

instance Semantics.Lexical.Roots.instDecidableViolatesBifurcation (r : Root) :

Decidable r.ViolatesBifurcation

Equations

Semantics.Lexical.Roots.instDecidableViolatesBifurcation r = id inferInstance

source

def Semantics.Lexical.Roots.Root.RespectsBifurcation (r : Root) :

Prop

Dual of ViolatesBifurcation. A root respects the thesis iff it has only ontological or only eventive entailments.

Equations

r.RespectsBifurcation = ¬r.ViolatesBifurcation

Instances For

source

@[implicit_reducible]

instance Semantics.Lexical.Roots.instDecidableRespectsBifurcation (r : Root) :

Decidable r.RespectsBifurcation

Equations

Semantics.Lexical.Roots.instDecidableRespectsBifurcation r = id inferInstance

source

def Semantics.Lexical.Roots.Root.HasMannerAndResult (r : Root) :

Prop

A root has both manner and result entailments — the Manner/Result Complementarity thesis (@cite{rappaport-hovav-levin-2010}) is the universal claim that no root does.

Equations