Documentation

Linglib.Semantics.Degree.Gradability.AntonymPrediction

Antonym Forms — Surface Quadruplet, Two Denotations, Prediction Skeleton #

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

Given an antonymic adjective pair (positive / negative — e.g., happy / unhappy), sentential negation generates four surface forms:

{happy, not happy, unhappy, not unhappy}

AntonymForm enumerates them; AntonymForm.complexity gives each form's default morphological-syntactic complexity, matching [Kri07b]'s ordering and [TF19]'s cost function. For the quadruplet, the literature contests two extensional denotations:

The two denotations are anchored by the substrate theorems contradictoryDenot_synonymy (DNE collapse) and strengthenedDenot_breaks_synonymy (gap exists).

The prediction skeleton predictionForAntonymy : NegationType → Asymmetry reads off Fragment-level antonymy classification (contrary vs contradictory) to predict the polarity-behaviour direction. It is anchored in the two denotation theorems: contradictory antonymy entails DNE (symmetric) and contrary antonymy admits the strengthened gap (asymmetric).

Per-paper analyses (Krifka's BiOT derivation, Tessler-Franke's RSA scoring, Alexandropoulou-Gotzner's three-case typology) consume these substrate primitives via Iff.rfl bridges that survive substrate transparency (both denotations are abbrevs).

source
inductive Semantics.Gradability.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 Semantics.Gradability.instReprAntonymForm.repr :
    AntonymForm → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[implicit_reducible]
      instance Semantics.Gradability.instReprAntonymForm :
      Repr AntonymForm
      Equations
      source
      @[implicit_reducible]
      instance Semantics.Gradability.instDecidableEqAntonymForm :
      DecidableEq AntonymForm
      Equations
      source
      @[implicit_reducible]
      instance Semantics.Gradability.instFintypeAntonymForm :
      Fintype AntonymForm
      Equations
      • One or more equations did not get rendered due to their size.
      source
      def Semantics.Gradability.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 Semantics.Gradability.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 Semantics.Gradability.AntonymForm.contradictoryDenot {max : ℕ} (θ : Degree.Threshold max) (q : AntonymForm) (d : Degree.Degree 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 Semantics.Gradability.AntonymForm.strengthenedDenot {max : ℕ} (tp : ThresholdPair max) (q : AntonymForm) (d : Degree.Degree 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 Semantics.Gradability.contradictoryDenot_synonymy {max : ℕ} (θ : Degree.Threshold max) (d : Degree.Degree 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 Semantics.Gradability.strengthenedDenot_breaks_synonymy {max : ℕ} (tp : ThresholdPair max) (h : { value := tp.neg.value.castSucc } < { value := tp.pos.value.castSucc }) :
            ∃ (d : Degree.Degree 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 Semantics.Gradability.isContradictory_contradictoryDenot {max : ℕ} (θ : Degree.Threshold max) :
            Aristotelian.IsContradictory (fun (d : Degree.Degree max) => AntonymForm.contradictoryDenot θ AntonymForm.positive d) fun (d : Degree.Degree 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 Semantics.Gradability.isContrary_strengthenedDenot {max : ℕ} (tp : ThresholdPair max) (h : { value := tp.neg.value.castSucc } < { value := tp.pos.value.castSucc }) :
            Aristotelian.IsContrary (fun (d : Degree.Degree max) => AntonymForm.strengthenedDenot tp AntonymForm.positive d) fun (d : Degree.Degree 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 Semantics.Gradability.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 Semantics.Gradability.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