@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) #
- Epistemic vagueness: Speakers avoid borderline cases to ensure safe communication (following Williamson 1994).
- 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.
- 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:
- 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.Constraint.Evaluation.superoptimal. - RSA model: @cite{tessler-franke-2019} (
Studies/TesslerFranke2020.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
Semantics.Gradability.AntonymForm (file
Theories/Semantics/Gradability/AntonymQuadruplet.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
Theories/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.
5-point happiness scale (matching @cite{tessler-franke-2019}'s model).
Equations
Instances For
Contradictory boundary at θ = 2 (the literal semantics).
Equations
Instances For
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 := Core.Scale.thr 2 Krifka2007.happyθ._proof_2, neg := Core.Scale.thr 1 Krifka2007.happyTP._proof_2, gap_exists := Krifka2007.happyTP._proof_3 }
Instances For
Prediction 1: Under contradictory semantics, all degrees are classified. No gap exists. (Krifka's H2: literal exhaustivity.)
Prediction 2: Under contradictory semantics, "not unhappy" iff "happy" at every degree. (The puzzle.)
Prediction 3: After strengthening, the gap breaks synonymy.
Prediction 4: The gap region is nonempty (degrees 1 and 2).
Prediction 5: Degree 0 is "unhappy", degree 4 is "happy".
FlexibleNegation classifies "unhappy" as contrary — this is the effective (post-strengthening) semantics, consistent with Krifka's analysis where the contrary behavior is pragmatically derived.
The empirical double-negation non-equivalence is derived from the strengthened model (§3): synonymy is broken by the gap.
The gap prediction from FlexibleNegation data corresponds to
contrary_gap_exists applied to the strengthened model.
Krifka's form complexity ordering matches the markedness infrastructure. "unhappy" is marked over "happy" by morphological complexity.
Cost asymmetry in FlexibleNegation data reflects Krifka's form complexity ordering.
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.
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.Constraint.Evaluation.
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.
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").
Instances For
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✝
Instances For
Equations
- Krifka2007.instReprRegion = { reprPrec := Krifka2007.instReprRegion.repr }
Equations
- Krifka2007.instDecidableEqRegion x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
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.
Instances For
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.
Instances For
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.
Instances For
Economy constraint: penalizes form complexity.
Violation count = AntonymForm.complexity.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Build the violation profile for a ranking of constraints.
Equations
- Krifka2007.biotProfile ranking p = List.map (fun (c : Core.Constraint.OT.NamedConstraint (Semantics.Gradability.AntonymForm × Krifka2007.Region)) => c.eval p) ranking
Instances For
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.
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).
Each quadruplet form receives a unique meaning. Derives from the BiOT
assignment via Finset.image.
Each region is assigned to exactly one form. Derives from the BiOT
assignment via Finset.image.
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.
The full quadruplet survives under both rankings.
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).