Causal Verb Frame #
@cite{nadathur-2023} @cite{nadathur-lauer-2020}
Deep foundation for complement-entailing constructions: implicative verbs
(manage, fail), ability modals (be able), and degree constructions
(enough/too). Analogous to MereoDim bridging mereology and scales,
this file bridges causation, modality, and aspect through a
single parameterized frame.
The Unifying Abstraction #
All three phenomena 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)
Closure-Operator Structure (§1) #
For positive dynamics, normalDevelopment is a closure operator on
(Situation, trueLE):
- Inflationary:
s ⊑ cl(s)— adding causal consequences only adds truths - Monotone:
s₁ ⊑ s₂ → cl(s₁) ⊑ cl(s₂)— more inputs → more outputs - Idempotent:
cl(cl(s)) = cl(s)— fixpoint stability
Causal sufficiency is closure membership: complement = true ∈ cl(s + trigger).
This is the deep structural reason that all three phenomena work the same way.
Linguistic Instances (§5–§6) #
| Instance | Trigger | Aspect-governed? |
|---|---|---|
| manage | managing event | No (lexical) |
| be able | agent's action | Yes (PFV/IMPF) |
| enough to VP | degree ≥ θ | Yes (PFV/IMPF) |
| too Adj to VP | degree ≥ θ | Yes (PFV/IMPF) |
For positive dynamics, normalDevelopment satisfies the three closure
operator axioms. The inflationary and monotonicity properties are proved
in Core/Causation.lean; we package them here and add the fixpoint return.
Monotone: if s₁ ⊑ s₂, then cl(s₁) ⊑ cl(s₂).
Imported from Core/Causation.lean.
Inflationary: every truth in s is preserved by normal development.
Imported from Core/Causation.lean.
Fixpoint return: if the first round of law application reaches a fixpoint,
normalDevelopment returns that result.
Causal sufficiency as closure membership.
causallySufficient dyn s trigger complement holds iff
complement = true ∈ cl(s + {trigger = true}).
This is definitional — we state it as a theorem for the conceptual bridge: sufficiency IS asking whether the complement is in the closure of the extended situation.
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)
aspectual: Grammatical aspect determines whether the trigger's occurrence is asserted. Perfective asserts it; imperfective doesn't. (be able, enough to VP, too Adj to VP)
- lexical : ActualizationMode
- aspectual : ActualizationMode
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Equations
- CausalVerb.instBEqActualizationMode.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)
Instances For
CausalFrame: The abstract frame underlying all complement-entailing verb constructions.
Parameterized by W (evaluation context type):
W = Unitfor implicative verbs (no modal dimension)W = Worldfor ability modals (Kripke worlds)W = Worldfor 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 three phenomena 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
Trigger is causally sufficient for complement at evaluation context w.
Equations
Instances For
Complement is actualized at w: trigger occurred AND complement developed.
Equations
Instances For
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
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 manageSem, abilityWithAspect,
and enoughWithAspect are all derived.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Generic actuality theorem (lexical mode): if a lexically-actualized frame holds, the complement is actualized.
This is the abstract version of manage_entails_complement.
Generic actuality theorem (aspectual + perfective): if an aspect-governed frame holds with perfective aspect, the complement is actualized.
This is the abstract version of perfective_ability_entails_complement
and perfective_enough_entails_complement.
Generic non-entailment (aspectual + imperfective): imperfective aspect is compatible with complement not being actualized.
This is the abstract version of
imperfective_ability_compatible_with_unrealized.
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.
Abstract version of aspect_governs_actuality.
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.
Show that existing structures are instances of CausalFrame.
An ImplicativeScenario is a CausalFrame Unit with lexical actualization.
Equations
- One or more equations did not get rendered due to their size.
Instances For
An AbilityScenario is a CausalFrame World with aspectual actualization.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The generic frame's sufficiency at `` matches manageSem's
sufficiency check.
The generic frame's sufficiency at w matches abilityAt.
The generic frame's actualization at w matches complementActualized.
Grounding theorem: the generic actualityWithAspect matches
abilityWithAspect for ability scenarios.
This is the key structural result: Ability.lean's hand-written
abilityWithAspect is exactly what falls out of the generic
CausalFrame.actualityWithAspect machinery.
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.