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/Basic.lean.

@[simp]

theorem Semantics.Gradability.Antonymy.contradictory_is_complement {max : ℕ} (d : Degree.Degree max) (θ : Degree.Threshold max) : contradictoryNeg d θ ↔ ¬Degree.positiveMeaning d θ

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

theorem Semantics.Gradability.Antonymy.contradictory_dne {max : ℕ} (d : Degree.Degree max) (θ : Degree.Threshold max) : ¬contradictoryNeg d θ ↔ Degree.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.

theorem Semantics.Gradability.Antonymy.contradictory_exhaustive {max : ℕ} (d : Degree.Degree max) (θ : Degree.Threshold max) : Degree.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.

@[simp]

theorem Semantics.Gradability.Antonymy.gap_iff_not_neg_and_not_pos {max : ℕ} (d : Degree.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.Gradability.Antonymy.contrary_gap_exists {max : ℕ} (tp : ThresholdPair max) (h : { value := tp.neg.value.castSucc } < { value := tp.pos.value.castSucc }) : ∃ (d : Degree.Degree 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).

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

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