Documentation

Linglib.Core.Subjectivity

Subjectivity Cline #

@cite{traugott-dasher-2002} @cite{traugott-2010}

Traugott & Dasher's synchronic cline of (inter)subjectivity, formalized as an ordered type. Expressions range from nonsubjective (ideational, propositional) through subjective (speaker attitude/belief) to intersubjective (addressee face/self-image). The diachronic hypothesis is that coded (inter)subjective meanings arise later than non-subjective ones; subjectification precedes intersubjectification.

Bridges #

EpistemicAuthority to SubjectivityLevel: ego = subjective, allocutive = intersubjective, nonparticipant = nonSubjective.
The cline connects modal semantics (speaker assessment = subjective), politeness (addressee face = intersubjective), and RSA (speaker model = subjectified speaker).

inductive Core.Subjectivity.SubjectivityLevel :

Synchronic subjectivity scale (@cite{traugott-dasher-2002} Table 1, @cite{traugott-2010} cline 2). Diachronic work shows that subjective polysemies arise later than ideational ones, and intersubjective polysemies arise later than subjective ones.

nonSubjective : SubjectivityLevel
subjective : SubjectivityLevel
intersubjective : SubjectivityLevel

Instances For

instance Core.Subjectivity.instDecidableEqSubjectivityLevel :

DecidableEq SubjectivityLevel

Equations

Core.Subjectivity.instDecidableEqSubjectivityLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Core.Subjectivity.instReprSubjectivityLevel :

Repr SubjectivityLevel

Equations

Core.Subjectivity.instReprSubjectivityLevel = { reprPrec := Core.Subjectivity.instReprSubjectivityLevel.repr }

def Core.Subjectivity.instReprSubjectivityLevel.repr :

SubjectivityLevel → ℕ → Std.Format

Equations

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

Instances For

def Core.Subjectivity.instBEqSubjectivityLevel.beq :

SubjectivityLevel → SubjectivityLevel → Bool

Equations

Core.Subjectivity.instBEqSubjectivityLevel.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Core.Subjectivity.instBEqSubjectivityLevel :

BEq SubjectivityLevel

Equations

Core.Subjectivity.instBEqSubjectivityLevel = { beq := Core.Subjectivity.instBEqSubjectivityLevel.beq }

def Core.Subjectivity.instInhabitedSubjectivityLevel.default :

SubjectivityLevel

Equations

Core.Subjectivity.instInhabitedSubjectivityLevel.default = Core.Subjectivity.SubjectivityLevel.nonSubjective

Instances For

instance Core.Subjectivity.instInhabitedSubjectivityLevel :

Inhabited SubjectivityLevel

Equations

Core.Subjectivity.instInhabitedSubjectivityLevel = { default := Core.Subjectivity.instInhabitedSubjectivityLevel.default }

def Core.Subjectivity.SubjectivityLevel.toNat :

SubjectivityLevel → ℕ

Numeric encoding for ordering.

Equations

Instances For

instance Core.Subjectivity.instLESubjectivityLevel :

LE SubjectivityLevel

Equations

Core.Subjectivity.instLESubjectivityLevel = { le := fun (a b : Core.Subjectivity.SubjectivityLevel) => a.toNat ≤ b.toNat }

instance Core.Subjectivity.instLTSubjectivityLevel :

LT SubjectivityLevel

Equations

Core.Subjectivity.instLTSubjectivityLevel = { lt := fun (a b : Core.Subjectivity.SubjectivityLevel) => a.toNat < b.toNat }

instance Core.Subjectivity.instDecidableLeSubjectivityLevel (a b : SubjectivityLevel) :

Decidable (a ≤ b)

Equations

Core.Subjectivity.instDecidableLeSubjectivityLevel a b = inferInstanceAs (Decidable (a.toNat ≤ b.toNat))

instance Core.Subjectivity.instDecidableLtSubjectivityLevel (a b : SubjectivityLevel) :

Decidable (a < b)

Equations

Core.Subjectivity.instDecidableLtSubjectivityLevel a b = inferInstanceAs (Decidable (a.toNat < b.toNat))

theorem Core.Subjectivity.le_total (a b : SubjectivityLevel) :

a ≤ b ∨ b ≤ a

The cline is totally ordered.

def Core.Subjectivity.SubjectivityLevel.ofEpistemicAuthority :

Epistemicity.EpistemicAuthority → SubjectivityLevel

Bridge: epistemic authority to subjectivity level.

ego (speaker has privileged access) maps to subjective
allocutive (addressee has privileged access) maps to intersubjective
nonparticipant maps to nonSubjective

Equations

Instances For

theorem Core.Subjectivity.intersubjective_ge_subjective :

SubjectivityLevel.subjective ≤ SubjectivityLevel.intersubjective

Intersubjectivity presupposes subjectivity (@cite{traugott-2010} section 2).

theorem Core.Subjectivity.nonSubjective_le (l : SubjectivityLevel) :

SubjectivityLevel.nonSubjective ≤ l

Non-subjective is the minimum.

inductive Core.Subjectivity.Performativity :

Whether the utterance constitutes the act it describes or merely reports it.

The performative/descriptive distinction originates with Austin (1962) and cross-cuts subjectivity: a speaker-oriented utterance can be performative ("You must go" — creates the obligation) or descriptive ("He must be home" — assesses without creating). @cite{narrog-2012} §2.4 argues that Traugott's subjectivity cline conflates speaker-orientation with performativity, collapsing distinctions that matter for face-threat, person restrictions, and diachronic change paths.

This dimension connects to:

Modal semantics: deontic = performative; epistemic = descriptive
Politeness: performative + volitive = face-threatening (Brown & Levinson)
Speech acts: performatives (Austin) vs constatives

performative : Performativity
descriptive : Performativity

Instances For

instance Core.Subjectivity.instDecidableEqPerformativity :

DecidableEq Performativity

Equations

Core.Subjectivity.instDecidableEqPerformativity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Subjectivity.instReprPerformativity.repr :

Performativity → ℕ → Std.Format

Equations

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

Instances For

instance Core.Subjectivity.instReprPerformativity :

Repr Performativity

Equations

Core.Subjectivity.instReprPerformativity = { reprPrec := Core.Subjectivity.instReprPerformativity.repr }

def Core.Subjectivity.instBEqPerformativity.beq :

Performativity → Performativity → Bool

Equations

Core.Subjectivity.instBEqPerformativity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Core.Subjectivity.instBEqPerformativity :

BEq Performativity

Equations

Core.Subjectivity.instBEqPerformativity = { beq := Core.Subjectivity.instBEqPerformativity.beq }

instance Core.Subjectivity.instInhabitedPerformativity :

Inhabited Performativity

Equations

Core.Subjectivity.instInhabitedPerformativity = { default := Core.Subjectivity.instInhabitedPerformativity.default }

def Core.Subjectivity.instInhabitedPerformativity.default :

Equations

Core.Subjectivity.instInhabitedPerformativity.default = Core.Subjectivity.Performativity.performative

Instances For