Morphological Causation: Causative Construction Typology

@cite{comrie-1989} @cite{song-1996} @cite{krejci-2012}

Causative constructions cross-linguistically vary along two orthogonal axes: morphological complexity (compact → analytic) and semantic directness (direct → indirect mediation). @cite{comrie-1989}'s central generalization: more complex morphology correlates with more indirect causation.

Causer Type

Causative constructions are sensitive to the causer's intentionality and ontological category. Following @cite{hafeez-2025}, we distinguish:

• intentional human (IHCr): volitional, controlled action → full agentivity
• accidental human (AHCr): unintentional, no control → marginal agentivity
• natural force (NFCr): non-human, non-volitional → non-agentive

The key dimension is intentionality, not ontological type: IHCr and AHCr are both human but differ in agentivity. This three-way distinction drives construction selection in Urdu and other languages.

Causee/Affectee Type

The second participant in a causal chain (causee or affectee) varies in four levels of control and animacy, following @cite{hafeez-2025}:

• controlling human (ContrHCEAF): exercises control over the induced action
• physically impacted human (PhysImpHCEAF): involuntarily coerced
• psychologically impacted human (PsychImpHCEAF): mentally affected
• inanimate (InanCEAF): no volition or sentience

Agentivity

Agentivity decomposes into intentionality × control (following @cite{van-valin-wilkins-1996}). Three degrees:

• full: intentional causer (IHCr)
• marginal: accidental human (AHCr) or natural force (NFCr)
• partial/induced: causee exercises control under causer's influence

Bridges

• CauserType.toCausalSource → CausalSource (psych causation)
• CauserType.toAgentivityNode → AgentivityNode (agentivity lattice)
• CauserType.volitionality → Volitionality (root dimensions)
• CauserType.agentivityDegree → AgentivityDegree
• CausativeConstruction bundles complexity + mediation + causer/causee restrictions for cross-linguistic comparison
• comrie_monotone formalizes the compact-diffuse correlation

Intransitivization (@cite{krejci-2012})

The causative/inchoative alternation has two directions: causativization (adding an external cause) and intransitivization (removing or coidentifying it). @cite{krejci-2012}'s central insight: intransitive variants are NOT structurally uniform. Reflexive intransitives (German sich, Hindi apne-aap) coidentify causer and causee, retaining bieventive structure. Anticausative intransitives remove the external cause entirely, yielding monoeventive structure.

• IntransitivizationType distinguishes reflexive, anticausative, and unmarked intransitivization
• Three diagnostics (again/re- ambiguity, negation over CAUSE, "by itself") all detect the causer position retained by reflexive intransitives but absent from anticausatives

inductive Semantics.Causation.MorphologicalCausation.CauserType : Type

Causer type distinguished by intentionality and ontological category.

The key dimension is intentionality: IHCr and AHCr are both human but have fundamentally different agentivity profiles. NFCr is non-human and non-intentional.

This three-way distinction drives construction selection in Urdu (@cite{hafeez-2025}) and other languages.

• intentionalHuman : CauserType
• accidentalHuman : CauserType
• naturalForce : CauserType

instance Semantics.Causation.MorphologicalCausation.instDecidableEqCauserType : DecidableEq CauserType

Equations

• Semantics.Causation.MorphologicalCausation.instDecidableEqCauserType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Causation.MorphologicalCausation.instBEqCauserType : BEq CauserType

Equations

• Semantics.Causation.MorphologicalCausation.instBEqCauserType = { beq := Semantics.Causation.MorphologicalCausation.instBEqCauserType.beq }

def Semantics.Causation.MorphologicalCausation.instBEqCauserType.beq : CauserType → CauserType → Bool

Equations

• Semantics.Causation.MorphologicalCausation.instBEqCauserType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Semantics.Causation.MorphologicalCausation.instReprCauserType.repr : CauserType → ℕ → Std.Format

Equations

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

instance Semantics.Causation.MorphologicalCausation.instReprCauserType : Repr CauserType

Equations

• Semantics.Causation.MorphologicalCausation.instReprCauserType = { reprPrec := Semantics.Causation.MorphologicalCausation.instReprCauserType.repr }

inductive Semantics.Causation.MorphologicalCausation.CauseeAffecteeType : Type

Causee/affectee type: four levels of control and animacy.

@cite{hafeez-2025}'s four-way distinction captures the gradient of the second participant's autonomy in a causal chain. A controlling causee reduces the causer's responsibility; an inanimate affectee increases it.

• controllingHuman : CauseeAffecteeType
• physImpactHuman : CauseeAffecteeType
• psychImpactHuman : CauseeAffecteeType
• inanimate : CauseeAffecteeType

instance Semantics.Causation.MorphologicalCausation.instDecidableEqCauseeAffecteeType : DecidableEq CauseeAffecteeType

Equations

• Semantics.Causation.MorphologicalCausation.instDecidableEqCauseeAffecteeType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Causation.MorphologicalCausation.instBEqCauseeAffecteeType.beq : CauseeAffecteeType → CauseeAffecteeType → Bool

Equations

• Semantics.Causation.MorphologicalCausation.instBEqCauseeAffecteeType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Causation.MorphologicalCausation.instBEqCauseeAffecteeType : BEq CauseeAffecteeType

Equations

• Semantics.Causation.MorphologicalCausation.instBEqCauseeAffecteeType = { beq := Semantics.Causation.MorphologicalCausation.instBEqCauseeAffecteeType.beq }

def Semantics.Causation.MorphologicalCausation.instReprCauseeAffecteeType.repr : CauseeAffecteeType → ℕ → Std.Format

Equations

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

instance Semantics.Causation.MorphologicalCausation.instReprCauseeAffecteeType : Repr CauseeAffecteeType

Equations

• Semantics.Causation.MorphologicalCausation.instReprCauseeAffecteeType = { reprPrec := Semantics.Causation.MorphologicalCausation.instReprCauseeAffecteeType.repr }

inductive Semantics.Causation.MorphologicalCausation.AgentivityDegree : Type

Degree of agentivity, decomposed from intentionality × control.

@cite{hafeez-2025}: "an intentional causer displays full agentivity, an accidental causer shows reduced or marginal agentivity, and a causee/affectee who exerts control displays induced or partial agentivity."

• full : AgentivityDegree
• marginal : AgentivityDegree
• induced : AgentivityDegree

instance Semantics.Causation.MorphologicalCausation.instDecidableEqAgentivityDegree : DecidableEq AgentivityDegree

Equations

• Semantics.Causation.MorphologicalCausation.instDecidableEqAgentivityDegree x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Causation.MorphologicalCausation.instBEqAgentivityDegree : BEq AgentivityDegree

Equations

• Semantics.Causation.MorphologicalCausation.instBEqAgentivityDegree = { beq := Semantics.Causation.MorphologicalCausation.instBEqAgentivityDegree.beq }

def Semantics.Causation.MorphologicalCausation.instBEqAgentivityDegree.beq : AgentivityDegree → AgentivityDegree → Bool

Equations

• Semantics.Causation.MorphologicalCausation.instBEqAgentivityDegree.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Semantics.Causation.MorphologicalCausation.instReprAgentivityDegree.repr : AgentivityDegree → ℕ → Std.Format

Equations

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

instance Semantics.Causation.MorphologicalCausation.instReprAgentivityDegree : Repr AgentivityDegree

Equations

• Semantics.Causation.MorphologicalCausation.instReprAgentivityDegree = { reprPrec := Semantics.Causation.MorphologicalCausation.instReprAgentivityDegree.repr }

def Semantics.Causation.MorphologicalCausation.CauserType.agentivityDegree : CauserType → AgentivityDegree

Causer type determines causer's agentivity degree.

Equations

• Semantics.Causation.MorphologicalCausation.CauserType.intentionalHuman.agentivityDegree = Semantics.Causation.MorphologicalCausation.AgentivityDegree.full
• Semantics.Causation.MorphologicalCausation.CauserType.accidentalHuman.agentivityDegree = Semantics.Causation.MorphologicalCausation.AgentivityDegree.marginal
• Semantics.Causation.MorphologicalCausation.CauserType.naturalForce.agentivityDegree = Semantics.Causation.MorphologicalCausation.AgentivityDegree.marginal

def Semantics.Causation.MorphologicalCausation.CauseeAffecteeType.hasInducedAgentivity : CauseeAffecteeType → Bool

A controlling causee has partial (induced) agentivity; all other causee types have no independent agentivity.

Equations

• Semantics.Causation.MorphologicalCausation.CauseeAffecteeType.controllingHuman.hasInducedAgentivity = true
• x✝.hasInducedAgentivity = false

inductive Semantics.Causation.MorphologicalCausation.Mediation : Type

Directness of causal mediation between causer and result.

@cite{comrie-1989}: direct causation involves no intermediary — the causer brings about the result without an intervening causee decision or action. Indirect causation involves a mediating causee who retains some autonomy over the caused event.

• direct : Mediation
• indirect : Mediation

instance Semantics.Causation.MorphologicalCausation.instDecidableEqMediation : DecidableEq Mediation

Equations

• Semantics.Causation.MorphologicalCausation.instDecidableEqMediation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Causation.MorphologicalCausation.instBEqMediation : BEq Mediation

Equations

• Semantics.Causation.MorphologicalCausation.instBEqMediation = { beq := Semantics.Causation.MorphologicalCausation.instBEqMediation.beq }

def Semantics.Causation.MorphologicalCausation.instBEqMediation.beq : Mediation → Mediation → Bool

Equations

• Semantics.Causation.MorphologicalCausation.instBEqMediation.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Semantics.Causation.MorphologicalCausation.instReprMediation.repr : Mediation → ℕ → Std.Format

Equations

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

instance Semantics.Causation.MorphologicalCausation.instReprMediation : Repr Mediation

Equations

• Semantics.Causation.MorphologicalCausation.instReprMediation = { reprPrec := Semantics.Causation.MorphologicalCausation.instReprMediation.repr }

inductive Semantics.Causation.MorphologicalCausation.CausativeComplexity : Type

Morphological complexity of a causative construction.

@cite{comrie-1989}'s compact-to-analytic continuum:

• lexical: suppletive or idiosyncratic (kill/die, fell/fall)
• morphological: productive affix (Urdu -aa, Japanese -(s)ase)
• periphrastic: analytic multi-word (English "make X do Y")

Ordered from compact to analytic.

• lexical : CausativeComplexity
• morphological : CausativeComplexity
• periphrastic : CausativeComplexity

instance Semantics.Causation.MorphologicalCausation.instDecidableEqCausativeComplexity : DecidableEq CausativeComplexity

Equations

• Semantics.Causation.MorphologicalCausation.instDecidableEqCausativeComplexity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Causation.MorphologicalCausation.instBEqCausativeComplexity.beq : CausativeComplexity → CausativeComplexity → Bool

Equations

• Semantics.Causation.MorphologicalCausation.instBEqCausativeComplexity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Causation.MorphologicalCausation.instBEqCausativeComplexity : BEq CausativeComplexity

Equations

• Semantics.Causation.MorphologicalCausation.instBEqCausativeComplexity = { beq := Semantics.Causation.MorphologicalCausation.instBEqCausativeComplexity.beq }

def Semantics.Causation.MorphologicalCausation.instReprCausativeComplexity.repr : CausativeComplexity → ℕ → Std.Format

Equations

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

instance Semantics.Causation.MorphologicalCausation.instReprCausativeComplexity : Repr CausativeComplexity

Equations

• Semantics.Causation.MorphologicalCausation.instReprCausativeComplexity = { reprPrec := Semantics.Causation.MorphologicalCausation.instReprCausativeComplexity.repr }

instance Semantics.Causation.MorphologicalCausation.instLTCausativeComplexity : LT CausativeComplexity

Equations

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

instance Semantics.Causation.MorphologicalCausation.instLECausativeComplexity : LE CausativeComplexity

Equations

• Semantics.Causation.MorphologicalCausation.instLECausativeComplexity = { le := fun (a b : Semantics.Causation.MorphologicalCausation.CausativeComplexity) => a = b ∨ a < b }

instance Semantics.Causation.MorphologicalCausation.instDecidableLtCausativeComplexity (a b : CausativeComplexity) : Decidable (a < b)

Equations

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

structure Semantics.Causation.MorphologicalCausation.CausativeConstruction : Type

A causative construction bundles morphological complexity with semantic parameters that govern its use.

Each language's causative system is a list of CausativeConstruction values — e.g., Urdu has 7 (acceptability study), Japanese has 3.

• complexity : CausativeComplexity

  Morphological complexity (compact → analytic)

• mediation : Mediation

  Direct vs. indirect mediation

• causerRestriction : Option CauserType

  Restriction on causer type (none = unrestricted)

• causeeRestriction : Option CauseeAffecteeType

  Required causee/affectee type (none = unrestricted)

instance Semantics.Causation.MorphologicalCausation.instDecidableEqCausativeConstruction : DecidableEq CausativeConstruction

Equations

• Semantics.Causation.MorphologicalCausation.instDecidableEqCausativeConstruction = Semantics.Causation.MorphologicalCausation.instDecidableEqCausativeConstruction.decEq

def Semantics.Causation.MorphologicalCausation.instDecidableEqCausativeConstruction.decEq (x✝ x✝¹ : CausativeConstruction) : Decidable (x✝ = x✝¹)

Equations

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

instance Semantics.Causation.MorphologicalCausation.instBEqCausativeConstruction : BEq CausativeConstruction

Equations

• Semantics.Causation.MorphologicalCausation.instBEqCausativeConstruction = { beq := Semantics.Causation.MorphologicalCausation.instBEqCausativeConstruction.beq }

def Semantics.Causation.MorphologicalCausation.instBEqCausativeConstruction.beq : CausativeConstruction → CausativeConstruction → Bool

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Causation.MorphologicalCausation.instBEqCausativeConstruction.beq x✝¹ x✝ = false

def Semantics.Causation.MorphologicalCausation.instReprCausativeConstruction.repr : CausativeConstruction → ℕ → Std.Format

Equations

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

instance Semantics.Causation.MorphologicalCausation.instReprCausativeConstruction : Repr CausativeConstruction

Equations

• Semantics.Causation.MorphologicalCausation.instReprCausativeConstruction = { reprPrec := Semantics.Causation.MorphologicalCausation.instReprCausativeConstruction.repr }

structure Semantics.Causation.MorphologicalCausation.SemanticPrototype : Type

A semantic prototype specifies the combination of semantic variables under which a construction receives its peak acceptability rating or is preferentially produced.

@cite{hafeez-2025} Table 25: each construction has a (possibly empty) set of features that define its prototype. A prototype is "hypothesized" when the acceptability peak exceeds 50% ceiling for a scene type.

Prototypes use both positive (e.g., [+IHCr]) and negative (e.g., [-IHCr]) feature specifications. Both are represented as lists: presentCausers/absentCausers etc.

• presentCausers : List CauserType

  Causer types that must be present (e.g., [+IHCr])

• absentCausers : List CauserType

  Causer types that must be absent (e.g., [-IHCr])

• presentCausees : List CauseeAffecteeType

  Causee/affectee types that must be present

• absentCausees : List CauseeAffecteeType

  Causee/affectee types that must be absent

• requiresMediation : Option Bool

  Whether mediation is part of the prototype

instance Semantics.Causation.MorphologicalCausation.instDecidableEqSemanticPrototype : DecidableEq SemanticPrototype

Equations

• Semantics.Causation.MorphologicalCausation.instDecidableEqSemanticPrototype = Semantics.Causation.MorphologicalCausation.instDecidableEqSemanticPrototype.decEq

def Semantics.Causation.MorphologicalCausation.instDecidableEqSemanticPrototype.decEq (x✝ x✝¹ : SemanticPrototype) : Decidable (x✝ = x✝¹)

Equations

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

def Semantics.Causation.MorphologicalCausation.instBEqSemanticPrototype.beq : SemanticPrototype → SemanticPrototype → Bool

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Causation.MorphologicalCausation.instBEqSemanticPrototype.beq x✝¹ x✝ = false

instance Semantics.Causation.MorphologicalCausation.instBEqSemanticPrototype : BEq SemanticPrototype

Equations

• Semantics.Causation.MorphologicalCausation.instBEqSemanticPrototype = { beq := Semantics.Causation.MorphologicalCausation.instBEqSemanticPrototype.beq }

instance Semantics.Causation.MorphologicalCausation.instReprSemanticPrototype : Repr SemanticPrototype

Equations

• Semantics.Causation.MorphologicalCausation.instReprSemanticPrototype = { reprPrec := Semantics.Causation.MorphologicalCausation.instReprSemanticPrototype.repr }

def Semantics.Causation.MorphologicalCausation.instReprSemanticPrototype.repr : SemanticPrototype → ℕ → Std.Format

Equations

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

def Semantics.Causation.MorphologicalCausation.comrie_monotone (c1 c2 : CausativeConstruction) : Prop

Comrie's monotonicity (@cite{comrie-1989} §8.4): within a single language, if construction A is morphologically more compact than construction B, then A encodes more direct causation than B.

Stated as a predicate on pairs: a system satisfies Comrie's generalization when complexity and mediation co-vary.

Equations

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

def Semantics.Causation.MorphologicalCausation.CauserType.toCausalSource : CauserType → PsychCausation.CausalSource

All causer types are "external" in @cite{kim-2024}'s sense.

The causer type taxonomy refines CausalSource.external: psych verbs' internal source (mental representation) is not a causer type in the morphological causation sense.

Equations

• Semantics.Causation.MorphologicalCausation.CauserType.intentionalHuman.toCausalSource = Semantics.Causation.PsychCausation.CausalSource.external
• Semantics.Causation.MorphologicalCausation.CauserType.accidentalHuman.toCausalSource = Semantics.Causation.PsychCausation.CausalSource.external
• Semantics.Causation.MorphologicalCausation.CauserType.naturalForce.toCausalSource = Semantics.Causation.PsychCausation.CausalSource.external

def Semantics.Causation.MorphologicalCausation.CauserType.volitionality : CauserType → Volitionality

Intentional human causers are volitional; accidental and natural force causers are not.

Equations

• Semantics.Causation.MorphologicalCausation.CauserType.intentionalHuman.volitionality = Volitionality.volitional
• Semantics.Causation.MorphologicalCausation.CauserType.accidentalHuman.volitionality = Volitionality.nonvolitional
• Semantics.Causation.MorphologicalCausation.CauserType.naturalForce.volitionality = Volitionality.nonvolitional

def Semantics.Causation.MorphologicalCausation.CauserType.toAgentivityNode : CauserType → Lexical.Verb.AgentivityLattice.AgentivityNode

Intentional human causers map to the agentive pole of the lattice (volition + sentience + instigation); accidental humans retain sentience but lack volition; natural forces have instigation only.

Equations

• Semantics.Causation.MorphologicalCausation.CauserType.intentionalHuman.toAgentivityNode = { volition := true, sentience := true, instigation := true, motion := false }
• Semantics.Causation.MorphologicalCausation.CauserType.accidentalHuman.toAgentivityNode = { volition := false, sentience := true, instigation := true, motion := false }
• Semantics.Causation.MorphologicalCausation.CauserType.naturalForce.toAgentivityNode = { volition := false, sentience := false, instigation := true, motion := false }

theorem Semantics.Causation.MorphologicalCausation.intentional_max_agentivity : CauserType.intentionalHuman.toAgentivityNode.volition = true ∧ CauserType.intentionalHuman.toAgentivityNode.sentience = true ∧ CauserType.intentionalHuman.toAgentivityNode.instigation = true

Intentional human causers have maximal agentivity among causer types.

theorem Semantics.Causation.MorphologicalCausation.accidental_sentient_not_volitional : CauserType.accidentalHuman.toAgentivityNode.sentience = true ∧ CauserType.accidentalHuman.toAgentivityNode.volition = false

Accidental human causers retain sentience but lack volition.

theorem Semantics.Causation.MorphologicalCausation.naturalForce_instigation_only : CauserType.naturalForce.toAgentivityNode = { volition := false, sentience := false, instigation := true, motion := false }

Natural force causers have only instigation (no sentience, no volition).

theorem Semantics.Causation.MorphologicalCausation.all_causers_external (ct : CauserType) : ct.toCausalSource = PsychCausation.CausalSource.external

All causer types project to external CausalSource.

theorem Semantics.Causation.MorphologicalCausation.intentional_full_agentivity : CauserType.intentionalHuman.agentivityDegree = AgentivityDegree.full

IHCr has full agentivity; AHCr and NFCr have marginal.

theorem Semantics.Causation.MorphologicalCausation.accidental_marginal_agentivity : CauserType.accidentalHuman.agentivityDegree = AgentivityDegree.marginal

theorem Semantics.Causation.MorphologicalCausation.naturalForce_marginal_agentivity : CauserType.naturalForce.agentivityDegree = AgentivityDegree.marginal

theorem Semantics.Causation.MorphologicalCausation.controlling_has_induced : CauseeAffecteeType.controllingHuman.hasInducedAgentivity = true

Controlling causees have induced agentivity; all other causee types do not.

theorem Semantics.Causation.MorphologicalCausation.inanimate_no_induced : CauseeAffecteeType.inanimate.hasInducedAgentivity = false

theorem Semantics.Causation.MorphologicalCausation.physImpact_no_induced : CauseeAffecteeType.physImpactHuman.hasInducedAgentivity = false

inductive Semantics.Causation.MorphologicalCausation.IntransitivizationType : Type

How an alternating verb forms its intransitive variant.

@cite{krejci-2012}'s central insight: intransitive variants of causative/inchoative alternation verbs are NOT structurally uniform. Two distinct operations produce surface intransitives:

• anticausative: the external cause is removed entirely. The result is monoeventive: [BECOME [x STATE]]. No causer position exists.
• reflexive: the causer and causee are coidentified — a single participant fills both roles. The result is bieventive: [x ACT] CAUSE [BECOME [x STATE]] with causer = causee. Morphologically marked: German sich, Marathi -un.
• unmarked: no morphological distinction (English break). Event structure must be diagnosed per-verb.

• anticausative : IntransitivizationType
• reflexive : IntransitivizationType
• unmarked : IntransitivizationType

instance Semantics.Causation.MorphologicalCausation.instDecidableEqIntransitivizationType : DecidableEq IntransitivizationType

Equations

• Semantics.Causation.MorphologicalCausation.instDecidableEqIntransitivizationType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Causation.MorphologicalCausation.instBEqIntransitivizationType : BEq IntransitivizationType

Equations

• Semantics.Causation.MorphologicalCausation.instBEqIntransitivizationType = { beq := Semantics.Causation.MorphologicalCausation.instBEqIntransitivizationType.beq }

def Semantics.Causation.MorphologicalCausation.instBEqIntransitivizationType.beq : IntransitivizationType → IntransitivizationType → Bool

Equations

• Semantics.Causation.MorphologicalCausation.instBEqIntransitivizationType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Semantics.Causation.MorphologicalCausation.instReprIntransitivizationType.repr : IntransitivizationType → ℕ → Std.Format

Equations

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

instance Semantics.Causation.MorphologicalCausation.instReprIntransitivizationType : Repr IntransitivizationType

Equations

• Semantics.Causation.MorphologicalCausation.instReprIntransitivizationType = { reprPrec := Semantics.Causation.MorphologicalCausation.instReprIntransitivizationType.repr }

def Semantics.Causation.MorphologicalCausation.IntransitivizationType.isBieventive : IntransitivizationType → Bool

Reflexive intransitives retain the causer position (coidentified with the causee), preserving bieventive structure. Anticausatives remove the causer entirely, yielding monoeventive structure.

Equations

• Semantics.Causation.MorphologicalCausation.IntransitivizationType.reflexive.isBieventive = true
• x✝.isBieventive = false

def Semantics.Causation.MorphologicalCausation.IntransitivizationType.hasCoidentification : IntransitivizationType → Bool

Does the intransitive variant involve coidentification of causer and causee (a single participant in both roles)?

Equations

• Semantics.Causation.MorphologicalCausation.IntransitivizationType.reflexive.hasCoidentification = true
• x✝.hasCoidentification = false

def Semantics.Causation.MorphologicalCausation.IntransitivizationType.licensesBySelf : IntransitivizationType → Bool

"By itself" (von selbst, apne-aap, aapo-aap) is licensed when a causer position exists, even if coidentified with the causee. Anticausatives lack a causer position entirely.

English unmarked intransitives also license "by itself" ("The door opened by itself"), because the unmarked form can be either reflexive or anticausative — only true anticausatives block the modifier.

Equations

• Semantics.Causation.MorphologicalCausation.IntransitivizationType.anticausative.licensesBySelf = false
• x✝.licensesBySelf = true

theorem Semantics.Causation.MorphologicalCausation.coidentification_implies_bieventive (it : IntransitivizationType) : it.hasCoidentification = true → it.isBieventive = true

Coidentification implies bieventivity (the causer position preserved by coidentification is what makes the structure bieventive).

theorem Semantics.Causation.MorphologicalCausation.bieventive_implies_bySelf (it : IntransitivizationType) : it.isBieventive = true → it.licensesBySelf = true

Bieventivity implies "by itself" licensing (both track the presence of a causer position).

theorem Semantics.Causation.MorphologicalCausation.anticausative_monoeventive : IntransitivizationType.anticausative.isBieventive = false ∧ IntransitivizationType.anticausative.hasCoidentification = false ∧ IntransitivizationType.anticausative.licensesBySelf = false

Anticausatives are monoeventive: no coidentification, no bieventivity, no "by itself" licensing.

theorem Semantics.Causation.MorphologicalCausation.reflexive_bieventive : IntransitivizationType.reflexive.isBieventive = true ∧ IntransitivizationType.reflexive.hasCoidentification = true ∧ IntransitivizationType.reflexive.licensesBySelf = true

Reflexive intransitives are bieventive with coidentification.

@cite{krejci-2012} proposes a cross-linguistic hierarchy of causativizability — the extent to which a morphological causative morpheme can apply to different verb classes:

    unaccusatives > middles/ingestives > unergatives > simple transitives

The hierarchy is implicational: if a morpheme causativizes a
higher verb class, it also causativizes all lower classes. This
is validated across 12 languages in @cite{krejci-2012} Table 2.8. 

structure Semantics.Causation.MorphologicalCausation.CausativizabilityData : Type

Cross-linguistic data on causativizability: which verb classes a given morphological causative morpheme can apply to.

• language : String
• morpheme : String
• unaccusative : Bool
• middlesIngestive : Bool
• unergative : Bool
• simpleTransitive : Bool

def Semantics.Causation.MorphologicalCausation.instReprCausativizabilityData.repr : CausativizabilityData → ℕ → Std.Format

Equations

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

instance Semantics.Causation.MorphologicalCausation.instReprCausativizabilityData : Repr CausativizabilityData

Equations

• Semantics.Causation.MorphologicalCausation.instReprCausativizabilityData = { reprPrec := Semantics.Causation.MorphologicalCausation.instReprCausativizabilityData.repr }

instance Semantics.Causation.MorphologicalCausation.instBEqCausativizabilityData : BEq CausativizabilityData

Equations

• Semantics.Causation.MorphologicalCausation.instBEqCausativizabilityData = { beq := Semantics.Causation.MorphologicalCausation.instBEqCausativizabilityData.beq }

def Semantics.Causation.MorphologicalCausation.instBEqCausativizabilityData.beq : CausativizabilityData → CausativizabilityData → Bool

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Causation.MorphologicalCausation.instBEqCausativizabilityData.beq x✝¹ x✝ = false

def Semantics.Causation.MorphologicalCausation.CausativizabilityData.respectsHierarchy (d : CausativizabilityData) : Bool

The hierarchy is implicational: each level implies all lower levels. simpleTransitive → unergative → middlesIngestive → unaccusative.

Equations

• d.respectsHierarchy = ((!d.simpleTransitive || d.unergative) && (!d.unergative || d.middlesIngestive) && (!d.middlesIngestive || d.unaccusative))

def Semantics.Causation.MorphologicalCausation.krejciLanguages : List CausativizabilityData

Cross-linguistic causativizability data from @cite{krejci-2012} Table 2.8. Languages are ordered from narrowest to broadest causative scope.

Equations

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

theorem Semantics.Causation.MorphologicalCausation.krejci_hierarchy_holds : (krejciLanguages.all fun (x : CausativizabilityData) => x.respectsHierarchy) = true

All 12 languages respect the implicational hierarchy.