Bifurcation and Manner/Result Complementarity for Roots

The two conjectures [BKG20] argue against, stated for roots by delegation to the signature level (Roots/Signature.lean):

• Bifurcation Thesis of Roots ([Emb09]; the assumption of [Ara05]): meaning introduced by a functional head — change, cause — can never be part of a root's meaning. As an order statement: every root's signature lies below Root.Kinds.ontological.
• Manner/Result Complementarity ([RHL10]): a single root entails a manner or a result, never both. As an order statement: no root's signature lies above {manner, result}.

Falsifying witnesses live in Studies/BeaversKoontzGarboden2020.lean.

Main declarations

• Root.ViolatesBifurcation, Root.HasMannerAndResult, and their negations Root.RespectsBifurcation, Root.RespectsMannerResultComplementarity

def Verb.Root.ViolatesBifurcation (r : Root) : Prop

A root violates Bifurcation iff it itself carries templatic (eventive) meaning — change of state or cause (Root.Kinds.violatesBifurcation_iff). The Bifurcation Thesis ([Emb09]; [Ara05]) is the universal claim that no root does. (The ditransitive prepositional heads P_loc and P_have, which [BKG20] also treat as templatic, are not modeled here.)

Equations

• r.ViolatesBifurcation = r.kinds.ViolatesBifurcation

@[implicit_reducible]

instance Verb.Root.instDecidableViolatesBifurcation (r : Root) : Decidable r.ViolatesBifurcation

Equations

• r.instDecidableViolatesBifurcation = Verb.Root.instDecidableViolatesBifurcation._aux_1 r

def Verb.Root.RespectsBifurcation (r : Root) : Prop

Negation of ViolatesBifurcation: the root carries only ontological entailments (state, manner).

Equations

• r.RespectsBifurcation = ¬r.ViolatesBifurcation

@[implicit_reducible]

instance Verb.Root.instDecidableRespectsBifurcation (r : Root) : Decidable r.RespectsBifurcation

Equations

• r.instDecidableRespectsBifurcation = Verb.Root.instDecidableRespectsBifurcation._aux_1 r

theorem Verb.Root.respectsBifurcation_iff_le {r : Root} : r.RespectsBifurcation ↔ r.kinds ≤ Kinds.ontological

The thesis as an order statement: a root respects Bifurcation iff its signature is bounded by the ontological kinds.

def Verb.Root.HasMannerAndResult (r : Root) : Prop

A root has both manner and result entailments — Manner/Result Complementarity ([RHL10]) is the universal claim that no root does.

Equations

• r.HasMannerAndResult = r.kinds.HasMannerAndResult

@[implicit_reducible]

instance Verb.Root.instDecidableHasMannerAndResult (r : Root) : Decidable r.HasMannerAndResult

Equations

• r.instDecidableHasMannerAndResult = Verb.Root.instDecidableHasMannerAndResult._aux_1 r

def Verb.Root.RespectsMannerResultComplementarity (r : Root) : Prop

Negation of HasMannerAndResult.

Equations

• r.RespectsMannerResultComplementarity = ¬r.HasMannerAndResult

@[implicit_reducible]

instance Verb.Root.instDecidableRespectsMannerResultComplementarity (r : Root) : Decidable r.RespectsMannerResultComplementarity

Equations

• r.instDecidableRespectsMannerResultComplementarity = Verb.Root.instDecidableRespectsMannerResultComplementarity._aux_1 r