Documentation

Linglib.Theories.Semantics.Causation.ProductionDependence

Burning Facts: Thick and Thin Causatives #

@cite{embick-2009} @cite{martin-rose-nichols-2025} @cite{rose-nichols-2021} @cite{wolff-2003}

Two concepts of CAUSE underlie lexical causative verb semantics:

P-CAUSE (production): Energy transfer from cause to effect. Physical, direct, requires concrete causer. Thick causatives (burn, break, melt) preferably encode P-CAUSE.
D-CAUSE (dependence): Counterfactual dependence of effect on cause. Abstract, allows absences/facts/degrees as causes. Thin causatives (kill, destroy, damage) are compatible with D-CAUSE.

Key Property #

P-CAUSE asymmetrically entails D-CAUSE: if x produces y (energy transfer), then y counterfactually depends on x. But not vice versa: absences can be d-causes without producing anything.

Bridges to Existing Infrastructure #

Concept	Maps to	Module
P-CAUSE (deterministic)	`causallySufficient` + directness	Sufficiency.lean
D-CAUSE (deterministic)	`causallyNecessary`	Necessity.lean
Thick → P-CAUSE preference	production constraint	(this file)
Thick → strong ASR	resultative compatibility	Causation/Studies/MartinRoseNichols2025.lean
Builder `.make`	sufficiency = P-CAUSE in deterministic limit	Builder.lean

Causation Type #

The two concepts of causation that lexical causative verbs can encode. This is orthogonal to the CausativeBuilder (which classifies periphrastic causatives by force-dynamic mechanism) — it classifies how lexical causatives encode the causal relation itself.

inductive MartinRoseNichols2025.CausationType :

Two concepts of CAUSE operating in lexical causative semantics.

production: Energy/force transfer from causer to causee (P-CAUSE). Requires a concrete, physical causer. Thick causatives preferably encode this. Entails dependence.
dependence: Counterfactual dependence of effect on cause (D-CAUSE). Compatible with abstract causes (absences, facts, degrees). Thin causatives and overt cause encode this.

production : CausationType
Production-based: energy transfer, requires concrete causer. burn, break, melt in their physical sense.
dependence : CausationType
Dependence-based: counterfactual, allows abstract causers. kill, destroy, damage, overt cause.

Instances For

instance MartinRoseNichols2025.instDecidableEqCausationType :

DecidableEq CausationType

Equations

MartinRoseNichols2025.instDecidableEqCausationType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def MartinRoseNichols2025.instReprCausationType.repr :

CausationType → ℕ → Std.Format

Equations

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

Instances For

instance MartinRoseNichols2025.instReprCausationType :

Repr CausationType

Equations

MartinRoseNichols2025.instReprCausationType = { reprPrec := MartinRoseNichols2025.instReprCausationType.repr }

instance MartinRoseNichols2025.instBEqCausationType :

BEq CausationType

Equations

MartinRoseNichols2025.instBEqCausationType = { beq := MartinRoseNichols2025.instBEqCausationType.beq }

def MartinRoseNichols2025.instBEqCausationType.beq :

CausationType → CausationType → Bool

Equations

MartinRoseNichols2025.instBEqCausationType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

Thick vs Thin Classification #

The core empirical distinction: thick causatives encode manner of causing (either via an event property like break or a state property like bury), while thin causatives specify only the result state.

inductive MartinRoseNichols2025.ThickThinClass :

Whether a lexical causative verb encodes manner of causing.

thick: Encodes manner — restricts subjects to productive causes. Subdivided by HOW manner is encoded (event predicate vs state property).
thin: Result-only — silent on manner, compatible with any cause type.

thickManner : ThickThinClass
Thick via event predicate: root is a predicate of the causing event. break, burn, melt, cut — @cite{embick-2009} break-class. Compatible with strong adjectival resultatives (burn clean).
thickState : ThickThinClass
Thick via state property: result state reveals production process. bury (buried → covered with earth). Not compatible with strong ASR.
thin : ThickThinClass
Thin: result-only, no manner specification. kill, destroy, damage, change, activate.

Instances For

instance MartinRoseNichols2025.instDecidableEqThickThinClass :

DecidableEq ThickThinClass

Equations

MartinRoseNichols2025.instDecidableEqThickThinClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def MartinRoseNichols2025.instReprThickThinClass.repr :

ThickThinClass → ℕ → Std.Format

Equations

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

Instances For

instance MartinRoseNichols2025.instReprThickThinClass :

Repr ThickThinClass

Equations

MartinRoseNichols2025.instReprThickThinClass = { reprPrec := MartinRoseNichols2025.instReprThickThinClass.repr }

def MartinRoseNichols2025.instBEqThickThinClass.beq :

ThickThinClass → ThickThinClass → Bool

Equations

MartinRoseNichols2025.instBEqThickThinClass.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance MartinRoseNichols2025.instBEqThickThinClass :

BEq ThickThinClass

Equations

MartinRoseNichols2025.instBEqThickThinClass = { beq := MartinRoseNichols2025.instBEqThickThinClass.beq }

def MartinRoseNichols2025.ThickThinClass.isThick :

ThickThinClass → Bool

Is the verb thick (encodes manner of causing)?

Equations

Instances For

def MartinRoseNichols2025.ThickThinClass.isCausativeMannerVerb :

ThickThinClass → Bool

Is the verb a causative manner verb (@cite{embick-2009} break-class)? These are the thick verbs whose root is an event predicate, compatible with strong adjectival resultatives.

Equations

Instances For

Asymmetric Entailment: P-CAUSE → D-CAUSE #

In the deterministic limit (our CausalDynamics), production-based causation (P-CAUSE) entails dependence-based causation (D-CAUSE).

Formally: in a single-pathway causal model (no overdetermination), if the cause is sufficient for the effect, it is also necessary. This captures: if x produces y via direct energy transfer, removing x would prevent y.

theorem MartinRoseNichols2025.single_pathway_sufficiency_implies_necessity (c e : Core.StructuralEquationModel.Variable) (_hne : c ≠ e) :

have dyn := { laws := [Core.StructuralEquationModel.CausalLaw.simple c e] }; Core.StructuralEquationModel.causallySufficient dyn Core.StructuralEquationModel.Situation.empty c e = true → Core.StructuralEquationModel.causallyNecessary dyn Core.StructuralEquationModel.Situation.empty c e = true

In a single-pathway model (one causal law, no background alternatives), sufficiency implies necessity.

This is the deterministic formalization of "P-CAUSE entails D-CAUSE": when there is exactly one causal pathway and no overdetermination, a sufficient cause is also necessary.

Note: This fails under overdetermination (see builders_truth_conditionally_distinct), which is exactly when P-CAUSE and D-CAUSE can come apart.

theorem MartinRoseNichols2025.single_pathway_concrete :

have a := Core.StructuralEquationModel.mkVar "a"; have b := Core.StructuralEquationModel.mkVar "b"; have dyn := { laws := [Core.StructuralEquationModel.CausalLaw.simple a b] }; Core.StructuralEquationModel.causallySufficient dyn Core.StructuralEquationModel.Situation.empty a b = true ∧ Core.StructuralEquationModel.causallyNecessary dyn Core.StructuralEquationModel.Situation.empty a b = true

Concrete instance of the single-pathway entailment, fully proved.

For specific variables a, b, the entailment P-CAUSE → D-CAUSE holds: sufficiency implies necessity in a single-pathway model. This is verified by computation.

Under overdetermination, sufficiency does NOT imply necessity.

This is when P-CAUSE and D-CAUSE come apart: a cause can transfer energy (sufficient) but the effect would have occurred anyway from another source (not necessary).

Reuses the existing witness from builders_truth_conditionally_distinct.

Production Constraint #

Thick causatives preferably convey P-CAUSE (production-based causation). This is a pragmatic constraint arising from competition between the lexical (covert) causative and the periphrastic (overt) cause.

def MartinRoseNichols2025.productionConstraint (cls : ThickThinClass) :

The production constraint: thick causatives prefer production causation.

When a thick causative is used in its physical sense, the CAUSE operator preferably receives a production-based interpretation. This is because the manner information makes P-CAUSE a salient alternative, and the more specific lexical form specializes in the more specific meaning.

Equations

MartinRoseNichols2025.productionConstraint cls = if cls.isThick = true then MartinRoseNichols2025.CausationType.production else MartinRoseNichols2025.CausationType.dependence

Instances For

theorem MartinRoseNichols2025.thick_prefers_production :

productionConstraint ThickThinClass.thickManner = CausationType.production ∧ productionConstraint ThickThinClass.thickState = CausationType.production

Thick verbs prefer production causation.

theorem MartinRoseNichols2025.thin_defaults_dependence :

productionConstraint ThickThinClass.thin = CausationType.dependence

Thin verbs default to dependence causation.

Bridge to CausativeBuilder #

P-CAUSE maps to makeSem (sufficiency): production causes are sufficient. D-CAUSE maps to causeSem (necessity): dependence causes are necessary.

The overt verb cause encodes D-CAUSE and uses CausativeBuilder.cause. Thick lexical causatives encode P-CAUSE and align with CausativeBuilder.make.

Note: lexical causatives don't literally use CausativeBuilder (which classifies periphrastic verbs), but their internal CAUSE operator has the same truth conditions as makeSem when P-CAUSE applies.

def MartinRoseNichols2025.CausationType.analogousBuilder :

CausationType → NadathurLauer2020.Builder.CausativeBuilder

Map causation type to the analogous CausativeBuilder.

This is the structural bridge: P-CAUSE's truth conditions correspond to sufficiency (makeSem), D-CAUSE's to necessity (causeSem).

Equations

Instances For

theorem MartinRoseNichols2025.production_analogous_make :

CausationType.production.analogousBuilder = NadathurLauer2020.Builder.CausativeBuilder.make

Production causation is analogous to the .make builder.

theorem MartinRoseNichols2025.dependence_analogous_cause :

CausationType.dependence.analogousBuilder = NadathurLauer2020.Builder.CausativeBuilder.cause

Dependence causation is analogous to the .cause builder.

theorem MartinRoseNichols2025.production_asserts_sufficiency :

CausationType.production.analogousBuilder.assertsSufficiency = true

P-CAUSE's analogous builder asserts sufficiency.

theorem MartinRoseNichols2025.dependence_asserts_necessity :

CausationType.dependence.analogousBuilder.assertsNecessity = true

D-CAUSE's analogous builder asserts necessity.

Bridge to Resultatives #

Thick causative manner verbs (break-class) are compatible with strong adjectival resultatives (break open, burn clean). This connects to the resultative infrastructure in ArgumentStructure/Studies/TheoryComparison.lean, where the constructional CAUSE uses CausativeBuilder.make.

def MartinRoseNichols2025.ThickThinClass.strongASRCompatible :

ThickThinClass → Bool

Causative manner verbs (thickManner) are compatible with strong ASR. This is the @cite{embick-2009} generalization formalized as a derived property.

Thin verbs and thick-state verbs (bury) are NOT compatible.

Equations

Instances For

theorem MartinRoseNichols2025.manner_verbs_asr_compatible :

ThickThinClass.thickManner.strongASRCompatible = true

Manner verbs are ASR-compatible.

theorem MartinRoseNichols2025.thin_verbs_not_asr :

ThickThinClass.thin.strongASRCompatible = false

Thin verbs are NOT ASR-compatible.

theorem MartinRoseNichols2025.thick_state_not_asr :

ThickThinClass.thickState.strongASRCompatible = false

Thick-state verbs (bury) are NOT ASR-compatible. bury is thick but not a causative manner verb.

def MartinRoseNichols2025.productionEntailsDirectness (ct : CausationType) :

Production entails directness (§6).

When a verb encodes P-CAUSE (energy transfer), the causal relation is necessarily direct: for energy to transfer, there must be physical contact or at least no intervening causer at the same level of granularity. This is why the directness constraint holds specifically for thick causatives.

Equations

MartinRoseNichols2025.productionEntailsDirectness ct = (ct == MartinRoseNichols2025.CausationType.production)

Instances For

theorem MartinRoseNichols2025.production_is_direct :

productionEntailsDirectness CausationType.production = true

theorem MartinRoseNichols2025.dependence_not_necessarily_direct :

productionEntailsDirectness CausationType.dependence = false

Bridge to CausalProfile #

The structural causal model's CausalProfile directly determines the dominant causation type via its directness and necessity fields. This connects model-level structural properties to the production/dependence distinction without going through any study-specific representation.

def MartinRoseNichols2025.profileCausationType (p : Core.StructuralEquationModel.CausalProfile) :

Option CausationType

Map a structural causal profile to the dominant causation type.

direct = true → P-CAUSE (production): a direct causal law implies energy/force transfer.
necessary = true (without directness) → D-CAUSE (dependence): counterfactual dependence without direct interaction.
Neither → no causal involvement.

Equations

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

Instances For

theorem MartinRoseNichols2025.profileCausationType_production_iff (p : Core.StructuralEquationModel.CausalProfile) :

profileCausationType p = some CausationType.production ↔ p.direct = true

Production type iff direct causal connection.

theorem MartinRoseNichols2025.profileCausationType_dependence_iff (p : Core.StructuralEquationModel.CausalProfile) :

profileCausationType p = some CausationType.dependence ↔ p.direct = false ∧ p.necessary = true

Dependence type iff necessary but not direct.