Psych Verb Causal Links

@cite{kim-2024} @cite{allen-1983} @cite{bach-1986} Formal integration of @cite{kim-2024}'s maintenance relation with existing @cite{lewis-1973} infrastructure: temporal intervals, event sorts, and counterfactual semantics.

Kim's core claim (§3.3): 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: EventSort, Interval.precedes/.overlaps. The fourth uses universalCounterfactualB 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 Semantics.Causation.PsychCausalLink.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 : Events.EventSort

  Ontological sort of the causing eventuality

• effectSort : Events.EventSort

  Ontological sort of the caused eventuality

• involvesTransition : Bool

  Does the effect involve a transition (BECOME in @cite{rappaport-hovav-levin-1998})? Eventive: [CAUSE [BECOME [STATE]]] — yes. Maintenance: [CAUSE [STATE]] — no.

• temporalConstraint : Core.Time.Interval Time → Core.Time.Interval Time → Prop

  Temporal constraint on the runtimes of cause and effect

def Semantics.Causation.PsychCausalLink.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 Semantics.Causation.PsychCausalLink.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.

@cite{kim-2024} 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 Semantics.Causation.PsychCausalLink.CausalSource.toLink (Time : Type u_1) [LinearOrder Time] : PsychCausation.CausalSource → PsychCausalLink Time

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

Equations

• Semantics.Causation.PsychCausalLink.CausalSource.toLink Time Semantics.Causation.PsychCausation.CausalSource.external = Semantics.Causation.PsychCausalLink.eventiveLink Time
• Semantics.Causation.PsychCausalLink.CausalSource.toLink Time Semantics.Causation.PsychCausation.CausalSource.internal = Semantics.Causation.PsychCausalLink.maintenanceLink Time

theorem Semantics.Causation.PsychCausalLink.maintenance_temporal_symmetric {Time : Type u_1} [LinearOrder Time] (i₁ i₂ : Core.Time.Interval Time) (h : (maintenanceLink Time).temporalConstraint i₁ i₂) : (maintenanceLink Time).temporalConstraint i₂ i₁

Maintenance is temporally symmetric: if cause overlaps effect, effect overlaps cause. This follows from Interval.overlaps being symmetric.

theorem Semantics.Causation.PsychCausalLink.eventive_temporal_irrefl {Time : Type u_1} [LinearOrder Time] (i : Core.Time.Interval Time) : ¬(eventiveLink Time).temporalConstraint i i

Eventive causation is temporally irreflexive: no eventuality can precede itself. Follows from Interval.precedes requiring i.finish < i.start, contradicting i.valid : i.start ≤ i.finish.

theorem Semantics.Causation.PsychCausalLink.precedes_excludes_overlap {Time : Type u_1} [LinearOrder Time] (i₁ i₂ : Core.Time.Interval 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.

theorem Semantics.Causation.PsychCausalLink.maintenance_both_states {Time : Type u_1} [LinearOrder Time] : (maintenanceLink Time).causeSort = Events.EventSort.state ∧ (maintenanceLink Time).effectSort = Events.EventSort.state

Maintenance relates two states (Kim §3.3 property (a)).

theorem Semantics.Causation.PsychCausalLink.eventive_both_dynamic {Time : Type u_1} [LinearOrder Time] : (eventiveLink Time).causeSort = Events.EventSort.action ∧ (eventiveLink Time).effectSort = Events.EventSort.action

Eventive causation relates two dynamic eventualities.

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

Maintenance involves no transition (no BECOME).

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

Eventive causation involves a transition (BECOME).

theorem Semantics.Causation.PsychCausalLink.flavors_differ_on_all_dimensions {Time : Type u_1} [LinearOrder Time] : (eventiveLink Time).causeSort = Events.EventSort.action ∧ (maintenanceLink Time).causeSort = Events.EventSort.state ∧ (eventiveLink Time).involvesTransition = true ∧ (maintenanceLink Time).involvesTransition = false

The two causal flavors assign opposite values on every dimension.

def Semantics.Causation.PsychCausalLink.counterfactuallyDependent {W : Type u_1} [DecidableEq W] (closer : W → W → W → Bool) (domain : List W) (causeProp effectProp : W → Bool) (w : W) : Bool

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

¬cause □→ ¬effect

This characterizes maintenance causation (Kim §3.3 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.

def Semantics.Causation.PsychCausalLink.counterfactuallyPersistent {W : Type u_1} [DecidableEq W] (closer : W → W → W → Bool) (domain : List W) (causeProp effectProp : W → Bool) (w : W) : Bool

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

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

theorem Semantics.Causation.PsychCausalLink.dependent_excludes_persistent {W : Type u_1} [DecidableEq W] (closer : W → W → W → Bool) (domain : List W) (causeProp effectProp : W → Bool) (w : W) (hDep : counterfactuallyDependent closer domain causeProp effectProp w = true) (hNonempty : (Conditionals.Counterfactual.closestWorldsB closer domain w (List.filter (fun (w : W) => !causeProp w) domain)).length > 0) : counterfactuallyPersistent closer domain causeProp effectProp w = false

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.

TODO: Proof via List.all reasoning — if l.all (fun w => !f w) and l ≠ [], then l.all f = false.

theorem Semantics.Causation.PsychCausalLink.maintenance_three_properties {Time : Type u_1} [LinearOrder Time] : (maintenanceLink Time).causeSort = Events.EventSort.state ∧ (maintenanceLink Time).effectSort = Events.EventSort.state ∧ (maintenanceLink Time).temporalConstraint = Core.Time.Interval.overlaps ∧ (maintenanceLink Time).involvesTransition = false

The three defining properties of maintenance causation from @cite{kim-2024}, formalized using existing infrastructure:

(a) Relates two eventualities — both are states (EventSort.state) (b) Temporal contemporaneity — Interval.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.