Berent (2026): Three arguments for abstraction in phonology

This file formalizes Berent's three experimental arguments that phonological grammar is substance-free. Phonology is abstract (§3.1): onsets with large sonority rises are preferred to small rises, these to plateaus, and these to falls, as in blif, bnif, bdif and lbif, and the preference survives print presentation and the suppression of the lips or the tongue. It is algebraic (§3.2): the Hebrew ban on roots that begin with two identical consonants extends to /θ/, which Hebrew lacks, and the preference of ASL signers for reduplication extends to unattested handshapes. It is amodal (§3.3): English speakers project the doubling restrictions of their spoken language onto novel ASL signs.

Each property is stated as an invariance. The markedness of an onset is its sonority rise, which depends on the two segments only through the major-class features that sonority reads, so it is blind to the articulator that the suppression experiments manipulate. Identity restrictions are invariant under any injective relabelling of the elements they compare, so they cannot distinguish attested from unattested feature values. The doubling reversal of Studies/BerentEtAl2016.lean holds over an arbitrary type of prosodic constituents, spoken or signed.

Main definitions

• onsetRise: the sonority rise across a two-consonant onset of feature-specified segments.
• InitialIdentity: a consonantal root begins with two identical consonants.

Main results

• sonority_cline: the onsets of blif, bnif, bdif and lbif are a large rise, a small rise, a plateau and a fall.
• onsetRise_congr, onsetRise_setFeature_left: the rise is unchanged by any difference outside Sonority.features, and the labial onsets of plik, pnik and ptik pattern with those of blif, bnif and bdif.
• initialIdentity_map, optimal_morphology_map: the root restriction and the preference for reduplication give the same verdict on a form and on its image under an injective relabelling.
• amodal_doubling_reversal: the doubling reversal holds for any type of constituents and either ranking of the OCP and DEP.

Implementation notes

The paper states the syllable hierarchy without a constraint set, deferring the formal analysis to earlier work, so the hierarchy is the order on sonority rises and no tableau is built. The acoustic, articulatory and neural measures of Figure 1 are not modelled.

References

• [Ber26]
• [BSLV07]
• [BBEB+16]
• [McC86]

Abstract: the syllable hierarchy

def Berent2026.onsetRise (c₁ c₂ : Phonology.Segment) : ℤ

The sonority rise across a two-consonant onset. Larger rises are better formed.

Equations

• Berent2026.onsetRise c₁ c₂ = (Phonology.Sonority.ofSegment c₁).rise (Phonology.Sonority.ofSegment c₂)

theorem Berent2026.onsetRise_congr {c₁ c₂ d₁ d₂ : Phonology.Segment} (h₁ : ∀ f ∈ Phonology.Sonority.features, c₁ f = d₁ f) (h₂ : ∀ f ∈ Phonology.Sonority.features, c₂ f = d₂ f) : onsetRise c₁ c₂ = onsetRise d₁ d₂

The rise of an onset depends on its segments only through the features that sonority reads, whatever their place of articulation and laryngeal setting.

theorem Berent2026.onsetRise_setFeature_left {c₁ c₂ : Phonology.Segment} {f : Phonology.Feature} (hf : f ∉ Phonology.Sonority.features) (v : Bool) : onsetRise (c₁.setFeature f v) c₂ = onsetRise c₁ c₂

Changing a feature that sonority does not read in the first consonant leaves the rise unchanged.

theorem Berent2026.onsetRise_setFeature_right {c₁ c₂ : Phonology.Segment} {f : Phonology.Feature} (hf : f ∉ Phonology.Sonority.features) (v : Bool) : onsetRise c₁ (c₂.setFeature f v) = onsetRise c₁ c₂

Changing a feature that sonority does not read in the second consonant leaves the rise unchanged.

theorem Berent2026.sonority_cline : 0 < onsetRise English.Phonology.b English.Phonology.n ∧ onsetRise English.Phonology.b English.Phonology.n < onsetRise English.Phonology.b English.Phonology.l ∧ onsetRise English.Phonology.b English.Phonology.d = 0 ∧ onsetRise English.Phonology.l English.Phonology.b < 0

The onset of blif is a larger rise than that of bnif, the onset of bdif is a plateau, and the onset of lbif is a fall.

theorem Berent2026.onsetRise_labial : onsetRise English.Phonology.p English.Phonology.l = onsetRise English.Phonology.b English.Phonology.l ∧ onsetRise English.Phonology.p English.Phonology.n = onsetRise English.Phonology.b English.Phonology.n ∧ onsetRise English.Phonology.p English.Phonology.t = onsetRise English.Phonology.b English.Phonology.d

The labial onsets of plik, pnik and ptik, heard under suppression of the lips or the tongue, have the rises of the onsets of blif, bnif and bdif.

Algebraic: identity restrictions

def Berent2026.InitialIdentity {α : Type u_1} (r : Morphology.ConsonantalRoot α) : Prop

A consonantal root begins with two identical consonants, the pattern that Hebrew bans while allowing identical consonants at the end of a root.

Equations

• Berent2026.InitialIdentity r = ¬OCP.IsClean (List.take 2 r.segments)

@[instance_reducible]

instance Berent2026.instDecidablePredConsonantalRootInitialIdentityOfDecidableEq {α : Type u_1} [DecidableEq α] : DecidablePred InitialIdentity

Equations

• Berent2026.instDecidablePredConsonantalRootInitialIdentityOfDecidableEq x✝ = { decide := !decide (OCP.IsClean (List.take 2 x✝.segments)), reflects_decide := ⋯ }

theorem Berent2026.initialIdentity_double_left {α : Type u_1} (x y : α) : InitialIdentity { segments := [x, x, y] }

theorem Berent2026.not_initialIdentity_double_right {α : Type u_1} {x y : α} (h : y ≠ x) : ¬InitialIdentity { segments := [y, x, x] }

theorem Berent2026.initialIdentity_map {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Function.Injective f) (r : Morphology.ConsonantalRoot α) : InitialIdentity { segments := List.map f r.segments } ↔ InitialIdentity r

The root restriction gives the same verdict on a root and on its image under an injective relabelling, so it extends to consonants the language lacks.

theorem Berent2026.initialIdentity_theta : ¬InitialIdentity { segments := [English.Phonology.k, English.Phonology.θ, English.Phonology.θ] } ∧ InitialIdentity { segments := [English.Phonology.θ, English.Phonology.θ, English.Phonology.k] }

The root of kathath ends in identical consonants and the root of thathak begins with them, so the restriction rejects thathak alone, although /θ/ is not a Hebrew consonant.

theorem Berent2026.optimal_morphology_map {α : Type u_1} {β : Type u_2} {f : α → β} {x y : α} [DecidableEq β] (hf : Function.Injective f) (h : x ≠ y) (r : OptimalityTheory.Ranking (Fin 2) 2) : (BerentEtAl2016.tableau (f x) (f y) BerentEtAl2016.Level.morphology r).optimal = {BerentEtAl2016.Parse.reduplicated [f x]}

The preference for reduplication carries over to the image of the constituents under an injective relabelling, so it extends to handshapes the language lacks.

Amodal: the doubling reversal

theorem Berent2026.amodal_doubling_reversal {α : Type u_1} [DecidableEq α] {x y : α} (h : x ≠ y) (r : OptimalityTheory.Ranking (Fin 2) 2) : (BerentEtAl2016.tableau x y BerentEtAl2016.Level.phonology r).optimal = {BerentEtAl2016.Parse.simplex [x, y]} ∧ (BerentEtAl2016.tableau x y BerentEtAl2016.Level.morphology r).optimal = {BerentEtAl2016.Parse.reduplicated [x]}

The same identity ban yields opposite surface preferences at the two levels of analysis. The constituents x and y range over any type, syllables of speech or of sign alike, and the dependence on the spoken language is BerentEtAl2016.exists_optimal_surface_iff.