Documentation

Linglib.Theories.Semantics.Lexical.Verb.VerbEntry

Cross-Linguistic Verb Infrastructure #

Framework-agnostic types for verb semantics: complement type, control type, attitude/causative builders, and the VerbCore structure that bundles all semantic fields shared across languages.

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 Core.Verbs.VoiceType :

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 Minimalism.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

Instances For

instance Core.Verbs.instDecidableEqVoiceType :

DecidableEq VoiceType

Equations

Core.Verbs.instDecidableEqVoiceType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Verbs.instBEqVoiceType.beq :

VoiceType → VoiceType → Bool

Equations

Core.Verbs.instBEqVoiceType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Core.Verbs.instBEqVoiceType :

Equations

Core.Verbs.instBEqVoiceType = { beq := Core.Verbs.instBEqVoiceType.beq }

instance Core.Verbs.instReprVoiceType :

Equations

Core.Verbs.instReprVoiceType = { reprPrec := Core.Verbs.instReprVoiceType.repr }

def Core.Verbs.instReprVoiceType.repr :

VoiceType → ℕ → Std.Format

Equations

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

Instances For

def Core.Verbs.VoiceType.assignsTheta :

VoiceType → Bool

Does this voice type introduce an external argument?

Equations

Instances For

inductive Core.Verbs.PreferentialBuilder :

Which Montague predicate builder this verb uses.

This links the Fragment entry to the compositional semantics in Semantics.Attitudes.Preferential. Properties like C-distributivity are DERIVED from the builder via theorems, not stipulated.

degreeComparison: Uses mkDegreeComparisonPredicate → C-distributive (PROVED)
uncertaintyBased: Uses worry constructor → NOT C-distributive (PROVED)
relevanceBased: Uses qidai constructor → NOT C-distributive

The connection to Montague is:

degreeComparison.positive → Preferential.hope, Preferential.expect, etc.
degreeComparison.negative → Preferential.fear, Preferential.dread
uncertaintyBased → Preferential.worry
relevanceBased.positive → Preferential.qidai

degreeComparison (valence : Semantics.Attitudes.Preferential.AttitudeValence) : PreferentialBuilder
Degree comparison semantics: ⟦x V Q⟧ = ∃p ∈ Q. μ(x,p) > θ. C-distributive.
uncertaintyBased : PreferentialBuilder
Uncertainty-based semantics (worry): involves global uncertainty. NOT C-distributive.
relevanceBased (valence : Semantics.Attitudes.Preferential.AttitudeValence) : PreferentialBuilder
Relevance-based semantics (qidai, care): involves resolution. NOT C-distributive.

Instances For

instance Core.Verbs.instDecidableEqPreferentialBuilder :

DecidableEq PreferentialBuilder

Equations

Core.Verbs.instDecidableEqPreferentialBuilder = Core.Verbs.instDecidableEqPreferentialBuilder.decEq

def Core.Verbs.instDecidableEqPreferentialBuilder.decEq (x✝ x✝¹ : PreferentialBuilder) :

Decidable (x✝ = x✝¹)

Equations

One or more equations did not get rendered due to their size.
Core.Verbs.instDecidableEqPreferentialBuilder.decEq (Core.Verbs.PreferentialBuilder.degreeComparison valence) Core.Verbs.PreferentialBuilder.uncertaintyBased = isFalse ⋯
Core.Verbs.instDecidableEqPreferentialBuilder.decEq (Core.Verbs.PreferentialBuilder.degreeComparison valence) (Core.Verbs.PreferentialBuilder.relevanceBased valence_1) = isFalse ⋯
Core.Verbs.instDecidableEqPreferentialBuilder.decEq Core.Verbs.PreferentialBuilder.uncertaintyBased (Core.Verbs.PreferentialBuilder.degreeComparison valence) = isFalse ⋯
Core.Verbs.instDecidableEqPreferentialBuilder.decEq Core.Verbs.PreferentialBuilder.uncertaintyBased Core.Verbs.PreferentialBuilder.uncertaintyBased = isTrue ⋯
Core.Verbs.instDecidableEqPreferentialBuilder.decEq Core.Verbs.PreferentialBuilder.uncertaintyBased (Core.Verbs.PreferentialBuilder.relevanceBased valence) = isFalse ⋯
Core.Verbs.instDecidableEqPreferentialBuilder.decEq (Core.Verbs.PreferentialBuilder.relevanceBased valence) (Core.Verbs.PreferentialBuilder.degreeComparison valence_1) = isFalse ⋯
Core.Verbs.instDecidableEqPreferentialBuilder.decEq (Core.Verbs.PreferentialBuilder.relevanceBased valence) Core.Verbs.PreferentialBuilder.uncertaintyBased = isFalse ⋯

Instances For

def Core.Verbs.instReprPreferentialBuilder.repr :

PreferentialBuilder → ℕ → Std.Format

Equations

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

Instances For

instance Core.Verbs.instReprPreferentialBuilder :

Repr PreferentialBuilder

Equations

Core.Verbs.instReprPreferentialBuilder = { reprPrec := Core.Verbs.instReprPreferentialBuilder.repr }

instance Core.Verbs.instBEqPreferentialBuilder :

BEq PreferentialBuilder

Equations

Core.Verbs.instBEqPreferentialBuilder = { beq := Core.Verbs.instBEqPreferentialBuilder.beq }

def Core.Verbs.PreferentialBuilder.valence :

PreferentialBuilder → Semantics.Attitudes.Preferential.AttitudeValence

Get the valence from the builder

Equations

Instances For

inductive Core.Verbs.AttitudeBuilder :

Unified builder for all attitude verbs, covering both doxastic (believe, know) and preferential (hope, fear) attitudes.

This is the minimal basis from which theoretical properties are derived:

Doxastic attitudes: Use accessibility relations (Hintikka semantics)
Preferential attitudes: Use degree/uncertainty semantics (Villalta)

Derived properties (in Theory layer):

C-distributivity: from PreferentialBuilder structure
NVP class: from C-distributivity + valence
Parasitic on belief: from being preferential
Presupposition projection: from veridicality + attitude type

doxastic (veridicality : Semantics.Attitudes.Doxastic.Veridicality) : AttitudeBuilder
Doxastic attitude (believe, know, think) with accessibility semantics
preferential (builder : PreferentialBuilder) : AttitudeBuilder
Preferential attitude (hope, fear, worry) with degree/uncertainty semantics

Instances For

def Core.Verbs.instDecidableEqAttitudeBuilder.decEq (x✝ x✝¹ : AttitudeBuilder) :

Decidable (x✝ = x✝¹)

Equations

Core.Verbs.instDecidableEqAttitudeBuilder.decEq (Core.Verbs.AttitudeBuilder.doxastic a) (Core.Verbs.AttitudeBuilder.doxastic b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
Core.Verbs.instDecidableEqAttitudeBuilder.decEq (Core.Verbs.AttitudeBuilder.doxastic veridicality) (Core.Verbs.AttitudeBuilder.preferential builder) = isFalse ⋯
Core.Verbs.instDecidableEqAttitudeBuilder.decEq (Core.Verbs.AttitudeBuilder.preferential builder) (Core.Verbs.AttitudeBuilder.doxastic veridicality) = isFalse ⋯
Core.Verbs.instDecidableEqAttitudeBuilder.decEq (Core.Verbs.AttitudeBuilder.preferential a) (Core.Verbs.AttitudeBuilder.preferential b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

Instances For

instance Core.Verbs.instDecidableEqAttitudeBuilder :

DecidableEq AttitudeBuilder

Equations

Core.Verbs.instDecidableEqAttitudeBuilder = Core.Verbs.instDecidableEqAttitudeBuilder.decEq

def Core.Verbs.instReprAttitudeBuilder.repr :

AttitudeBuilder → ℕ → Std.Format

Equations

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

Instances For

instance Core.Verbs.instReprAttitudeBuilder :

Repr AttitudeBuilder

Equations

Core.Verbs.instReprAttitudeBuilder = { reprPrec := Core.Verbs.instReprAttitudeBuilder.repr }

def Core.Verbs.instBEqAttitudeBuilder.beq :

AttitudeBuilder → AttitudeBuilder → Bool

Equations

Core.Verbs.instBEqAttitudeBuilder.beq (Core.Verbs.AttitudeBuilder.doxastic a) (Core.Verbs.AttitudeBuilder.doxastic b) = (a == b)
Core.Verbs.instBEqAttitudeBuilder.beq (Core.Verbs.AttitudeBuilder.preferential a) (Core.Verbs.AttitudeBuilder.preferential b) = (a == b)
Core.Verbs.instBEqAttitudeBuilder.beq x✝¹ x✝ = false

Instances For

instance Core.Verbs.instBEqAttitudeBuilder :

BEq AttitudeBuilder

Equations

Core.Verbs.instBEqAttitudeBuilder = { beq := Core.Verbs.instBEqAttitudeBuilder.beq }

def Core.Verbs.AttitudeBuilder.veridicality :

AttitudeBuilder → Semantics.Attitudes.Doxastic.Veridicality

Get veridicality from an attitude builder

Equations

Instances For

def Core.Verbs.AttitudeBuilder.isDoxastic :

AttitudeBuilder → Bool

Is this a doxastic attitude?

Equations

Instances For

def Core.Verbs.AttitudeBuilder.isPreferential :

AttitudeBuilder → Bool

Is this a preferential attitude?

Equations

Instances For

def Core.Verbs.AttitudeBuilder.getPreferentialBuilder :

AttitudeBuilder → Option PreferentialBuilder

Get the preferential builder if this is a preferential attitude

Equations

Instances For

def Core.Verbs.AttitudeBuilder.valence :

AttitudeBuilder → Option Semantics.Attitudes.Preferential.AttitudeValence

Get valence for preferential attitudes

Equations

Instances For

inductive Core.Verbs.PresupTriggerType :

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

Instances For

instance Core.Verbs.instDecidableEqPresupTriggerType :

DecidableEq PresupTriggerType

Equations

Core.Verbs.instDecidableEqPresupTriggerType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Verbs.instReprPresupTriggerType.repr :

PresupTriggerType → ℕ → Std.Format

Equations

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

Instances For

instance Core.Verbs.instReprPresupTriggerType :

Repr PresupTriggerType

Equations

Core.Verbs.instReprPresupTriggerType = { reprPrec := Core.Verbs.instReprPresupTriggerType.repr }

def Core.Verbs.instBEqPresupTriggerType.beq :

PresupTriggerType → PresupTriggerType → Bool

Equations

Core.Verbs.instBEqPresupTriggerType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Core.Verbs.instBEqPresupTriggerType :

BEq PresupTriggerType

Equations

Core.Verbs.instBEqPresupTriggerType = { beq := Core.Verbs.instBEqPresupTriggerType.beq }

def Core.Verbs.PresupTriggerType.isSoft :

PresupTriggerType → Bool

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

Equations

Instances For

inductive Core.Verbs.ProjectionBehavior :

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)

Instances For

instance Core.Verbs.instDecidableEqProjectionBehavior :

DecidableEq ProjectionBehavior

Equations

Core.Verbs.instDecidableEqProjectionBehavior x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Core.Verbs.instReprProjectionBehavior :

Repr ProjectionBehavior

Equations

Core.Verbs.instReprProjectionBehavior = { reprPrec := Core.Verbs.instReprProjectionBehavior.repr }

def Core.Verbs.instReprProjectionBehavior.repr :

ProjectionBehavior → ℕ → Std.Format

Equations

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

Instances For

instance Core.Verbs.instBEqProjectionBehavior :

BEq ProjectionBehavior

Equations

Core.Verbs.instBEqProjectionBehavior = { beq := Core.Verbs.instBEqProjectionBehavior.beq }

def Core.Verbs.instBEqProjectionBehavior.beq :

ProjectionBehavior → ProjectionBehavior → Bool

Equations

Core.Verbs.instBEqProjectionBehavior.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

inductive Core.Verbs.SenseTag :

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

Instances For

instance Core.Verbs.instDecidableEqSenseTag :

DecidableEq SenseTag

Equations

Core.Verbs.instDecidableEqSenseTag x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Core.Verbs.instBEqSenseTag :

Equations

Core.Verbs.instBEqSenseTag = { beq := Core.Verbs.instBEqSenseTag.beq }

def Core.Verbs.instBEqSenseTag.beq :

SenseTag → SenseTag → Bool

Equations

Core.Verbs.instBEqSenseTag.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Core.Verbs.instReprSenseTag :

Equations

Core.Verbs.instReprSenseTag = { reprPrec := Core.Verbs.instReprSenseTag.repr }

def Core.Verbs.instReprSenseTag.repr :

SenseTag → ℕ → Std.Format

Equations

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

Instances For

inductive Core.Verbs.ComplementType :

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

Instances For

instance Core.Verbs.instDecidableEqComplementType :

DecidableEq ComplementType

Equations

Core.Verbs.instDecidableEqComplementType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Verbs.instReprComplementType.repr :

ComplementType → ℕ → Std.Format

Equations

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

Instances For

instance Core.Verbs.instReprComplementType :

Repr ComplementType

Equations

Core.Verbs.instReprComplementType = { reprPrec := Core.Verbs.instReprComplementType.repr }

instance Core.Verbs.instBEqComplementType :

BEq ComplementType

Equations

Core.Verbs.instBEqComplementType = { beq := Core.Verbs.instBEqComplementType.beq }

def Core.Verbs.instBEqComplementType.beq :

ComplementType → ComplementType → Bool

Equations

Core.Verbs.instBEqComplementType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

def Core.Verbs.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

Instances For

inductive Core.Verbs.ControlType :

Control type for verbs with infinitival complements.

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

Instances For

instance Core.Verbs.instDecidableEqControlType :

DecidableEq ControlType

Equations

Core.Verbs.instDecidableEqControlType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Core.Verbs.instReprControlType :

Repr ControlType

Equations

Core.Verbs.instReprControlType = { reprPrec := Core.Verbs.instReprControlType.repr }

def Core.Verbs.instReprControlType.repr :

ControlType → ℕ → Std.Format

Equations

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

Instances For

def Core.Verbs.instBEqControlType.beq :

ControlType → ControlType → Bool

Equations

Core.Verbs.instBEqControlType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Core.Verbs.instBEqControlType :

BEq ControlType

Equations

Core.Verbs.instBEqControlType = { beq := Core.Verbs.instBEqControlType.beq }

inductive Core.Verbs.ImplicitInterp :

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

Instances For

instance Core.Verbs.instDecidableEqImplicitInterp :

DecidableEq ImplicitInterp

Equations

Core.Verbs.instDecidableEqImplicitInterp x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Verbs.instBEqImplicitInterp.beq :

ImplicitInterp → ImplicitInterp → Bool

Equations

Core.Verbs.instBEqImplicitInterp.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Core.Verbs.instBEqImplicitInterp :

BEq ImplicitInterp

Equations

Core.Verbs.instBEqImplicitInterp = { beq := Core.Verbs.instBEqImplicitInterp.beq }

def Core.Verbs.instReprImplicitInterp.repr :

ImplicitInterp → ℕ → Std.Format

Equations

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

Instances For

instance Core.Verbs.instReprImplicitInterp :

Repr ImplicitInterp

Equations

Core.Verbs.instReprImplicitInterp = { reprPrec := Core.Verbs.instReprImplicitInterp.repr }

structure Core.Verbs.VerbCore :

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 Semantics.Lexical.Verb.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 Semantics.Lexical.Verb.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 Semantics.Tense.Aspect.LexicalAspect.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 Semantics.Lexical.Verb.DegreeAchievement.DegreeAchievementScale
For degree achievements: the scale structure from which default vendlerClass is derived. When present, vendlerClass should agree with degreeAchievementScale.defaultVendlerClass.
verbIncClass : Option Semantics.Events.Krifka1998.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?
projectionBehavior : Option ProjectionBehavior
How does the verb treat presuppositions of its complement? Orthogonal to presupType. @cite{karttunen-1973}
selectsDimension : Option Semantics.Probabilistic.Measurement.Dimension
For measure predicates: which dimension this verb selects for. Determines per-phrase interpretation: simplex dimension → compositional, quotient → math speak.
cosType : Option Semantics.Lexical.Verb.ChangeOfState.CoSType
For CoS verbs: which type (cessation, inception, continuation)?
implicativeBuilder : Option Nadathur2024.Implicative.ImplicativeBuilder
For implicative verbs: which semantic builder (links to compositional semantics).
causativeBuilder : Option NadathurLauer2020.CausativeBuilder
For causative verbs: which semantic builder (links to compositional semantics).
causalSource : Option Semantics.Causation.PsychCausation.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?
attitudeBuilder : Option AttitudeBuilder
Unified attitude builder 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 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 RootProfile
Root-specific quality dimensions (within-class variation).

Instances For

def Core.Verbs.instReprVerbCore.repr :

VerbCore → ℕ → Std.Format

Equations

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

Instances For

instance Core.Verbs.instReprVerbCore :

Equations

Core.Verbs.instReprVerbCore = { reprPrec := Core.Verbs.instReprVerbCore.repr }

def Core.Verbs.instBEqVerbCore.beq :

VerbCore → VerbCore → Bool

Equations

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

Instances For

instance Core.Verbs.instBEqVerbCore :

Equations

Core.Verbs.instBEqVerbCore = { beq := Core.Verbs.instBEqVerbCore.beq }

def Core.Verbs.VerbCore.derivedUnaccusative (v : VerbCore) :

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

Instances For

def Core.Verbs.VerbCore.derivedVendlerClass (v : VerbCore) :

Option Semantics.Tense.Aspect.LexicalAspect.VendlerClass

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

Equations

v.derivedVendlerClass = (v.vendlerClass <|> Option.map (fun (x : Semantics.Lexical.Verb.DegreeAchievement.DegreeAchievementScale) => x.defaultVendlerClass) v.degreeAchievementScale)

Instances For

def Core.Verbs.VerbCore.effectiveSubjectEntailments (v : VerbCore) :

Option Semantics.Lexical.Verb.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 : LevinClass) => x.subjectProfile)

Instances For

def Core.Verbs.VerbCore.effectiveObjectEntailments (v : VerbCore) :

Option Semantics.Lexical.Verb.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 : LevinClass) => x.objectProfile)

Instances For

def Core.Verbs.VerbCore.veridicality (v : VerbCore) :

Option Semantics.Attitudes.Doxastic.Veridicality

Veridicality is DERIVED from the attitude builder

Equations

v.veridicality = Option.map (fun (x : Core.Verbs.AttitudeBuilder) => x.veridicality) v.attitudeBuilder

Instances For

def Core.Verbs.VerbCore.isDoxastic (v : VerbCore) :

Is this verb a doxastic attitude?

Equations

v.isDoxastic = (Option.map (fun (x : Core.Verbs.AttitudeBuilder) => x.isDoxastic) v.attitudeBuilder).getD false

Instances For

def Core.Verbs.VerbCore.isPreferential (v : VerbCore) :

Is this verb a preferential attitude?

Equations

v.isPreferential = (Option.map (fun (x : Core.Verbs.AttitudeBuilder) => x.isPreferential) v.attitudeBuilder).getD false

Instances For

def Core.Verbs.VerbCore.distribOverConj (v : VerbCore) :

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 (x : Core.NaturalLogic.EntailmentSig) => x.refines Core.NaturalLogic.EntailmentSig.mono) v.complementSig).getD false

Instances For

def Core.Verbs.VerbCore.isComplementUE (v : VerbCore) :

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

Equations

v.isComplementUE = (Option.map (fun (x : Core.NaturalLogic.EntailmentSig) => x.refines Core.NaturalLogic.EntailmentSig.mono) v.complementSig).getD false

Instances For

def Core.Verbs.VerbCore.preferentialValence (v : VerbCore) :

Option Semantics.Attitudes.Preferential.AttitudeValence

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

Equations

v.preferentialValence = v.attitudeBuilder.bind fun (x : Core.Verbs.AttitudeBuilder) => x.valence

Instances For

def Core.Verbs.VerbCore.getCoSSemantics {W : Type u_1} (v : VerbCore) (P : W → Bool) :

Option (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 : Semantics.Lexical.Verb.ChangeOfState.CoSType) => Semantics.Lexical.Verb.ChangeOfState.cosSemantics t P) v.cosType

Instances For

def Core.Verbs.VerbCore.factivePresup (v : VerbCore) :

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

Equations

v.factivePresup = match v.attitudeBuilder with | some (Core.Verbs.AttitudeBuilder.doxastic Semantics.Attitudes.Doxastic.Veridicality.veridical) => true | x => false

Instances For

def Core.Verbs.VerbCore.presupposesComplement (v : VerbCore) :

Does this verb presuppose its complement?

Equations

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

Instances For

def Core.Verbs.VerbCore.isPresupTrigger (v : VerbCore) :

Is this verb a presupposition trigger?

Equations

v.isPresupTrigger = v.presupType.isSome

Instances For

def Core.Verbs.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 Core.Verbs.PresupTriggerType.softTrigger else none

Instances For

def Core.Verbs.VerbCore.isCausative (v : VerbCore) :

Is this verb a causative? DERIVED from causativeBuilder.

Equations

v.isCausative = v.causativeBuilder.isSome

Instances For

def Core.Verbs.VerbCore.assertsSufficiency (v : VerbCore) :

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

DERIVED from the builder: delegates to CausativeBuilder.assertsSufficiency.

Equations

v.assertsSufficiency = (Option.map (fun (x : NadathurLauer2020.CausativeBuilder) => x.assertsSufficiency) v.causativeBuilder).getD false

Instances For

def Core.Verbs.VerbCore.isENTrigger (v : VerbCore) :

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

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

Instances For

def Core.Verbs.VerbCore.assertsNecessity (v : VerbCore) :

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

DERIVED from the builder: delegates to CausativeBuilder.assertsNecessity.

Equations

v.assertsNecessity = (Option.map (fun (x : NadathurLauer2020.CausativeBuilder) => x.assertsNecessity) v.causativeBuilder).getD false

Instances For

def Core.Verbs.VerbCore.entailsComplement (v : VerbCore) :

Does success of this implicative verb entail the complement?

DERIVED from the builder: delegates to ImplicativeBuilder.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 : Nadathur2024.Implicative.ImplicativeBuilder) => x.entailsComplement) v.implicativeBuilder

Instances For

def Core.Verbs.VerbCore.isPreferentialAttitude (v : VerbCore) :

Is this verb a preferential attitude predicate?

Equations

v.isPreferentialAttitude = v.preferentialValence.isSome

Instances For

def Core.Verbs.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

Instances For

def Core.Verbs.lookupSense (verbs : List VerbCore) (form : String) (tag : SenseTag := SenseTag.default) :

Option VerbCore

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

Equations

Core.Verbs.lookupSense verbs form tag = List.find? (fun (v : Core.Verbs.VerbCore) => v.form == form && v.senseTag == tag) verbs

Instances For