Antonymy — Contradictory vs Contrary Distinction #

The classical lexical-semantic distinction between two kinds of opposite pairs:

Contradictories (e.g., clean / dirty) — cannot both be true and cannot both be false. Negation of one entails the other: not clean ⟹ dirty. No extension gap between the two standards.

Contraries (e.g., tall / short, large / small) — cannot both be true but can both be false. Negation of one does NOT entail the other: not large ⊭ small. Extension gap between the two standards.

Note: The type is named NegationType for backward compatibility with existing call sites; the linguistically accurate name is antonymy type. The file is named Antonymy.lean to signal the right concept.

source

inductive Features.NegationType :

Type

Antonymy type: contradictory (no gap) vs contrary (gap).

See Antonymy.lean module docstring for the diagnostics. Used in gradable-adjective semantics to distinguish licensing patterns of the two-threshold model.

Antonymy is genuinely binary (an antonym pair is either contradictory or contrary — never subcontrary or unconnected), so this stays a 2-case type; NegationType.toOpposition embeds it as the {contradictory, contrary} slice of the substrate's Aristotelian.OppositionRel, and AntonymPrediction's isContradictory_*Denot ground the tag in the real opposition between the adjective denotations.

contradictory : NegationType
contrary : NegationType

Instances For

source

@[implicit_reducible]

instance Features.instReprNegationType :

Repr NegationType

Equations

Features.instReprNegationType = { reprPrec := Features.instReprNegationType.repr }

source

def Features.instReprNegationType.repr :

NegationType → ℕ → Std.Format

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[implicit_reducible]

instance Features.instDecidableEqNegationType :

DecidableEq NegationType

Equations

Features.instDecidableEqNegationType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

@[implicit_reducible]

instance Features.instFintypeNegationType :

Fintype NegationType

Equations

Features.instFintypeNegationType = { elems := { val := ↑Features.NegationType.enumList, nodup := Features.NegationType.enumList_nodup }, complete := Features.instFintypeNegationType._proof_1 }

source

def Features.NegationType.toOpposition :

NegationType → Aristotelian.OppositionRel

Embed the antonymy type into the substrate's opposition relation: an antonym pair occupies exactly the contradictory or contrary cell of OppositionRel.

Equations

Instances For

source

@[implicit_reducible]

instance Features.instCoeNegationTypeOppositionRel :

Coe NegationType Aristotelian.OppositionRel

Equations

Features.instCoeNegationTypeOppositionRel = { coe := Features.NegationType.toOpposition }

source

theorem Features.NegationType.toOpposition_injective :

Function.Injective toOpposition

source

theorem Features.NegationType.range_toOpposition (r : Aristotelian.OppositionRel) :

(∃ (n : NegationType), n.toOpposition = r) ↔ r = Aristotelian.OppositionRel.contradictory ∨ r = Aristotelian.OppositionRel.contrary

The image of toOpposition is exactly the two antonym cells of OppositionRel.

source

inductive Features.Asymmetry :

Type

Predicted behaviour of an antonymic adjective pair under sentential negation: do positive and negative forms diverge under polarity (asymmetric — gap-licensed strengthening) or behave in parallel (symmetric — no gap available)?

Used as the codomain of prediction signatures in studies of negated antonymic adjectives (Horn 1989, Krifka 2007, Tessler & Franke 2019, Alexandropoulou & Gotzner 2024). Anchored in Semantics/Gradability/AntonymPrediction.lean's predictionForAntonymy map and its substrate witness theorems.