Antonymy: Contradictory vs. Contrary Negation

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

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.

@cite{krifka-2007b} 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 Phenomena/Negation/Studies/Krifka2007.lean.

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

theorem Semantics.Lexical.Adjective.Antonymy.contradictory_is_complement {max : ℕ} (d : Core.Scale.Degree max) (θ : Core.Scale.Threshold max) : contradictoryNeg d θ = !Degree.positiveMeaning d θ

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

theorem Semantics.Lexical.Adjective.Antonymy.contradictory_dne {max : ℕ} (d : Core.Scale.Degree max) (θ : Core.Scale.Threshold max) : (!decide (contradictoryNeg d θ = Degree.positiveMeaning d θ)) = true

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

@cite{krifka-2007b}: this is the LITERAL semantics. If antonyms are contradictory, then "not unhappy" and "happy" are synonymous — the puzzle that motivates pragmatic strengthening.

theorem Semantics.Lexical.Adjective.Antonymy.contradictory_exhaustive {max : ℕ} (d : Core.Scale.Degree max) (θ : Core.Scale.Threshold max) : Degree.positiveMeaning d θ = true ∨ contradictoryNeg d θ = true

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

theorem Semantics.Lexical.Adjective.Antonymy.gap_eq_not_neg_and_not_pos {max : ℕ} (d : Core.Scale.Degree 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.

theorem Semantics.Lexical.Adjective.Antonymy.contrary_gap_exists {max : ℕ} (tp : ThresholdPair max) (h : { value := tp.neg.value.castSucc } < { value := tp.pos.value.castSucc }) : ∃ (d : Core.Scale.Degree max), notContraryNegMeaning d tp = true ∧ positiveMeaning' d tp = false

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

theorem Semantics.Lexical.Adjective.Antonymy.gap_nonempty {max : ℕ} (tp : ThresholdPair max) (h : { value := tp.neg.value.castSucc } < { value := tp.pos.value.castSucc }) : ∃ (d : Core.Scale.Degree max), inGapRegion d tp = true

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