This file captures the empirical patterns around flexible negation, where:

• "not unhappy" ≠ "happy" (there's a gap region)
• "unhappy" is NOT the logical negation of "happy"
• Morphological negation (un-) and syntactic negation (not) can be either contradictory or contrary

Key Distinction

@cite{cruse-1986} @cite{horn-1989}

Contradictory negation: P and ¬P partition the space

• "not happy" (contradictory) = x ≤ θ (complement of x > θ)
• Every point is either happy or not-happy

Contrary negation: P and Q can both be false (gap region)

• "happy" = x > θ_pos, "unhappy" = x < θ_neg where θ_neg < θ_pos
• Gap region: θ_neg ≤ x ≤ θ_pos (neither happy nor unhappy)

inductive Phenomena.Negation.FlexibleNegation.NegationMarker : Type

Negation markers in English and their flexibility.

The key insight: both morphological (un-) and syntactic (not) negation can receive either contradictory OR contrary interpretations. The interpretation is pragmatically determined.

Source: @cite{tessler-franke-2019}

• syntactic : NegationMarker

  Syntactic negation: "not happy"

• morphological : NegationMarker

  Morphological negation: "unhappy"

def Phenomena.Negation.FlexibleNegation.instReprNegationMarker.repr : NegationMarker → ℕ → Std.Format

Equations

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

instance Phenomena.Negation.FlexibleNegation.instReprNegationMarker : Repr NegationMarker

Equations

• Phenomena.Negation.FlexibleNegation.instReprNegationMarker = { reprPrec := Phenomena.Negation.FlexibleNegation.instReprNegationMarker.repr }

instance Phenomena.Negation.FlexibleNegation.instDecidableEqNegationMarker : DecidableEq NegationMarker

Equations

• Phenomena.Negation.FlexibleNegation.instDecidableEqNegationMarker x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Negation.FlexibleNegation.instBEqNegationMarker.beq : NegationMarker → NegationMarker → Bool

Equations

• Phenomena.Negation.FlexibleNegation.instBEqNegationMarker.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Negation.FlexibleNegation.instBEqNegationMarker : BEq NegationMarker

Equations

• Phenomena.Negation.FlexibleNegation.instBEqNegationMarker = { beq := Phenomena.Negation.FlexibleNegation.instBEqNegationMarker.beq }

structure Phenomena.Negation.FlexibleNegation.FlexibleNegationDatum : Type

A judgment about the interpretation of a negated form.

Captures the empirical observation that negated forms can be interpreted as contradictory or contrary, with varying strength.

Source: @cite{tessler-franke-2019} experiments

• adjective : String

  The base (positive) adjective

• negatedForm : String

  The negated form being judged

• marker : NegationMarker

  Which negation marker is used

• expectedInterpretation : Core.NegationType

  Expected primary interpretation

• strength : ℚ

  Strength of preference (0-1 scale)

• notes : String

  Notes on the judgment

instance Phenomena.Negation.FlexibleNegation.instReprFlexibleNegationDatum : Repr FlexibleNegationDatum

Equations

• Phenomena.Negation.FlexibleNegation.instReprFlexibleNegationDatum = { reprPrec := Phenomena.Negation.FlexibleNegation.instReprFlexibleNegationDatum.repr }

def Phenomena.Negation.FlexibleNegation.instReprFlexibleNegationDatum.repr : FlexibleNegationDatum → ℕ → Std.Format

Equations

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

def Phenomena.Negation.FlexibleNegation.unhappy_contrary : FlexibleNegationDatum

"unhappy" strongly prefers contrary interpretation.

Intuition: "unhappy" means positively unhappy (below a low threshold), not just "not happy" (anything at or below the happy threshold).

Source: @cite{tessler-franke-2019} Experiment 1

Equations

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

def Phenomena.Negation.FlexibleNegation.not_happy_ambiguous : FlexibleNegationDatum

"not happy" is ambiguous between contradictory and contrary.

Intuition: "not happy" can mean either:

• Contradictory: anything at or below the happy threshold
• Contrary: positively unhappy (like "unhappy")

The costly form (2 words) licenses the marked (contradictory) reading.

Source: @cite{tessler-franke-2019} Experiment 1

Equations

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

def Phenomena.Negation.FlexibleNegation.not_unhappy_not_happy : FlexibleNegationDatum

"not unhappy" ≠ "happy" - THE KEY EMPIRICAL FACT.

This is the central observation that motivates the paper: "not unhappy" does NOT reduce to "happy".

Why? If "unhappy" is contrary (x < θ_neg), then:

• "not unhappy" = x ≥ θ_neg
• "happy" = x > θ_pos where θ_pos > θ_neg
• Gap region: θ_neg ≤ x ≤ θ_pos is "not unhappy" but NOT "happy"

Source: @cite{tessler-franke-2019} Section 1

Equations

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

def Phenomena.Negation.FlexibleNegation.sad_contrary : FlexibleNegationDatum

"sad" as independent contrary antonym.

Note: "sad" is not morphologically derived from "happy" (unlike "unhappy"), but still functions as a contrary antonym with a gap.

Source: @cite{kennedy-mcnally-2005}

Equations

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

def Phenomena.Negation.FlexibleNegation.flexibleNegationExamples : List FlexibleNegationDatum

All flexible negation examples.

Equations

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

structure Phenomena.Negation.FlexibleNegation.DoubleNegationDatum : Type

Data capturing the non-equivalence pattern: "not un-X" ≠ "X".

This is the central empirical claim: double negation doesn't cancel out when the inner negation is contrary.

Source: @cite{tessler-franke-2019}, @cite{horn-1989}

• positive : String

  The positive adjective

• antonym : String

  The morphologically negated form

• doubleNeg : String

  The double negation

• areEquivalent : Bool

  Are they equivalent?

• explanation : String

  Why or why not?

def Phenomena.Negation.FlexibleNegation.instReprDoubleNegationDatum.repr : DoubleNegationDatum → ℕ → Std.Format

Equations

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

instance Phenomena.Negation.FlexibleNegation.instReprDoubleNegationDatum : Repr DoubleNegationDatum

Equations

• Phenomena.Negation.FlexibleNegation.instReprDoubleNegationDatum = { reprPrec := Phenomena.Negation.FlexibleNegation.instReprDoubleNegationDatum.repr }

def Phenomena.Negation.FlexibleNegation.happy_double_neg : DoubleNegationDatum

"not unhappy" ≠ "happy" because of the gap.

Someone in the gap region (neither happy nor unhappy) is:

• "not unhappy" ✓ (they're not below θ_neg)
• "happy" ✗ (they're not above θ_pos)

Source: @cite{tessler-franke-2019}

Equations

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

def Phenomena.Negation.FlexibleNegation.safe_double_neg : DoubleNegationDatum

"not unsafe" ≈ "safe" (closer to equivalent).

For closed-scale adjectives with minimum standard, the gap is smaller or nonexistent, making double negation closer to canceling.

Source: @cite{kennedy-2007}

Equations

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

def Phenomena.Negation.FlexibleNegation.doubleNegationExamples : List DoubleNegationDatum

Equations

• Phenomena.Negation.FlexibleNegation.doubleNegationExamples = [Phenomena.Negation.FlexibleNegation.happy_double_neg, Phenomena.Negation.FlexibleNegation.safe_double_neg]

structure Phenomena.Negation.FlexibleNegation.CostAsymmetryDatum : Type

Cost asymmetry between negation forms.

Shorter/simpler forms are cheaper to produce, creating:

• Unmarked form (cheap) → unmarked meaning (default, most common)
• Marked form (costly) → marked meaning (special, contrastive)

This follows Horn's Division of Pragmatic Labor.

Source: @cite{horn-1984}, @cite{tessler-franke-2019}

• cheapForm : String

  Shorter/cheaper form

• costlyForm : String

  Longer/costlier form

• costDifference : String

  Cost difference (words, morphemes, etc.)

• cheapMeaning : Core.NegationType

  Expected meaning of cheap form

• costlyMeaning : Core.NegationType

  Expected meaning of costly form

def Phenomena.Negation.FlexibleNegation.instReprCostAsymmetryDatum.repr : CostAsymmetryDatum → ℕ → Std.Format

Equations

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

instance Phenomena.Negation.FlexibleNegation.instReprCostAsymmetryDatum : Repr CostAsymmetryDatum

Equations

• Phenomena.Negation.FlexibleNegation.instReprCostAsymmetryDatum = { reprPrec := Phenomena.Negation.FlexibleNegation.instReprCostAsymmetryDatum.repr }

def Phenomena.Negation.FlexibleNegation.unhappy_vs_not_happy : CostAsymmetryDatum

"unhappy" (1 word) vs "not happy" (2 words).

The cheaper "unhappy" gets the default (contrary) reading. The costlier "not happy" is available for the marked (contradictory) reading.

Source: @cite{tessler-franke-2019}

Equations

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

def Phenomena.Negation.FlexibleNegation.costAsymmetryExamples : List CostAsymmetryDatum

Equations

• Phenomena.Negation.FlexibleNegation.costAsymmetryExamples = [Phenomena.Negation.FlexibleNegation.unhappy_vs_not_happy]

structure Phenomena.Negation.FlexibleNegation.TwoThresholdModel : Type

The two-threshold model for contrary antonyms.

For contrary pairs like happy/unhappy, there are TWO thresholds:

• θ_pos: threshold for "happy" (degree > θ_pos)
• θ_neg: threshold for "unhappy" (degree < θ_neg)
• Gap: θ_neg ≤ degree ≤ θ_pos (neither happy nor unhappy)

This is the key semantic insight that explains the non-equivalence.

Source: @cite{tessler-franke-2019}, @cite{kennedy-2007}

• positive : String

  The positive adjective

• negative : String

  The negative adjective

• thresholdRelation : String

  Relation between thresholds

• gapDescription : String

  Description of gap region

• gapExample : String

  Example of gap case

instance Phenomena.Negation.FlexibleNegation.instReprTwoThresholdModel : Repr TwoThresholdModel

Equations

• Phenomena.Negation.FlexibleNegation.instReprTwoThresholdModel = { reprPrec := Phenomena.Negation.FlexibleNegation.instReprTwoThresholdModel.repr }

def Phenomena.Negation.FlexibleNegation.instReprTwoThresholdModel.repr : TwoThresholdModel → ℕ → Std.Format

Equations

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

def Phenomena.Negation.FlexibleNegation.happyUnhappyThresholds : TwoThresholdModel

Happy/Unhappy two-threshold model.

The happiness scale has two thresholds creating three regions:

• Unhappy: degree < θ_neg (clearly unhappy)
• Gap: θ_neg ≤ degree ≤ θ_pos (neither/ambivalent)
• Happy: degree > θ_pos (clearly happy)

Source: @cite{tessler-franke-2019}

Equations

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

def Phenomena.Negation.FlexibleNegation.twoThresholdExamples : List TwoThresholdModel

Equations

• Phenomena.Negation.FlexibleNegation.twoThresholdExamples = [Phenomena.Negation.FlexibleNegation.happyUnhappyThresholds]

structure Phenomena.Negation.FlexibleNegation.FlexibleNegationPrediction : Type

Predictions that a theory of flexible negation should satisfy.

These are the empirical targets for the RSA implementation.

Source: @cite{tessler-franke-2019}

• name : String

  Name of the prediction

• statement : String

  Formal statement

• explanation : String

  Why this matters

instance Phenomena.Negation.FlexibleNegation.instReprFlexibleNegationPrediction : Repr FlexibleNegationPrediction

Equations

• Phenomena.Negation.FlexibleNegation.instReprFlexibleNegationPrediction = { reprPrec := Phenomena.Negation.FlexibleNegation.instReprFlexibleNegationPrediction.repr }

def Phenomena.Negation.FlexibleNegation.instReprFlexibleNegationPrediction.repr : FlexibleNegationPrediction → ℕ → Std.Format

Equations

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

def Phenomena.Negation.FlexibleNegation.prediction_unhappy_contrary : FlexibleNegationPrediction

Equations

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

def Phenomena.Negation.FlexibleNegation.prediction_not_happy_flexible : FlexibleNegationPrediction

Equations

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

def Phenomena.Negation.FlexibleNegation.prediction_double_neg_gap : FlexibleNegationPrediction

Equations

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

def Phenomena.Negation.FlexibleNegation.prediction_cost_effect : FlexibleNegationPrediction

Equations

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

def Phenomena.Negation.FlexibleNegation.predictions : List FlexibleNegationPrediction

Equations

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