The Monotonicity Hypothesis (MH) states that word formation operations do not remove operators from lexical semantic representations (LSRs). Given an LSR modeled as a set of operators, a word formation operation f : LSR → LSR satisfies the MH iff for all inputs r, the operators in r are a subset of the operators in f(r).

The MH is an empirical hypothesis, not a logical necessity. KG 2009 argues that anticausativization — the strongest apparent counterexample — is consistent with the MH under a reflexivization analysis (the deletion analysis would violate it). The MH is distinct from the Bifurcation Thesis and Manner/Result Complementarity.

def KoontzGarboden2009.Monotonicity.isMonotonic {Op : Type} [BEq Op] (inputOps outputOps : List Op) : Bool

An operation over operator lists is monotonic if every operator in the input is preserved in the output.

Equations

• KoontzGarboden2009.Monotonicity.isMonotonic inputOps outputOps = inputOps.all fun (x : Op) => outputOps.contains x

def KoontzGarboden2009.Monotonicity.satisfiesMH {Op : Type} [BEq Op] (f : List Op → List Op) : Prop

A word formation operation f satisfies the Monotonicity Hypothesis if it is monotonic for all inputs.

Equations

• KoontzGarboden2009.Monotonicity.satisfiesMH f = ∀ (ops : List Op), KoontzGarboden2009.Monotonicity.isMonotonic ops (f ops) = true

def KoontzGarboden2009.Monotonicity.identityOp {Op : Type} (ops : List Op) : List Op

Identity on operator lists. Models any operation that constrains argument structure without adding or removing operators (e.g., reflexivization: λℜλx[ℜ(x,x)]).

Equations

• KoontzGarboden2009.Monotonicity.identityOp ops = ops

def KoontzGarboden2009.Monotonicity.deleteOp {Op : Type} [BEq Op] (target : Op) (ops : List Op) : List Op

Deletion of a specific operator from the list.

Equations

• KoontzGarboden2009.Monotonicity.deleteOp target ops = List.filter (fun (x : Op) => x != target) ops

theorem KoontzGarboden2009.Monotonicity.isMonotonic_refl {Op : Type} [BEq Op] [LawfulBEq Op] (ops : List Op) : isMonotonic ops ops = true

theorem KoontzGarboden2009.Monotonicity.isMonotonic_append_right {Op : Type} [BEq Op] [LawfulBEq Op] (input output extra : List Op) (h : isMonotonic input output = true) : isMonotonic input (output ++ extra) = true

theorem KoontzGarboden2009.Monotonicity.identityOp_satisfiesMH {Op : Type} [BEq Op] [LawfulBEq Op] : satisfiesMH identityOp

theorem KoontzGarboden2009.Monotonicity.deleteOp_not_satisfiesMH {Op : Type} [DecidableEq Op] (target : Op) : ¬satisfiesMH (deleteOp target)

theorem KoontzGarboden2009.Monotonicity.satisfiesMH_iff_noRemoval {Op : Type} [BEq Op] [LawfulBEq Op] (f : List Op → List Op) : satisfiesMH f ↔ ∀ (ops : List Op), ∀ x ∈ ops, x ∈ f ops

theorem KoontzGarboden2009.Monotonicity.satisfiesMH_comp {Op : Type} [BEq Op] [LawfulBEq Op] (f g : List Op → List Op) (hf : satisfiesMH f) (hg : satisfiesMH g) : satisfiesMH (g ∘ f)

@cite{koontz-garboden-2009} — Anticausativization

Koontz-Garboden, Andrew. 2009. Anticausativization. Natural Language & Linguistic Theory 27(1): 77–138.

Core thesis

Anticausativization is semantically a reflexivization operation: the reflexive clitic (se, sich, -da, -wa) takes the two-place causative denotation and identifies the EFFECTOR with the THEME. Derived inchoatives retain CAUSE in their lexical semantic representation, contra the deletion analysis (Grimshaw 1982; @cite{krejci-2012}).

Key formal apparatus

• ⟦se⟧ = λℜλx[ℜ(x,x)] — the reflexivization operator
• ⟦romper⟧ = λxλyλsλe[∃v[CAUSE(v,e) ∧ EFFECTOR(v,y) ∧ BECOME(e,s) ∧ THEME(s,x) ∧ not-whole(s)]]
• ⟦romperse⟧ = ⟦se⟧(⟦romper⟧) = λxλsλe[∃v[CAUSE(v,e) ∧ EFFECTOR(v,x) ∧ BECOME(e,s) ∧ THEME(s,x) ∧ not-whole(s)]]

Predictions

1. Only verbs with underspecified causers (EFFECTOR) anticausativize. Verbs with specified causers (AGENT) yield reflexive-only readings.
2. Causative does NOT entail inchoative (the inchoative requires the single argument to be both EFFECTOR and THEME).
3. Derived inchoatives license por sí solo / by itself (because CAUSE is in their denotation).
4. Internally caused COS verbs (empeorar, crecer) lack CAUSE in their LSR and reject por sí solo.

Monotonicity Hypothesis

The Monotonicity Hypothesis (MH) states that word formation operations do not remove operators from lexical semantic representations. The reflexivization analysis preserves the MH; the deletion analysis violates it. Evidence from por sí solo, negation scope, NPI licensing, and the Albanian "feel like" construction independently confirms that derived inchoatives have CAUSE.

Bridges

• CauserSpec (Spanish fragment) — EFFECTOR vs AGENT verb taxonomy
• CausationType.HasCauseInLSR — internally vs externally caused distinction
• IntransitivizationType — competing structural analysis (@cite{krejci-2012})
• reflexivization / decausativization — valency alternation types

The reflexivization operator (eq. 11) = λℜλx[ℜ(x,x)]. It takes a relation as an argument, setting both arguments of the relation to be the same.

In set-theoretic terms: if a relation is a set of pairs,
reflexivization restricts it to those pairs whose members are
identical. 

def KoontzGarboden2009.reflexivize {Entity : Type} (R : Entity → Entity → Prop) : Entity → Prop

Reflexivization of a two-place relation over entities. ⟦se⟧ = λℜλx[ℜ(x,x)]

Equations

• KoontzGarboden2009.reflexivize R x = R x x

def KoontzGarboden2009.reflexivizeBool {Entity : Type} (R : Entity → Entity → Bool) : Entity → Bool

Reflexivization of a Boolean two-place predicate.

Equations

• KoontzGarboden2009.reflexivizeBool R x = R x x

The critical distinction between verbs that anticausativize (romper) and those that do not (asesinar) reduces to the thematic specification of the participant in the causing subevent.

`CauserSpec` from the Spanish fragment encodes this.
The prediction: `reflexivize` applied to an EFFECTOR verb yields
an anticausative reading; applied to an AGENT verb, a reflexive-only
reading. 

def KoontzGarboden2009.reflexivizationYieldsAnticausative : Fragments.Spanish.Predicates.CauserSpec → Bool

Reflexivization of an EFFECTOR verb: the single argument becomes both the undergoer (THEME) and the underspecified causer (EFFECTOR). Because EFFECTOR carries no agent entailments, the result is compatible with inanimate subjects → anticausative reading.

Reflexivization of an AGENT verb: the single argument must be both undergoer and AGENT. AGENT entails volition/sentience → the result requires an animate, agentive subject → reflexive reading only.

Equations

• KoontzGarboden2009.reflexivizationYieldsAnticausative Fragments.Spanish.Predicates.CauserSpec.effector = true
• KoontzGarboden2009.reflexivizationYieldsAnticausative Fragments.Spanish.Predicates.CauserSpec.agent = false

K-G's EFFECTOR/AGENT distinction (@cite{van-valin-wilkins-1996}) partially reduces to @cite{dowty-1991}'s proto-role entailments.

The reduction: EFFECTOR verbs entail causation but NOT volition
for their subject. AGENT verbs entail both. Volition is the
discriminating feature.

Where it reduces: for every Spanish verb with a `causerSpec`,
checking `volition` in the subject's entailment profile yields
the same classification. The alternation prediction chains:
entailment profile → CauserSpec → anticausativization.

Where it doesn't reduce conceptually: K-G's EFFECTOR is defined
by what the verb LACKS (thematic specification of the causer),
while Dowty's system specifies what the verb ENTAILS (individual
proto-role features). These are different theoretical objects that
happen to align for the causative alternation. A hypothetical verb
entailing sentience but not volition for its causer would be
classified as EFFECTOR by `toCauserSpec` — correctly, since it
would still admit non-agentive causers — but its EFFECTOR status
would carry more structure than K-G's underspecification account
predicts. 

def KoontzGarboden2009.toCauserSpec (p : Semantics.ArgumentStructure.EntailmentProfile.EntailmentProfile) : Option Fragments.Spanish.Predicates.CauserSpec

Derive CauserSpec from a proto-role entailment profile. Volition is the discriminating feature:

• volition → AGENT (thematically specified causer)
• causation without volition → EFFECTOR (underspecified causer)
• neither → not a causer at all

Equations

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

theorem KoontzGarboden2009.causerSpec_matches_profile : ((List.filter (fun (v : Fragments.Spanish.Predicates.SpanishVerbEntry) => v.causerSpec.isSome && v.subjectEntailments.isSome) Fragments.Spanish.Predicates.allVerbs).all fun (v : Fragments.Spanish.Predicates.SpanishVerbEntry) => v.subjectEntailments.bind toCauserSpec == v.causerSpec) = true

The derivation matches the stipulated causerSpec for every Spanish verb that has both fields populated.

theorem KoontzGarboden2009.effector_lacks_volition : ((List.filter (fun (v : Fragments.Spanish.Predicates.SpanishVerbEntry) => v.causerSpec == some Fragments.Spanish.Predicates.CauserSpec.effector) Fragments.Spanish.Predicates.allVerbs).all fun (v : Fragments.Spanish.Predicates.SpanishVerbEntry) => Option.map (fun (x : Semantics.ArgumentStructure.EntailmentProfile.EntailmentProfile) => x.volition) v.subjectEntailments == some false) = true

Volition is the discriminating feature: all EFFECTOR verbs have volition = false in their subject profile.

theorem KoontzGarboden2009.agent_has_volition : ((List.filter (fun (v : Fragments.Spanish.Predicates.SpanishVerbEntry) => v.causerSpec == some Fragments.Spanish.Predicates.CauserSpec.agent) Fragments.Spanish.Predicates.allVerbs).all fun (v : Fragments.Spanish.Predicates.SpanishVerbEntry) => Option.map (fun (x : Semantics.ArgumentStructure.EntailmentProfile.EntailmentProfile) => x.volition) v.subjectEntailments == some true) = true

All AGENT verbs have volition = true in their subject profile.

theorem KoontzGarboden2009.both_satisfy_causation : ((List.filter (fun (v : Fragments.Spanish.Predicates.SpanishVerbEntry) => v.causerSpec.isSome) Fragments.Spanish.Predicates.allVerbs).all fun (v : Fragments.Spanish.Predicates.SpanishVerbEntry) => Option.map (fun (x : Semantics.ArgumentStructure.EntailmentProfile.EntailmentProfile) => x.causation) v.subjectEntailments == some true) = true

Both EFFECTOR and AGENT verbs satisfy IsEffector (movement ∨ IE with causation). This is why IsEffector alone cannot distinguish them — it's a necessary but not sufficient condition for K-G's EFFECTOR. The AGENT/EFFECTOR split requires checking volition.

The central empirical prediction: a verb anticausativizes iff its causer is underspecified (EFFECTOR). This is validated against the Spanish fragment data.

theorem KoontzGarboden2009.effector_verbs_alternate : ((List.filter (fun (v : Fragments.Spanish.Predicates.SpanishVerbEntry) => v.causerSpec == some Fragments.Spanish.Predicates.CauserSpec.effector) Fragments.Spanish.Predicates.allVerbs).all fun (x : Fragments.Spanish.Predicates.SpanishVerbEntry) => x.causativeAlternation) = true

All EFFECTOR verbs in the Spanish fragment alternate.

theorem KoontzGarboden2009.agent_verbs_dont_alternate : ((List.filter (fun (v : Fragments.Spanish.Predicates.SpanishVerbEntry) => v.causerSpec == some Fragments.Spanish.Predicates.CauserSpec.agent) Fragments.Spanish.Predicates.allVerbs).all fun (x : Fragments.Spanish.Predicates.SpanishVerbEntry) => !x.causativeAlternation) = true

No AGENT verb in the Spanish fragment alternates.

Contrary to the received wisdom (from @cite{lakoff-1965}), the reflexivization analysis predicts that causative does NOT entail inchoative for derived inchoatives.

Causative *romper*: ∃v[CAUSE(v,e) ∧ EFFECTOR(v,y) ∧ ...]
  — the effector y and undergoer x can be DISTINCT participants.
Inchoative *romperse*: ∃v[CAUSE(v,e) ∧ EFFECTOR(v,x) ∧ ...]
  — the effector and undergoer MUST be the SAME participant.

A causative event where the effector and undergoer are distinct
satisfies the causative but not the inchoative. The Spanish data
in exx. 56–57 confirm this: a causative can be true while the
derived inchoative is denied.

We model this with a minimal 2-entity domain. 

inductive KoontzGarboden2009.SmallEntity : Type

A minimal 2-entity domain for the non-entailment model.

• glass : SmallEntity
• juan : SmallEntity

@[implicit_reducible]

instance KoontzGarboden2009.instDecidableEqSmallEntity : DecidableEq SmallEntity

Equations

• KoontzGarboden2009.instDecidableEqSmallEntity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance KoontzGarboden2009.instReprSmallEntity : Repr SmallEntity

Equations

• KoontzGarboden2009.instReprSmallEntity = { reprPrec := KoontzGarboden2009.instReprSmallEntity.repr }

def KoontzGarboden2009.instReprSmallEntity.repr : SmallEntity → ℕ → Std.Format

Equations

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

def KoontzGarboden2009.breakRelation : SmallEntity → SmallEntity → Bool

A causative relation R(effector, undergoer) representing a specific breaking event: Juan broke the glass. Only the pair (Juan, glass) satisfies the relation.

Equations

• KoontzGarboden2009.breakRelation KoontzGarboden2009.SmallEntity.juan KoontzGarboden2009.SmallEntity.glass = true
• KoontzGarboden2009.breakRelation x✝¹ x✝ = false

theorem KoontzGarboden2009.causative_satisfied : breakRelation SmallEntity.juan SmallEntity.glass = true

The causative is satisfied: Juan broke the glass.

theorem KoontzGarboden2009.inchoative_not_satisfied : reflexivizeBool breakRelation SmallEntity.glass = false

The inchoative denotation is the reflexivization of the causative (§2.2, eq. 19): ⟦se⟧(⟦romper⟧) restricts to the diagonal. The glass is not its own effector in this scenario.

theorem KoontzGarboden2009.causative_does_not_entail_inchoative : breakRelation SmallEntity.juan SmallEntity.glass = true ∧ reflexivizeBool breakRelation SmallEntity.glass = false

Non-entailment derived from reflexivization: there exists a model where the causative is true but the inchoative is false. This follows from the reflexivization operator restricting R to its diagonal — a point (Juan, glass) off the diagonal satisfies the causative but the diagonal point (glass, glass) does not. (exx. 56–57)

por sí solo 'by itself' requires a CAUSE operator in the denotation of the verb it modifies. It is: - Acceptable with derived inchoatives (romperse, abrirse) - Unacceptable with passives (fue hundido 'was sunk') - Unacceptable with statives (saber 'know', ser rojo 'be red') - Unacceptable with internally caused COS verbs (empeorar, crecer)

This diagnostic independently confirms that derived inchoatives
retain CAUSE. 

theorem KoontzGarboden2009.external_has_cause : Features.EventStructure.CausationType.external.HasCauseInLSR

Externally caused COS verbs have CAUSE in their LSR and license por sí solo.

theorem KoontzGarboden2009.internal_no_cause : ¬Features.EventStructure.CausationType.internal.HasCauseInLSR

Internally caused COS verbs lack CAUSE and reject por sí solo.

theorem KoontzGarboden2009.feel_like_requires_cause : Features.EventStructure.CausationType.external.HasCauseInLSR ∧ ¬Features.EventStructure.CausationType.internal.HasCauseInLSR

The Albanian "feel like" construction (§4.2) provides independent evidence: its "unintended cause" reading (Kallulli 2006b) is available only for verbs with CAUSE in their LSR. COS verbs like break get the reading; non-causative verbs like eat do not. This is the same structural property that HasCauseInLSR tests.

The Monotonicity Hypothesis (MH): word formation operations do not remove operators from lexical semantic representations. This is a constraint on the FORM of word formation rules, not on their output.

@cite{koontz-garboden-2009} argues that anticausativization is the
strongest apparent counterexample to the MH, since the deletion
analysis requires removing the CAUSE operator. The reflexivization
analysis resolves this: no operator is deleted, the relation is
simply reflexivized. 

theorem KoontzGarboden2009.reflexivization_satisfiesMH_verbHead : Monotonicity.satisfiesMH Monotonicity.identityOp

On the reflexivization analysis, anticausativization is the identity on operator lists — it satisfies the MH.

theorem KoontzGarboden2009.deletion_of_cause_not_satisfiesMH : ¬Monotonicity.satisfiesMH (Monotonicity.deleteOp Minimalist.VerbHead.vCAUSE)

On the deletion analysis, anticausativization removes vCAUSE — it does not satisfy the MH.

theorem KoontzGarboden2009.reflexivization_monotonic : Monotonicity.isMonotonic [Minimalist.VerbHead.vCAUSE, Minimalist.VerbHead.vGO, Minimalist.VerbHead.vBE] [Minimalist.VerbHead.vCAUSE, Minimalist.VerbHead.vGO, Minimalist.VerbHead.vBE] = true

Concrete instance: the inchoative operator list [vCAUSE, vGO, vBE] is monotonically preserved by reflexivization.

theorem KoontzGarboden2009.deletion_not_monotonic : Monotonicity.isMonotonic [Minimalist.VerbHead.vCAUSE, Minimalist.VerbHead.vGO, Minimalist.VerbHead.vBE] [Minimalist.VerbHead.vGO, Minimalist.VerbHead.vBE] = false

Concrete instance: deleting vCAUSE from the inchoative list breaks monotonicity.

@cite{koontz-garboden-2009}'s core claim is that what @cite{creissels-2025} calls decausativization (A suppressed from participant structure) is semantically reflexivization (A and P cumulated). The structural effect looks like decausativization — the derived construction is intransitive with a single S argument — but the semantic operation is reflexivization of the causative denotation.

On Creissels' framework, reflexivization and decausativization are
distinct: reflexivization cumulates A and P, while decausativization
suppresses A. K-G argues the surface decausativization in languages
with SE-marking is semantically reflexivization. 

theorem KoontzGarboden2009.structural_distinction : Syntax.ArgumentStructure.Alternation.decausativization.fateOfA = Syntax.ArgumentStructure.Alternation.ParticipantFate.suppressed ∧ Syntax.ArgumentStructure.Alternation.reflexivization.fateOfA = Syntax.ArgumentStructure.Alternation.ParticipantFate.cumulated

Decausativization suppresses A; reflexivization cumulates A and P.

theorem KoontzGarboden2009.reflexivization_is_cumulation : Syntax.ArgumentStructure.Alternation.reflexivization.involvesCumulation = true ∧ Syntax.ArgumentStructure.Alternation.decausativization.involvesCumulation = false

K-G's claim: the SE-marked form is semantically reflexivization (cumulation of A and P), not decausativization (suppression of A). The surface effect looks like valency decrease, but the underlying operation is cumulation — both arguments are still semantically present, identified with each other.

@cite{krejci-2012}'s IntransitivizationType.anticausative says the external cause is removed (monoeventive). @cite{koontz-garboden-2009} says it is retained via reflexivization (bieventive). These are competing analyses.

The library now records both. On K-G's analysis, what Krejci calls
"anticausative" is actually a special case of "reflexive" where the
EFFECTOR underspecification makes the reflexive reading look like
an anticausative. 

theorem KoontzGarboden2009.krejci_anticausative_monoeventive : Semantics.Causation.Morphological.IntransitivizationType.anticausative.isBieventive = false

On Krejci's analysis, anticausatives are monoeventive.

theorem KoontzGarboden2009.krejci_reflexive_bieventive : Semantics.Causation.Morphological.IntransitivizationType.reflexive.isBieventive = true

On Krejci's analysis, reflexives are bieventive.

K-G's central claim is that anticausativization IS reflexivization (not deletion): the "anticausative" reading arises from EFFECTOR underspecification, not from a structurally distinct operation. This entails CAUSE retention (so K-G's analysis preserves the Monotonicity Hypothesis), against deletion analyses which violate it. The structural content lives in reflexivize above and the causative_does_not_entail_inchoative theorem below.

Haspelmath (1990): in 9 of 13 languages with anticausative markers, the same marker also serves as a reflexive marker. This is the expected state of affairs if anticausativization IS reflexivization, and would be a remarkable coincidence on any other analysis.

structure KoontzGarboden2009.MarkerSyncretismDatum : Type

Cross-linguistic anticausative/reflexive marker syncretism data from Haspelmath 1990, cited in @cite{koontz-garboden-2009} (35).

• language : String
• hasReflexiveUse : Bool
• hasAnticausativeUse : Bool

@[implicit_reducible]

instance KoontzGarboden2009.instReprMarkerSyncretismDatum : Repr MarkerSyncretismDatum

Equations

• KoontzGarboden2009.instReprMarkerSyncretismDatum = { reprPrec := KoontzGarboden2009.instReprMarkerSyncretismDatum.repr }

def KoontzGarboden2009.instReprMarkerSyncretismDatum.repr : MarkerSyncretismDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KoontzGarboden2009.instBEqMarkerSyncretismDatum : BEq MarkerSyncretismDatum

Equations

• KoontzGarboden2009.instBEqMarkerSyncretismDatum = { beq := KoontzGarboden2009.instBEqMarkerSyncretismDatum.beq }

def KoontzGarboden2009.instBEqMarkerSyncretismDatum.beq : MarkerSyncretismDatum → MarkerSyncretismDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• KoontzGarboden2009.instBEqMarkerSyncretismDatum.beq x✝¹ x✝ = false

def KoontzGarboden2009.haspelmathData : List MarkerSyncretismDatum

Equations

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

theorem KoontzGarboden2009.syncretism_majority : (List.filter (fun (d : MarkerSyncretismDatum) => d.hasReflexiveUse && d.hasAnticausativeUse) haspelmathData).length = 9

9 of 13 languages have syncretism (marker serves both functions).

theorem KoontzGarboden2009.all_have_anticausative : (haspelmathData.all fun (x : MarkerSyncretismDatum) => x.hasAnticausativeUse) = true

All 13 languages have anticausative use (selection criterion).