Antifaithfulness — Alderete 2001

[Ald01] [Ald99]

Antifaithfulness is the polarity flip of faithfulness: rather than penalising positions where corresponding elements differ, it penalises positions where they agree. The same correspondence diagram is used — the difference is purely in the sign of the comparator. Introduced in [Ald99] and developed as transderivational anti-faithfulness in [Ald01].

Empirical motivation

Antifaithfulness derives paradigmatic contrast effects:

• Lexical-class alternations where two related stems must phonologically differ (e.g. English transitive/intransitive ablaut: rise/raise, lie/lay).
• Anti-homophony: morphologically-related forms surfacing with distinct phonologies even when default markedness would predict identity.

Standard faithfulness alone cannot derive these — under faithfulness the most harmonic outcome is identity between related forms. Antifaith (¬OO-Ident) flips the polarity, so the most harmonic outcome is difference. Ranked above OO-Ident-style preservation but below markedness, it forces a minimal contrast that satisfies markedness.

Relation to the paradigm-uniformity family

Optimal Paradigms ([McC05], Studies/McCarthy2005.lean) and TCT ([Ben97], Studies/Benua1997.lean) both posit OO-Faith constraints that prefer identity; Lexical Conservatism ([Ste97], Studies/Steriade1997.lean) is an attestation-anchored variant. Antifaithfulness is the opposite-polarity sibling: the same correspondence diagrams and edges, the opposite comparator.

Main definitions

• antifaithViol — the ¬IDENT violation count (agreeing corresponding pairs).
• antifaith_plus_ident_eq_edge_card — ¬IDENT and IDENT partition the edge.
• identity_antifaith_max — the identity correspondence is maximally antifaith-violating.
• toAntifaithConstraint — the Constraint bridge.

Modeling note

antifaithViol here is the gradient count of every agreeing pair, so the most harmonic outcome under ¬IDENT alone is total dissimilation. Alderete's ¬F is, strictly, the logical negation of F (satisfied iff F is violated at least once), which under TETU-of-dominance yields minimal differentiation — a single change. A categorical-indicator variant (1 iff identViol = 0) would capture that minimal-contrast reading; the gradient count is kept here because it composes with the Corr.identViol partition theorem below, and the two agree on the qualitative claim (identity is dispreferred). Refining to the categorical reading is left as a TODO.

Antifaithfulness violation count

def Alderete2001.antifaithViol {Role : Type u_1} {α : Type u_2} [DecidableEq α] (c : OptimalityTheory.Correspondence.Corr Role α) (r₁ r₂ : Role) : ℕ

¬IDENT (antifaithfulness): the polarity-flipped sibling of Corr.identViol. Counts pairs (i, j) ∈ edge r₁ r₂ where the corresponding elements agree. Under ¬IDENT-OO ≫ OO-Ident, paradigmatically related forms are pushed apart rather than together.

Equations

• Alderete2001.antifaithViol c r₁ r₂ = {p ∈ c.edge r₁ r₂ | (c.form r₁)[p.1] = (c.form r₂)[p.2]}.card

Polarity duality with IDENT

theorem Alderete2001.antifaith_plus_ident_eq_edge_card {Role : Type u_1} {α : Type u_2} [DecidableEq α] (c : OptimalityTheory.Correspondence.Corr Role α) (r₁ r₂ : Role) : antifaithViol c r₁ r₂ + c.identViol r₁ r₂ = (c.edge r₁ r₂).card

Polarity duality: IDENT and antifaith partition the edge. Every correspondence pair contributes to exactly one of the two violation counts, so together they sum to the edge cardinality. This is the formal content of "antifaith is the polarity flip of faith": shared correspondence diagram, opposite subset counted as a violation.

Identity correspondence is maximally antifaith-violating

theorem Alderete2001.identity_antifaith_max {α : Type u_2} [DecidableEq α] (s : List α) : antifaithViol (OptimalityTheory.Correspondence.Corr.identity s) OptimalityTheory.Correspondence.Side.lhs OptimalityTheory.Correspondence.Side.rhs = s.length

The identity correspondence — input = output, all pairs identical — achieves maximum antifaith violations: every paired position counts.

Constraint bridge

def Alderete2001.toAntifaithConstraint {Role : Type u_1} {α : Type u_2} [DecidableEq α] (r₁ r₂ : Role) : Constraints.Constraint (OptimalityTheory.Correspondence.Corr Role α)

Wrap antifaithViol as a Constraint. The dual of Corr.toIdentConstraint.

Equations

• Alderete2001.toAntifaithConstraint r₁ r₂ c = Alderete2001.antifaithViol c r₁ r₂

Worked example: English ablaut contrast

inductive Alderete2001.Seg : Type

A minimal segmental alphabet for the rise/raise ablaut contrast.

• r : Seg
• a : Seg
• e : Seg
• z : Seg

@[implicit_reducible]

instance Alderete2001.instDecidableEqSeg : DecidableEq Seg

Equations

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

@[implicit_reducible]

instance Alderete2001.instReprSeg : Repr Seg

Equations

• Alderete2001.instReprSeg = { reprPrec := Alderete2001.instReprSeg.repr }

def Alderete2001.instReprSeg.repr : Seg → ℕ → Std.Format

Equations

• Alderete2001.instReprSeg.repr Alderete2001.Seg.r prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Alderete2001.Seg.r")).group prec✝
• Alderete2001.instReprSeg.repr Alderete2001.Seg.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Alderete2001.Seg.a")).group prec✝
• Alderete2001.instReprSeg.repr Alderete2001.Seg.e prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Alderete2001.Seg.e")).group prec✝
• Alderete2001.instReprSeg.repr Alderete2001.Seg.z prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Alderete2001.Seg.z")).group prec✝

def Alderete2001.rise : List Seg

rise ≈ [r a z].

Equations

• Alderete2001.rise = [Alderete2001.Seg.r, Alderete2001.Seg.a, Alderete2001.Seg.z]

def Alderete2001.raise : List Seg

raise ≈ [r e z], differing from rise only at the vowel.

Equations

• Alderete2001.raise = [Alderete2001.Seg.r, Alderete2001.Seg.e, Alderete2001.Seg.z]