[Kri07b] — Negated Antonyms: Creating and Filling the Gap

[Kri07b]

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

Krifka's Thesis

Krifka argues, against the received view ([Cru86], [Hor89]), 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 ([Hor84]).

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 states transfer equations against [TF19]'s quadruplet rows (Data/Examples/TesslerFranke2019.json). The pragmatic mechanism connecting contradictory base → effective ThresholdPair is derived via two routes:

1. Bidirectional OT (§ 9 below): [Blu00]'s weak BiOT (eq. 14) derives the four-way form-meaning assignment via the greatest-fixed-point computation in Core.Optimization.Evaluation.superoptimal.
2. RSA model: [TF19] (Studies/TesslerFranke2020PMF.lean) derives the same effect through Bayesian pragmatic reasoning.

Krifka's quadruplet (ex. 1) — the four forms {happy, not happy, unhappy, not unhappy} generated by combining an antonym pair with sentential negation — is provided as substrate by Degree.AntonymForm (file Semantics/Degree/Gradability/AntonymPrediction.lean). The complexity ordering 0 < 2 < 3 < 5 lives there as AntonymForm.complexity.

Krifka's H2 — antonyms are literally contradictory (single threshold θ); all four forms derive from propositional operations on d > θ — is captured by substrate AntonymForm.contradictoryDenot (file Semantics/Gradability/AntonymPrediction.lean). The synonymy puzzle (negative ≡ notPositive, notNegative ≡ positive under contradictory semantics) is the substrate theorem contradictoryDenot_synonymy.

See also `Antonymy.contradictory_dne` for the DNE form (the puzzle
Krifka's pragmatic strengthening solves). 

After pragmatic strengthening (M-principle) the effective semantics uses a ThresholdPair; the four forms split via the borderline region. This is captured by substrate AntonymForm.strengthenedDenot. The synonymy breaking witness for notNegative vs positive under strict gap is the substrate theorem strengthenedDenot_breaks_synonymy.

@[reducible, inline]

abbrev Krifka2007.HappyDeg : Type

5-point happiness scale (matching [TF19]'s model).

Equations

• Krifka2007.HappyDeg = Degree.Bounded 4

@[reducible, inline]

abbrev Krifka2007.happyθ : Degree.Threshold 4

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

Equations

• Krifka2007.happyθ = Degree.thr 2 Krifka2007.happyθ._proof_2

def Krifka2007.happyTP : Degree.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

• Krifka2007.happyTP = { pos := Degree.thr 2 Krifka2007.happyθ._proof_2, neg := Degree.thr 1 Krifka2007.happyTP._proof_2 }

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

theorem Krifka2007.contradictory_exhaustive_concrete (d : HappyDeg) : Degree.AntonymForm.contradictoryDenot happyθ Degree.AntonymForm.positive d ∨ Degree.AntonymForm.contradictoryDenot happyθ Degree.AntonymForm.negative d

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

theorem Krifka2007.contradictory_not_unhappy_iff_happy (d : HappyDeg) : Degree.AntonymForm.contradictoryDenot happyθ Degree.AntonymForm.notNegative d ↔ Degree.AntonymForm.contradictoryDenot happyθ Degree.AntonymForm.positive d

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

theorem Krifka2007.strengthened_not_unhappy_witnesses_gap : ∃ (d : HappyDeg), Degree.AntonymForm.strengthenedDenot happyTP Degree.AntonymForm.notNegative d ∧ ¬Degree.AntonymForm.strengthenedDenot happyTP Degree.AntonymForm.positive d

Prediction 3: After strengthening, the gap breaks synonymy.

theorem Krifka2007.gap_degrees : Degree.inGapRegion (Degree.deg 1 ⋯) happyTP ∧ Degree.inGapRegion (Degree.deg 2 ⋯) happyTP

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

theorem Krifka2007.extreme_degrees : Degree.contraryNegMeaning (Degree.deg 0 ⋯) happyTP ∧ Degree.positiveMeaning' (Degree.deg 4 ⋯) happyTP

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

[TF19]'s quadruplet rows (Data/Examples/TesslerFranke2019.json) classify each form by its innermost negation (inner_neg), preferred interpretation (interpretation), cost parameter (cost), and whether the form is judged equivalent to the bare positive (equivalent_to_positive). The theorems below are the transfer equations between those classifications and the strengthened model (§ 4-5).

def Krifka2007.formOf (row : Data.Examples.LinguisticExample) : Option Degree.AntonymForm

Quadruplet-form adapter: the row's form feature as an AntonymForm.

Equations

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

def Krifka2007.interpretationOf (row : Data.Examples.LinguisticExample) : Option Features.NegationType

Interpretation adapter: the row's preferred interpretation feature as a NegationType.

Equations

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

theorem Krifka2007.interpretation_follows_inner_neg (row : Data.Examples.LinguisticExample) : row ∈ TesslerFranke2019.Examples.all → (row.feature? "inner_neg" = some "morphological" ↔ interpretationOf row = some Features.NegationType.contrary)

Interpretation follows the innermost negation: a row's preferred interpretation is contrary iff its innermost negation is morphological. "Not unhappy" inherits the contrary reading of the inner un- — the effective (post-strengthening) semantics, consistent with Krifka's analysis where the contrary behavior is pragmatically derived.

theorem Krifka2007.equivalent_to_positive_iff_strengthened (row : Data.Examples.LinguisticExample) : row ∈ TesslerFranke2019.Examples.all → ∀ f ∈ formOf row, row.feature? "equivalent_to_positive" = some "true" ↔ ∀ (d : HappyDeg), Degree.AntonymForm.strengthenedDenot happyTP f d ↔ Degree.AntonymForm.strengthenedDenot happyTP Degree.AntonymForm.positive d

Transfer equation: a row is judged equivalent to the bare positive iff the strengthened denotation of its form coincides with positive at every degree. The load-bearing case is notNegative ("not unhappy"): the gap (§ 5, Prediction 3-4) puts it on the non-equivalent side.

theorem Krifka2007.cost_eq_complexity (row : Data.Examples.LinguisticExample) : row ∈ TesslerFranke2019.Examples.all → ∀ f ∈ formOf row, row.feature? "cost" = some (toString f.complexity)

Cost = complexity: the rows' cost parameters (C(un-) = 2, C(not) = 3, additive) equal Krifka's form complexity (AntonymForm.complexity) at every quadruplet form. With interpretation_follows_inner_neg this is Horn's division of pragmatic labor: the cheaper single negation ("unhappy") takes the contrary reading, the costlier one ("not happy") the marked contradictory one.

theorem Krifka2007.unconditional_exhaustive (d : HappyDeg) : Degree.AntonymForm.contradictoryDenot happyθ Degree.AntonymForm.positive d ∨ Degree.AntonymForm.contradictoryDenot happyθ Degree.AntonymForm.negative d

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 Krifka2007.strengthened_not_exhaustive : ∃ (d : HappyDeg), ¬Degree.AntonymForm.strengthenedDenot happyTP Degree.AntonymForm.positive d ∧ ¬Degree.AntonymForm.strengthenedDenot happyTP Degree.AntonymForm.negative d

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

[Blu00]'s weak Bidirectional OT (eq. 14, "weak optimality") derives the form-meaning assignment from constraint competition. Krifka explicitly invokes this version (p. 6, citing [Blu00] and [jaeger-2002]). The evaluation uses superoptimal from Core.Optimization.Evaluation.

Two ranked constraints:
1. **M-principle** ([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 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

def Krifka2007.instReprRegion.repr : Region → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Krifka2007.instReprRegion.repr Krifka2007.Region.positive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka2007.Region.positive")).group prec✝
• Krifka2007.instReprRegion.repr Krifka2007.Region.negative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka2007.Region.negative")).group prec✝

@[instance_reducible]

instance Krifka2007.instReprRegion : Repr Region

Equations

• Krifka2007.instReprRegion = { reprPrec := Krifka2007.instReprRegion.repr }

@[instance_reducible]

instance Krifka2007.instDecidableEqRegion : DecidableEq Region

Equations

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

def Krifka2007.biotPairs : Finset (Degree.AntonymForm × Region)

Semantically compatible form-meaning pairs as a Finset (decidable membership; supports decide-based per-pair blocking checks via the substrate's Blocks.decidableOnFinset instance).

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 Krifka2007.krifkaQuadruplet : Finset (Degree.AntonymForm × Region)

Krifka's predicted form-meaning quadruplet: each form gets a unique meaning region. The substrate-superoptimalSet-as-greatest-fixed-point formulation hits this set as the GFP under both M>>E and E>>M rankings (see krifka_biot_prediction and economy_ranking_independent).

Equations

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

def Krifka2007.mPrinciple : Constraints.Constraint (Degree.AntonymForm × Region)

M-Principle constraint ([Hor84], 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

• Krifka2007.mPrinciple (Degree.AntonymForm.positive, Krifka2007.Region.positive) = 0
• Krifka2007.mPrinciple (Degree.AntonymForm.positive, Krifka2007.Region.plateauHigh) = 1
• Krifka2007.mPrinciple (Degree.AntonymForm.notNegative, Krifka2007.Region.positive) = 1
• Krifka2007.mPrinciple (Degree.AntonymForm.notNegative, Krifka2007.Region.plateauHigh) = 0
• Krifka2007.mPrinciple (Degree.AntonymForm.negative, Krifka2007.Region.negative) = 0
• Krifka2007.mPrinciple (Degree.AntonymForm.negative, Krifka2007.Region.plateauLow) = 1
• Krifka2007.mPrinciple (Degree.AntonymForm.notPositive, Krifka2007.Region.negative) = 1
• Krifka2007.mPrinciple (Degree.AntonymForm.notPositive, Krifka2007.Region.plateauLow) = 0
• Krifka2007.mPrinciple x✝ = 0

def Krifka2007.economyQ : Constraints.Constraint (Degree.AntonymForm × Region)

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

Equations

• Krifka2007.economyQ p = p.1.complexity

def Krifka2007.biotProfile (ranking : List (Constraints.Constraint (Degree.AntonymForm × Region))) (p : Degree.AntonymForm × Region) : List ℕ

Build the violation profile for a ranking of constraints.

Equations

• Krifka2007.biotProfile ranking p = List.map (fun (c : Constraints.Constraint (Degree.AntonymForm × Krifka2007.Region)) => c p) ranking

theorem Krifka2007.krifka_biot_prediction : Pragmatics.Bidirectional.superoptimal biotPairs (biotProfile [mPrinciple, economyQ]) = krifkaQuadruplet

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)

Stated on the Finset-native canonical form superoptimal from the substrate; equality with the literal Finset is decide-checked directly.

theorem Krifka2007.krifka_biot_prediction_gfp : Pragmatics.Bidirectional.superoptimalSet (↑biotPairs) (biotProfile [mPrinciple, economyQ]) = ↑krifkaQuadruplet

Structural lift to abstract gfp form: the same equality holds at the set-valued OrderHom.gfp level (via the substrate bridge theorem superoptimal_coe_eq_set). Useful for arguments that reason about the abstract gfp directly (e.g. universal properties of superoptimal sets, comparisons across BiOT variants).

theorem Krifka2007.biot_covers_all_forms : Finset.image Prod.fst krifkaQuadruplet = {Degree.AntonymForm.positive, Degree.AntonymForm.notNegative, Degree.AntonymForm.negative, Degree.AntonymForm.notPositive}

Each quadruplet form receives a unique meaning. Derives from the BiOT assignment via Finset.image.

theorem Krifka2007.biot_covers_all_regions : Finset.image Prod.snd krifkaQuadruplet = {Region.positive, Region.plateauHigh, Region.negative, Region.plateauLow}

Each region is assigned to exactly one form. Derives from the BiOT assignment via Finset.image.

theorem Krifka2007.economy_ranking_independent : Pragmatics.Bidirectional.superoptimal biotPairs (biotProfile [economyQ, mPrinciple]) = Pragmatics.Bidirectional.superoptimal biotPairs (biotProfile [mPrinciple, economyQ])

Headline ranking-invariance: 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, Economy >> M would collapse the quadruplet to only two pairs.

Direct kernel-verified decide: both Finset iterations stabilize to the same fixed point.

theorem Krifka2007.both_rankings_give_quadruplet : Pragmatics.Bidirectional.superoptimal biotPairs (biotProfile [mPrinciple, economyQ]) = krifkaQuadruplet ∧ Pragmatics.Bidirectional.superoptimal biotPairs (biotProfile [economyQ, mPrinciple]) = krifkaQuadruplet

The full quadruplet survives under both rankings.

theorem Krifka2007.biot_breaks_synonymy : (Degree.AntonymForm.positive, Region.positive) ∈ Pragmatics.Bidirectional.superoptimal biotPairs (biotProfile [mPrinciple, economyQ]) ∧ (Degree.AntonymForm.notNegative, Region.plateauHigh) ∈ Pragmatics.Bidirectional.superoptimal biotPairs (biotProfile [mPrinciple, economyQ])

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).