Psych Verb Causal Links

[Kim24] [All83] [Bac86] Formal integration of [Kim24]'s maintenance relation with existing [Lew73b] infrastructure: temporal intervals, event sorts, and counterfactual semantics.

Kim's core claim: stative Class II psych verbs involve a maintenance causal relation, not eventive causation. The two flavors differ along three dimensions:

Property	Eventive	Maintenance
Cause sort	event (external percept)	state (mental representation)
Effect	BECOME + state (transition)	state only (no transition)
Temporal	cause precedes effect	cause and effect contemporaneous
Counterfactual	effect persists after cause ceases	effect ceases with cause

The first three properties are formalized using existing Linglib types: Features.Dynamicity, NonemptyInterval.precedes/.overlaps. The fourth uses universalCounterfactual from Counterfactual.lean.

Key results

• Maintenance is temporally symmetric (states overlap); eventive is asymmetric
• Temporal precedence and overlap are mutually exclusive (the two flavors can't hold simultaneously for the same pair of eventualities)
• CausalSource.toLink grounds the two-constructor enum in event structure

structure Causation.PsychLink.PsychCausalLink (Time : Type u_1) [LinearOrder Time] : Type u_1

A causal link between two eventualities in psych verb semantics.

Bundles event-structural and temporal properties that distinguish eventive causation (percept → state change) from maintenance causation (representation → state persistence).

• causeSort : Features.Dynamicity

  Ontological sort of the causing eventuality

• effectSort : Features.Dynamicity

  Ontological sort of the caused eventuality

• involvesTransition : Bool

  Does the effect involve a transition (BECOME in [RHL98])? Eventive: [CAUSE [BECOME [STATE]]] — yes. Maintenance: [CAUSE [STATE]] — no.

• temporalConstraint : NonemptyInterval Time → NonemptyInterval Time → Prop

  Temporal constraint on the runtimes of cause and effect

def Causation.PsychLink.eventiveLink (Time : Type u_1) [LinearOrder Time] : PsychCausalLink Time

Eventive causation: an external percept/event CAUSES a change of mental state. The cause temporally precedes the effect.

Event structure: [[percept ACT] CAUSE [BECOME [experiencer STATE]]] Example: "The noise frightened John" — the noise event happens, THEN John enters the frightened state.

Equations

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

def Causation.PsychLink.maintenanceLink (Time : Type u_1) [LinearOrder Time] : PsychCausalLink Time

Maintenance causation: a mental representation MAINTAINS a psychological state. Cause and effect are temporally contemporaneous.

Event structure: [[representation STATE] CAUSE [experiencer STATE]] Example: "The problem concerns John" — the problem's mental representation and John's concern state coexist; if the representation ceased, the concern would cease.

[Kim24] identifies three defining properties: (a) Relates two eventualities (both states) (b) Temporal contemporaneity (τ(cause) overlaps τ(effect)) (c) Counterfactual dependence (effect ceases when cause ceases)

Equations

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

def Causation.PsychLink.CausalSource.toLink (Time : Type u_1) [LinearOrder Time] : Psych.CausalSource → PsychCausalLink Time

Ground CausalSource (a two-constructor enum) in the richer PsychCausalLink structure. External source = eventive causation; internal source = maintenance causation.

Equations

• Causation.PsychLink.CausalSource.toLink Time Causation.Psych.CausalSource.external = Causation.PsychLink.eventiveLink Time
• Causation.PsychLink.CausalSource.toLink Time Causation.Psych.CausalSource.internal = Causation.PsychLink.maintenanceLink Time

theorem Causation.PsychLink.maintenance_temporal_symmetric {Time : Type u_1} [LinearOrder Time] (i₁ i₂ : NonemptyInterval Time) (h : (maintenanceLink Time).temporalConstraint i₁ i₂) : (maintenanceLink Time).temporalConstraint i₂ i₁

Maintenance is temporally symmetric: if cause overlaps effect, effect overlaps cause. Delegates to NonemptyInterval.overlaps_symm.

theorem Causation.PsychLink.eventive_temporal_irrefl {Time : Type u_1} [LinearOrder Time] (i : NonemptyInterval Time) : ¬(eventiveLink Time).temporalConstraint i i

Eventive causation is temporally irreflexive: no eventuality can precede itself. Delegates to NonemptyInterval.precedes_irrefl.

theorem Causation.PsychLink.precedes_excludes_overlap {Time : Type u_1} [LinearOrder Time] (i₁ i₂ : NonemptyInterval Time) (h : (eventiveLink Time).temporalConstraint i₁ i₂) : ¬(maintenanceLink Time).temporalConstraint i₁ i₂

Precedence and overlap are mutually exclusive: if cause precedes effect, they cannot overlap. This is the structural basis for the eventive/stative dichotomy — the two temporal configurations are incompatible for any given pair of eventualities. Delegates to NonemptyInterval.precedes_not_overlaps.

theorem Causation.PsychLink.maintenance_both_states {Time : Type u_1} [LinearOrder Time] : (maintenanceLink Time).causeSort = Features.Dynamicity.stative ∧ (maintenanceLink Time).effectSort = Features.Dynamicity.stative

Maintenance relates two states ([Kim24] property (a)).

theorem Causation.PsychLink.eventive_both_dynamic {Time : Type u_1} [LinearOrder Time] : (eventiveLink Time).causeSort = Features.Dynamicity.dynamic ∧ (eventiveLink Time).effectSort = Features.Dynamicity.dynamic

Eventive causation relates two dynamic eventualities.

theorem Causation.PsychLink.maintenance_no_transition {Time : Type u_1} [LinearOrder Time] : (maintenanceLink Time).involvesTransition = false

Maintenance involves no transition (no BECOME).

theorem Causation.PsychLink.eventive_has_transition {Time : Type u_1} [LinearOrder Time] : (eventiveLink Time).involvesTransition = true

Eventive causation involves a transition (BECOME).

theorem Causation.PsychLink.flavors_differ_on_all_dimensions {Time : Type u_1} [LinearOrder Time] : (eventiveLink Time).causeSort = Features.Dynamicity.dynamic ∧ (maintenanceLink Time).causeSort = Features.Dynamicity.stative ∧ (eventiveLink Time).involvesTransition = true ∧ (maintenanceLink Time).involvesTransition = false

The two causal flavors assign opposite values on every dimension.

def Causation.PsychLink.counterfactuallyDependent {W : Type u_1} [DecidableEq W] [Fintype W] (sim : Core.Order.SimilarityOrdering W) (causeProp effectProp : W → Prop) [DecidablePred causeProp] [DecidablePred effectProp] (w : W) : Prop

Counterfactual dependence: in the closest worlds where the cause doesn't hold, the effect doesn't hold either.

¬cause □→ ¬effect

This characterizes maintenance causation ([Kim24] property (c)): "The problem concerns John" — in the closest worlds where John no longer has the mental representation, the concern ceases.

Equations

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

@[implicit_reducible]

instance Causation.PsychLink.counterfactuallyDependent_decidable {W : Type u_1} [DecidableEq W] [Fintype W] (sim : Core.Order.SimilarityOrdering W) (causeProp effectProp : W → Prop) [DecidablePred causeProp] [DecidablePred effectProp] (w : W) : Decidable (counterfactuallyDependent sim causeProp effectProp w)

Equations

• Causation.PsychLink.counterfactuallyDependent_decidable sim causeProp effectProp w = Causation.PsychLink.counterfactuallyDependent_decidable._aux_1 sim causeProp effectProp w

def Causation.PsychLink.counterfactuallyPersistent {W : Type u_1} [DecidableEq W] [Fintype W] (sim : Core.Order.SimilarityOrdering W) (causeProp effectProp : W → Prop) [DecidablePred causeProp] [DecidablePred effectProp] (w : W) : Prop

Counterfactual persistence: in the closest worlds where the cause doesn't hold, the effect STILL holds.

¬cause □→ effect

This characterizes eventive causation: "The noise frightened John" — even if the noise hadn't occurred (in the closest worlds), the frightened state, once established by BECOME, persists independently.

Equations

• Causation.PsychLink.counterfactuallyPersistent sim causeProp effectProp w = Semantics.Conditionals.Counterfactual.universalCounterfactual sim (fun (w : W) => ¬causeProp w) effectProp w

@[implicit_reducible]

instance Causation.PsychLink.counterfactuallyPersistent_decidable {W : Type u_1} [DecidableEq W] [Fintype W] (sim : Core.Order.SimilarityOrdering W) (causeProp effectProp : W → Prop) [DecidablePred causeProp] [DecidablePred effectProp] (w : W) : Decidable (counterfactuallyPersistent sim causeProp effectProp w)

Equations

• Causation.PsychLink.counterfactuallyPersistent_decidable sim causeProp effectProp w = Causation.PsychLink.counterfactuallyPersistent_decidable._aux_1 sim causeProp effectProp w

theorem Causation.PsychLink.dependent_excludes_persistent {W : Type u_1} [DecidableEq W] [Fintype W] (sim : Core.Order.SimilarityOrdering W) (causeProp effectProp : W → Prop) [DecidablePred causeProp] [DecidablePred effectProp] (w : W) (hDep : counterfactuallyDependent sim causeProp effectProp w) (hNonempty : (sim.closestWorlds w {w : W | ¬causeProp w}).Nonempty) : ¬counterfactuallyPersistent sim causeProp effectProp w

Counterfactual dependence and persistence are mutually exclusive when the set of closest ¬cause worlds is non-empty.

If all closest ¬cause worlds satisfy ¬effect (dependence), then at least one closest world falsifies effect, so persistence fails.

Proved by extracting a witness from the non-empty closest-world list and showing it satisfies ¬ effectProp w (from dependence) and effectProp w (from persistence), a contradiction.

theorem Causation.PsychLink.maintenance_three_properties {Time : Type u_1} [LinearOrder Time] : (maintenanceLink Time).causeSort = Features.Dynamicity.stative ∧ (maintenanceLink Time).effectSort = Features.Dynamicity.stative ∧ (maintenanceLink Time).temporalConstraint = NonemptyInterval.overlaps ∧ (maintenanceLink Time).involvesTransition = false

The three defining properties of maintenance causation from [Kim24], formalized using existing infrastructure:

(a) Relates two eventualities — both are states (Features.Dynamicity.stative) (b) Temporal contemporaneity — NonemptyInterval.overlaps (c) No transition — effect is a persisting state, not a change

Property (c) is formalized structurally (no BECOME) rather than via counterfactuals, because the counterfactual characterization ("effect ceases when cause ceases") requires a concrete world space and similarity ordering. The structural version — no BECOME means no independent grounding for the effect — is the deeper explanation for WHY maintenance-caused states are counterfactually dependent.