Antonymy

import Linglib.Semantics.Degree.Antonymy · namespace Degree

This file defines the vocabulary of an antonym pair of gradable adjectives, tall and short or happy and unhappy. Following Kennedy (2007) and Kennedy and McNally (2005), the two members measure the same degrees under inverse orderings, so an adjective's Polarity is which member it is, positive for the member measuring in the scale's increasing direction (tall) and negative for the inverted one (short). Inverting twice restores the ordering, so negative * p is the polarity of the antonym of a p adjective, and polarity acts on scale boundedness and on comparisons through the order dual. The positive forms of the members are contradictory (clean and dirty) or contrary (tall and short, which leave a gap), two cells of the Aristotelian square in the sense of Cruse and Horn; a lexical pair is contradictory when its poles take complementary standards, Degree.AntonymPair.ComplementaryStandards.

The contrary case is modelled by a Degree.ThresholdPair on a linearly ordered scale, the positive form true above its upper threshold and the negative form below its lower one, and Degree.AntonymForm is the quadruplet happy, not happy, unhappy, not unhappy that sentential negation generates from a pair, with a contradictory denotation on one threshold, where not unhappy collapses to happy, and a strengthened denotation on a pair, where the gap keeps them apart, as in Krifka's account. Evaluative valence, whether a predicate denotes a good or a bad property, is a second axis on which the poles differ, distinct from polarity.

Main definitions

The actions of Polarity on Boundedness and on Comparison, the negative polarity by the order dual.
EvaluativeValence: whether a gradable predicate denotes a good, a bad or a neutral property.
ThresholdPair and its ThresholdPair.gap, the interval between the two thresholds.
AntonymForm with AntonymForm.contradictoryDenotation, AntonymForm.strengthenedDenotation and AntonymForm.complexity.

Main results

AntonymForm.contradictoryDenotation_notPositive: contradictory negation is the complement, so double negation eliminates.
ThresholdPair.gap_nonempty_iff, AntonymForm.strengthenedDenotation_notNegative_diff_positive, AntonymForm.strengthenedDenotation_notPositive_diff_negative: a pair leaves a gap when its lower threshold does not exceed its upper one, and the gap is what each negated form adds to the opposite simple form.
isCompl_contradictoryDenotation, isContrary_strengthenedDenotation: the two denotations realize the two cells of the Aristotelian square.

References

Kennedy 2007, Vagueness and Grammar: The Semantics of Relative and Absolute Gradable Adjectives formalized
Kennedy & McNally 2005, Scale Structure, Degree Modification, and the Semantics of Gradable Predicates
Cruse 1986, Lexical Semantics
Horn 1989, A Natural History of Negation
Krifka 2007b, Negated Antonyms: Creating and Filling the Gap formalized
Tessler & Franke 2019, Not Unreasonable: Why Two Negatives Don’t Make a Positive
Nouwen 2024, The Semantics and Probabilistic Pragmatics of Deadjectival Intensifiers formalized

Polarity

Evaluative valence

The evaluative valence of a gradable predicate records whether it denotes a good, a bad or an evaluatively neutral property, which is distinct from scalar polarity (Nouwen 2024). Negative valence yields high-degree intensifiers and positive valence moderate-degree ones, which Nouwen explains by the Goldilocks effect, the negative evaluation of a scale's extremes.

inductive EvaluativeValence L91–99

Type

positive : EvaluativeValence
negative : EvaluativeValence
neutral : EvaluativeValence

Derives Repr, DecidableEq.

Used by EvaluativeValence.flip

Used in Semantics/Attitudes/Basic, Semantics/Degree/Adjective, QingEtAl2025

L101–106

The two-threshold model of a contrary pair

The two thresholds of a contrary antonym pair (happy and unhappy) are pos for the positive form, true above it, and neg for the negative form, true below it. That the lower threshold does not exceed the upper is a hypothesis where a gap is needed, not a stored invariant.

structure ThresholdPair L110–117

(D : Type u_1) :

Type u_1

pos : D
neg : D

Derives Repr, DecidableEq.

Used by ThresholdPair.gap, ThresholdPair.mem_gap, ThresholdPair.gap_nonempty_iff, AntonymForm.strengthenedDenotation, AntonymForm.decidableMemStrengthenedDenotation, AntonymForm.strengthenedDenotation_notNegative_diff_positive, AntonymForm.strengthenedDenotation_notPositive_diff_negative, AntonymForm.isContrary_strengthenedDenotation

Used in AlexandropoulouGotzner2024a, AlexandropoulouGotzner2024b, Beltrama2025

The gap of a pair is the region that is neither positive nor negative, from the lower threshold to the upper.

def ThresholdPair.gap L122–124

{D : Type u_1} [Preorder D] (tp : ThresholdPair D) :

Set D

tp.gap = Set.Icc tp.neg tp.pos

Built from

Used by ThresholdPair.mem_gap, ThresholdPair.gap_nonempty_iff, AntonymForm.strengthenedDenotation_notNegative_diff_positive, AntonymForm.strengthenedDenotation_notPositive_diff_negative

Used in AlexandropoulouGotzner2024a, Beltrama2025

L126

A pair leaves a gap exactly when its lower threshold does not exceed its upper one.

theorem ThresholdPair.gap_nonempty_iff L128–129

{D : Type u_1} [Preorder D] (tp : ThresholdPair D) :

tp.gap.Nonempty ↔ tp.neg ≤ tp.pos

Built from ,

The quadruplet

An antonym form is one of the four surface forms that sentential negation generates from an antonym pair, happy, not happy, unhappy and not unhappy. The type carries no semantics; a contradictory account collapses the four to two denotations and a contrary account keeps four, and each is a function on it.

inductive AntonymForm L135–144

Type

positive : AntonymForm
notPositive : AntonymForm
negative : AntonymForm
notNegative : AntonymForm

Derives Repr, DecidableEq, Fintype.

Used by AntonymForm.flip, AntonymForm.flip_flip, AntonymForm.instMulActionPolarity, AntonymForm.negative_smul, AntonymForm.complexity, AntonymForm.contradictoryDenotation, AntonymForm.strengthenedDenotation, AntonymForm.decidableMemContradictoryDenotation, AntonymForm.decidableMemStrengthenedDenotation

Used in AlexandropoulouGotzner2024a, Krifka2007b

The morphosyntactic complexity of a form, the number of negations counted as Krifka 2007b orders them, 0 < 2 < 3 < 5, matching Tessler & Franke 2019's utterance cost.

def AntonymForm.complexity L166–172

AntonymForm → ℕ

AntonymForm.positive.complexity = 0
AntonymForm.negative.complexity = 2
AntonymForm.notPositive.complexity = 3
AntonymForm.notNegative.complexity = 5

Built from

Used in AlexandropoulouGotzner2024a, Krifka2007b

The contradictory denotation of a form on a single threshold θ, which both poles share, so that the four forms collapse to two, happy and not unhappy above it, not happy and unhappy at or below it. This is the literal semantics Krifka 2007b attributes to a pair before pragmatic strengthening.

def AntonymForm.contradictoryDenotation L177–183

{D : Type u_1} [Preorder D] (θ : D) :

AntonymForm → Set D

AntonymForm.contradictoryDenotation θ AntonymForm.positive = Set.Ioi θ
AntonymForm.contradictoryDenotation θ AntonymForm.notNegative = Set.Ioi θ
AntonymForm.contradictoryDenotation θ AntonymForm.notPositive = Set.Iic θ
AntonymForm.contradictoryDenotation θ AntonymForm.negative = Set.Iic θ

Built from

Used by AntonymForm.decidableMemContradictoryDenotation, AntonymForm.contradictoryDenotation_synonymy, AntonymForm.contradictoryDenotation_notPositive, AntonymForm.isCompl_contradictoryDenotation

Used in Krifka2007b

The strengthened denotation of a form on a threshold pair, whose gap lifts not unhappy away from happy and not happy away from unhappy. This is the effective semantics after strengthening (Krifka 2007b) or the lexical one (Alexandropoulou & Gotzner 2024a).

def AntonymForm.strengthenedDenotation L185–192

{D : Type u_1} [Preorder D] (tp : ThresholdPair D) :

AntonymForm → Set D

AntonymForm.strengthenedDenotation tp AntonymForm.positive = Set.Ioi tp.pos
AntonymForm.strengthenedDenotation tp AntonymForm.notPositive = Set.Iic tp.pos
AntonymForm.strengthenedDenotation tp AntonymForm.negative = Set.Iio tp.neg
AntonymForm.strengthenedDenotation tp AntonymForm.notNegative = Set.Ici tp.neg

Built from ,

Used by AntonymForm.decidableMemStrengthenedDenotation, AntonymForm.strengthenedDenotation_notNegative_diff_positive, AntonymForm.strengthenedDenotation_notPositive_diff_negative, AntonymForm.isContrary_strengthenedDenotation

Used in AlexandropoulouGotzner2024a, AlexandropoulouGotzner2024b

L196–199

L201–206

L208–211

Contradictory negation is the complement of the positive form, so double negation eliminates and not unhappy is happy, the puzzle Krifka solves pragmatically.

theorem AntonymForm.contradictoryDenotation_notPositive L213–217

{D : Type u_1} [LinearOrder D] (θ : D) :

contradictoryDenotation θ notPositive = (contradictoryDenotation θ positive)ᶜ

Built from

What not unhappy adds to happy under the strengthened denotation is the gap.

theorem AntonymForm.strengthenedDenotation_notNegative_diff_positive L219–223

{D : Type u_1} [LinearOrder D] (tp : ThresholdPair D) :

strengthenedDenotation tp notNegative \ strengthenedDenotation tp positive = tp.gap

Built from , ,

What not happy adds to unhappy under the strengthened denotation is the gap too.

theorem AntonymForm.strengthenedDenotation_notPositive_diff_negative L225–229

{D : Type u_1} [LinearOrder D] (tp : ThresholdPair D) :

strengthenedDenotation tp notPositive \ strengthenedDenotation tp negative = tp.gap

Built from , ,

With one threshold the negative form is the complement of the positive form, so the pair is contradictory.

theorem AntonymForm.isCompl_contradictoryDenotation L231–235

{D : Type u_1} [LinearOrder D] (θ : D) :

IsCompl (contradictoryDenotation θ positive) (contradictoryDenotation θ negative)

Built from

With a pair that leaves a gap the positive and negative forms are disjoint but not exhaustive, so the pair is contrary.

theorem AntonymForm.isContrary_strengthenedDenotation L238–246

{D : Type u_1} [LinearOrder D] (tp : ThresholdPair D) (h : tp.neg ≤ tp.pos) :

Aristotelian.IsContrary (strengthenedDenotation tp positive) (strengthenedDenotation tp negative)

Built from ,