Documentation

Linglib.Studies.Krifka2007

[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 Semantics.Gradability.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]

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

Equations
Instances For
    @[reducible, inline]

    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
      Instances For
        theorem Krifka2007.happy_gap_strict :
        { value := happyTP.neg.value.castSucc } < { value := happyTP.pos.value.castSucc }

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

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

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

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

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

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

            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.

            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.

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

            theorem Krifka2007.cost_eq_complexity (row : Data.Examples.LinguisticExample) :
            row TesslerFranke2019.Examples.allfformOf 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.

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

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

            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
              def Krifka2007.instReprRegion.repr :
              RegionStd.Format
              Equations
              Instances For
                @[implicit_reducible]
                Equations
                @[implicit_reducible]
                Equations

                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

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

                    Equations
                    Instances For

                      Build the violation profile for a ranking of constraints.

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