@cite{krifka-2007b} — Negated Antonyms: Creating and Filling the Gap

@cite{krifka-2007b}

In:, Presupposition and Implicature in Compositional Semantics, Palgrave Macmillan.

Krifka's Thesis

Krifka argues, against the received view (@cite{cruse-1986}, @cite{horn-1989}), that antonyms like happy/unhappy are literally contradictory — they exhaustively partition the scale with a single threshold. The gap between "not unhappy" and "happy" arises through pragmatic strengthening, not through the semantics of contrary negation.

Three Hypotheses (§3)

1. Epistemic vagueness: Speakers avoid borderline cases to ensure safe communication (following Williamson 1994).
2. Exhaustive antonymy: happy and unhappy are contradictories — they literally exhaust their scale. Evidence: unconditionals like "Regardless whether you are happy or unhappy, you should read this book" (ex. 22) entail the predicate covers everyone.
3. M-principle: Of two expressions with similar meaning, the simpler one is restricted to stereotypical interpretations, the complex one to non-stereotypical interpretations (@cite{horn-1984}).

Central Argument

Under contradictory semantics (single θ), "not unhappy" = "happy" (DNE). The M-principle breaks this synonymy: since "not unhappy" is more complex than "happy" (5 vs 0 cost units), the complex form is pragmatically restricted to the non-stereotypical region — the plateau/gap between clearly happy and clearly unhappy.

Quadruplet Structure (ex. 1)

Krifka's analysis centers on quadruplets: happy, not happy, unhappy, not unhappy with form complexity: |happy| < |unhappy| < |not happy| < |not unhappy|

Verification

Formalizes the quadruplet structure, proves the contradictory synonymy puzzle and its resolution via ThresholdPair, and bridges to the empirical data in FlexibleNegation.lean. The pragmatic mechanism connecting contradictory base → effective ThresholdPair is derived via two routes:

1. Bidirectional OT (§ 9 below): @cite{blutner-2000}'s weak BiOT (eq. 14) derives the four-way form-meaning assignment via the greatest-fixed-point computation in Core.ConstraintEvaluation.superoptimal.
2. RSA model: @cite{tessler-franke-2019} (Studies/TesslerFranke2020.lean) derives the same effect through Bayesian pragmatic reasoning.

inductive Phenomena.Negation.Studies.Krifka2007.QuadForm : Type

Krifka's quadruplet (ex. 1): the four forms generated from an adjective and its antonym by applying syntactic negation.

• positive : QuadForm
• notPositive : QuadForm
• negative : QuadForm
• notNegative : QuadForm

def Phenomena.Negation.Studies.Krifka2007.instReprQuadForm.repr : QuadForm → ℕ → Std.Format

Equations

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

instance Phenomena.Negation.Studies.Krifka2007.instReprQuadForm : Repr QuadForm

Equations

• Phenomena.Negation.Studies.Krifka2007.instReprQuadForm = { reprPrec := Phenomena.Negation.Studies.Krifka2007.instReprQuadForm.repr }

instance Phenomena.Negation.Studies.Krifka2007.instDecidableEqQuadForm : DecidableEq QuadForm

Equations

• Phenomena.Negation.Studies.Krifka2007.instDecidableEqQuadForm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Negation.Studies.Krifka2007.instBEqQuadForm : BEq QuadForm

Equations

• Phenomena.Negation.Studies.Krifka2007.instBEqQuadForm = { beq := Phenomena.Negation.Studies.Krifka2007.instBEqQuadForm.beq }

def Phenomena.Negation.Studies.Krifka2007.instBEqQuadForm.beq : QuadForm → QuadForm → Bool

Equations

• Phenomena.Negation.Studies.Krifka2007.instBEqQuadForm.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Negation.Studies.Krifka2007.QuadForm.complexity : QuadForm → ℕ

Form complexity ordering: |happy| < |unhappy| < |not happy| < |not unhappy|

Matches utteranceCost in @cite{tessler-franke-2019}'s RSA model.

Equations

• Phenomena.Negation.Studies.Krifka2007.QuadForm.positive.complexity = 0
• Phenomena.Negation.Studies.Krifka2007.QuadForm.negative.complexity = 2
• Phenomena.Negation.Studies.Krifka2007.QuadForm.notPositive.complexity = 3
• Phenomena.Negation.Studies.Krifka2007.QuadForm.notNegative.complexity = 5

theorem Phenomena.Negation.Studies.Krifka2007.complexity_ordering : QuadForm.positive.complexity < QuadForm.negative.complexity ∧ QuadForm.negative.complexity < QuadForm.notPositive.complexity ∧ QuadForm.notPositive.complexity < QuadForm.notNegative.complexity

Form complexity is monotonically increasing across the quadruplet.

def Phenomena.Negation.Studies.Krifka2007.contradictoryQuad {max : ℕ} (θ : Core.Scale.Threshold max) (q : QuadForm) (d : Core.Scale.Degree max) : Bool

Krifka's H2: Antonyms are literally contradictory (single threshold θ). All four quadruplet forms derive from Boolean operations on d > θ.

Equations

• Phenomena.Negation.Studies.Krifka2007.contradictoryQuad θ Phenomena.Negation.Studies.Krifka2007.QuadForm.positive d = Semantics.Degree.positiveMeaning d θ
• Phenomena.Negation.Studies.Krifka2007.contradictoryQuad θ Phenomena.Negation.Studies.Krifka2007.QuadForm.notPositive d = !Semantics.Degree.positiveMeaning d θ
• Phenomena.Negation.Studies.Krifka2007.contradictoryQuad θ Phenomena.Negation.Studies.Krifka2007.QuadForm.negative d = !Semantics.Degree.positiveMeaning d θ
• Phenomena.Negation.Studies.Krifka2007.contradictoryQuad θ Phenomena.Negation.Studies.Krifka2007.QuadForm.notNegative d = Semantics.Degree.positiveMeaning d θ

theorem Phenomena.Negation.Studies.Krifka2007.contradictory_synonymy {max : ℕ} (d : Core.Scale.Degree max) (θ : Core.Scale.Threshold max) : contradictoryQuad θ QuadForm.negative d = contradictoryQuad θ QuadForm.notPositive d ∧ contradictoryQuad θ QuadForm.notNegative d = contradictoryQuad θ QuadForm.positive d

The puzzle: Under contradictory semantics, "unhappy" = "not happy" and "not unhappy" = "happy". Each pair is synonymous.

theorem Phenomena.Negation.Studies.Krifka2007.dne_synonymy {max : ℕ} (d : Core.Scale.Degree max) (θ : Core.Scale.Threshold max) : contradictoryQuad θ QuadForm.notNegative d = contradictoryQuad θ QuadForm.positive d

The puzzle makes a prediction: "not unhappy" should mean the same as "happy". But empirically it doesn't (@cite{tessler-franke-2019}). contradictory_dne from Antonymy proves this synonymy formally.

def Phenomena.Negation.Studies.Krifka2007.strengthenedQuad {max : ℕ} (tp : Semantics.Lexical.Adjective.ThresholdPair max) (q : QuadForm) (d : Core.Scale.Degree max) : Bool

After pragmatic strengthening (M-principle), the effective semantics uses two thresholds. The M-principle assigns different scale regions to forms of different complexity:

• "happy" (simple) → stereotypical positive (d > θ_pos)
• "unhappy" (moderate) → stereotypical negative (d < θ_neg)
• "not happy" (complex) → includes borderline low
• "not unhappy" (most complex) → borderline high / plateau

Equations

• Phenomena.Negation.Studies.Krifka2007.strengthenedQuad tp Phenomena.Negation.Studies.Krifka2007.QuadForm.positive d = Semantics.Lexical.Adjective.positiveMeaning' d tp
• Phenomena.Negation.Studies.Krifka2007.strengthenedQuad tp Phenomena.Negation.Studies.Krifka2007.QuadForm.notPositive d = Semantics.Lexical.Adjective.contradictoryNeg d tp.pos
• Phenomena.Negation.Studies.Krifka2007.strengthenedQuad tp Phenomena.Negation.Studies.Krifka2007.QuadForm.negative d = Semantics.Lexical.Adjective.contraryNegMeaning d tp
• Phenomena.Negation.Studies.Krifka2007.strengthenedQuad tp Phenomena.Negation.Studies.Krifka2007.QuadForm.notNegative d = Semantics.Lexical.Adjective.notContraryNegMeaning d tp

theorem Phenomena.Negation.Studies.Krifka2007.strengthened_breaks_synonymy {max : ℕ} (tp : Semantics.Lexical.Adjective.ThresholdPair max) (h : { value := tp.neg.value.castSucc } < { value := tp.pos.value.castSucc }) : ∃ (d : Core.Scale.Degree max), strengthenedQuad tp QuadForm.notNegative d ≠ strengthenedQuad tp QuadForm.positive d

The solution: With ThresholdPair, "not unhappy" ≠ "happy" when the gap is strict. The M-principle-derived two-threshold model breaks the synonymy that contradictory semantics creates.

@[reducible, inline]

abbrev Phenomena.Negation.Studies.Krifka2007.HappyDeg : Type

5-point happiness scale (matching @cite{tessler-franke-2019}'s model).

Equations

• Phenomena.Negation.Studies.Krifka2007.HappyDeg = Core.Scale.Degree 4

@[reducible, inline]

abbrev Phenomena.Negation.Studies.Krifka2007.happyθ : Core.Scale.Threshold 4

Contradictory boundary at θ = 2 (the literal semantics).

Equations

• Phenomena.Negation.Studies.Krifka2007.happyθ = Core.Scale.thr 2 Phenomena.Negation.Studies.Krifka2007.happyθ._proof_2

def Phenomena.Negation.Studies.Krifka2007.happyTP : Semantics.Lexical.Adjective.ThresholdPair 4

Effective threshold pair after pragmatic strengthening: θ_pos = 2, θ_neg = 1. The gap [1, 2] is the plateau region where "not unhappy" lands.

Equations

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

theorem Phenomena.Negation.Studies.Krifka2007.happy_gap_strict : { value := happyTP.neg.value.castSucc } < { value := happyTP.pos.value.castSucc }

theorem Phenomena.Negation.Studies.Krifka2007.contradictory_exhaustive_concrete (d : HappyDeg) : contradictoryQuad happyθ QuadForm.positive d = true ∨ contradictoryQuad happyθ QuadForm.negative d = true

Prediction 1: Under contradictory semantics, all degrees are classified. No gap exists. (Krifka's H2: literal exhaustivity.)

theorem Phenomena.Negation.Studies.Krifka2007.contradictory_not_unhappy_eq_happy (d : HappyDeg) : contradictoryQuad happyθ QuadForm.notNegative d = contradictoryQuad happyθ QuadForm.positive d

Prediction 2: Under contradictory semantics, "not unhappy" = "happy" at every degree. (The puzzle.)

theorem Phenomena.Negation.Studies.Krifka2007.strengthened_not_unhappy_ne_happy : ∃ (d : HappyDeg), strengthenedQuad happyTP QuadForm.notNegative d ≠ strengthenedQuad happyTP QuadForm.positive d

Prediction 3: After strengthening, the gap breaks synonymy.

theorem Phenomena.Negation.Studies.Krifka2007.gap_degrees : Semantics.Lexical.Adjective.inGapRegion (Core.Scale.deg 1 ⋯) happyTP = true ∧ Semantics.Lexical.Adjective.inGapRegion (Core.Scale.deg 2 ⋯) happyTP = true

Prediction 4: The gap region is nonempty (degrees 1 and 2).

theorem Phenomena.Negation.Studies.Krifka2007.extreme_degrees : Semantics.Lexical.Adjective.contraryNegMeaning (Core.Scale.deg 0 ⋯) happyTP = true ∧ Semantics.Lexical.Adjective.positiveMeaning' (Core.Scale.deg 4 ⋯) happyTP = true

Prediction 5: Degree 0 is "unhappy", degree 4 is "happy".

theorem Phenomena.Negation.Studies.Krifka2007.unhappy_effectively_contrary : FlexibleNegation.unhappy_contrary.expectedInterpretation = Core.NegationType.contrary

FlexibleNegation classifies "unhappy" as contrary — this is the effective (post-strengthening) semantics, consistent with Krifka's analysis where the contrary behavior is pragmatically derived.

theorem Phenomena.Negation.Studies.Krifka2007.double_neg_nonequivalence : FlexibleNegation.happy_double_neg.areEquivalent = false

The empirical double-negation non-equivalence is derived from the strengthened model (§3): synonymy is broken by the gap.

theorem Phenomena.Negation.Studies.Krifka2007.gap_prediction_derived : FlexibleNegation.prediction_double_neg_gap.statement = "∃d, P(d | 'not unhappy') > 0 ∧ P(d | 'happy') = 0" ∧ ∃ (d : HappyDeg), Semantics.Lexical.Adjective.notContraryNegMeaning d happyTP = true ∧ Semantics.Lexical.Adjective.positiveMeaning' d happyTP = false

The gap prediction from FlexibleNegation data corresponds to contrary_gap_exists applied to the strengthened model.

theorem Phenomena.Negation.Studies.Krifka2007.unhappy_marked_by_morphology : Implicature.Markedness.computeMarked Implicature.Markedness.happy_with_morphology Implicature.Markedness.unhappy_with_morphology = some "unhappy"

Krifka's form complexity ordering matches the markedness infrastructure. "unhappy" is marked over "happy" by morphological complexity.

theorem Phenomena.Negation.Studies.Krifka2007.cost_asymmetry_reflects_complexity : FlexibleNegation.unhappy_vs_not_happy.cheapForm = "unhappy" ∧ FlexibleNegation.unhappy_vs_not_happy.costlyForm = "not happy" ∧ FlexibleNegation.unhappy_vs_not_happy.cheapMeaning = Core.NegationType.contrary ∧ FlexibleNegation.unhappy_vs_not_happy.costlyMeaning = Core.NegationType.contradictory

Cost asymmetry in FlexibleNegation data reflects Krifka's form complexity ordering.

theorem Phenomena.Negation.Studies.Krifka2007.unconditional_exhaustive (d : HappyDeg) : contradictoryQuad happyθ QuadForm.positive d = true ∨ contradictoryQuad happyθ QuadForm.negative d = true

Krifka's unconditional argument: "Regardless whether you are happy or unhappy, you should read this book."

This sentence entails the predicate covers EVERYONE — no gap. Under the contradictory model, happy ∨ unhappy = universal (exhaustive). Under a contrary model, this would exclude the gap region.

Unconditionals provide evidence that the literal semantics IS contradictory, with the gap being purely pragmatic.

theorem Phenomena.Negation.Studies.Krifka2007.strengthened_not_exhaustive : ∃ (d : HappyDeg), strengthenedQuad happyTP QuadForm.positive d = false ∧ strengthenedQuad happyTP QuadForm.negative d = false

Contrast: the strengthened model does NOT exhaust the scale. There exist degrees in the gap that are neither "happy" nor "unhappy".

@cite{blutner-2000}'s weak Bidirectional OT (eq. 14, "weak optimality") derives the form-meaning assignment from constraint competition. Krifka explicitly invokes this version (p. 6, citing @cite{blutner-2000} and @cite{jaeger-2002}). The evaluation uses superoptimal from Core.Logic.ConstraintEvaluation.

Two ranked constraints:
1. **M-principle** (@cite{horn-1984}): simple forms pair with stereotypical
   meanings; complex forms pair with non-stereotypical meanings.
2. **Economy**: minimize form complexity.

Under weak BiOT, the four-way form-meaning assignment emerges from the
greatest-fixed-point computation regardless of ranking. This is because
the weak BiOT fixed point re-admits pairs whose blockers were themselves
eliminated — producing Horn's division of pragmatic labour in all cases
where each form has a unique best meaning and vice versa. 

inductive Phenomena.Negation.Studies.Krifka2007.Region : Type

Meaning regions on the scale after pragmatic strengthening. The contradictory threshold θ splits into four regions: two stereotypical (clearly above/below) and two non-stereotypical (borderline, the plateau that becomes the "gap").

• positive : Region
• plateauHigh : Region
• plateauLow : Region
• negative : Region

instance Phenomena.Negation.Studies.Krifka2007.instReprRegion : Repr Region

Equations

• Phenomena.Negation.Studies.Krifka2007.instReprRegion = { reprPrec := Phenomena.Negation.Studies.Krifka2007.instReprRegion.repr }

def Phenomena.Negation.Studies.Krifka2007.instReprRegion.repr : Region → ℕ → Std.Format

Equations

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

instance Phenomena.Negation.Studies.Krifka2007.instDecidableEqRegion : DecidableEq Region

Equations

• Phenomena.Negation.Studies.Krifka2007.instDecidableEqRegion x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Negation.Studies.Krifka2007.instBEqRegion.beq : Region → Region → Bool

Equations

• Phenomena.Negation.Studies.Krifka2007.instBEqRegion.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Negation.Studies.Krifka2007.instBEqRegion : BEq Region

Equations

• Phenomena.Negation.Studies.Krifka2007.instBEqRegion = { beq := Phenomena.Negation.Studies.Krifka2007.instBEqRegion.beq }

def Phenomena.Negation.Studies.Krifka2007.biotPairs : List (QuadForm × Region)

Semantically compatible form-meaning pairs. Under contradictory semantics (H2), forms partition by literal denotation:

• Literally positive (happy, not unhappy): d > θ → positive or plateauHigh
• Literally negative (unhappy, not happy): d ≤ θ → negative or plateauLow

Equations

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

def Phenomena.Negation.Studies.Krifka2007.mPrinciple : Core.OT.NamedConstraint (QuadForm × Region)

M-Principle constraint (@cite{horn-1984}, Horn's Division of Pragmatic Labor): penalizes mismatch between form complexity and meaning stereotypicality.

• Simple form + stereotypical meaning → 0 violations (match)
• Complex form + non-stereotypical meaning → 0 violations (match)
• Cross-assignment → 1 violation (mismatch)

Equations

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

def Phenomena.Negation.Studies.Krifka2007.economyQ : Core.OT.NamedConstraint (QuadForm × Region)

Economy constraint: penalizes form complexity. Violation count = QuadForm.complexity.

Equations

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

def Phenomena.Negation.Studies.Krifka2007.biotProfile (ranking : List (Core.OT.NamedConstraint (QuadForm × Region))) (p : QuadForm × Region) : List ℕ

Build the violation profile for a ranking of constraints.

Equations

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

theorem Phenomena.Negation.Studies.Krifka2007.krifka_biot_prediction : Core.ConstraintEvaluation.superoptimal biotPairs (biotProfile [mPrinciple, economyQ]) = [(QuadForm.positive, Region.positive), (QuadForm.notNegative, Region.plateauHigh), (QuadForm.negative, Region.negative), (QuadForm.notPositive, Region.plateauLow)]

Main BiOT result: M-Principle >> Economy derives Krifka's quadruplet assignment. Each form gets a unique meaning region:

• "happy" → clearly positive (stereotypical)
• "not unhappy" → borderline positive / plateau (non-stereotypical)
• "unhappy" → clearly negative (stereotypical)
• "not happy" → borderline negative / plateau (non-stereotypical)

theorem Phenomena.Negation.Studies.Krifka2007.biot_covers_all_forms : List.map Prod.fst (Core.ConstraintEvaluation.superoptimal biotPairs (biotProfile [mPrinciple, economyQ])) = [QuadForm.positive, QuadForm.notNegative, QuadForm.negative, QuadForm.notPositive]

Each quadruplet form receives a unique meaning: the BiOT assignment is a bijection between the four forms and the four regions.

theorem Phenomena.Negation.Studies.Krifka2007.biot_covers_all_regions : List.map Prod.snd (Core.ConstraintEvaluation.superoptimal biotPairs (biotProfile [mPrinciple, economyQ])) = [Region.positive, Region.plateauHigh, Region.negative, Region.plateauLow]

Each region is assigned to exactly one form.

theorem Phenomena.Negation.Studies.Krifka2007.economy_ranking_independent : Core.ConstraintEvaluation.superoptimal biotPairs (biotProfile [economyQ, mPrinciple]) = Core.ConstraintEvaluation.superoptimal biotPairs (biotProfile [mPrinciple, economyQ])

Under weak BiOT, Economy >> M produces the same four-way assignment as M >> Economy. The greatest-fixed-point computation re-admits the complex forms after their blockers are removed: pairs like ⟨notNegative, plateauHigh⟩ are initially blocked by ⟨positive, plateauHigh⟩, but that pair is itself blocked by ⟨positive, positive⟩, so ⟨notNegative, plateauHigh⟩ returns.

This ranking-independence is a general property of weak BiOT for form-meaning games where each form has a unique best meaning. Under strong BiOT (strongOptimal), Economy >> M would collapse the quadruplet to only two pairs.

theorem Phenomena.Negation.Studies.Krifka2007.both_rankings_give_quadruplet : (Core.ConstraintEvaluation.superoptimal biotPairs (biotProfile [mPrinciple, economyQ])).length = 4 ∧ (Core.ConstraintEvaluation.superoptimal biotPairs (biotProfile [economyQ, mPrinciple])).length = 4

The full quadruplet survives under both rankings.

theorem Phenomena.Negation.Studies.Krifka2007.biot_breaks_synonymy : have result := Core.ConstraintEvaluation.superoptimal biotPairs (biotProfile [mPrinciple, economyQ]); ((result.any fun (x : QuadForm × Region) => x == (QuadForm.positive, Region.positive)) && result.any fun (x : QuadForm × Region) => x == (QuadForm.notNegative, Region.plateauHigh)) = true

The BiOT derivation agrees with the strengthened semantics (§ 3): "happy" and "not unhappy" are assigned to different meaning regions, breaking the synonymy that holds under contradictory semantics (§ 2).