Labov (2006): The Social Stratification of English in New York City

Labov's survey of the Lower East Side measures phonological variables by social class, by contextual style from casual speech to minimal pairs, and by age. This file states what the book reads off its printed tables: the stratification of three department stores, the class and stylistic stratification of every variable except the lower class's (oh), and the fit of each variable's table of age by class to Labov's models of a stigmatized feature, stable or changing, and of an incoming prestige feature.

Main statements

• classDeviant_iff_styleDeviant: a class group deviates from class stratification exactly when it deviates from stylistic stratification.
• r_caseIIB: (r) is distributed as a prestige feature in change.
• ing_careful_caseIA: (ing) in careful speech is distributed as a stable stigmatized feature.

Implementation notes

• The printed tables are Data/Experiments/Labov2006.json. Variable.toStandard negates the (th) and (dh) indexes, which score stops and affricates above the prestige fricative, so that every signed index grows toward the standard.
• The models keep the cells the prose explains: an extreme word puts the lowest or highest class at that age's extreme, and a comparative compares the two ages within the middle-ranking classes. The lower class gets no age clause, being parenthesized in the model of a changing stigmatized feature and flat in the (r) table Labov matches to an incoming prestige feature.
• The deviation predicates use weak order, so the (æh) tie in word lists is no deviation, as the book reads it.

TODO

• Change from below is not formalized: Labov reads (æh) as Case III-B from the lower-class rise and (oh) as Case III-A from the ethnic table, and the ethnic table of (æh) is not stored.
• The (r) crossover of the lower middle class appears only in figures over six class groups.

References

• [Lab06]

The scales

@[instance_reducible]

instance Labov2006.instLinearOrderStore_studies : LinearOrder Store

Equations

• Labov2006.instLinearOrderStore_studies = LinearOrder.lift' Labov2006.Store.ctorIdx Labov2006.instLinearOrderStore_studies._proof_1

@[instance_reducible]

instance Labov2006.instLinearOrderStyle_studies : LinearOrder Style

Equations

• Labov2006.instLinearOrderStyle_studies = LinearOrder.lift' Labov2006.Style.ctorIdx Labov2006.instLinearOrderStyle_studies._proof_1

@[instance_reducible]

instance Labov2006.instLinearOrderClassGroup_studies : LinearOrder ClassGroup

Equations

• Labov2006.instLinearOrderClassGroup_studies = LinearOrder.lift' Labov2006.ClassGroup.ctorIdx Labov2006.instLinearOrderClassGroup_studies._proof_1

@[instance_reducible]

instance Labov2006.instLinearOrderSocioeconomicClass_studies : LinearOrder SocioeconomicClass

Equations

• Labov2006.instLinearOrderSocioeconomicClass_studies = LinearOrder.lift' Labov2006.SocioeconomicClass.ctorIdx Labov2006.instLinearOrderSocioeconomicClass_studies._proof_1

@[instance_reducible]

instance Labov2006.instLinearOrderSocialClass_studies : LinearOrder SocialClass

Equations

• Labov2006.instLinearOrderSocialClass_studies = LinearOrder.lift' Labov2006.SocialClass.ctorIdx Labov2006.instLinearOrderSocialClass_studies._proof_1

@[instance_reducible]

instance Labov2006.instLinearOrderAehAgeLevel_studies : LinearOrder AehAgeLevel

Equations

• Labov2006.instLinearOrderAehAgeLevel_studies = LinearOrder.lift' Labov2006.AehAgeLevel.ctorIdx Labov2006.instLinearOrderAehAgeLevel_studies._proof_1

@[instance_reducible]

instance Labov2006.instLinearOrderOhAgeLevel_studies : LinearOrder OhAgeLevel

Equations

• Labov2006.instLinearOrderOhAgeLevel_studies = LinearOrder.lift' Labov2006.OhAgeLevel.ctorIdx Labov2006.instLinearOrderOhAgeLevel_studies._proof_1

@[instance_reducible]

instance Labov2006.instBoundedOrderSocioeconomicClass_studies : BoundedOrder SocioeconomicClass

Equations

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

@[instance_reducible]

instance Labov2006.instBoundedOrderSocialClass_studies : BoundedOrder SocialClass

Equations

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

def Labov2006.AgeGroup.toLevel : AgeGroup → AgeLevel

a.toLevel is the age level of the (r) table that the adult age group a names.

Equations

• Labov2006.AgeGroup.younger.toLevel = Labov2006.AgeLevel.younger
• Labov2006.AgeGroup.older.toLevel = Labov2006.AgeLevel.older

The department store survey

def Labov2006.anyR1 (s : Store) : ℕ

anyR1 s is the percentage of the employees of s who used constricted [r] in all or some positions.

Equations

• Labov2006.anyR1 s = (Labov2006.completeResponses s).allR1 + (Labov2006.completeResponses s).someR1

theorem Labov2006.anyR1_strictMono : StrictMono anyR1

Constricted [r] rises with the prestige of the store.

theorem Labov2006.fourthStops_strictAnti : StrictAnti fun (s : Store) => (fourthStops s).percent

Stops in fourth fall with the prestige of the store.

Class and stylistic stratification

def Labov2006.cell (v : Variable) (g : ClassGroup) : Style → Option Data.Experiments.Decimal

cell v g s is the printed index of v for the class group g in the style s, if v was measured there.

Equations

• Labov2006.cell v g Labov2006.Style.casual = (Labov2006.classStratification g v).casual
• Labov2006.cell v g Labov2006.Style.careful = (Labov2006.classStratification g v).careful
• Labov2006.cell v g Labov2006.Style.reading = (Labov2006.classStratification g v).reading
• Labov2006.cell v g Labov2006.Style.wordList = (Labov2006.classStratification g v).wordList
• Labov2006.cell v g Labov2006.Style.minimalPair = (Labov2006.classStratification g v).minimalPair

def Labov2006.Variable.styles (v : Variable) : Set Style

v.styles is the set of styles in which v was measured.

Equations

• v.styles = {s : Labov2006.Style | ∀ (g : Labov2006.ClassGroup), (Labov2006.cell v g s).isSome = true}

@[instance_reducible]

instance Labov2006.instDecidablePredStyleMemSetStyles (v : Variable) : DecidablePred fun (x : Style) => x ∈ v.styles

Equations

• Labov2006.instDecidablePredStyleMemSetStyles v s = { decide := decide (∀ a ∈ Finset.univ, (fun (g : Labov2006.ClassGroup) => (Labov2006.cell v g s).isSome = true) a), reflects_decide := ⋯ }

theorem Labov2006.mem_styles (s : Style) : s ∈ Variable.r.styles ∧ (s ∈ Variable.aeh.styles ↔ s ≤ Style.wordList) ∧ (s ∈ Variable.oh.styles ↔ s ≤ Style.wordList) ∧ (s ∈ Variable.th.styles ↔ s ≤ Style.reading) ∧ (s ∈ Variable.dh.styles ↔ s ≤ Style.reading)

(r) was measured in all five styles, the vowels in all but minimal pairs, and the consonants in the three styles of connected speech.

def Labov2006.Variable.toStandard : Variable → ℚ → ℚ

v.toStandard signs an index of v so that it grows toward the prestige form. The (r) index counts the constricted variant and the vowel indexes grow toward the corrected low vowels, while the (th) and (dh) indexes score the stop and the affricate above the fricative and are negated.

Equations

• Labov2006.Variable.r.toStandard = id
• Labov2006.Variable.aeh.toStandard = id
• Labov2006.Variable.oh.toStandard = id
• Labov2006.Variable.th.toStandard = Neg.neg
• Labov2006.Variable.dh.toStandard = Neg.neg

def Labov2006.standardIndex (v : Variable) (g : ClassGroup) (s : Style) : ℚ

standardIndex v g s is the signed index of v for g in s, and 0 where nothing was measured.

Equations

• Labov2006.standardIndex v g s = v.toStandard ((Option.map Data.Experiments.Decimal.toRat (Labov2006.cell v g s)).getD 0)

def Labov2006.ClassStratified (v : Variable) (s : Style) : Prop

v is class stratified in the style s when a higher class group is closer to the standard.

Equations

• Labov2006.ClassStratified v s = StrictMono fun (g : Labov2006.ClassGroup) => Labov2006.standardIndex v g s

def Labov2006.StyleStratified (v : Variable) (g : ClassGroup) : Prop

v is stylistically stratified in the class group g when a more formal style is closer to the standard.

Equations

• Labov2006.StyleStratified v g = StrictMonoOn (Labov2006.standardIndex v g) v.styles

def Labov2006.ClassDeviant (v : Variable) (g : ClassGroup) : Prop

A class group deviates from the class stratification of v when the groups are out of order in some style and the other groups are in order in every style.

Equations

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

def Labov2006.StyleDeviant (v : Variable) (g : ClassGroup) : Prop

A class group deviates from the stylistic stratification of v when its index does not move toward the standard with formality.

Equations

• Labov2006.StyleDeviant v g = ¬MonotoneOn (Labov2006.standardIndex v g) v.styles

@[instance_reducible]

instance Labov2006.instDecidableClassStratified (v : Variable) (s : Style) : Decidable (ClassStratified v s)

Equations

• Labov2006.instDecidableClassStratified v s = id inferInstance

@[instance_reducible]

instance Labov2006.instDecidableStyleStratified (v : Variable) (g : ClassGroup) : Decidable (StyleStratified v g)

Equations

• Labov2006.instDecidableStyleStratified v g = id inferInstance

@[instance_reducible]

instance Labov2006.instDecidableClassDeviant (v : Variable) (g : ClassGroup) : Decidable (ClassDeviant v g)

Equations

• Labov2006.instDecidableClassDeviant v g = id inferInstance

@[instance_reducible]

instance Labov2006.instDecidableStyleDeviant (v : Variable) (g : ClassGroup) : Decidable (StyleDeviant v g)

Equations

• Labov2006.instDecidableStyleDeviant v g = id inferInstance

theorem Labov2006.r_stratified : (∀ s ∈ Variable.r.styles, ClassStratified Variable.r s) ∧ ∀ (g : ClassGroup), StyleStratified Variable.r g

The class groups are differentiated on (r) in every style, and every group's (r) rises with formality, at all fifteen points of the table.

theorem Labov2006.aeh_stratified : (∀ (g : ClassGroup), StyleStratified Variable.aeh g) ∧ (∀ s ∈ Variable.aeh.styles, s ≠ Style.wordList → ClassStratified Variable.aeh s) ∧ (Monotone fun (g : ClassGroup) => standardIndex Variable.aeh g Style.wordList) ∧ standardIndex Variable.aeh ClassGroup.lower Style.wordList = standardIndex Variable.aeh ClassGroup.working Style.wordList

Every class group shifts (æh) with style, and the groups are differentiated except that the lower and working classes reach the same point in word lists.

theorem Labov2006.th_stratified : (∀ s ∈ Variable.th.styles, ClassStratified Variable.th s) ∧ ∀ (g : ClassGroup), StyleStratified Variable.th g

(th) is stratified regularly by class and by style.

theorem Labov2006.dh_stratified : (∀ s ∈ Variable.dh.styles, ClassStratified Variable.dh s) ∧ ∀ (g : ClassGroup), StyleStratified Variable.dh g

(dh) is stratified regularly by class and by style.

theorem Labov2006.oh_double_deviation : ClassDeviant Variable.oh ClassGroup.lower ∧ StyleDeviant Variable.oh ClassGroup.lower ∧ (∀ (g : ClassGroup), g ≠ ClassGroup.lower → StyleStratified Variable.oh g) ∧ ∀ s ∈ Variable.oh.styles, StrictMonoOn (fun (g : ClassGroup) => standardIndex Variable.oh g s) {g : ClassGroup | g ≠ ClassGroup.lower}

On (oh) the lower class deviates from class and from stylistic stratification, while the working and middle classes are stratified against each other and each shifts with style.

theorem Labov2006.classDeviant_iff_styleDeviant (v : Variable) (g : ClassGroup) : ClassDeviant v g ↔ StyleDeviant v g

On the table, a class group deviates from class stratification exactly when it deviates from stylistic stratification, as Labov's hypothesis has it.

theorem Labov2006.classDeviant_iff (v : Variable) (g : ClassGroup) : ClassDeviant v g ↔ v = Variable.oh ∧ g = ClassGroup.lower

The lower class on (oh) is the only deviation in the table.

Apparent time

def Labov2006.CaseIA {κ : Type u_1} {β : Type u_2} [LinearOrder κ] [BoundedOrder κ] [Preorder β] (f : AgeGroup → κ → β) : Prop

CaseIA f says that the use f of a feature by age and class is Labov's Case I-A, a stigmatized feature with no change in progress. The lowest-ranking class uses it most and the highest least at either age, and the middle-ranking classes use it less as they age.

Equations

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

def Labov2006.CaseIB {κ : Type u_1} {β : Type u_2} [LinearOrder κ] [BoundedOrder κ] [Preorder β] (f : AgeGroup → κ → β) : Prop

CaseIB f says that f is Labov's Case I-B, a stigmatized feature with change in progress. The highest-ranking class uses it least at either age, and the middle-ranking classes use it more as they age.

Equations

• Labov2006.CaseIB f = ((∀ (a : Labov2006.AgeGroup) (c : κ), f a ⊤ ≤ f a c) ∧ ∀ c ∈ Set.Ioo ⊥ ⊤, f Labov2006.AgeGroup.younger c < f Labov2006.AgeGroup.older c)

def Labov2006.CaseIIB {κ : Type u_1} {β : Type u_2} [LinearOrder κ] [BoundedOrder κ] [Preorder β] (f : AgeGroup → κ → β) : Prop

CaseIIB f says that f is Labov's Case II-B, a prestige feature with change in progress. The highest-ranking class leads the younger speakers and uses it more when young than when old, and the middle-ranking classes acquire it as they age.

Equations

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

def Labov2006.ReversesAtTop {κ : Type u_1} {β : Type u_2} [LinearOrder κ] [BoundedOrder κ] [Preorder β] (f : AgeGroup → κ → β) : Prop

ReversesAtTop f says that below the highest-ranking class the younger speakers use the feature more than the older, and that the highest class reverses this.

Equations

• Labov2006.ReversesAtTop f = ((∀ c < ⊤, f Labov2006.AgeGroup.older c < f Labov2006.AgeGroup.younger c) ∧ f Labov2006.AgeGroup.younger ⊤ < f Labov2006.AgeGroup.older ⊤)

theorem Labov2006.CaseIA.not_caseIB {κ : Type u_1} {β : Type u_2} [LinearOrder κ] [BoundedOrder κ] [Preorder β] {f : AgeGroup → κ → β} {c : κ} (hc : c ∈ Set.Ioo ⊥ ⊤) (h : CaseIA f) : ¬CaseIB f

The two schemes for a stigmatized feature are opposite in the middle-ranking classes.

@[instance_reducible]

instance Labov2006.instDecidableCaseIA {κ : Type u_1} {β : Type u_2} [LinearOrder κ] [BoundedOrder κ] [Preorder β] (f : AgeGroup → κ → β) [Fintype κ] [DecidableLT κ] [DecidableLE β] [DecidableLT β] : Decidable (CaseIA f)

Equations

• Labov2006.instDecidableCaseIA f = id inferInstance

@[instance_reducible]

instance Labov2006.instDecidableCaseIB {κ : Type u_1} {β : Type u_2} [LinearOrder κ] [BoundedOrder κ] [Preorder β] (f : AgeGroup → κ → β) [Fintype κ] [DecidableLT κ] [DecidableLE β] [DecidableLT β] : Decidable (CaseIB f)

Equations

• Labov2006.instDecidableCaseIB f = id inferInstance

@[instance_reducible]

instance Labov2006.instDecidableCaseIIB {κ : Type u_1} {β : Type u_2} [LinearOrder κ] [BoundedOrder κ] [Preorder β] (f : AgeGroup → κ → β) [Fintype κ] [DecidableLT κ] [DecidableLE β] [DecidableLT β] : Decidable (CaseIIB f)

Equations

• Labov2006.instDecidableCaseIIB f = id inferInstance

@[instance_reducible]

instance Labov2006.instDecidableReversesAtTop {κ : Type u_1} {β : Type u_2} [LinearOrder κ] [BoundedOrder κ] [Preorder β] (f : AgeGroup → κ → β) [Fintype κ] [DecidableLT κ] [DecidableLT β] : Decidable (ReversesAtTop f)

Equations

• Labov2006.instDecidableReversesAtTop f = id inferInstance

theorem Labov2006.upgliding_caseIB : CaseIB fun (a : AgeGroup) (c : SocioeconomicClass) => (upglidingByAgeAndClass a c).percent

/ʌy/ is distributed as a stigmatized feature in change.

theorem Labov2006.r_caseIIB : CaseIIB fun (a : AgeGroup) (c : SocioeconomicClass) => (rCasualByAgeAndClass a.toLevel c).index

(r) in casual speech is distributed as a prestige feature in change, in every detail.

theorem Labov2006.r_gap_widens : ↑(someRCasualByAge AgeGroup.older).upperMiddle - ↑(someRCasualByAge AgeGroup.older).lowerClasses < ↑(someRCasualByAge AgeGroup.younger).upperMiddle - ↑(someRCasualByAge AgeGroup.younger).lowerClasses

The stratification of (r) sharpens, the upper middle class's lead in using any (r-1) in casual speech being wider among the younger speakers.

theorem Labov2006.aeh_caseIIB : CaseIIB fun (a : AgeGroup) (c : SocialClass) => (aehByAgeAndClass a c).index

By social class, (æh) is distributed as a prestige feature in change, the corrected low vowel. Labov goes on to read it as change from below with a later correction from above, since the lower class also raises the vowel (aeh_lowerClass_monotone).

theorem Labov2006.aeh_lowerClass_monotone : Monotone fun (a : AehAgeLevel) => (aehLowerClassByAge a).index

The lower class raises (æh) steadily, its index falling from the oldest level to the youngest.

theorem Labov2006.oh_no_case : (¬CaseIA fun (a : AgeGroup) (c : SocialClass) => (ohByAgeAndClass a c).index) ∧ (¬CaseIB fun (a : AgeGroup) (c : SocialClass) => (ohByAgeAndClass a c).index) ∧ ¬CaseIIB fun (a : AgeGroup) (c : SocialClass) => (ohByAgeAndClass a c).index

By social class, (oh) shows none of the models' age contrasts.

theorem Labov2006.oh_oldest_lowest : (∀ (a : OhAgeLevel), a ≠ OhAgeLevel.age60 → (ohByAgeAndEthnicity a).jews < (ohByAgeAndEthnicity OhAgeLevel.age60).jews ∧ (ohByAgeAndEthnicity a).italians < (ohByAgeAndEthnicity OhAgeLevel.age60).italians ∧ (ohByAgeAndEthnicity a).others < (ohByAgeAndEthnicity OhAgeLevel.age60).others) ∧ Monotone fun (a : OhAgeLevel) => (ohByAgeAndEthnicity a).italians

In each ethnic group of the three lower social classes the oldest speakers have the lowest (oh) vowels, and the Italian index falls level by level toward the young.

theorem Labov2006.same_pattern : (ReversesAtTop fun (a : AgeGroup) (c : SocialClass) => (thDhByAgeAndClass a c).th) ∧ (ReversesAtTop fun (a : AgeGroup) (c : SocialClass) => (thDhByAgeAndClass a c).dh) ∧ ReversesAtTop fun (a : AgeGroup) (c : SocialClass) => (ingByAgeAndClass a c).casual

(th), (dh) and casual (ing) share one pattern, in which the younger speakers of the three lower social classes use more of the stigmatized form and the upper middle class reverses this.

theorem Labov2006.pooled_reversal : (pooledLowerClasses AgeGroup.younger).th < (pooledLowerClasses AgeGroup.older).th ∧ (pooledLowerClasses AgeGroup.younger).dh < (pooledLowerClasses AgeGroup.older).dh ∧ (∀ c < ⊤, (rCasualByAgeAndClass AgeLevel.younger c).index ≤ (rCasualByAgeAndClass AgeLevel.older c).index) ∧ (pooledLowerClasses AgeGroup.younger).r < (pooledLowerClasses AgeGroup.older).r

Pooling the three lower social classes reverses the age relation for (th) and (dh) but not for (r), whose classes below the upper middle already have the older speakers at or above the younger. The pooled (r) is by social class and the (r) table by socioeconomic class, a crossing the book makes.

theorem Labov2006.ing_older_less (c : SocialClass) : c < ⊤ → (ingByAgeAndClass AgeGroup.older c).casual < (ingByAgeAndClass AgeGroup.younger c).casual ∧ (ingByAgeAndClass AgeGroup.older c).careful < (ingByAgeAndClass AgeGroup.younger c).careful

The older members of the three lower social classes use less /in/ than the younger, in both styles.

theorem Labov2006.ing_careful_caseIA : CaseIA fun (a : AgeGroup) (c : SocialClass) => (ingByAgeAndClass a c).careful

(ing) in careful speech is distributed as a stable stigmatized feature.

theorem Labov2006.ing_casual_departure : (∀ (a : AgeGroup) (c : SocialClass), (ingByAgeAndClass a c).casual ≤ (ingByAgeAndClass a ⊥).casual) ∧ (∀ c ∈ Set.Ioo ⊥ ⊤, (ingByAgeAndClass AgeGroup.older c).casual < (ingByAgeAndClass AgeGroup.younger c).casual) ∧ (∀ (c : SocialClass), (ingByAgeAndClass AgeGroup.younger ⊤).casual ≤ (ingByAgeAndClass AgeGroup.younger c).casual) ∧ (ingByAgeAndClass AgeGroup.older SocialClass.sc3).casual < (ingByAgeAndClass AgeGroup.older ⊤).casual

(ing) in casual speech departs from a stable stigmatized feature only in that the older upper middle class does not use it least.