Causative Builder

@cite{nadathur-lauer-2020} @cite{talmy-1988} @cite{wolff-2003}

Links causative verb lexical entries to their compositional semantics, following the same pattern as PreferentialBuilder for attitude verbs.

Design principle

The builder names a force-dynamic mechanism, not a causal-model property. Properties like "asserts sufficiency" or "asserts necessity" are derived from the builder via theorems.

Builder	Mechanism	English verbs	N&L property (derived)
cause	Counterfactual dependence	cause	necessity
make	Direct sufficient guarantee	make, have, get	sufficiency
force	Coercive (overcome resistance)	force	sufficiency + coercion
enable	Barrier removal (permissive)	let, enable	sufficiency
prevent	Barrier addition (blocking)	prevent	preventSem

inductive NadathurLauer2020.Builder.CausativeBuilder : Type

How a causative verb's semantics is built from causal model infrastructure.

The builder names a force-dynamic mechanism, not a causal-model property. toSemantics maps each builder to its truth-condition function; properties like sufficiency/necessity are derived via theorems.

• cause: Counterfactual dependence — removing cause blocks effect.
• make: Direct sufficient guarantee — adding cause ensures effect.
• force: Coercive sufficiency — overcome resistance, no alternatives.
• enable: Permissive — remove barrier so effect can occur.
• prevent: Blocking — add barrier so effect cannot occur.

• cause : CausativeBuilder

  Counterfactual dependence: removing cause → no effect. Semantic function: causeSem.

• make : CausativeBuilder

  Direct sufficient guarantee: adding cause → effect. Semantic function: makeSem.

• force : CausativeBuilder

  Coercive sufficiency: overcome resistance, no alternatives. Same truth conditions as make; distinguished by isCoercive.

• enable : CausativeBuilder

  Permissive: remove barrier so effect can occur. Same truth conditions as make; distinguished by isPermissive.

• prevent : CausativeBuilder

  Blocking: add barrier so effect cannot occur. Semantic function: preventSem (dual of causeSem).

instance NadathurLauer2020.Builder.instDecidableEqCausativeBuilder : DecidableEq CausativeBuilder

Equations

• NadathurLauer2020.Builder.instDecidableEqCausativeBuilder x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance NadathurLauer2020.Builder.instReprCausativeBuilder : Repr CausativeBuilder

Equations

• NadathurLauer2020.Builder.instReprCausativeBuilder = { reprPrec := NadathurLauer2020.Builder.instReprCausativeBuilder.repr }

def NadathurLauer2020.Builder.instReprCausativeBuilder.repr : CausativeBuilder → ℕ → Std.Format

Equations

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

def NadathurLauer2020.Builder.instBEqCausativeBuilder.beq : CausativeBuilder → CausativeBuilder → Bool

Equations

• NadathurLauer2020.Builder.instBEqCausativeBuilder.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance NadathurLauer2020.Builder.instBEqCausativeBuilder : BEq CausativeBuilder

Equations

• NadathurLauer2020.Builder.instBEqCausativeBuilder = { beq := NadathurLauer2020.Builder.instBEqCausativeBuilder.beq }

Prevent semantics

preventSem is the dual of causeSem: the preventer blocks an effect that would otherwise occur.

def NadathurLauer2020.Builder.preventSem (dyn : Core.StructuralEquationModel.CausalDynamics) (bg : Core.StructuralEquationModel.Situation) (preventer effect : Core.StructuralEquationModel.Variable) : Bool

Semantics of "prevent" (causative verb asserting blocking).

"X prevented Y" is true iff:

1. With the preventer present, the effect does NOT occur
2. Without the preventer, the effect WOULD have occurred

This is the dual of causeSem: cause asserts the effect depends on the cause being present; prevent asserts the effect depends on the preventer being absent.

Equations

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

def NadathurLauer2020.Builder.CausativeBuilder.toSemantics : CausativeBuilder → Core.StructuralEquationModel.CausalDynamics → Core.StructuralEquationModel.Situation → Core.StructuralEquationModel.Variable → Core.StructuralEquationModel.Variable → Bool

Map a causative builder to its semantic function.

This is the structural link between the lexical annotation and the formal semantics. The builder NAMES the force-dynamic mechanism; this function provides the actual truth-condition computation.

Note: force and enable share makeSem truth conditions with make. They differ in force-dynamic properties (coercion, permissivity), which are captured by isCoercive and isPermissive.

Equations

• NadathurLauer2020.Builder.CausativeBuilder.cause.toSemantics = NadathurLauer2020.Necessity.causeSem
• NadathurLauer2020.Builder.CausativeBuilder.make.toSemantics = NadathurLauer2020.Sufficiency.makeSem
• NadathurLauer2020.Builder.CausativeBuilder.force.toSemantics = NadathurLauer2020.Sufficiency.makeSem
• NadathurLauer2020.Builder.CausativeBuilder.enable.toSemantics = NadathurLauer2020.Sufficiency.makeSem
• NadathurLauer2020.Builder.CausativeBuilder.prevent.toSemantics = NadathurLauer2020.Builder.preventSem

Derived property functions

These functions derive causal-model properties from the force-dynamic builder. They are the interface between the fine-grained builder and Nadathur & Lauer's binary sufficiency/necessity classification.

def NadathurLauer2020.Builder.CausativeBuilder.assertsSufficiency : CausativeBuilder → Bool

Does this builder assert causal sufficiency (N&L Def 23)?

DERIVED: true for builders whose toSemantics maps to makeSem.

Equations

• NadathurLauer2020.Builder.CausativeBuilder.make.assertsSufficiency = true
• NadathurLauer2020.Builder.CausativeBuilder.force.assertsSufficiency = true
• NadathurLauer2020.Builder.CausativeBuilder.enable.assertsSufficiency = true
• NadathurLauer2020.Builder.CausativeBuilder.cause.assertsSufficiency = false
• NadathurLauer2020.Builder.CausativeBuilder.prevent.assertsSufficiency = false

def NadathurLauer2020.Builder.CausativeBuilder.assertsNecessity : CausativeBuilder → Bool

Does this builder assert causal necessity (N&L Def 24)?

DERIVED: true only for .cause, whose toSemantics maps to causeSem.

Equations

• NadathurLauer2020.Builder.CausativeBuilder.cause.assertsNecessity = true
• x✝.assertsNecessity = false

def NadathurLauer2020.Builder.CausativeBuilder.isCoercive : CausativeBuilder → Bool

Does this builder encode coercion (overcoming resistance)?

Force-dynamic property: .force encodes that the causer overcame the causee's resistance.

Equations

• NadathurLauer2020.Builder.CausativeBuilder.force.isCoercive = true
• x✝.isCoercive = false

def NadathurLauer2020.Builder.CausativeBuilder.isPermissive : CausativeBuilder → Bool

Does this builder encode permissivity (barrier removal)?

Force-dynamic property: .enable encodes that the causer removed a barrier, allowing the effect to occur naturally.

Equations

• NadathurLauer2020.Builder.CausativeBuilder.enable.isPermissive = true
• x✝.isPermissive = false

Derivation theorems

These theorems show that N&L's sufficiency/necessity classification is derivable from the force-dynamic builder, rather than being independently stipulated.

theorem NadathurLauer2020.Builder.sufficiency_builders_use_makeSem : CausativeBuilder.make.toSemantics = Sufficiency.makeSem ∧ CausativeBuilder.force.toSemantics = Sufficiency.makeSem ∧ CausativeBuilder.enable.toSemantics = Sufficiency.makeSem

All sufficiency-asserting builders (make, force, enable) compute truth conditions via makeSem.

theorem NadathurLauer2020.Builder.cause_builder_uses_causeSem : CausativeBuilder.cause.toSemantics = Necessity.causeSem

The cause builder computes truth conditions via causeSem.

theorem NadathurLauer2020.Builder.make_force_same_truth_conditions : CausativeBuilder.make.toSemantics = CausativeBuilder.force.toSemantics

make and force have the same truth conditions.

Both map to makeSem. They are distinguished by isCoercive: force lexically encodes coercion while make does not.

theorem NadathurLauer2020.Builder.enable_make_same_truth_conditions : CausativeBuilder.enable.toSemantics = CausativeBuilder.make.toSemantics

enable and make have the same truth conditions.

Both map to makeSem. They are distinguished by isPermissive: enable encodes barrier removal while make does not.

theorem NadathurLauer2020.Builder.prevent_cause_duality (dyn : Core.StructuralEquationModel.CausalDynamics) (bg : Core.StructuralEquationModel.Situation) (x e : Core.StructuralEquationModel.Variable) : preventSem dyn bg x e = (!(Core.StructuralEquationModel.normalDevelopment dyn (bg.extend x true)).hasValue e true && (Core.StructuralEquationModel.normalDevelopment dyn (bg.extend x false)).hasValue e true)

prevent and cause are duals.

cause asserts the effect depends on the cause being present; prevent asserts the effect depends on the preventer being absent.

Formally: preventSem holds when effect is blocked WITH the preventer and would occur WITHOUT it — the mirror of causeSem which holds when effect occurs WITH the cause and wouldn't occur WITHOUT it.

theorem NadathurLauer2020.Builder.builders_truth_conditionally_distinct : ∃ (dyn : Core.StructuralEquationModel.CausalDynamics), ∃ (s : Core.StructuralEquationModel.Situation), ∃ (c : Core.StructuralEquationModel.Variable), ∃ (e : Core.StructuralEquationModel.Variable), CausativeBuilder.make.toSemantics dyn s c e ≠ CausativeBuilder.cause.toSemantics dyn s c e

At least two builders produce genuinely different truth conditions.

Witnessed by the overdetermination scenario (lightning + arsonist): makeSem returns true (lightning sufficient) but causeSem returns false (lightning not necessary).

theorem NadathurLauer2020.Builder.make_force_distinguished_by_coercion : CausativeBuilder.make.isCoercive = false ∧ CausativeBuilder.force.isCoercive = true

make and force are distinguished by coercion despite sharing truth conditions.

theorem NadathurLauer2020.Builder.make_enable_distinguished_by_permissivity : CausativeBuilder.make.isPermissive = false ∧ CausativeBuilder.enable.isPermissive = true

make and enable are distinguished by permissivity despite sharing truth conditions.

theorem NadathurLauer2020.Builder.assertsSufficiency_iff_makeSem (b : CausativeBuilder) : b.assertsSufficiency = true ↔ b.toSemantics = Sufficiency.makeSem

Sufficiency-asserting builders all use makeSem.

This is the key bridge: assertsSufficiency exactly characterizes builders whose toSemantics returns makeSem.

TODO: The prevent case requires showing preventSem ≠ makeSem, which needs a witness (a model where they differ).

theorem NadathurLauer2020.Builder.sufficiency_implies_causallySufficient (dyn : Core.StructuralEquationModel.CausalDynamics) (s : Core.StructuralEquationModel.Situation) (c e : Core.StructuralEquationModel.Variable) (h : CausativeBuilder.make.toSemantics dyn s c e = true) : Core.StructuralEquationModel.causallySufficient dyn s c e = true

When a sufficiency builder's semantics holds, the cause is causally sufficient for the effect.

This is DERIVED: it follows from the fact that makeSem is defined as causallySufficient.

theorem NadathurLauer2020.Builder.necessity_implies_causallyNecessary (dyn : Core.StructuralEquationModel.CausalDynamics) (s : Core.StructuralEquationModel.Situation) (c e : Core.StructuralEquationModel.Variable) (h : CausativeBuilder.cause.toSemantics dyn s c e = true) : Core.StructuralEquationModel.causallyNecessary dyn s c e = true

When the cause builder's semantics holds, the cause is causally necessary for the effect.

DERIVED from the fact that causeSem conjoins occurrence with causallyNecessary.