Empathy

@cite{kuno-1987}

Empathy in the sense of @cite{kuno-1987}: 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 (@cite{charnavel-mateu-2015}); in Japanese, transferring verbs yaru/kureru lexically alternate by speaker-empathy (@cite{kuno-1987} p. 246).

This file provides the minimal primitive. Frameworks that use empathy (e.g., @cite{charnavel-mateu-2015}'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 @cite{kuno-1987} 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 (@cite{kuno-1987} 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 @cite{charnavel-mateu-2015}) 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 }

def Features.Empathy.instInhabitedEmpathyDefault.default : EmpathyDefault

Equations

• Features.Empathy.instInhabitedEmpathyDefault.default = Features.Empathy.EmpathyDefault.speaker

@[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