Antifaithfulness — Alderete 2001

@cite{alderete-2001}

Antifaithfulness is the polarity flip of faithfulness: rather than penalizing positions where corresponding elements differ, it penalizes positions where they agree. The same correspondence diagram is used — the difference is purely in the sign of the comparator.

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. When ranked above OO-Ident-style preservation but below markedness, antifaith forces a minimal contrast that satisfies markedness.

Connection to OP / TCT / LC

OP (@cite{mccarthy-2005}) and TCT (@cite{benua-1997}) both posit OO-Faith constraints that prefer identity. LC (@cite{steriade-2000}) is a weighted/anchored variant. Antifaithfulness is the opposite-polarity sibling in the same paradigm-uniformity family: same diagrams, same edges, opposite comparator. It is the fourth corner of the four-corner ParadigmUniformity taxonomy.

Formal content

antifaithViol c r₁ r₂ counts position pairs (i, j) ∈ edge r₁ r₂ where (form r₁)[i] = (form r₂)[j]. Compare Corr.identViol, which counts pairs where they differ. Together they partition the edge:

identViol c r₁ r₂ + antifaithViol c r₁ r₂ = (edge r₁ r₂).card

def Phonology.ParadigmUniformity.Antifaithfulness.antifaithViol {Role : Type u_1} {α : Type u_2} [DecidableEq α] (c : 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

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

theorem Phonology.ParadigmUniformity.Antifaithfulness.antifaith_plus_ident_eq_edge_card {Role : Type u_1} {α : Type u_2} [DecidableEq α] (c : 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. Together they sum to the edge cardinality.

This is the formal content of "antifaith is the polarity flip of faith" — they share an underlying correspondence diagram and differ only in which subset of pairs is counted as a violation.

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

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

def Phonology.ParadigmUniformity.Antifaithfulness.toAntifaithConstraint {Role α : Type} [DecidableEq α] (r₁ r₂ : Role) (label : String) : Core.Constraint.OT.NamedConstraint (Correspondence.Corr Role α)

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

Equations

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