Documentation

Linglib.Theories.Semantics.Causation.PsychLink

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: stative Class II psych verbs involve a maintenance causal relation, not eventive causation. The two flavors differ along three dimensions:

PropertyEventiveMaintenance
Cause sortevent (external percept)state (mental representation)
EffectBECOME + state (transition)state only (no transition)
Temporalcause precedes effectcause and effect contemporaneous
Counterfactualeffect persists after cause ceaseseffect ceases with cause

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

Key results #

source
theorem Semantics.Causation.PsychLink.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. Delegates to Interval.overlaps_symm.

source
theorem Semantics.Causation.PsychLink.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. Delegates to Interval.precedes_irrefl.

source
theorem Semantics.Causation.PsychLink.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. Delegates to Interval.precedes_not_overlaps.

source
theorem Semantics.Causation.PsychLink.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 (@cite{kim-2024} property (a)).

source
theorem Semantics.Causation.PsychLink.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.

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

Maintenance involves no transition (no BECOME).

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

Eventive causation involves a transition (BECOME).

source
theorem Semantics.Causation.PsychLink.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.

source
def Semantics.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 (@cite{kim-2024} 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.
Instances For
    source
    @[implicit_reducible]
    instance Semantics.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
    source
    def Semantics.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
    Instances For
      source
      @[implicit_reducible]
      instance Semantics.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
      source
      theorem Semantics.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.

      source
      theorem Semantics.Causation.PsychLink.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.