Documentation

Linglib.Semantics.Degree.Antonymy

Antonymy: Contradictory vs. Contrary Negation #

[Kri07b] [Cru86] [Hor89]

Two models of gradable adjective antonymy and their formal properties.

Contradictory model (single threshold θ): happy and unhappy partition the scale. contradictoryNeg d θ = !positiveMeaning d θ — double negation eliminates and "not unhappy" = "happy".

Contrary model (two thresholds θ_neg < θ_pos): happy and unhappy leave a gap. notContraryNegMeaning d tp ≠ positiveMeaning' d tp in the gap region. Double negation does NOT eliminate.

[Kri07b] argues that antonyms are literally contradictory (single θ) and the gap emerges through pragmatic strengthening (M-principle). The contrary model captures the effective semantics after strengthening. Both models are formalized here; the pragmatic derivation connecting them is in Studies/Krifka2007.lean.

The core operations (contradictoryNeg, contraryNeg, inGapRegion, ThresholdPair, positiveMeaning', contraryNegMeaning, notContraryNegMeaning) are defined in Gradability/Adjective.lean.

Contradictory Negation: Involutory (DNE holds) #

source
@[simp]
theorem Degree.Antonymy.contradictory_is_complement {max : ℕ} (d : Bounded max) (θ : Threshold max) :
contradictoryNeg d θ ↔ ¬positiveMeaning d θ

Contradictory negation is the propositional complement of positive meaning. Both compute threshold comparisons: d ≤ ↑θ vs ↑θ < d.

source
theorem Degree.Antonymy.contradictory_dne {max : ℕ} (d : Bounded max) (θ : Threshold max) :
¬contradictoryNeg d θ ↔ positiveMeaning d θ

Double contradictory negation eliminates: "not [not happy]" = "happy".

[Kri07b]: this is the LITERAL semantics. If antonyms are contradictory, then "not unhappy" and "happy" are synonymous — the puzzle that motivates pragmatic strengthening.

source
theorem Degree.Antonymy.contradictory_exhaustive {max : ℕ} (d : Bounded max) (θ : Threshold max) :
positiveMeaning d θ ∨ contradictoryNeg d θ

Under contradictory semantics, the scale is exhaustively partitioned: every degree is either positive or in the antonym region, with no gap.

Contrary Negation: Gap (DNE fails) #

source
@[simp]
theorem Degree.Antonymy.gap_iff_not_neg_and_not_pos {max : ℕ} (d : Bounded max) (tp : ThresholdPair max) :
inGapRegion d tp ↔ notContraryNegMeaning d tp ∧ ¬positiveMeaning' d tp

The gap region is exactly "not unhappy" ∧ "not happy": degrees that escape the contrary negative without reaching the positive threshold.

source
theorem Degree.Antonymy.contrary_gap_exists {max : ℕ} (tp : ThresholdPair max) (h : { value := tp.neg.value.castSucc } < { value := tp.pos.value.castSucc }) :
∃ (d : Bounded max), notContraryNegMeaning d tp ∧ ¬positiveMeaning' d tp

When the gap is strict (θ_neg < θ_pos), there exists a degree that is "not unhappy" but NOT "happy" — double negation through contrary fails. Witness: the negative threshold itself (as a degree).

source
theorem Degree.Antonymy.gap_nonempty {max : ℕ} (tp : ThresholdPair max) (h : { value := tp.neg.value.castSucc } < { value := tp.pos.value.castSucc }) :
∃ (d : Bounded max), inGapRegion d tp

The gap region is nonempty when θ_neg < θ_pos.

The surface quadruplet and prediction skeleton #

[Cru86] [Hor89] [Kri07b] [TF19]

Absorbed from the retired AntonymPrediction.lean: AntonymForm (happy / not happy / unhappy / not unhappy), its two contested denotations, and the complexity/prediction skeleton.

source
inductive Degree.AntonymForm :
Type

The four surface forms generated from an antonymic adjective pair (positive, negative) by sentential negation. Four-cell substrate; no semantic commitment — a paper claiming all four forms collapse to two (contradictory analysis) and a paper claiming a four-way gap (contrary analysis) both consume this enum and provide their own denotations.

Instances For
    source
    def Degree.instReprAntonymForm.repr :
    AntonymForm → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[implicit_reducible]
      instance Degree.instReprAntonymForm :
      Repr AntonymForm
      Equations
      source
      @[implicit_reducible]
      instance Degree.instDecidableEqAntonymForm :
      DecidableEq AntonymForm
      Equations
      source
      @[implicit_reducible]
      instance Degree.instFintypeAntonymForm :
      Fintype AntonymForm
      Equations
      source
      def Degree.AntonymForm.complexity :
      AntonymForm → ℕ

      Default morphological-syntactic complexity of each form: count of negation operators (morphological un- + syntactic not), scaled to [Kri07b]'s integer ordering 0 < 2 < 3 < 5. Matches [TF19]'s utteranceCost exactly.

      Per-paper analyses may override the cost (TF2020 uses a ℚ-valued coercion of this; Krifka's Economy constraint reads it directly).

      Equations
      Instances For
        source
        theorem Degree.AntonymForm.complexity_strictMono :
        positive.complexity < negative.complexity ∧ negative.complexity < notPositive.complexity ∧ notPositive.complexity < notNegative.complexity

        The complexity ordering is strictly monotone across the quadruplet in the canonical order positive < negative < notPositive < notNegative.

        source
        @[reducible, inline]
        abbrev Degree.AntonymForm.contradictoryDenot {max : ℕ} (θ : Threshold max) (q : AntonymForm) (d : Bounded max) :
        Prop

        Contradictory denotation of an antonym form on a single threshold θ. Both poles share θ; the four forms collapse to two distinct truth values (positive/notNegative ≡ d > θ; notPositive/negative ≡ d ≤ θ). This is the literal-semantic position [Kri07b] attributes to antonyms before pragmatic strengthening.

        Equations
        Instances For
          source
          @[reducible, inline]
          abbrev Degree.AntonymForm.strengthenedDenot {max : ℕ} (tp : ThresholdPair max) (q : AntonymForm) (d : Bounded max) :
          Prop

          Strengthened denotation of an antonym form on a ThresholdPair. Two thresholds tp.neg ≤ tp.pos; the borderline region [tp.neg, tp.pos] lifts notNegative ("not unhappy") away from positive ("happy") and notPositive ("not happy") away from negative ("unhappy"). This is the effective-semantic position post-pragmatic-strengthening (Krifka 2007 §4) or the lexically-encoded position (Alexandropoulou-Gotzner 2024).

          Equations
          Instances For
            source
            theorem Degree.contradictoryDenot_synonymy {max : ℕ} (θ : Threshold max) (d : Bounded max) :
            (AntonymForm.contradictoryDenot θ AntonymForm.negative d ↔ AntonymForm.contradictoryDenot θ AntonymForm.notPositive d) ∧ (AntonymForm.contradictoryDenot θ AntonymForm.notNegative d ↔ AntonymForm.contradictoryDenot θ AntonymForm.positive d)

            Under the contradictory denotation, the negative-notPositive and notNegative-positive form pairs are extensionally identical. This is the formal puzzle [Kri07b] solves pragmatically: literal contradictory semantics predicts not unhappy ≡ happy.

            source
            theorem Degree.strengthenedDenot_breaks_synonymy {max : ℕ} (tp : ThresholdPair max) (h : { value := tp.neg.value.castSucc } < { value := tp.pos.value.castSucc }) :
            ∃ (d : Bounded max), AntonymForm.strengthenedDenot tp AntonymForm.notNegative d ∧ ¬AntonymForm.strengthenedDenot tp AntonymForm.positive d

            Under the strengthened denotation with strict gap (tp.neg < tp.pos), the notNegative and positive extensions come apart: there exists a degree (the negative threshold itself) where not unhappy holds but happy does not. This is the witness for the polarity asymmetry.

            Grounding in the Aristotelian opposition relation #

            The antonym classification is not a stipulated tag: the two form denotations genuinely stand in the substrate's Aristotelian.IsContradictory / IsContrary ([DKD25]), so predictionForAntonymy rides on a real opposition.

            source
            theorem Degree.isContradictory_contradictoryDenot {max : ℕ} (θ : Threshold max) :
            Aristotelian.IsContradictory (fun (d : Bounded max) => AntonymForm.contradictoryDenot θ AntonymForm.positive d) fun (d : Bounded max) => AntonymForm.contradictoryDenot θ AntonymForm.negative d

            Contradictory denotation ⇒ IsContradictory. With a single threshold the negative form is the literal complement of the positive form, so the two are complementary in the Boolean algebra Degree → Prop — forced (it is IsCompl). contradictoryDenot_synonymy (DNE collapse) is a corollary.

            source
            theorem Degree.isContrary_strengthenedDenot {max : ℕ} (tp : ThresholdPair max) (h : { value := tp.neg.value.castSucc } < { value := tp.pos.value.castSucc }) :
            Aristotelian.IsContrary (fun (d : Bounded max) => AntonymForm.strengthenedDenot tp AntonymForm.positive d) fun (d : Bounded max) => AntonymForm.strengthenedDenot tp AntonymForm.negative d

            Strengthened denotation with a strict gap ⇒ IsContrary. Positive (d > tp.pos) and contrary-negative (d < tp.neg) are jointly impossible (Disjoint) but, by the gap [tp.neg, tp.pos], not jointly exhaustive (¬ Codisjoint — contrary_gap_exists is the witness).

            source
            def Degree.predictionForAntonymy :
            Features.NegationType → Features.Asymmetry

            Anchored prediction skeleton. Map an antonymy type to predicted polarity-asymmetry direction:

            • .contradictory ↦ .symmetric — anchored by isContradictory_contradictoryDenot (the forms are genuinely complementary, so the contradictory base collapses notPositive and negative; no asymmetry to derive).
            • .contrary ↦ .asymmetric — anchored by isContrary_strengthenedDenot (the forms are genuinely contrary, so the gap admits a witness where notNegative holds but positive does not).

            The map thus rides on the substrate's IsContradictory/IsContrary between the two form denotations — the antonym tag is the real opposition, not a stipulation.

            Consumed by per-paper prediction signatures (Horn 1989, Krifka 2007, Alexandropoulou-Gotzner 2024 JoS) which read this map via predictionForEntry against a Fragment lexical entry's antonymRelation field.

            Equations
            Instances For
              source
              def Degree.predictionForEntry (e : GradableAdjective) :
              Features.Asymmetry

              Read prediction off a Fragment lexical entry's antonymRelation. Defaults to .symmetric for entries without an explicit antonymy classification.

              Equations
              Instances For