Cross-Linguistic Verb Infrastructure

Framework-agnostic types for verb semantics: complement type, control type, and the VerbCore structure that bundles all semantic fields shared across languages. Verb classification enums (Causative, Implicative, Attitude, etc.) are in Core/Lexical/VerbClass.lean.

English-specific morphology (3sg, past, participles) lives in Fragments/English/Predicates/Verbal.lean; other languages extend VerbCore with their own inflectional paradigms.

Design

@cite{bale-schwarz-2026} @cite{dayal-2025} @cite{heim-1992} @cite{icard-2012} @cite{kennedy-2007} @cite{maier-2015} @cite{qing-uegaki-2025} @cite{rappaport-hovav-levin-2024} @cite{solstad-bott-2024} @cite{rappaport-hovav-levin-1998}

VerbCore is the semantic spine of a verb entry. It carries:

• Argument structure (theta roles, complement type, control)
• Primitive semantic features (factivity, opacity, speech-act status, …)
• Links to compositional semantics (attitude builder, causative builder, …)

Verb classification (factive, causative, attitude, etc.) is DERIVED from these primitive fields, not stipulated as an enum.

Language-specific fragments extend VerbCore with morphological fields:

• English: form3sg, formPast, formPastPart, formPresPart
• Japanese: form3sg (nonpast), formPast, formGerund, formProgressive
• Mandarin: (none — isolating language)

inductive Semantics.Lexical.VoiceType : Type

Framework-neutral voice type for deriving argument structure properties.

Captures the external-argument dimension of the verb's syntactic frame without committing to a specific syntactic framework. Maps to Minimalist.VoiceFlavor via bridge theorems in interface files.

• agentive: External argument introduced (transitive/unergative)
• nonThematic: No external argument (unaccusative/anticausative)
• expletive: No specifier, no semantics (middle voice)
• reflexive: Agent that binds internal argument (@cite{wood-2015})
• experiencer: Experiencer external argument (@cite{wood-2015})

• agentive : VoiceType
• nonThematic : VoiceType
• expletive : VoiceType
• reflexive : VoiceType
• experiencer : VoiceType

@[implicit_reducible]

instance Semantics.Lexical.instDecidableEqVoiceType : DecidableEq VoiceType

Equations

• Semantics.Lexical.instDecidableEqVoiceType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.Lexical.instReprVoiceType : Repr VoiceType

Equations

• Semantics.Lexical.instReprVoiceType = { reprPrec := Semantics.Lexical.instReprVoiceType.repr }

def Semantics.Lexical.instReprVoiceType.repr : VoiceType → ℕ → Std.Format

Equations

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

def Semantics.Lexical.VoiceType.assignsTheta : VoiceType → Bool

Does this voice type introduce an external argument?

Equations

• Semantics.Lexical.VoiceType.agentive.assignsTheta = true
• Semantics.Lexical.VoiceType.reflexive.assignsTheta = true
• Semantics.Lexical.VoiceType.experiencer.assignsTheta = true
• Semantics.Lexical.VoiceType.nonThematic.assignsTheta = false
• Semantics.Lexical.VoiceType.expletive.assignsTheta = false

inductive Semantics.Lexical.PresupTriggerType : Type

Presupposition trigger type (@cite{tonhauser-beaver-roberts-simons-2013} classification).

• Hard triggers: Always project (too, again, also)
• Soft triggers: Context-sensitive projection (stop, know)

• hardTrigger : PresupTriggerType
• softTrigger : PresupTriggerType
• prerequisiteSoft : PresupTriggerType

@[implicit_reducible]

instance Semantics.Lexical.instDecidableEqPresupTriggerType : DecidableEq PresupTriggerType

Equations

• Semantics.Lexical.instDecidableEqPresupTriggerType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.Lexical.instReprPresupTriggerType : Repr PresupTriggerType

Equations

• Semantics.Lexical.instReprPresupTriggerType = { reprPrec := Semantics.Lexical.instReprPresupTriggerType.repr }

def Semantics.Lexical.instReprPresupTriggerType.repr : PresupTriggerType → ℕ → Std.Format

Equations

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

def Semantics.Lexical.PresupTriggerType.isSoft : PresupTriggerType → Bool

Is this trigger locally accommodatable (soft)? Both factive and prerequisite triggers are soft.

Equations

• Semantics.Lexical.PresupTriggerType.hardTrigger.isSoft = false
• Semantics.Lexical.PresupTriggerType.softTrigger.isSoft = true
• Semantics.Lexical.PresupTriggerType.prerequisiteSoft.isSoft = true

inductive Semantics.Lexical.PostsupType : Type

Postsupposition type: output-context constraint distinct from presuppositions.

@cite{glass-2025} argues that Mandarin yǐwéi has a postsupposition ◇¬p — after accepting "x yǐwéi p", the CG must be compatible with ¬p. This cannot be derived from veridicality alone.

The concrete Core.Postsupposition.Postsupposition W is parameterized by the world type; this enum is the world-type-independent tag stored in VerbCore.

• weakContrafactive : PostsupType

  Output context must be compatible with ¬p: ◇¬p (@cite{glass-2025}).

• strongContrafactive : PostsupType

  Output context must entail ¬p: ⊨¬p (hypothetical, UNATTESTED).

@[implicit_reducible]

instance Semantics.Lexical.instDecidableEqPostsupType : DecidableEq PostsupType

Equations

• Semantics.Lexical.instDecidableEqPostsupType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.Lexical.instReprPostsupType : Repr PostsupType

Equations

• Semantics.Lexical.instReprPostsupType = { reprPrec := Semantics.Lexical.instReprPostsupType.repr }

def Semantics.Lexical.instReprPostsupType.repr : PostsupType → ℕ → Std.Format

Equations

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

inductive Semantics.Lexical.ProjectionBehavior : Type

Complement presupposition projection behavior (@cite{karttunen-1973}).

Orthogonal to PresupTriggerType (whether the verb triggers presuppositions): this classifies what the verb does with presuppositions of its complement.

• plug: blocks all complement presuppositions (say, tell, promise)
• hole: lets all complement presuppositions project (know, regret, stop)
• filter: conditionally cancels some complement presuppositions (if...then, and, or)

• plug : ProjectionBehavior
• hole : ProjectionBehavior
• filter : ProjectionBehavior

@[implicit_reducible]

instance Semantics.Lexical.instDecidableEqProjectionBehavior : DecidableEq ProjectionBehavior

Equations

• Semantics.Lexical.instDecidableEqProjectionBehavior x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.Lexical.instReprProjectionBehavior : Repr ProjectionBehavior

Equations

• Semantics.Lexical.instReprProjectionBehavior = { reprPrec := Semantics.Lexical.instReprProjectionBehavior.repr }

def Semantics.Lexical.instReprProjectionBehavior.repr : ProjectionBehavior → ℕ → Std.Format

Equations

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

inductive Semantics.Lexical.SenseTag : Type

Disambiguates polysemous verb entries that share a citation form.

When a verb has multiple lexical entries (e.g., "remember" as implicative vs. "remember" as factive question-embedding), the SenseTag records why multiple entries exist:

• .default: primary/unmarked sense
• .rogative: question-embedding sense
• .causative: causative use of otherwise non-causative verb
• .instrumental: instrument-specific sense
• .occasion: occasion verb sense with experiencer subject

• default : SenseTag
• rogative : SenseTag
• causative : SenseTag
• instrumental : SenseTag
• occasion : SenseTag
• stative : SenseTag

@[implicit_reducible]

instance Semantics.Lexical.instDecidableEqSenseTag : DecidableEq SenseTag

Equations

• Semantics.Lexical.instDecidableEqSenseTag x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.Lexical.instReprSenseTag : Repr SenseTag

Equations

• Semantics.Lexical.instReprSenseTag = { reprPrec := Semantics.Lexical.instReprSenseTag.repr }

def Semantics.Lexical.instReprSenseTag.repr : SenseTag → ℕ → Std.Format

Equations

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

inductive Semantics.Lexical.ComplementType : Type

Complement type that the verb selects.

• Finite: "that" clauses ("John knows that Mary left")
• Infinitival: "to" complements ("John managed to leave")
• Gerund: "-ing" complements ("John stopped smoking")
• NP: Direct object ("John kicked the ball")
• None: Intransitive ("John slept")

• none : ComplementType
• np : ComplementType
• np_np : ComplementType
• np_pp : ComplementType
• finiteClause : ComplementType
• infinitival : ComplementType
• gerund : ComplementType
• smallClause : ComplementType
• question : ComplementType

@[implicit_reducible]

instance Semantics.Lexical.instDecidableEqComplementType : DecidableEq ComplementType

Equations

• Semantics.Lexical.instDecidableEqComplementType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.Lexical.instReprComplementType : Repr ComplementType

Equations

• Semantics.Lexical.instReprComplementType = { reprPrec := Semantics.Lexical.instReprComplementType.repr }

def Semantics.Lexical.instReprComplementType.repr : ComplementType → ℕ → Std.Format

Equations

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

def Semantics.Lexical.ComplementType.isFinite : ComplementType → Bool

Is this complement type finite (i.e., does it contain a tense head)?

Finite complements (.finiteClause,.question) have independent tense morphology; non-finite complements (.infinitival,.gerund,.smallClause) do not.

Equations

• Semantics.Lexical.ComplementType.finiteClause.isFinite = true
• Semantics.Lexical.ComplementType.question.isFinite = true
• x✝.isFinite = false

def Semantics.Lexical.ComplementType.isNominal : ComplementType → Bool

Is this complement type a nominal (DP) argument?

Nominal complements project DP: the verb selects a noun phrase in object position. Relevant to c-selection in coordination: a verb that only selects nominal complements cannot independently license a CP conjunct (@cite{schwarzer-2026}).

Equations

• Semantics.Lexical.ComplementType.np.isNominal = true
• Semantics.Lexical.ComplementType.np_np.isNominal = true
• Semantics.Lexical.ComplementType.np_pp.isNominal = true
• x✝.isNominal = false

def Semantics.Lexical.ComplementType.isClausal : ComplementType → Bool

Is this complement type a clausal (CP) argument?

Clausal complements project CP or reduced clausal structure. This covers finite clauses (dass-clauses), infinitivals, gerunds, small clauses, and embedded questions.

Equations

• Semantics.Lexical.ComplementType.finiteClause.isClausal = true
• Semantics.Lexical.ComplementType.infinitival.isClausal = true
• Semantics.Lexical.ComplementType.gerund.isClausal = true
• Semantics.Lexical.ComplementType.smallClause.isClausal = true
• Semantics.Lexical.ComplementType.question.isClausal = true
• x✝.isClausal = false

inductive Semantics.Lexical.ControlType : Type

Control type for verbs with infinitival complements.

• subjectControl : ControlType
• objectControl : ControlType
• raising : ControlType
• none : ControlType

@[implicit_reducible]

instance Semantics.Lexical.instDecidableEqControlType : DecidableEq ControlType

Equations

• Semantics.Lexical.instDecidableEqControlType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.Lexical.instReprControlType : Repr ControlType

Equations

• Semantics.Lexical.instReprControlType = { reprPrec := Semantics.Lexical.instReprControlType.repr }

def Semantics.Lexical.instReprControlType.repr : ControlType → ℕ → Std.Format

Equations

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

inductive Semantics.Lexical.ImplicitInterp : Type

Interpretation of an implicit (unexpressed) argument.

Cross-linguistic: applies to any argument position where the verb allows the argument to be absent. The distinction captures whether the missing referent must be pragmatically recoverable (definite) or can be unspecified (indefinite). @cite{bruening-2021}, @cite{fillmore-1986}.

• indef : ImplicitInterp
• def : ImplicitInterp

@[implicit_reducible]

instance Semantics.Lexical.instDecidableEqImplicitInterp : DecidableEq ImplicitInterp

Equations

• Semantics.Lexical.instDecidableEqImplicitInterp x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.Lexical.instReprImplicitInterp : Repr ImplicitInterp

Equations

• Semantics.Lexical.instReprImplicitInterp = { reprPrec := Semantics.Lexical.instReprImplicitInterp.repr }

def Semantics.Lexical.instReprImplicitInterp.repr : ImplicitInterp → ℕ → Std.Format

Equations

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

structure Semantics.Lexical.VerbCore : Type

Cross-linguistic verb core: all semantic fields shared across languages.

Bundles argument structure, semantic class, and links to compositional semantics. Language-specific fragments extend this with morphological fields appropriate to their inflectional system.

• form : String

  Citation form (cross-linguistic)

• complementType : ComplementType

  What complement does the verb select?

• subjectEntailments : Option ArgumentStructure.EntailmentProfile.EntailmentProfile

  Proto-role entailment profile for the subject (external argument). The authoritative representation of argument semantics (@cite{dowty-1991}, @cite{grimm-2011}, @cite{levin-2019}). Convenience role labels can be derived via EntailmentProfile.toRole.

• objectEntailments : Option ArgumentStructure.EntailmentProfile.EntailmentProfile

  Proto-role entailment profile for the first object (internal argument).

• controlType : ControlType

  Control type for infinitival complements

• altComplementType : Option ComplementType

  Alternate complement frame, for verbs with two complement types. E.g., "hope" primarily takes.finiteClause ("hope that...") but also takes.infinitival ("hope to...") with subject control. When set, altControlType specifies the control type for this frame.

• altControlType : ControlType

  Control type for the alternate complement frame.

• unaccusative : Bool

  Is the verb unaccusative? (subject is underlying object) When voiceType is present, prefer derivedUnaccusative which derives this from Voice selection (@cite{kratzer-1996}).

• voiceType : Option VoiceType

  Framework-neutral voice type: determines whether an external argument is introduced. When set, derivedUnaccusative derives unaccusativity from this field, connecting the Fragment entry to Voice theory.

• passivizable : Bool

  Can the verb passivize?

• implicitObj : Option ImplicitInterp

  Can the direct object (theme/patient) be left unexpressed? Applies to monotransitives (eat vs devour) and the theme of ditransitives. none = object always required.

• implicitGoal : Option ImplicitInterp

  Can the goal/recipient argument be left unexpressed? Applies to the IO of double object constructions and the PP of dative frames. none = goal always required.

• speechActVerb : Bool

  Does the verb denote the performance of an illocutionary act? True for speech-act verbs (say, tell, claim, ask). This is a genuine semantic primitive that cannot be derived from other fields.

• vendlerClass : Option Features.VendlerClass

  @cite{vendler-1957} aspectual class of the verb's base VP. For verbs whose class depends on the object NP (eat apples = activity, eat two apples = accomplishment), record the class with a quantized (bounded) object. none for verbs where Vendler class is inapplicable (e.g., clause-embedding verbs).

• degreeAchievementScale : Option Features.DegreeAchievement.DegreeAchievementScale

  For degree achievements: the scale structure from which default vendlerClass is derived. When present, vendlerClass should agree with degreeAchievementScale.defaultVendlerClass.

• verbIncClass : Option Aspect.Incremental.VerbIncClass

  @cite{krifka-1998} incrementality class of the object/theme role. .sinc = strictly incremental (eat, build); .inc = incremental with backups (read); .cumOnly = cumulative only (push, carry). none for intransitives and clause-embedding verbs.

• presupType : Option PresupTriggerType

  Is the verb a presupposition trigger?

• postsupType : Option PostsupType

  Output-context constraint (postsupposition), distinct from presuppositions. @cite{glass-2025}: yǐwéi has ◇¬p postsupposition.

• projectionBehavior : Option ProjectionBehavior

  How does the verb treat presuppositions of its complement? Orthogonal to presupType. @cite{karttunen-1973}

• selectsDimension : Option Features.Dimension.Dimension

  For measure predicates: which dimension this verb selects for. Determines per-phrase interpretation: simplex dimension → compositional, quotient → math speak.

• cosType : Option Features.ChangeOfState.CoSType

  For CoS verbs: which type (cessation, inception, continuation)?

• implicative : Option Features.Implicative

  For implicative verbs: complement entailment polarity (links to compositional semantics).

• causative : Option Features.Causative

  For causative verbs: force-dynamic mechanism (links to compositional semantics).

• causalSource : Option Causation.Psych.CausalSource

  Source of causation for psych causatives (@cite{kim-2024} UPH). .external = mind-external percept, .internal = mind-internal representation.

• opaqueContext : Bool

  Does the verb create an opaque context for its complement?

• attitude : Option Features.Attitude

  Unified attitude classification covering doxastic and preferential attitudes. Theoretical properties (C-distributivity, parasitic, etc.) are DERIVED.

• takesQuestionBase : Bool

  For non-preferential question-embedding verbs (know, wonder, ask)

• complementSig : Option Core.NaturalLogic.EntailmentSig

  Entailment signature of the complement position. Classifies this verb's monotonicity w.r.t. its clausal complement. .mono = upward monotone (believe, know); .mult = multiplicative only (be surprised). Used to derive conjunction distribution and neg-raising. See @cite{bondarenko-elliott-2026}.

• senseTag : SenseTag

  Disambiguates entries that share a citation form. Most verbs use .default; polysemous entries use descriptive tags.

• levinClass : Option LevinClass

  @cite{levin-1993} verb class (§§ 9–57).

• rootProfile : Option Roots.RootProfile

  Root-specific quality dimensions (within-class variation).

@[implicit_reducible]

instance Semantics.Lexical.instReprVerbCore : Repr VerbCore

Equations

• Semantics.Lexical.instReprVerbCore = { reprPrec := Semantics.Lexical.instReprVerbCore.repr }

def Semantics.Lexical.instReprVerbCore.repr : VerbCore → ℕ → Std.Format

Equations

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

def Semantics.Lexical.instBEqVerbCore.beq : VerbCore → VerbCore → Bool

Equations

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

@[implicit_reducible]

instance Semantics.Lexical.instBEqVerbCore : BEq VerbCore

Equations

• Semantics.Lexical.instBEqVerbCore = { beq := Semantics.Lexical.instBEqVerbCore.beq }

def Semantics.Lexical.VerbCore.derivedUnaccusative (v : VerbCore) : Bool

Derive unaccusativity from voice type when present, falling back to the stored unaccusative field. A verb is unaccusative iff its Voice does not introduce an external argument (@cite{kratzer-1996}).

Equations

• v.derivedUnaccusative = match v.voiceType with | some vt => !vt.assignsTheta | none => v.unaccusative

def Semantics.Lexical.VerbCore.derivedVendlerClass (v : VerbCore) : Option Features.VendlerClass

Derive vendlerClass from degreeAchievementScale if present. Falls back to the stipulated vendlerClass field.

Equations

• v.derivedVendlerClass = (v.vendlerClass <|> Option.map (fun (x : Features.DegreeAchievement.DegreeAchievementScale) => x.defaultVendlerClass) v.degreeAchievementScale)

def Semantics.Lexical.VerbCore.effectiveSubjectEntailments (v : VerbCore) : Option ArgumentStructure.EntailmentProfile.EntailmentProfile

Effective subject entailment profile: verb-level override if present, otherwise falls back to the Levin class–level profile (@cite{levin-1993}, @cite{dowty-1991}).

Equations

• v.effectiveSubjectEntailments = (v.subjectEntailments <|> v.levinClass.bind fun (x : Semantics.Lexical.LevinClass) => x.subjectProfile)

def Semantics.Lexical.VerbCore.effectiveObjectEntailments (v : VerbCore) : Option ArgumentStructure.EntailmentProfile.EntailmentProfile

Effective object entailment profile: verb-level override if present, otherwise falls back to the Levin class–level profile.

Equations

• v.effectiveObjectEntailments = (v.objectEntailments <|> v.levinClass.bind fun (x : Semantics.Lexical.LevinClass) => x.objectProfile)

def Semantics.Lexical.VerbCore.veridicality (v : VerbCore) : Option Features.Veridicality

Veridicality is DERIVED from the attitude builder

Equations

• v.veridicality = Option.map (fun (x : Features.Attitude) => x.veridicality) v.attitude

def Semantics.Lexical.VerbCore.isDoxastic (v : VerbCore) : Bool

Is this verb a doxastic attitude?

Equations

• v.isDoxastic = (Option.map (fun (x : Features.Attitude) => x.isDoxastic) v.attitude).getD false

def Semantics.Lexical.VerbCore.isPreferential (v : VerbCore) : Bool

Is this verb a preferential attitude?

Equations

• v.isPreferential = (Option.map (fun (x : Features.Attitude) => x.isPreferential) v.attitude).getD false

def Semantics.Lexical.VerbCore.distribOverConj (v : VerbCore) : Bool

Does this attitude distribute over conjunction? DERIVED from complementSig: any signature that refines .mono (mono, additive, mult, addMult, all) distributes.

Equations

• v.distribOverConj = (Option.map (fun (s : Core.NaturalLogic.EntailmentSig) => decide (s ≤ Core.NaturalLogic.EntailmentSig.mono)) v.complementSig).getD false

def Semantics.Lexical.VerbCore.isComplementUE (v : VerbCore) : Bool

Is the complement position upward-entailing? DERIVED from complementSig.

Equations

• v.isComplementUE = (Option.map (fun (s : Core.NaturalLogic.EntailmentSig) => decide (s ≤ Core.NaturalLogic.EntailmentSig.mono)) v.complementSig).getD false

def Semantics.Lexical.VerbCore.preferentialValence (v : VerbCore) : Option Features.AttitudeValence

Valence is DERIVED from the attitude builder (for preferential attitudes)

Equations

• v.preferentialValence = v.attitude.bind fun (x : Features.Attitude) => x.valence

def Semantics.Lexical.VerbCore.getCoSSemantics {W : Type u_1} (v : VerbCore) (P : W → Prop) : Option (Core.Presupposition.PrProp W)

Get the CoS semantics for a verb (if it's a CoS verb).

Returns some (cosSemantics t P) if the verb has a CoS type, where P is the activity predicate (complement denotation).

Equations

• v.getCoSSemantics P = Option.map (fun (t : Features.ChangeOfState.CoSType) => Features.ChangeOfState.cosSemantics t P) v.cosType

def Semantics.Lexical.VerbCore.factivePresup (v : VerbCore) : Bool

Does this verb presuppose its complement via factivity? DERIVED from attitude: true iff the verb is doxastic veridical.

Equations

• v.factivePresup = match v.attitude with | some (Features.Attitude.doxastic Features.Veridicality.veridical) => true | x => false

def Semantics.Lexical.VerbCore.presupposesComplement (v : VerbCore) : Bool

Does this verb presuppose its complement?

Equations

• v.presupposesComplement = (v.factivePresup || v.cosType.isSome)

def Semantics.Lexical.VerbCore.isPresupTrigger (v : VerbCore) : Bool

Is this verb a presupposition trigger?

Equations

• v.isPresupTrigger = v.presupType.isSome

def Semantics.Lexical.VerbCore.hasPostsupposition (v : VerbCore) : Bool

Does this verb have a postsupposition (output-context constraint)? DERIVED from postsupType.

Equations

• v.hasPostsupposition = v.postsupType.isSome

def Semantics.Lexical.VerbCore.derivedPresupType (v : VerbCore) : Option PresupTriggerType

Presupposition trigger type DERIVED from event structure rather than stipulated. @cite{roberts-simons-2024} argue that presupposition status follows from a verb's event structure (factivity, CoS type), not from a lexically specified trigger type. This accessor derives the prediction: verbs with factive or CoS event structure are presupposition triggers.

Note: R&S (p. 705) argue that the soft/hard trigger distinction "has never been clearly operationalized." We use .softTrigger here as a placeholder, not as an endorsement of a binary soft/hard taxonomy.

Equations

• v.derivedPresupType = if v.presupposesComplement = true then some Semantics.Lexical.PresupTriggerType.softTrigger else none

def Semantics.Lexical.VerbCore.isCausative (v : VerbCore) : Bool

Is this verb a causative? DERIVED from causative field.

Equations

• v.isCausative = v.causative.isSome

def Semantics.Lexical.VerbCore.assertsSufficiency (v : VerbCore) : Bool

Does this causative verb assert sufficiency (like "make")?

DERIVED: delegates to Causative.assertsSufficiency.

Equations

• v.assertsSufficiency = (Option.map (fun (x : Features.Causative) => x.assertsSufficiency) v.causative).getD false

def Semantics.Lexical.VerbCore.predictedSubjectTheta (v : VerbCore) : Option ThetaRole

Lexicalist prediction of the external argument's theta role (@cite{levin-1993}, @cite{rappaport-hovav-levin-1998}), based solely on verb-internal properties.

The cascade mirrors traditional linking rules:

• raising / weather → no external role
• external causal source → stimulus (Class II psych, @cite{kim-2024})
• attitude builder or factive presupposition → experiencer
• occasion sense (manage-to) → experiencer
• Levin class flinch / learn → experiencer
• unaccusative / measure → theme
• default → agent

Contrasts with the Kratzer severing prediction (VoiceFlavor.thetaRole), which derives the role from Voice flavor rather than verb-internal semantics. Studies comparing the two accounts can apply both to the same VerbCore and inspect divergence.

Equations

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

def Semantics.Lexical.VerbCore.isENTrigger (v : VerbCore) : Bool

Does this verb's semantics predict it is an expletive negation trigger?

DERIVED from attitude, implicative, and causative builders. Captures the propositional attitude licensing condition from @cite{jin-koenig-2021} §5.5, ex. 13a:

• FEAR class: negative-valence preferential attitudes activate p (feared content) and ¬p (desired alternative).
• FORGET class: negative implicative verbs entail ¬p in w₀.
• STOP/PREVENT: causative preventatives entail ¬p in w₀.

DENY class triggers (doubt, question) are excluded — their EN-triggering requires matrix negation/questioning (pragmatic, via neg-raising), not purely lexical semantics. Temporal, logical, and comparative triggers are operators/connectives, not verbs.

Equations

• v.isENTrigger = (v.preferentialValence == some Features.AttitudeValence.negative || v.implicative == some Features.Implicative.negative || v.causative == some Features.Causative.prevent)

def Semantics.Lexical.VerbCore.assertsNecessity (v : VerbCore) : Bool

Does this causative verb assert necessity (like "cause")?

DERIVED: delegates to Causative.assertsNecessity.

Equations

• v.assertsNecessity = (Option.map (fun (x : Features.Causative) => x.assertsNecessity) v.causative).getD false

def Semantics.Lexical.VerbCore.entailsComplement (v : VerbCore) : Option Bool

Does success of this implicative verb entail the complement?

DERIVED: delegates to Implicative.entailsComplement. Returns some true for positive implicatives (manage, remember), some false for negative (fail, forget), none for non-implicatives.

Equations

• v.entailsComplement = Option.map (fun (x : Features.Implicative) => x.entailsComplement) v.implicative

def Semantics.Lexical.VerbCore.isPreferentialAttitude (v : VerbCore) : Bool

Is this verb a preferential attitude predicate?

Equations

• v.isPreferentialAttitude = v.preferentialValence.isSome

def Semantics.Lexical.complementToValence : ComplementType → Valence

Map complement type to syntactic valence. Clause-embedding types (.finiteClause,.infinitival,.gerund,.question, .smallClause) map to .clausal — they take xcomp/ccomp, not obj. checkVerbSubcat skips .clausal verbs (their frames require different validation than NP-argument counting).

Equations

• Semantics.Lexical.complementToValence Semantics.Lexical.ComplementType.none = Valence.intransitive
• Semantics.Lexical.complementToValence Semantics.Lexical.ComplementType.np = Valence.transitive
• Semantics.Lexical.complementToValence Semantics.Lexical.ComplementType.np_np = Valence.ditransitive
• Semantics.Lexical.complementToValence Semantics.Lexical.ComplementType.np_pp = Valence.locative
• Semantics.Lexical.complementToValence x✝ = Valence.clausal

def Semantics.Lexical.VerbCore.canTakeClausalComplement (v : VerbCore) : Bool

Can this verb take a clausal (CP) complement?

Checks both primary and alternate complement frames. Used to classify verbs as CP-selecting vs non-CP-selecting for coordination studies (@cite{schwarzer-2026}).

Equations

• v.canTakeClausalComplement = (v.complementType.isClausal || match v.altComplementType with | some ct => ct.isClausal | none => false)

def Semantics.Lexical.VerbCore.canTakeNominalComplement (v : VerbCore) : Bool

Can this verb take a nominal (DP) complement?

Checks both primary and alternate complement frames.

Equations

• v.canTakeNominalComplement = (v.complementType.isNominal || match v.altComplementType with | some ct => ct.isNominal | none => false)

def Semantics.Lexical.lookupSense (verbs : List VerbCore) (form : String) (tag : SenseTag := SenseTag.default) : Option VerbCore

Look up a verb core by citation form and sense tag.

Equations

• Semantics.Lexical.lookupSense verbs form tag = List.find? (fun (v : Semantics.Lexical.VerbCore) => v.form == form && v.senseTag == tag) verbs