Documentation

Linglib.Theories.Semantics.Gradability.AntonymPrediction

Antonym Prediction — Two Extensional Denotations + Prediction Skeleton #

@cite{cruse-1986} @cite{horn-1989} @cite{krifka-2007b}

For the four-form quadruplet of a negated antonymic adjective pair (see AntonymQuadruplet.lean), 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
@[reducible, inline]
abbrev Semantics.Gradability.AntonymForm.contradictoryDenot {max : ℕ} (θ : Core.Scale.Threshold max) (q : AntonymForm) (d : Core.Scale.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 @cite{krifka-2007b} attributes to antonyms before pragmatic strengthening.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev Semantics.Gradability.AntonymForm.strengthenedDenot {max : ℕ} (tp : ThresholdPair max) (q : AntonymForm) (d : Core.Scale.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 : ℕ} (θ : Core.Scale.Threshold max) (d : Core.Scale.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 @cite{krifka-2007b} 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 : Core.Scale.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.

      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 contradictoryDenot_synonymy (the contradictory base collapses notPositive and negative; no asymmetry to derive).
      • .contrary ↦ .asymmetric — anchored by strengthenedDenot_breaks_synonymy (the strengthened semantics admits a witness where notNegative holds but positive does not).

      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 : GradableAdjEntry) :
        Features.Asymmetry

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

        Equations
        Instances For