McCarthy & Prince (1995): Faithfulness and Reduplicative Identity

@cite{mccarthy-prince-1995}

Formalizes the core empirical results of Correspondence Theory: the interaction between I-O faithfulness, B-R identity, and phonological markedness produces three typological patterns in the Basic Model — non-application, emergence of the unmarked, and overapplication — via ranking permutation of universal constraints. A fourth pattern, normal application, requires additional candidates beyond the Basic Model and is demonstrated by concrete language examples.

The paper's most striking theoretical result (§5) is that underapplication is not a Basic Model category: no ranking of the three core constraints can produce it. We prove this as basic_model_no_underapplication.

Sections (keyed to the paper's numbering)

• §3.4: Javanese intervocalic h-deletion — the paper's signature example of overapplication (ex. 1, 6–7).
• §4.2: Balangao partial reduplication — emergence of the unmarked (ex. 106–107). MAX-IO >> NO-CODA >> MAX-BR.
• §4: Basic Model factorial typology — the abstract 3-constraint interaction space. All 6 rankings of {IO-Faith, Phono, BR-Id} are computed; the distinct optima are verified.
• §5: Underapplication impossibility — the Basic Model cannot produce underapplication; every ranking selects faithful, over, or normal.
• §5.1: Akan underapplication — a 4th constraint (OCP) blocks overapplication, producing underapplication. Demonstrates the mechanism predicted by the Basic Model impossibility result.

Javanese h-deletion (ex. 1, 6-7)

Javanese disallows h between vowels (*VhV). In reduplication, h is lost in both base and reduplicant (overapplication): the expected form *bədah–bəda–e is avoided in favor of bəda–bəda–e, maintaining B-R identity at the cost of I-O faithfulness.

Ranking: IDENT-BR, *VhV >> MAX-IO

inductive McCarthyPrince1995.JavaneseCand : Type

Candidates for RED-bədah + -e in Javanese. Each represents a different resolution of the *VhV vs. B-R identity conflict.

• over : JavaneseCand
• under : JavaneseCand
• normal : JavaneseCand

@[implicit_reducible]

instance McCarthyPrince1995.instDecidableEqJavaneseCand : DecidableEq JavaneseCand

Equations

• McCarthyPrince1995.instDecidableEqJavaneseCand x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def McCarthyPrince1995.instReprJavaneseCand.repr : JavaneseCand → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance McCarthyPrince1995.instReprJavaneseCand : Repr JavaneseCand

Equations

• McCarthyPrince1995.instReprJavaneseCand = { reprPrec := McCarthyPrince1995.instReprJavaneseCand.repr }

def McCarthyPrince1995.javIdentBR : Core.Constraint.OT.NamedConstraint JavaneseCand

IDENT-BR: penalizes featural mismatch between base and reduplicant. Only the normal candidate has B ≠ R (B retains h, R lacks it).

Equations

• McCarthyPrince1995.javIdentBR = Phonology.Constraints.mkIdent "IDENT-BR" fun (x : McCarthyPrince1995.JavaneseCand) => x = McCarthyPrince1995.JavaneseCand.normal

def McCarthyPrince1995.javStarVhV : Core.Constraint.OT.NamedConstraint JavaneseCand

*VhV: markedness constraint against intervocalic h. Violated by under (h in both B and R) and normal (h in B).

Equations

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

def McCarthyPrince1995.javMaxIO : Core.Constraint.OT.NamedConstraint JavaneseCand

MAX-IO: I-O faithfulness — penalizes deletion from the input. Only the over candidate deletes h from the input stem.

Equations

• McCarthyPrince1995.javMaxIO = Phonology.Constraints.mkMax "MAX-IO" fun (x : McCarthyPrince1995.JavaneseCand) => x = McCarthyPrince1995.JavaneseCand.over

def McCarthyPrince1995.javRanking : List (Core.Constraint.OT.NamedConstraint JavaneseCand)

Skeletal ranking for overapplication (ex. 7): IDENT-BR, *VhV >> MAX-IO

Equations

• McCarthyPrince1995.javRanking = [McCarthyPrince1995.javIdentBR, McCarthyPrince1995.javStarVhV, McCarthyPrince1995.javMaxIO]

def McCarthyPrince1995.javCandidates : List JavaneseCand

Equations

• McCarthyPrince1995.javCandidates = [McCarthyPrince1995.JavaneseCand.over, McCarthyPrince1995.JavaneseCand.under, McCarthyPrince1995.JavaneseCand.normal]

theorem McCarthyPrince1995.javCandidates_ne : javCandidates ≠ []

theorem McCarthyPrince1995.javanese_overapplication : (Core.Constraint.OT.mkTableau javCandidates javRanking javCandidates_ne).optimal = {JavaneseCand.over}

Overapplication wins in Javanese: the doubly h-lacking form bəda–bəda–e is optimal under IDENT-BR, *VhV >> MAX-IO.

This is the paper's central empirical result: B-R identity and phonological markedness both outrank I-O faithfulness, so the output sacrifices faithfulness to achieve both identity and phonological well-formedness.

Grounding the Javanese tableau in Corr

The constraints javMaxIO, javIdentBR, javStarVhV above stipulate violation counts via λ-tables. This section adds the structural substrate: each candidate is associated with a Corr Phonology.Correspondence.RedupRole Seg recording the input → base / base ↔ reduplicant correspondences. MAX-IO and "IDENT-BR" violation counts are then derived from Corr.maxViol rather than stipulated.

The 3-role substrate (RedupRole, Corr.reduplication, Reduplication.maxIO/maxBR) lives in Theories/Phonology/OptimalityTheory/Correspondence.lean — paper-agnostic and reusable across reduplicative studies (Balangao, Akan, Tagalog, …). This section supplies only the Javanese-specific data + agreement theorems.

(*VhV remains a markedness constraint with no Corr-derived form — markedness is structural over a single output, not a correspondence relation.)

inductive McCarthyPrince1995.JavaneseCorr.Seg : Type

Phonological segments for the Javanese stem. Minimal abstract inventory (just the contrasts that matter for h-deletion).

• b : Seg
• schwa : Seg
• d : Seg
• a : Seg
• h : Seg

@[implicit_reducible]

instance McCarthyPrince1995.JavaneseCorr.instDecidableEqSeg : DecidableEq Seg

Equations

• McCarthyPrince1995.JavaneseCorr.instDecidableEqSeg x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance McCarthyPrince1995.JavaneseCorr.instReprSeg : Repr Seg

Equations

• McCarthyPrince1995.JavaneseCorr.instReprSeg = { reprPrec := McCarthyPrince1995.JavaneseCorr.instReprSeg.repr }

def McCarthyPrince1995.JavaneseCorr.instReprSeg.repr : Seg → ℕ → Std.Format

Equations

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

def McCarthyPrince1995.JavaneseCorr.stemInput : List Seg

The input stem /bədah/ (5 segments).

Equations

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

def McCarthyPrince1995.JavaneseCorr.baseDeleted : List Seg

The base output [bəda] (h deleted, 4 segments). For .over.

Equations

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

def McCarthyPrince1995.JavaneseCorr.baseFaithful : List Seg

The base output [bədah] (h preserved, 5 segments). For .under/.normal.

Equations

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

def McCarthyPrince1995.JavaneseCorr.overCorr : Phonology.Correspondence.Corr Phonology.Correspondence.RedupRole Seg

The Corr for the over candidate: h deleted from base and reduplicant.

Equations

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

def McCarthyPrince1995.JavaneseCorr.underCorr : Phonology.Correspondence.Corr Phonology.Correspondence.RedupRole Seg

The Corr for the under candidate: h preserved everywhere.

Equations

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

def McCarthyPrince1995.JavaneseCorr.normalCorr : Phonology.Correspondence.Corr Phonology.Correspondence.RedupRole Seg

The Corr for the normal candidate: h preserved in base, not in reduplicant. The default Corr.reduplication constructor uses parallel-pair correspondence truncated to min-length, which gives the right BR-MAX count (1 violation: base position 4 = h has no R correspondent).

Equations

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

def McCarthyPrince1995.JavaneseCorr.toCorr : JavaneseCand → Phonology.Correspondence.Corr Phonology.Correspondence.RedupRole Seg

Each candidate's structural Corr representation.

Equations

• McCarthyPrince1995.JavaneseCorr.toCorr McCarthyPrince1995.JavaneseCand.over = McCarthyPrince1995.JavaneseCorr.overCorr
• McCarthyPrince1995.JavaneseCorr.toCorr McCarthyPrince1995.JavaneseCand.under = McCarthyPrince1995.JavaneseCorr.underCorr
• McCarthyPrince1995.JavaneseCorr.toCorr McCarthyPrince1995.JavaneseCand.normal = McCarthyPrince1995.JavaneseCorr.normalCorr

theorem McCarthyPrince1995.JavaneseCorr.javMaxIO_eq_corr (c : JavaneseCand) : javMaxIO.eval c = (toCorr c).maxViol Phonology.Correspondence.RedupRole.input Phonology.Correspondence.RedupRole.base

Structural derivation of MAX-IO: the Corr-derived MAX-IO violation count equals the original stipulated javMaxIO.eval. The deletion-based stipulation (mkMax "MAX-IO" (· = .over)) now follows from the structural fact that over's base lacks an input correspondent.

theorem McCarthyPrince1995.JavaneseCorr.javIdentBR_eq_corr (c : JavaneseCand) : javIdentBR.eval c = (toCorr c).maxViol Phonology.Correspondence.RedupRole.base Phonology.Correspondence.RedupRole.reduplicant

Structural derivation of "IDENT-BR": the original constraint (mkIdent "IDENT-BR" (· = .normal)) is empirically MAX-BR — it penalizes the normal candidate's base-only h (which has no R correspondent). The structural count from Corr.maxViol .base .reduplicant matches the stipulation.

@[reducible, inline]

abbrev McCarthyPrince1995.JavaneseCorr.javMaxIOFromCorr : Core.Constraint.OT.NamedConstraint (Phonology.Correspondence.Corr Phonology.Correspondence.RedupRole Seg)

The Javanese tableau as NamedConstraint (Corr RedupRole Seg)s. These are direct uses of the paper-agnostic Phonology.Correspondence.Reduplication.maxIO / maxBR — no Javanese-specific constraint construction needed.

Equations

• McCarthyPrince1995.JavaneseCorr.javMaxIOFromCorr = Phonology.Correspondence.Reduplication.maxIO

@[reducible, inline]

abbrev McCarthyPrince1995.JavaneseCorr.javMaxBRFromCorr : Core.Constraint.OT.NamedConstraint (Phonology.Correspondence.Corr Phonology.Correspondence.RedupRole Seg)

Equations

• McCarthyPrince1995.JavaneseCorr.javMaxBRFromCorr = Phonology.Correspondence.Reduplication.maxBR

Balangao partial reduplication (ex. 106-107)

Balangao has a disyllabic prefixed reduplicant without a final coda: /RED-tagtag/ → tagta–tagtag, not *tagtag–tagtag. The reduplicant obeys NO-CODA even though the base (and the language generally) permits codas. This is emergence of the unmarked: a marked structure (codas) is avoided in the reduplicant because B-R identity is low-ranked.

Ranking (ex. 107): MAX-IO >> NO-CODA >> MAX-BR

inductive McCarthyPrince1995.BalangaoCand : Type

Candidates for /RED-tagtag/ in Balangao. Violation counts from the paper's tableau (ex. 106).

• totalFaithful : BalangaoCand
• totalRedup : BalangaoCand
• partialRedup : BalangaoCand

@[implicit_reducible]

instance McCarthyPrince1995.instDecidableEqBalangaoCand : DecidableEq BalangaoCand

Equations

• McCarthyPrince1995.instDecidableEqBalangaoCand x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def McCarthyPrince1995.instReprBalangaoCand.repr : BalangaoCand → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance McCarthyPrince1995.instReprBalangaoCand : Repr BalangaoCand

Equations

• McCarthyPrince1995.instReprBalangaoCand = { reprPrec := McCarthyPrince1995.instReprBalangaoCand.repr }

def McCarthyPrince1995.balMaxIO : Core.Constraint.OT.NamedConstraint BalangaoCand

MAX-IO: penalizes deletion from input. Only totalFaithful deletes a segment from the base.

Equations

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

def McCarthyPrince1995.balNoCoda : Core.Constraint.OT.NamedConstraint BalangaoCand

NO-CODA: markedness constraint against syllable codas. Violation counts from the tableau (ex. 106):

• totalFaithful (tagta–tagta): 2 codas (medial g in each half)
• totalRedup (tagtag–tagtag): 4 codas
• partial (tagta–tagtag): 3 codas (2 in base, 1 in R medial)

Equations

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

def McCarthyPrince1995.balMaxBR : Core.Constraint.OT.NamedConstraint BalangaoCand

MAX-BR: B-R identity — penalizes incomplete copying. Only partial has a segment in the base without a correspondent in the reduplicant (the final coda).

Equations

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

def McCarthyPrince1995.balRanking : List (Core.Constraint.OT.NamedConstraint BalangaoCand)

Ranking for emergence of the unmarked (ex. 107): MAX-IO >> NO-CODA >> MAX-BR

Equations

• McCarthyPrince1995.balRanking = [McCarthyPrince1995.balMaxIO, McCarthyPrince1995.balNoCoda, McCarthyPrince1995.balMaxBR]

def McCarthyPrince1995.balCandidates : List BalangaoCand

Equations

• McCarthyPrince1995.balCandidates = [McCarthyPrince1995.BalangaoCand.totalFaithful, McCarthyPrince1995.BalangaoCand.totalRedup, McCarthyPrince1995.BalangaoCand.partialRedup]

theorem McCarthyPrince1995.balCandidates_ne : balCandidates ≠ []

theorem McCarthyPrince1995.balangao_emergence_unmarked : (Core.Constraint.OT.mkTableau balCandidates balRanking balCandidates_ne).optimal = {BalangaoCand.partialRedup}

Emergence of the unmarked in Balangao: the partial reduplicant tagta–tagtag is optimal under MAX-IO >> NO-CODA >> MAX-BR.

The reduplicant is coda-free even though the base and the language generally permit codas — because B-R identity (MAX-BR) is low-ranked, the unmarked (coda-free) structure emerges in the reduplicant.

Grounding the Balangao tableau in Corr

Mirroring the Javanese §1.5 refactor: the MAX-IO and MAX-BR violation counts now follow from the structural correspondence diagram via Corr.maxViol, rather than being stipulated as λ-tables. NO-CODA is markedness over a single output and stays as the original stipulation.

inductive McCarthyPrince1995.BalangaoCorr.Seg : Type

Phonological segments for the Balangao stem. Minimal abstract inventory (just the contrasts that matter for tagtag-reduplication).

• t : Seg
• a : Seg
• g : Seg

@[implicit_reducible]

instance McCarthyPrince1995.BalangaoCorr.instDecidableEqSeg : DecidableEq Seg

Equations

• McCarthyPrince1995.BalangaoCorr.instDecidableEqSeg x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def McCarthyPrince1995.BalangaoCorr.instReprSeg.repr : Seg → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance McCarthyPrince1995.BalangaoCorr.instReprSeg : Repr Seg

Equations

• McCarthyPrince1995.BalangaoCorr.instReprSeg = { reprPrec := McCarthyPrince1995.BalangaoCorr.instReprSeg.repr }

def McCarthyPrince1995.BalangaoCorr.stemInput : List Seg

The input stem /tagtag/ (6 segments).

Equations

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

def McCarthyPrince1995.BalangaoCorr.baseFaithful : List Seg

The faithful base output [tagtag] (6 segments). For .totalRedup and .partialRedup.

Equations

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

def McCarthyPrince1995.BalangaoCorr.baseDeleted : List Seg

The deleted base output [tagta] (5 segments, final g deleted). For .totalFaithful (counter-intuitively named: it deletes from the input to make the base match the reduplicant's coda-less shape).

Equations

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

def McCarthyPrince1995.BalangaoCorr.redFull : List Seg

The full reduplicant [tagtag] (6 segments) for .totalRedup.

Equations

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

def McCarthyPrince1995.BalangaoCorr.redPartial : List Seg

The partial (coda-less) reduplicant [tagta] (5 segments) for .totalFaithful and .partialRedup.

Equations

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

def McCarthyPrince1995.BalangaoCorr.totalFaithfulCorr : Phonology.Correspondence.Corr Phonology.Correspondence.RedupRole Seg

The Corr for the totalFaithful candidate: input deleted to fit the coda-less shape (1 MAX-IO violation); B = R structurally.

Equations

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

def McCarthyPrince1995.BalangaoCorr.totalRedupCorr : Phonology.Correspondence.Corr Phonology.Correspondence.RedupRole Seg

The Corr for the totalRedup candidate: full faithful copy everywhere; 0 MAX-IO, 0 MAX-BR violations.

Equations

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

def McCarthyPrince1995.BalangaoCorr.partialRedupCorr : Phonology.Correspondence.Corr Phonology.Correspondence.RedupRole Seg

The Corr for the partialRedup candidate: faithful base, but reduplicant misses the final coda (1 MAX-BR violation, 0 MAX-IO).

Equations

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

def McCarthyPrince1995.BalangaoCorr.toCorr : BalangaoCand → Phonology.Correspondence.Corr Phonology.Correspondence.RedupRole Seg

Each candidate's structural Corr representation.

Equations

• McCarthyPrince1995.BalangaoCorr.toCorr McCarthyPrince1995.BalangaoCand.totalFaithful = McCarthyPrince1995.BalangaoCorr.totalFaithfulCorr
• McCarthyPrince1995.BalangaoCorr.toCorr McCarthyPrince1995.BalangaoCand.totalRedup = McCarthyPrince1995.BalangaoCorr.totalRedupCorr
• McCarthyPrince1995.BalangaoCorr.toCorr McCarthyPrince1995.BalangaoCand.partialRedup = McCarthyPrince1995.BalangaoCorr.partialRedupCorr

theorem McCarthyPrince1995.BalangaoCorr.balMaxIO_eq_corr (c : BalangaoCand) : balMaxIO.eval c = (toCorr c).maxViol Phonology.Correspondence.RedupRole.input Phonology.Correspondence.RedupRole.base

Structural derivation of MAX-IO: the Corr-derived MAX-IO violation count equals the original stipulated balMaxIO.eval.

theorem McCarthyPrince1995.BalangaoCorr.balMaxBR_eq_corr (c : BalangaoCand) : balMaxBR.eval c = (toCorr c).maxViol Phonology.Correspondence.RedupRole.base Phonology.Correspondence.RedupRole.reduplicant

Structural derivation of MAX-BR: the Corr-derived MAX-BR violation count equals the original stipulated balMaxBR.eval.

Basic Model (§4)

The Basic Model has faithfulness constraints on two correspondence dimensions — I-O faithfulness and B-R identity — interacting with a phonological markedness constraint ("Phono-Constraint"). Permuting the three constraints produces the factorial typology.

We model this with an abstract candidate type carrying violation profiles, and verify the distinct optima across all 6 rankings.

inductive McCarthyPrince1995.BasicCand : Type

Abstract candidate for the Basic Model interaction space. Each candidate represents a different resolution of the three-way conflict between I-O faithfulness, phonological well-formedness, and B-R identity.

• faithful: preserves input, B=R, but phonologically marked
• over: unfaithful to input, B=R, but phonologically unmarked
• normal: preserves input, phonologically unmarked in R, but B≠R

• faithful : BasicCand
• over : BasicCand
• normal : BasicCand

@[implicit_reducible]

instance McCarthyPrince1995.instDecidableEqBasicCand : DecidableEq BasicCand

Equations

• McCarthyPrince1995.instDecidableEqBasicCand x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def McCarthyPrince1995.instReprBasicCand.repr : BasicCand → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance McCarthyPrince1995.instReprBasicCand : Repr BasicCand

Equations

• McCarthyPrince1995.instReprBasicCand = { reprPrec := McCarthyPrince1995.instReprBasicCand.repr }

def McCarthyPrince1995.basicIOFaith : Core.Constraint.OT.NamedConstraint BasicCand

Equations

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

def McCarthyPrince1995.basicPhono : Core.Constraint.OT.NamedConstraint BasicCand

Equations

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

def McCarthyPrince1995.basicBRId : Core.Constraint.OT.NamedConstraint BasicCand

Equations

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

def McCarthyPrince1995.basicCandidates : List BasicCand

Equations

• McCarthyPrince1995.basicCandidates = [McCarthyPrince1995.BasicCand.faithful, McCarthyPrince1995.BasicCand.over, McCarthyPrince1995.BasicCand.normal]

theorem McCarthyPrince1995.basicCandidates_ne : basicCandidates ≠ []

theorem McCarthyPrince1995.nonapplication_io_br_phono : (Core.Constraint.OT.mkTableau basicCandidates [basicIOFaith, basicBRId, basicPhono] basicCandidates_ne).optimal = {BasicCand.faithful}

Non-application ranking (ex. 104): IO-Faith, BR-Id >> Phono. The faithful candidate wins — phonology cannot affect anything.

theorem McCarthyPrince1995.nonapplication_br_io_phono : (Core.Constraint.OT.mkTableau basicCandidates [basicBRId, basicIOFaith, basicPhono] basicCandidates_ne).optimal = {BasicCand.faithful}

Non-application (symmetric): BR-Id, IO-Faith >> Phono. Same outcome — faithful candidate wins regardless of IO/BR order.

theorem McCarthyPrince1995.emergence_unmarked : (Core.Constraint.OT.mkTableau basicCandidates [basicIOFaith, basicPhono, basicBRId] basicCandidates_ne).optimal = {BasicCand.normal}

Emergence of the unmarked (ex. 105): IO-Faith >> Phono >> BR-Id. The normal candidate wins — phonology affects the reduplicant (low BR-Id), but the base is protected (high IO-Faith).

theorem McCarthyPrince1995.overapplication_phono_io_br : (Core.Constraint.OT.mkTableau basicCandidates [basicPhono, basicIOFaith, basicBRId] basicCandidates_ne).optimal = {BasicCand.over}

Overapplication: Phono >> IO-Faith >> BR-Id. The over candidate wins — phonological unmarking applies to both B and R, sacrificing IO faithfulness.

theorem McCarthyPrince1995.overapplication_phono_br_io : (Core.Constraint.OT.mkTableau basicCandidates [basicPhono, basicBRId, basicIOFaith] basicCandidates_ne).optimal = {BasicCand.over}

Overapplication: Phono >> BR-Id >> IO-Faith. Same outcome — phonology dominates.

theorem McCarthyPrince1995.overapplication_br_phono_io : (Core.Constraint.OT.mkTableau basicCandidates [basicBRId, basicPhono, basicIOFaith] basicCandidates_ne).optimal = {BasicCand.over}

Overapplication: BR-Id >> Phono >> IO-Faith. B-R identity copies phonological effects to both B and R.

theorem McCarthyPrince1995.basic_model_factorial : Core.Constraint.OT.mkFactorialOptima basicCandidates [basicIOFaith, basicPhono, basicBRId] basicCandidates_ne = [{BasicCand.normal}, {BasicCand.over}, {BasicCand.faithful}]

Factorial typology summary: all 6 rankings of 3 constraints produce exactly 3 distinct optima — faithful (non-application), normal (emergence of the unmarked), and over (overapplication).

The 4th interaction type from the paper — normal application — requires additional candidates (where phonology targets the reduplicant independently) and is demonstrated by the Balangao and Tagalog examples in §§3-5 rather than the abstract model.

Underapplication is not a Basic Model category (§5)

@cite{mccarthy-prince-1995} §5 argues that underapplication cannot emerge from the Basic Model. Unlike overapplication and emergence of the unmarked, which follow from ranking permutations of {IO-Faith, Phono, BR-Id}, underapplication requires an additional independent constraint (like the OCP in Akan) that blocks the overapplicational candidate. In the Basic Model, B-R identity can restrict the candidate set to B=R pairs, but within that set the choice between over and under is determined by Phono-Constraint — and Phono-Constraint always prefers the phonologically unmarked form (= over), never the marked form (= under).

The factorial typology theorem already proves this: .faithful (non- application), .over (overapplication), and .normal (emergence of the unmarked) are the only optima. No ranking produces a 4th outcome.

theorem McCarthyPrince1995.basic_model_no_underapplication (optima : Finset BasicCand) : optima ∈ Core.Constraint.OT.mkFactorialOptima basicCandidates [basicIOFaith, basicPhono, basicBRId] basicCandidates_ne → optima = {BasicCand.faithful} ∨ optima = {BasicCand.over} ∨ optima = {BasicCand.normal}

Underapplication impossibility: every ranking of the Basic Model selects one of faithful, over, or normal. No ranking can select an underapplicational candidate because the Basic Model has no independent blocking constraint to exclude overapplication.

This is the formal content of @cite{mccarthy-prince-1995} §5's argument that underapplication requires an additional constraint beyond the three in the Basic Model.

theorem McCarthyPrince1995.basic_model_exactly_three_types : Core.Constraint.OT.mkFactorialTypologySize basicCandidates [basicIOFaith, basicPhono, basicBRId] basicCandidates_ne = 3

The factorial typology produces exactly 3 distinct language types, not 4 — confirming that underapplication is absent from the Basic Model.

Akan underapplication (ex. 125, 130–131)

Akan has a monosyllabic reduplicative prefix with a high vowel. Palatalization (velar → palatal before front vowels) is productive in the language but fails to apply in reduplication: /RED-ka/ surfaces as kɪ–ka, not *tɕɪ–tɕa (overapplication) or *tɕɪ–ka (normal application).

This is underapplication: a process that normally applies (PAL) is blocked in reduplication. The mechanism is a 4th constraint — OCP(+cor) — that blocks the overapplicational candidate. Since B-R identity (IDENT-BR) is high-ranked, normal application is also blocked, leaving underapplication as the only survivor.

Ranking (ex. 129, 131): OCP(+cor) >> IDENT-BR(−cor) >> PAL >> IDENT-IO(−cor)

This confirms the Basic Model impossibility result: underapplication requires a blocking constraint (here OCP) beyond the three in the Basic Model.

inductive McCarthyPrince1995.AkanCand : Type

Candidates for /RED-ka/ in Akan (ex. 130). Each represents a different resolution of the palatalization vs. B-R identity vs. OCP conflict.

• over : AkanCand
• normal : AkanCand
• under : AkanCand

@[implicit_reducible]

instance McCarthyPrince1995.instDecidableEqAkanCand : DecidableEq AkanCand

Equations

• McCarthyPrince1995.instDecidableEqAkanCand x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def McCarthyPrince1995.instReprAkanCand.repr : AkanCand → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance McCarthyPrince1995.instReprAkanCand : Repr AkanCand

Equations

• McCarthyPrince1995.instReprAkanCand = { reprPrec := McCarthyPrince1995.instReprAkanCand.repr }

def McCarthyPrince1995.akanOCP : Core.Constraint.OT.NamedConstraint AkanCand

OCP(+cor): prohibits cooccurrence of [+coronal] segments in successive syllables. The overapplicational candidate tɕɪ–tɕa has coronal obstruents in both syllables of the output.

Violation counts from tableau (131):

• over (tɕɪ–tɕa): 2 violations (coronal in each syllable of B+R)
• normal (tɕɪ–ka): 0
• under (kɪ–ka): 0

Equations

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

def McCarthyPrince1995.akanIdentBR : Core.Constraint.OT.NamedConstraint AkanCand

IDENT-BR(−cor): B-R identity for the [−coronal] feature. Penalizes featural mismatch between base and reduplicant consonants. Only the normal candidate has B ≠ R (R has palatalized tɕ, B retains velar k).

Violation counts from tableau (131):

• over (tɕɪ–tɕa): 0 (B = R)
• normal (tɕɪ–ka): 1 (R ≠ B in coronal feature)
• under (kɪ–ka): 0 (B = R)

Equations

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

def McCarthyPrince1995.akanPAL : Core.Constraint.OT.NamedConstraint AkanCand

PAL: palatalization constraint — velars must be palatalized before front vowels. The underapplicational candidate kɪ–ka has a velar before the front vowel ɪ in the reduplicant.

Violation counts from tableau (131):

• over (tɕɪ–tɕa): 0
• normal (tɕɪ–ka): 0
• under (kɪ–ka): 1 (velar k before front vowel ɪ)

Equations

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

def McCarthyPrince1995.akanIdentIO : Core.Constraint.OT.NamedConstraint AkanCand

IDENT-IO(−cor): I-O faithfulness for the [−coronal] feature. Penalizes changing the coronal specification of an input segment. Only the overapplicational candidate changes the base consonant from velar to palatal (unfaithful to input /k/).

Violation counts from tableau (131):

• over (tɕɪ–tɕa): 1 (input /k/ → output tɕ in base)
• normal (tɕɪ–ka): 0
• under (kɪ–ka): 0

Equations

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

def McCarthyPrince1995.akanRanking : List (Core.Constraint.OT.NamedConstraint AkanCand)

Ranking for Akan underapplication (ex. 129, 131): OCP(+cor) >> IDENT-BR(−cor) >> PAL >> IDENT-IO(−cor)

Equations

• McCarthyPrince1995.akanRanking = [McCarthyPrince1995.akanOCP, McCarthyPrince1995.akanIdentBR, McCarthyPrince1995.akanPAL, McCarthyPrince1995.akanIdentIO]

def McCarthyPrince1995.akanCandidates : List AkanCand

Equations

• McCarthyPrince1995.akanCandidates = [McCarthyPrince1995.AkanCand.over, McCarthyPrince1995.AkanCand.normal, McCarthyPrince1995.AkanCand.under]

theorem McCarthyPrince1995.akanCandidates_ne : akanCandidates ≠ []

theorem McCarthyPrince1995.akan_underapplication : (Core.Constraint.OT.mkTableau akanCandidates akanRanking akanCandidates_ne).optimal = {AkanCand.under}

Underapplication wins in Akan: the non-palatalized form kɪ–ka is optimal under OCP(+cor) >> IDENT-BR(−cor) >> PAL >> IDENT-IO(−cor).

This is the paper's key demonstration that underapplication requires a 4th blocking constraint (OCP) beyond the Basic Model's three: OCP blocks overapplication, IDENT-BR blocks normal application, leaving underapplication as the only surviving candidate.

Grounding the Akan tableau in phonological features

The violation counts in §5 are grounded in the featural representations from Fragments.Akan.Phonology. The key connection: palatalization is a [coronal] feature change (/k/ [−cor] → /tɕ/ [+cor]), and the four constraints target exactly this feature dimension.

• OCP(+cor): violated by adjacent [+coronal] segments — i.e., /tɕ/ in successive syllables. Only the over candidate has this.
• IDENT-BR(−cor): violated when B and R differ in [coronal]. Only normal (R has /tɕ/, B has /k/).
• PAL: violated when a velar ([−coronal]) precedes a front vowel without palatalizing. Only under (/kɪ/).
• IDENT-IO(−cor): violated when the output changes an input segment's [coronal] value. Only over (input /k/ → output /tɕ/ in base).

theorem McCarthyPrince1995.akan_over_ocp_grounded : Fragments.Akan.Phonology.seg_tc.HasValue Phonology.Feature.coronal true = (true = true)

The over candidate's OCP violation is grounded: /tɕ/ is [+coronal], so two /tɕ/ in successive syllables violate OCP(+cor).

theorem McCarthyPrince1995.akan_normal_identBR_grounded : Fragments.Akan.Phonology.seg_tc.HasValue Phonology.Feature.coronal true = (true = true) ∧ Fragments.Akan.Phonology.seg_k.HasValue Phonology.Feature.coronal false = (true = true)

The normal candidate's IDENT-BR violation is grounded: the reduplicant has /tɕ/ ([+cor]) but the base has /k/ ([−cor]) — a featural mismatch on [coronal].

theorem McCarthyPrince1995.akan_under_pal_grounded : Fragments.Akan.Phonology.seg_k.HasValue Phonology.Feature.coronal false = (true = true) ∧ Fragments.Akan.Phonology.seg_i.HasValue Phonology.Feature.front true = (true = true)

The under candidate's PAL violation is grounded: /k/ is [−coronal] and /ɪ/ is [+front] — a velar before a front vowel without palatalization.

theorem McCarthyPrince1995.akan_over_identIO_grounded : Fragments.Akan.Phonology.seg_k.HasValue Phonology.Feature.coronal false = (true = true) ∧ Fragments.Akan.Phonology.seg_tc.HasValue Phonology.Feature.coronal true = (true = true)

The over candidate's IDENT-IO violation is grounded: input /k/ is [−coronal] but output /tɕ/ is [+coronal] — an IO faithfulness violation on the [coronal] feature.

Grounding the Akan tableau in Corr via featural IDENT

Mirroring the Javanese §1.5 / Balangao §2.5 refactors, with one addition: Akan's IDENT-BR(-cor) and IDENT-IO(-cor) are featural faithfulness constraints on the [coronal] feature, not segmental identity. This section uses Corr.identViolFeature with a coronal projection to derive the constraint values structurally.

This is the first study file to exercise Corr.identViolFeature (introduced in 0.230.217). Successful agreement theorems here validate the featural-IDENT pattern for any future paper using IDENT-[F] constraints.

inductive McCarthyPrince1995.AkanCorr.Seg : Type

Phonological segments for the Akan /RED-ka/ paradigm. The minimal abstract inventory tracking the [coronal] feature contrast.

• k : Seg
• tCpal : Seg
• a : Seg
• iSmCap : Seg

@[implicit_reducible]

instance McCarthyPrince1995.AkanCorr.instDecidableEqSeg : DecidableEq Seg

Equations

• McCarthyPrince1995.AkanCorr.instDecidableEqSeg x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance McCarthyPrince1995.AkanCorr.instReprSeg : Repr Seg

Equations

• McCarthyPrince1995.AkanCorr.instReprSeg = { reprPrec := McCarthyPrince1995.AkanCorr.instReprSeg.repr }

def McCarthyPrince1995.AkanCorr.instReprSeg.repr : Seg → ℕ → Std.Format

Equations

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

def McCarthyPrince1995.AkanCorr.coronal : Seg → Bool

The [coronal] feature projection. Vowels are false (out of the relevant natural class for this paradigm; their featural value doesn't enter the IDENT-[coronal] computation).

Equations

• McCarthyPrince1995.AkanCorr.coronal McCarthyPrince1995.AkanCorr.Seg.k = false
• McCarthyPrince1995.AkanCorr.coronal McCarthyPrince1995.AkanCorr.Seg.tCpal = true
• McCarthyPrince1995.AkanCorr.coronal McCarthyPrince1995.AkanCorr.Seg.a = false
• McCarthyPrince1995.AkanCorr.coronal McCarthyPrince1995.AkanCorr.Seg.iSmCap = false

def McCarthyPrince1995.AkanCorr.stemInput : List Seg

Input /ka/.

Equations

• McCarthyPrince1995.AkanCorr.stemInput = [McCarthyPrince1995.AkanCorr.Seg.k, McCarthyPrince1995.AkanCorr.Seg.a]

def McCarthyPrince1995.AkanCorr.baseFaithful : List Seg

Faithful base (k a) — for .normal and .under.

Equations

• McCarthyPrince1995.AkanCorr.baseFaithful = [McCarthyPrince1995.AkanCorr.Seg.k, McCarthyPrince1995.AkanCorr.Seg.a]

def McCarthyPrince1995.AkanCorr.basePalatalized : List Seg

Palatalized base (tɕ a) — for .over (palatalization in B).

Equations

• McCarthyPrince1995.AkanCorr.basePalatalized = [McCarthyPrince1995.AkanCorr.Seg.tCpal, McCarthyPrince1995.AkanCorr.Seg.a]

def McCarthyPrince1995.AkanCorr.redPalatalized : List Seg

Palatalized reduplicant (tɕ ɪ) — for .over and .normal.

Equations

• McCarthyPrince1995.AkanCorr.redPalatalized = [McCarthyPrince1995.AkanCorr.Seg.tCpal, McCarthyPrince1995.AkanCorr.Seg.iSmCap]

def McCarthyPrince1995.AkanCorr.redFaithful : List Seg

Faithful reduplicant (k ɪ) — for .under.

Equations

• McCarthyPrince1995.AkanCorr.redFaithful = [McCarthyPrince1995.AkanCorr.Seg.k, McCarthyPrince1995.AkanCorr.Seg.iSmCap]

def McCarthyPrince1995.AkanCorr.overCorr : Phonology.Correspondence.Corr Phonology.Correspondence.RedupRole Seg

The Corr for the over candidate: palatalization in both B and R.

Equations

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

def McCarthyPrince1995.AkanCorr.normalCorr : Phonology.Correspondence.Corr Phonology.Correspondence.RedupRole Seg

The Corr for the normal candidate: palatalization in R only.

Equations

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

def McCarthyPrince1995.AkanCorr.underCorr : Phonology.Correspondence.Corr Phonology.Correspondence.RedupRole Seg

The Corr for the under candidate: no palatalization.

Equations

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

def McCarthyPrince1995.AkanCorr.toCorr : AkanCand → Phonology.Correspondence.Corr Phonology.Correspondence.RedupRole Seg

Each candidate's structural Corr representation.

Equations

• McCarthyPrince1995.AkanCorr.toCorr McCarthyPrince1995.AkanCand.over = McCarthyPrince1995.AkanCorr.overCorr
• McCarthyPrince1995.AkanCorr.toCorr McCarthyPrince1995.AkanCand.normal = McCarthyPrince1995.AkanCorr.normalCorr
• McCarthyPrince1995.AkanCorr.toCorr McCarthyPrince1995.AkanCand.under = McCarthyPrince1995.AkanCorr.underCorr

theorem McCarthyPrince1995.AkanCorr.akanIdentIO_eq_corr (c : AkanCand) : akanIdentIO.eval c = Phonology.Correspondence.Corr.identViolFeature coronal (toCorr c) Phonology.Correspondence.RedupRole.input Phonology.Correspondence.RedupRole.base

Structural derivation of IDENT-IO(-cor) via featural IDENT on the (.input, .base) edge. Input /k/ → base /tɕ/ is the only IO coronal mismatch; only over violates.

theorem McCarthyPrince1995.AkanCorr.akanIdentBR_eq_corr (c : AkanCand) : akanIdentBR.eval c = Phonology.Correspondence.Corr.identViolFeature coronal (toCorr c) Phonology.Correspondence.RedupRole.base Phonology.Correspondence.RedupRole.reduplicant

Structural derivation of IDENT-BR(-cor) via featural IDENT on the (.base, .reduplicant) edge. Only normal has B/R coronal mismatch (B has /k/ [-cor], R has /tɕ/ [+cor]); the vowels' coronal values agree (both [-cor] in this featural inventory).

Each tableau lifts to a generic ConstraintSystem via tableauSystem. For these deterministic OT analyses, the unique-winner pattern collapses the argminDecoder distribution to probability 1 on the winner.

noncomputable def McCarthyPrince1995.javaneseSystem : Core.Constraint.ConstraintSystem JavaneseCand (Core.Constraint.LexProfile ℕ 3)

Javanese overapplication tableau as a generic ConstraintSystem.

Equations

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

theorem McCarthyPrince1995.javaneseSystem_predict_over : javaneseSystem.predict JavaneseCand.over = 1

The OT prediction lifts: the overapplicational candidate is assigned probability 1 under IDENT-BR, *VhV >> MAX-IO.

noncomputable def McCarthyPrince1995.balangaoSystem : Core.Constraint.ConstraintSystem BalangaoCand (Core.Constraint.LexProfile ℕ 3)

Balangao emergence-of-the-unmarked tableau as a generic ConstraintSystem.

Equations

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

theorem McCarthyPrince1995.balangaoSystem_predict_partial : balangaoSystem.predict BalangaoCand.partialRedup = 1

The OT prediction lifts: the partial-reduplicant candidate is assigned probability 1 under MAX-IO >> NO-CODA >> MAX-BR.

noncomputable def McCarthyPrince1995.akanSystem : Core.Constraint.ConstraintSystem AkanCand (Core.Constraint.LexProfile ℕ 4)

Akan underapplication tableau as a generic ConstraintSystem.

Equations

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

theorem McCarthyPrince1995.akanSystem_predict_under : akanSystem.predict AkanCand.under = 1

The OT prediction lifts: the underapplicational candidate is assigned probability 1 under OCP(+cor) >> IDENT-BR(−cor) >> PAL >> IDENT-IO(−cor).