Empathy

[Kun87]

Empathy in the sense of [Kun87]: the speaker's identification with an event participant. Empathy is a graded notion — the speaker can identify more or less strongly with a given participant — and it cross-cuts person, animacy, and discourse role.

Why a separate primitive

Empathy is not an attitude in the propositional sense (Sells's self), nor is it discourse participation (Sells's source). It is a third perspectival relation: the speaker's affective alignment with a participant. In Romance, dative clitics tend to encode empathy ([CM15]); in Japanese, transferring verbs yaru/kureru lexically alternate by speaker-empathy ([Kun87] p. 246).

This file provides the minimal primitive. Frameworks that use empathy (e.g., [CM15]'s antilogophoricity hierarchy) live in their own files and import this one.

def Features.Empathy.IsEmpathyLocus (p : Prop) : Prop

A binary empathy property. The speaker either identifies with the referent or does not. This is the simplest possible primitive; graded variants (the Empathy Hierarchy of [Kun87] ch. 5) can be added when downstream consumers need them.

Equations

• Features.Empathy.IsEmpathyLocus p = p

inductive Features.Empathy.EmpathyDefault : Type

Kuno's Speech-Act Empathy Hierarchy ([Kun87] p. 207): speaker > addressee > third person, in terms of empathy default. Captured here as a coarse three-level enum; the application of this hierarchy to specific syntactic positions (e.g., dative clitic = empathy locus, per [CM15]) is downstream.

• speaker : EmpathyDefault

  Speaker — empathy is automatic.

• addressee : EmpathyDefault

  Addressee — empathy is highly accessible.

• thirdPerson : EmpathyDefault

  Third person — empathy must be linguistically marked.

@[implicit_reducible]

instance Features.Empathy.instDecidableEqEmpathyDefault : DecidableEq EmpathyDefault

Equations

• Features.Empathy.instDecidableEqEmpathyDefault x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Features.Empathy.instReprEmpathyDefault.repr : EmpathyDefault → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Features.Empathy.instReprEmpathyDefault : Repr EmpathyDefault

Equations

• Features.Empathy.instReprEmpathyDefault = { reprPrec := Features.Empathy.instReprEmpathyDefault.repr }

@[implicit_reducible]

instance Features.Empathy.instInhabitedEmpathyDefault : Inhabited EmpathyDefault

Equations

• Features.Empathy.instInhabitedEmpathyDefault = { default := Features.Empathy.instInhabitedEmpathyDefault.default }

def Features.Empathy.EmpathyDefault.rank : EmpathyDefault → Nat

Numeric rank for the empathy default hierarchy.

Equations

• Features.Empathy.EmpathyDefault.speaker.rank = 2
• Features.Empathy.EmpathyDefault.addressee.rank = 1
• Features.Empathy.EmpathyDefault.thirdPerson.rank = 0

theorem Features.Empathy.EmpathyDefault.hierarchy : speaker.rank > addressee.rank ∧ addressee.rank > thirdPerson.rank