Spanish Verb Entries for the Causative Alternation

@cite{cuervo-2003} @cite{munoz-perez-2026}

Verbs from Muñoz @cite{munoz-perez-2026} classified by anticausative marking (SE) and event-structural decomposition. The key empirical generalization: stylistic LE is licensed only by verbs with inchoative structure (vGO ∧ vBE) that require SE-marking.

Anticausative Marking Types

• Marked: Anticausative requires SE (quebrar → quebrarse)
• Unmarked: No SE in anticausative (mejorar → mejorar)
• Optional: SE is marginal (hervir → ?hervirse)

inductive Fragments.Spanish.Predicates.AnticausativeMarking : Type

How an anticausative verb is morphologically marked in Spanish.

• marked : AnticausativeMarking
• unmarked : AnticausativeMarking
• optional : AnticausativeMarking

instance Fragments.Spanish.Predicates.instDecidableEqAnticausativeMarking : DecidableEq AnticausativeMarking

Equations

• Fragments.Spanish.Predicates.instDecidableEqAnticausativeMarking x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Fragments.Spanish.Predicates.instBEqAnticausativeMarking.beq : AnticausativeMarking → AnticausativeMarking → Bool

Equations

• Fragments.Spanish.Predicates.instBEqAnticausativeMarking.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Spanish.Predicates.instBEqAnticausativeMarking : BEq AnticausativeMarking

Equations

• Fragments.Spanish.Predicates.instBEqAnticausativeMarking = { beq := Fragments.Spanish.Predicates.instBEqAnticausativeMarking.beq }

instance Fragments.Spanish.Predicates.instReprAnticausativeMarking : Repr AnticausativeMarking

Equations

• Fragments.Spanish.Predicates.instReprAnticausativeMarking = { reprPrec := Fragments.Spanish.Predicates.instReprAnticausativeMarking.repr }

def Fragments.Spanish.Predicates.instReprAnticausativeMarking.repr : AnticausativeMarking → ℕ → Std.Format

Equations

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

structure Fragments.Spanish.Predicates.SpanishVerbEntryextends Core.Verbs.VerbCore : Type

A Spanish verb with its causative alternation properties.

Extends VerbCore with Spanish-specific fields for anticausative marking and event-structural decomposition.

• form : String
• complementType : ComplementType
• subjectEntailments : Option Semantics.Lexical.Verb.EntailmentProfile.EntailmentProfile
• objectEntailments : Option Semantics.Lexical.Verb.EntailmentProfile.EntailmentProfile
• controlType : ControlType
• altComplementType : Option ComplementType
• altControlType : ControlType
• unaccusative : Bool
• voiceType : Option VoiceType
• passivizable : Bool
• implicitObj : Option ImplicitInterp
• implicitGoal : Option ImplicitInterp
• speechActVerb : Bool
• vendlerClass : Option Semantics.Tense.Aspect.LexicalAspect.VendlerClass
• degreeAchievementScale : Option Semantics.Lexical.Verb.DegreeAchievement.DegreeAchievementScale
• verbIncClass : Option Semantics.Events.Krifka1998.VerbIncClass
• presupType : Option PresupTriggerType
• projectionBehavior : Option ProjectionBehavior
• selectsDimension : Option Semantics.Probabilistic.Measurement.Dimension
• cosType : Option Semantics.Lexical.Verb.ChangeOfState.CoSType
• implicativeBuilder : Option Nadathur2024.Implicative.ImplicativeBuilder
• causativeBuilder : Option NadathurLauer2020.CausativeBuilder
• causalSource : Option Semantics.Causation.PsychCausation.CausalSource
• opaqueContext : Bool
• attitudeBuilder : Option AttitudeBuilder
• takesQuestionBase : Bool
• complementSig : Option NaturalLogic.EntailmentSig
• senseTag : SenseTag
• levinClass : Option LevinClass
• rootProfile : Option RootProfile
• anticausativeMarking : AnticausativeMarking

  How the anticausative is marked

• causativeAlternation : Bool

  Participates in causative/anticausative alternation

• verbHead : List Minimalism.VerbHead

  Cuervo's decomposition of the inchoative form

• licensesStylLE : Bool

  Empirical: does this verb license stylistic LE?

def Fragments.Spanish.Predicates.instReprSpanishVerbEntry.repr : SpanishVerbEntry → ℕ → Std.Format

Equations

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

instance Fragments.Spanish.Predicates.instReprSpanishVerbEntry : Repr SpanishVerbEntry

Equations

• Fragments.Spanish.Predicates.instReprSpanishVerbEntry = { reprPrec := Fragments.Spanish.Predicates.instReprSpanishVerbEntry.repr }

instance Fragments.Spanish.Predicates.instBEqSpanishVerbEntry : BEq SpanishVerbEntry

Equations

• Fragments.Spanish.Predicates.instBEqSpanishVerbEntry = { beq := Fragments.Spanish.Predicates.instBEqSpanishVerbEntry.beq }

def Fragments.Spanish.Predicates.instBEqSpanishVerbEntry.beq : SpanishVerbEntry → SpanishVerbEntry → Bool

Equations

• One or more equations did not get rendered due to their size.
• Fragments.Spanish.Predicates.instBEqSpanishVerbEntry.beq x✝¹ x✝ = false

def Fragments.Spanish.Predicates.abrir : SpanishVerbEntry

abrir "open" — marked anticausative, licenses stylistic LE.

Equations

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

def Fragments.Spanish.Predicates.romper : SpanishVerbEntry

romper "break" — marked anticausative, licenses stylistic LE. (exx. 7–8 in Muñoz @cite{munoz-perez-2026})

Equations

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

def Fragments.Spanish.Predicates.hundir : SpanishVerbEntry

hundir "sink" — marked anticausative, licenses stylistic LE. (exx. 9–10)

Equations

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

def Fragments.Spanish.Predicates.caer : SpanishVerbEntry

caer "fall" — marked anticausative, licenses stylistic LE. (exx. 11–12, unaccusative)

Equations

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

def Fragments.Spanish.Predicates.morir : SpanishVerbEntry

morir "die" — marked anticausative, licenses stylistic LE. (exx. 13–14)

Equations

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

def Fragments.Spanish.Predicates.quebrar : SpanishVerbEntry

quebrar "crack" — marked anticausative, licenses stylistic LE. (ex. 39a)

Equations

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

def Fragments.Spanish.Predicates.hervir : SpanishVerbEntry

hervir "boil" — optional SE marking, but still licenses stylistic LE. (ex. 40)

Equations

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

def Fragments.Spanish.Predicates.olvidar : SpanishVerbEntry

olvidar "forget" — marked anticausative, licenses stylistic LE. (exx. 15–16, psych verb)

Equations

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

def Fragments.Spanish.Predicates.ocurrir : SpanishVerbEntry

ocurrir "occur" — marked anticausative, licenses stylistic LE. (exx. 17–18)

Equations

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

def Fragments.Spanish.Predicates.mejorar : SpanishVerbEntry

mejorar "improve" — UNMARKED anticausative, does NOT license stylistic LE. (ex. 39b)

Equations

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

def Fragments.Spanish.Predicates.rasgar : SpanishVerbEntry

rasgar "tear (gash-like)" — Levin 45.1 equivalent; marked anticausative. Unlike English tear, rasgar requires flimsy/insubstantial patients and implies unidirectional (linear, gash-like) separation. Incompatible with careful controlled action. @cite{spalek-mcnally-2026} (§3.2).

Equations

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

def Fragments.Spanish.Predicates.allVerbs : List SpanishVerbEntry

All verb entries in the fragment.

Equations

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

theorem Fragments.Spanish.Predicates.abrir_licenses_stylLE : abrir.licensesStylLE = true

theorem Fragments.Spanish.Predicates.romper_licenses_stylLE : romper.licensesStylLE = true

theorem Fragments.Spanish.Predicates.hundir_licenses_stylLE : hundir.licensesStylLE = true

theorem Fragments.Spanish.Predicates.caer_licenses_stylLE : caer.licensesStylLE = true

theorem Fragments.Spanish.Predicates.morir_licenses_stylLE : morir.licensesStylLE = true

theorem Fragments.Spanish.Predicates.quebrar_licenses_stylLE : quebrar.licensesStylLE = true

theorem Fragments.Spanish.Predicates.hervir_licenses_stylLE : hervir.licensesStylLE = true

theorem Fragments.Spanish.Predicates.olvidar_licenses_stylLE : olvidar.licensesStylLE = true

theorem Fragments.Spanish.Predicates.ocurrir_licenses_stylLE : ocurrir.licensesStylLE = true

theorem Fragments.Spanish.Predicates.mejorar_blocks_stylLE : mejorar.licensesStylLE = false

theorem Fragments.Spanish.Predicates.stylLE_verbs_are_inchoative : ((List.filter (fun (x : SpanishVerbEntry) => x.licensesStylLE) allVerbs).all fun (v : SpanishVerbEntry) => Minimalism.isInchoative v.verbHead) = true

All verbs that license stylistic LE are inchoative.

theorem Fragments.Spanish.Predicates.blocking_verb_is_unmarked : ((List.filter (fun (x : SpanishVerbEntry) => !x.licensesStylLE) allVerbs).all fun (v : SpanishVerbEntry) => v.anticausativeMarking == AnticausativeMarking.unmarked) = true

The only verb that blocks stylistic LE is unmarked.