Causal Frame: Unified Abstraction for Complement-Entailing Constructions #

@cite{nadathur-2023} @cite{nadathur-lauer-2020}

The single parameterized type underlying implicative verbs (manage, fail), ability modals (be able, sak), light verbs (le), and degree constructions (enough/too).

The Unifying Abstraction #

All complement-entailing constructions share the same causal skeleton:

A causal dynamics (structural equations)
A trigger variable (action, degree threshold, managing event)
A complement variable (the VP outcome)
A background function mapping evaluation contexts to causal situations
An actualization mode controlling what asserts trigger occurrence

The actuality inference in all cases reduces to the same syllogism:

The trigger is causally sufficient for the complement (causal premise)
The trigger actually occurred (assertion premise — from aspect or lexicon)
Therefore the complement occurred (actuality conclusion)

Actualization Mode #

The key parameter distinguishing implicatives from ability modals (@cite{nadathur-2023}, Chapter 1):

Instance	Trigger	Actualization
manage	managing event	`.lexical` (aspect-independent)
le (Hindi LV)	volitional choice	`.lexical` (aspect-independent)
be able / sak	agent's action	`.aspectual` (PFV/IMPF)
enough to VP	degree ≥ θ	`.aspectual` (PFV/IMPF)

source

inductive CausalVerb.ActualizationMode :

Type

How the actuality of the trigger gets asserted.

lexical: The verb's lexical semantics asserts that the trigger occurred. The complement entailment holds regardless of grammatical aspect. (manage, fail, force, prevent, le)
aspectual: Grammatical aspect determines whether the trigger's occurrence is asserted. Perfective asserts it; imperfective doesn't. (be able, sak, enough to VP, too Adj to VP)

lexical : ActualizationMode
aspectual : ActualizationMode

Instances For

source

instance CausalVerb.instDecidableEqActualizationMode :

DecidableEq ActualizationMode

Equations

CausalVerb.instDecidableEqActualizationMode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

instance CausalVerb.instReprActualizationMode :

Repr ActualizationMode

Equations

CausalVerb.instReprActualizationMode = { reprPrec := CausalVerb.instReprActualizationMode.repr }

source

def CausalVerb.instReprActualizationMode.repr :

ActualizationMode → ℕ → Std.Format

Equations

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

Instances For

source

def CausalVerb.instBEqActualizationMode.beq :

ActualizationMode → ActualizationMode → Bool

Equations

CausalVerb.instBEqActualizationMode.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

instance CausalVerb.instBEqActualizationMode :

BEq ActualizationMode

Equations

CausalVerb.instBEqActualizationMode = { beq := CausalVerb.instBEqActualizationMode.beq }

source

structure CausalVerb.CausalFrame (W : Type) :

Type

CausalFrame: The abstract frame underlying all complement-entailing verb constructions.

Parameterized by W (evaluation context type):

W = Unit for implicative verbs (no modal dimension)
W = World for ability modals (Kripke worlds)
W = World for degree constructions (degree evaluated at worlds)

The frame bundles:

Causal model (dynamics + trigger + complement)
Background projection (evaluation context → causal situation)
Actualization mode (what controls trigger assertion)

All complement-entailing constructions are instances differing only in the choice of W, actualization, and what the "trigger" represents.

dynamics : Core.StructuralEquationModel.CausalDynamics
Structural equations governing trigger → complement
trigger : Core.StructuralEquationModel.Variable
The trigger variable (action, degree threshold, managing event)
complement : Core.StructuralEquationModel.Variable
The complement variable (VP outcome)
background : W → Core.StructuralEquationModel.Situation
Maps evaluation contexts to causal background situations
actualization : ActualizationMode
How trigger occurrence is asserted

Instances For

source

def CausalVerb.CausalFrame.sufficientAt {W : Type} (f : CausalFrame W) (w : W) :

Bool

Trigger is causally sufficient for complement at evaluation context w.

Equations

f.sufficientAt w = Core.StructuralEquationModel.causallySufficient f.dynamics (f.background w) f.trigger f.complement

Instances For

source

def CausalVerb.CausalFrame.actualizedAt {W : Type} (f : CausalFrame W) (w : W) :

Bool

Complement is actualized at w: trigger occurred AND complement developed.

Equations

f.actualizedAt w = Core.StructuralEquationModel.factuallyDeveloped f.dynamics (f.background w) f.trigger f.complement

Instances For

source

def CausalVerb.CausalFrame.complementBlockedAt {W : Type} (f : CausalFrame W) (w : W) :

Bool

The complement did NOT develop at w (for negative-polarity verbs like fail, too Adj to VP).

Equations

f.complementBlockedAt w = ((f.background w).hasValue f.trigger true && !(Core.StructuralEquationModel.normalDevelopment f.dynamics (f.background w)).hasValue f.complement true)

Instances For

source

def CausalVerb.CausalFrame.actualityWithAspect {W : Type} (f : CausalFrame W) (asp : Semantics.Tense.Aspect.Core.ViewpointAspectB) (w : W) :

Bool

Generic actuality predicate with aspectual modulation.

Lexical: sufficiency AND actualization (always, regardless of aspect)
Aspectual + perfective: sufficiency AND actualization
Aspectual + imperfective: sufficiency only (no actualization required)

This is the single function from which the semantics of manage, ability modals, and degree constructions are all derived.

Equations

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

Instances For

source

theorem CausalVerb.CausalFrame.lexical_entails_complement {W : Type} (f : CausalFrame W) (w : W) (asp : Semantics.Tense.Aspect.Core.ViewpointAspectB) (h : f.actualityWithAspect asp w = true) (hMode : f.actualization = ActualizationMode.lexical) :

f.actualizedAt w = true

Generic actuality theorem (lexical mode): if a lexically-actualized frame holds, the complement is actualized.

This is the abstract version of the entailment pattern for manage.

source

theorem CausalVerb.CausalFrame.perfective_entails_complement {W : Type} (f : CausalFrame W) (w : W) (h : f.actualityWithAspect Semantics.Tense.Aspect.Core.ViewpointAspectB.perfective w = true) (hMode : f.actualization = ActualizationMode.aspectual) :

f.actualizedAt w = true

Generic actuality theorem (aspectual + perfective): if an aspect-governed frame holds with perfective aspect, the complement is actualized.

This is the abstract version of actuality entailments for ability modals and degree constructions.

source

theorem CausalVerb.CausalFrame.imperfective_compatible_with_unrealized :

∃ (f : CausalFrame Unit), f.actualization = ActualizationMode.aspectual ∧ f.actualityWithAspect Semantics.Tense.Aspect.Core.ViewpointAspectB.imperfective () = true ∧ f.actualizedAt () = false

Generic non-entailment (aspectual + imperfective): imperfective aspect is compatible with complement not being actualized.

This is the abstract version of the observation that imperfective ability modals don't entail their complements.

source

Aspect governs actuality (generic): the same frame yields different entailment patterns under different aspects, demonstrated with a frame over Bool where true = action performed, false = not.

source

theorem CausalVerb.CausalFrame.lexical_aspect_independent {W : Type} (f : CausalFrame W) (w : W) (hMode : f.actualization = ActualizationMode.lexical) :

f.actualityWithAspect Semantics.Tense.Aspect.Core.ViewpointAspectB.perfective w = f.actualityWithAspect Semantics.Tense.Aspect.Core.ViewpointAspectB.imperfective w

Lexical mode is aspect-independent: the result is the same for perfective and imperfective when the trigger is present.

This captures manage being aspect-independent: the entailment doesn't change with aspect because the lexical semantics already asserts trigger occurrence.

source

theorem CausalVerb.CausalFrame.imperfective_is_pure_sufficiency {W : Type} (f : CausalFrame W) (w : W) (hMode : f.actualization = ActualizationMode.aspectual) :

f.actualityWithAspect Semantics.Tense.Aspect.Core.ViewpointAspectB.imperfective w = f.sufficientAt w

Imperfective is pure sufficiency for aspectually-governed frames: imperfective asserts only causal sufficiency, with no event actualization.

source

theorem CausalVerb.CausalFrame.perfective_adds_actualization {W : Type} (f : CausalFrame W) (w : W) (hMode : f.actualization = ActualizationMode.aspectual) :

f.actualityWithAspect Semantics.Tense.Aspect.Core.ViewpointAspectB.perfective w = (f.actualityWithAspect Semantics.Tense.Aspect.Core.ViewpointAspectB.imperfective w && f.actualizedAt w)

Perfective adds actualization: perfective = imperfective ∧ actualized for aspectually-governed frames.

source

theorem CausalVerb.CausalFrame.sufficiency_monotone {W : Type} (f : CausalFrame W) (w : W) (extra : Core.StructuralEquationModel.Variable) (hPos : Core.StructuralEquationModel.isPositiveDynamics f.dynamics = true) (h : f.sufficientAt w = true) :

Core.StructuralEquationModel.causallySufficient f.dynamics ((f.background w).extend extra true) f.trigger f.complement = true

Causal sufficiency in a frame is monotone for positive dynamics: adding truths to the background preserves sufficiency.

This is the frame-level version of sufficiency_monotone_positive.

source

def CausalVerb.abilityFrame (dynamics : Core.StructuralEquationModel.CausalDynamics) (action complement : Core.StructuralEquationModel.Variable) (background : Semantics.Attitudes.Intensional.World → Core.StructuralEquationModel.Situation) :

CausalFrame Semantics.Attitudes.Intensional.World

Construct an ability-modal CausalFrame: a world-indexed causal model where actualization is governed by aspect (not lexical assertion).

Each possible world w : World projects to a Situation in the causal model via background. Ability at w reduces to causal sufficiency in the projected situation.

Imperfective: sufficiency only (pure ability, compatible with complement unrealized)
Perfective: sufficiency AND actualization (actuality entailment)

This replaces the former AbilityScenario structure — ability modals are just CausalFrame World with actualization = .aspectual.

Equations

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

Instances For

source

theorem CausalVerb.abilityFrame_aspectual (dyn : Core.StructuralEquationModel.CausalDynamics) (act comp : Core.StructuralEquationModel.Variable) (bg : Semantics.Attitudes.Intensional.World → Core.StructuralEquationModel.Situation) :

(abilityFrame dyn act comp bg).actualization = ActualizationMode.aspectual

abilityFrame always produces aspectual actualization.

source

theorem CausalVerb.CausalFrame.ability_differs_from_implicative :

∃ (f : CausalFrame Semantics.Attitudes.Intensional.World) (w : Semantics.Attitudes.Intensional.World), f.actualization = ActualizationMode.aspectual ∧ f.sufficientAt w = true ∧ f.actualizedAt w = false

Ability differs from implicative verbs: ability can hold without actualization (impossible for manage).

For manage (.lexical mode), actualityWithAspect ALWAYS includes complement truth. For ability (.aspectual mode), only perfective aspect forces complement truth.

source

Aspect governs actuality for ability: the same ability frame yields different entailment patterns under different aspects.

With perfective: ability → complement actualized. With imperfective: ability ↛ complement actualized.

For positive dynamics, normalDevelopment is a closure operator on (Situation, trueLE): 1. Inflationary: s ⊑ cl(s) 2. Monotone: s₁ ⊑ s₂ → cl(s₁) ⊑ cl(s₂) 3. Idempotent: cl(cl(s)) = cl(s)

Causal sufficiency is **closure membership**: `complement = true ∈ cl(s + trigger)`.
This is the deep structural reason all complement-entailing constructions work.

source