Traugott (2010): (Inter)subjectivity and (Inter)subjectification: A Reassessment

This file formalizes Traugott's cline of (inter)subjectivity and its diachronic reading. An expression is subjective when it codes the speaker's attitude or viewpoint, and intersubjective when it codes the speaker's attention to the addressee's self-image. The cline orders coded meanings from nonsubjective through subjective to intersubjective (SubjectivityLevel). The diachronic claim is that the meanings an item newly codes move up the cline one level at a time, so that an intersubjective meaning arises from a subjectified one (Unidirectional). It follows that an item with an intersubjective meaning has a subjective one (subjective_mem_of_intersubjective_mem).

The case studies a piece of, a bit of and a shred of run from Partitive through Extended Partitive to Quantifier (Stage), the last stage they share. The Quantifier is the subjectified stage, and it alone shows all three of the expansions that Himmelmann makes criterial for grammaticalization (isGrammaticalized_iff).

Implementation notes

• A history records coded meanings only. A bit of is used intersubjectively as a hedge but codes only the subjective downtoner, so its history stops at the subjective level.
• Earlier and later meanings of an item coexist, which is why a history is a list and not a single current level.

References

• [Tra10a]
• [TD02]
• [Him04]

The cline

inductive Traugott2010.SubjectivityLevel : Type

The levels of the cline of (inter)subjectivity, from least to most subjective.

• nonSubjective : SubjectivityLevel

  The meaning describes the world or an event. Traugott labels this level as non-subjective or less subjective.

• subjective : SubjectivityLevel

  The meaning codes the speaker's attitude, belief or evaluation.

• intersubjective : SubjectivityLevel

  The meaning codes the speaker's attention to the addressee's face or self-image.

@[instance_reducible]

instance Traugott2010.instDecidableEqSubjectivityLevel : DecidableEq SubjectivityLevel

Equations

• Traugott2010.instDecidableEqSubjectivityLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Traugott2010.instFintypeSubjectivityLevel : Fintype SubjectivityLevel

Equations

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

def Traugott2010.instReprSubjectivityLevel.repr : SubjectivityLevel → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Traugott2010.instReprSubjectivityLevel : Repr SubjectivityLevel

Equations

• Traugott2010.instReprSubjectivityLevel = { reprPrec := Traugott2010.instReprSubjectivityLevel.repr }

@[instance_reducible]

instance Traugott2010.instLinearOrderSubjectivityLevel : LinearOrder SubjectivityLevel

The levels are ordered as they are listed.

Equations

• Traugott2010.instLinearOrderSubjectivityLevel = LinearOrder.lift' Traugott2010.SubjectivityLevel.ctorIdx ⋯

@[reducible, inline]

abbrev Traugott2010.History : Type

The levels of an item's coded meanings in the order they arose.

Equations

• Traugott2010.History = List Traugott2010.SubjectivityLevel

def Traugott2010.Unidirectional (h : History) : Prop

A history follows the cline when each newly coded meaning is at the level of the previous one or at the next level up.

Equations

• Traugott2010.Unidirectional h = List.IsChain (fun (x1 x2 : Traugott2010.SubjectivityLevel) => x1 ⩿ x2) h

@[instance_reducible]

instance Traugott2010.instDecidablePredHistoryUnidirectional : DecidablePred Unidirectional

Equations

• Traugott2010.instDecidablePredHistoryUnidirectional h = Traugott2010.instDecidablePredHistoryUnidirectional._aux_1 h

theorem Traugott2010.subjective_mem_of_intersubjective_mem {a : SubjectivityLevel} {h : History} (hc : Unidirectional (a :: h)) (ha : a ≤ SubjectivityLevel.subjective) (hi : SubjectivityLevel.intersubjective ∈ a :: h) : SubjectivityLevel.subjective ∈ a :: h

An item whose history begins at or below the subjective level and reaches an intersubjective meaning has a subjective one.

Partitive to Quantifier (section 4)

inductive Traugott2010.Stage : Type

The stages the three case studies share are the Partitive, the Extended Partitive with non-food and abstract complements, and the Quantifier, Stage III; the Degree Modifier is a later stage.

• partitive : Stage
• extendedPartitive : Stage
• quantifier : Stage

@[instance_reducible]

instance Traugott2010.instDecidableEqStage : DecidableEq Stage

Equations

• Traugott2010.instDecidableEqStage x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Traugott2010.instFintypeStage : Fintype Stage

Equations

• Traugott2010.instFintypeStage = { elems := { val := ↑Traugott2010.Stage.enumList, nodup := Traugott2010.Stage.enumList_nodup }, complete := Traugott2010.instFintypeStage._proof_1 }

def Traugott2010.instReprStage.repr : Stage → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Traugott2010.instReprStage : Repr Stage

Equations

• Traugott2010.instReprStage = { reprPrec := Traugott2010.instReprStage.repr }

@[instance_reducible]

instance Traugott2010.instLinearOrderStage : LinearOrder Stage

The stages are ordered as they are listed.

Equations

• Traugott2010.instLinearOrderStage = LinearOrder.lift' Traugott2010.Stage.ctorIdx Traugott2010.instLinearOrderStage._proof_1

def Traugott2010.Stage.level : Stage → SubjectivityLevel

The coded level at each stage. The Extended Partitive's implication that the unit is small is an invited inference and not yet coded, while the Quantifier's scalar meaning is coded and subjective.

Equations

• Traugott2010.Stage.partitive.level = Traugott2010.SubjectivityLevel.nonSubjective
• Traugott2010.Stage.extendedPartitive.level = Traugott2010.SubjectivityLevel.nonSubjective
• Traugott2010.Stage.quantifier.level = Traugott2010.SubjectivityLevel.subjective

theorem Traugott2010.stages_unidirectional : Unidirectional (List.map Stage.level [Stage.partitive, Stage.extendedPartitive, Stage.quantifier])

The stages' coded levels follow the cline.

inductive Traugott2010.Expansion : Type

The three expansions of [Him04].

• hostClass : Expansion
• syntactic : Expansion
• semanticPragmatic : Expansion

@[instance_reducible]

instance Traugott2010.instDecidableEqExpansion : DecidableEq Expansion

Equations

• Traugott2010.instDecidableEqExpansion x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Traugott2010.instFintypeExpansion : Fintype Expansion

Equations

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

def Traugott2010.instReprExpansion.repr : Expansion → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Traugott2010.instReprExpansion : Repr Expansion

Equations

• Traugott2010.instReprExpansion = { reprPrec := Traugott2010.instReprExpansion.repr }

def Traugott2010.Expansion.stage : Expansion → Stage

The stage at which each expansion first occurs. The complement generalizes at the Extended Partitive. At the Quantifier the string gains a second syntactic analysis, and its first noun loses partitive meaning and is enriched as a quantifier.

Equations

• Traugott2010.Expansion.hostClass.stage = Traugott2010.Stage.extendedPartitive
• Traugott2010.Expansion.syntactic.stage = Traugott2010.Stage.quantifier
• Traugott2010.Expansion.semanticPragmatic.stage = Traugott2010.Stage.quantifier

def Traugott2010.Stage.IsGrammaticalized (s : Stage) : Prop

A stage is grammaticalized, by [Him04]'s criteria, once every expansion has occurred.

Equations

• s.IsGrammaticalized = ∀ (e : Traugott2010.Expansion), e.stage ≤ s

@[instance_reducible]

instance Traugott2010.instDecidableIsGrammaticalized (s : Stage) : Decidable s.IsGrammaticalized

Equations

• Traugott2010.instDecidableIsGrammaticalized s = { decide := decide (∀ a ∈ Finset.univ, (fun (x : Traugott2010.Expansion) => x.stage ≤ s) a), reflects_decide := ⋯ }

theorem Traugott2010.isGrammaticalized_iff {s : Stage} : s.IsGrammaticalized ↔ s = Stage.quantifier

The Quantifier is the grammaticalized stage.