Krifka (2007): Negated Antonyms: Creating and Filling the Gap

This file formalizes [krifka-2007b]'s account of antonym quadruplets such as happy, not happy, unhappy, not unhappy, and in particular of the double negative, which reports a mild state of happiness rather than the middle ground between happiness and unhappiness that the received contrary analysis of antonyms ([Hor89]) predicts. The paper's three hypotheses: the border between an antonym pair is sharp but its location is not fixed, the epistemic view of vagueness of [williamson-1994]; the pair exhausts its scale, so happy and unhappy are literally contradictories; and the M principle ([Hor84], [Lev00]), on which the more complex of two equivalent expressions is reserved for the non-stereotypical cases. Speakers use the simple forms only where every admissible border agrees (Safe), which opens the gap, and the complex forms where the simple form is literally true at the speaker's border but not safely usable (Marked), which fills it: not happy below the border and not unhappy above it, with no fixed border between the two (lt_of_marked, marked_both). The M principle is derived within bidirectional optimality theory ([blutner-2000]) on the two-form, two-interpretation example of [mccawley-1978], and the same evaluation over the quadruplet's forms and regions yields Krifka's assignment (krifkaQuadruplet).

Implementation notes

• Literal meanings are the substrate's single-threshold AntonymForm.contradictoryDenot; the admissible borders form a finite set of thresholds, and the paper's diagrams are read relative to a speaker's border within that set.
• Bidirectional evaluation is the substrate's superoptimal, the weak optimality of (14). The quadruplet game is built from the literal semantics (a form and a region on the same side of the border), form complexity (AntonymForm.complexity) and the markedness of the border regions.
• The other uses of double negatives the paper sets aside (denial, irony, amplification) and the local strengthening of neither happy nor unhappy are not formalized.

References

• [krifka-2007b]
• [Hor89], [Hor84] — the contrary analysis and the division of pragmatic labor
• [williamson-1994] — the epistemic theory of vagueness
• [Lev00] — the M principle
• [blutner-2000] — weak bidirectional optimality
• [mccawley-1978] — kill and cause to die

Safe and marked uses

def Krifka2007b.simple : Degree.AntonymForm → Degree.AntonymForm

The simpler form with the same literal meaning: happy for not unhappy and unhappy for not happy.

Equations

• Krifka2007b.simple Degree.AntonymForm.notNegative = Degree.AntonymForm.positive
• Krifka2007b.simple Degree.AntonymForm.notPositive = Degree.AntonymForm.negative
• Krifka2007b.simple x✝ = x✝

@[reducible, inline]

abbrev Krifka2007b.literal {max : ℕ} (θ : Degree.Threshold max) (f : Degree.AntonymForm) (d : Degree.Bounded max) : Prop

The literal meaning at a border θ: antonyms are contradictories (16).

Equations

• Krifka2007b.literal θ f d = Degree.AntonymForm.contradictoryDenot θ f d

def Krifka2007b.Safe {max : ℕ} (Θ : Finset (Degree.Threshold max)) (f : Degree.AntonymForm) (d : Degree.Bounded max) : Prop

A safe use (18): true under every admissible border, so that speaker and addressee agree on it whichever border they set.

Equations

• Krifka2007b.Safe Θ f d = ∀ θ ∈ Θ, Krifka2007b.literal θ f d

def Krifka2007b.Marked {max : ℕ} (Θ : Finset (Degree.Threshold max)) (θ : Degree.Threshold max) (f : Degree.AntonymForm) (d : Degree.Bounded max) : Prop

A marked use of a complex form ((19), (20)): literally true at the speaker's border, where the simpler form with the same literal meaning is not safe.

Equations

• Krifka2007b.Marked Θ θ f d = (Krifka2007b.literal θ f d ∧ ¬Krifka2007b.Safe Θ (Krifka2007b.simple f) d)

theorem Krifka2007b.literal_positive_or_negative {max : ℕ} (θ : Degree.Threshold max) (d : Degree.Bounded max) : literal θ Degree.AntonymForm.positive d ∨ literal θ Degree.AntonymForm.negative d

The literal meanings exhaust the scale: neither happy nor unhappy (21) is a contradiction, and an unconditional over the pair (22) covers everyone.

theorem Krifka2007b.not_safe_of_between {max : ℕ} {Θ : Finset (Degree.Threshold max)} {θ₁ θ₂ : Degree.Threshold max} {d : Degree.Bounded max} (h₂ : θ₂ ∈ Θ) (h₁ : θ₁ ∈ Θ) (hd : { value := θ₁.value.castSucc } < d) (hd' : d ≤ { value := θ₂.value.castSucc }) : ¬Safe Θ Degree.AntonymForm.positive d ∧ ¬Safe Θ Degree.AntonymForm.negative d

Two admissible borders open a gap: a degree between them is safely neither happy nor unhappy, which is how neither happy nor unhappy comes to be sayable.

theorem Krifka2007b.marked_notNegative_iff {max : ℕ} {Θ : Finset (Degree.Threshold max)} {θ : Degree.Threshold max} {d : Degree.Bounded max} : Marked Θ θ Degree.AntonymForm.notNegative d ↔ { value := θ.value.castSucc } < d ∧ ∃ θ' ∈ Θ, d ≤ { value := θ'.value.castSucc }

A marked not unhappy is a mild state of happiness ((3), (19)): happy at the speaker's border, but not safely so.

theorem Krifka2007b.marked_notPositive_iff {max : ℕ} {Θ : Finset (Degree.Threshold max)} {θ : Degree.Threshold max} {d : Degree.Bounded max} : Marked Θ θ Degree.AntonymForm.notPositive d ↔ d ≤ { value := θ.value.castSucc } ∧ ∃ θ' ∈ Θ, { value := θ'.value.castSucc } < d

A marked not happy is a mild state of unhappiness ((9), (20)): unhappy at the speaker's border, but not safely so.

theorem Krifka2007b.lt_of_marked {max : ℕ} {Θ : Finset (Degree.Threshold max)} {θ : Degree.Threshold max} {d₁ d₂ : Degree.Bounded max} (h₁ : Marked Θ θ Degree.AntonymForm.notPositive d₁) (h₂ : Marked Θ θ Degree.AntonymForm.notNegative d₂) : d₁ < d₂

At a given border, not unhappy reports higher states than not happy (20).

theorem Krifka2007b.marked_both {max : ℕ} {Θ : Finset (Degree.Threshold max)} {θ₁ θ₂ : Degree.Threshold max} (h₁ : θ₁ ∈ Θ) (h₂ : θ₂ ∈ Θ) (hlt : { value := θ₁.value.castSucc } < { value := θ₂.value.castSucc }) : Marked Θ θ₁ Degree.AntonymForm.notNegative { value := θ₂.value.castSucc } ∧ Marked Θ θ₂ Degree.AntonymForm.notPositive { value := θ₂.value.castSucc }

Between two admissible borders a degree is not unhappy for a speaker with the lower border and not happy for one with the higher: the two expressions are not exhaustive and have no fixed border between them (20).

The M principle in bidirectional optimality theory

inductive Krifka2007b.Form : Type

The two forms of (13).

• killed : Form
• causedToDie : Form

@[instance_reducible]

instance Krifka2007b.instDecidableEqForm : DecidableEq Form

Equations

• Krifka2007b.instDecidableEqForm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Krifka2007b.instReprForm.repr : Form → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Krifka2007b.instReprForm.repr Krifka2007b.Form.killed prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka2007b.Form.killed")).group prec✝

@[instance_reducible]

instance Krifka2007b.instReprForm : Repr Form

Equations

• Krifka2007b.instReprForm = { reprPrec := Krifka2007b.instReprForm.repr }

inductive Krifka2007b.Interp : Type

The two interpretations of (13).

• direct : Interp
• indirect : Interp

@[instance_reducible]

instance Krifka2007b.instDecidableEqInterp : DecidableEq Interp

Equations

• Krifka2007b.instDecidableEqInterp x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Krifka2007b.instReprInterp.repr : Interp → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Krifka2007b.instReprInterp.repr Krifka2007b.Interp.direct prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka2007b.Interp.direct")).group prec✝

@[instance_reducible]

instance Krifka2007b.instReprInterp : Repr Interp

Equations

• Krifka2007b.instReprInterp = { reprPrec := Krifka2007b.instReprInterp.repr }

def Krifka2007b.mccawleyPairs : Finset (Form × Interp)

The four form-interpretation pairs of (13).

Equations

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

def Krifka2007b.formCost : Form × Interp → ℕ

The preference for the simpler form.

Equations

• Krifka2007b.formCost (Krifka2007b.Form.killed, snd) = 0
• Krifka2007b.formCost (Krifka2007b.Form.causedToDie, snd) = 1

def Krifka2007b.interpCost : Form × Interp → ℕ

The preference for the stereotypical interpretation.

Equations

• Krifka2007b.interpCost (fst, Krifka2007b.Interp.direct) = 0
• Krifka2007b.interpCost (fst, Krifka2007b.Interp.indirect) = 1

theorem Krifka2007b.superoptimal_mccawley : Pragmatics.Bidirectional.superoptimal mccawleyPairs (Pragmatics.Bidirectional.profile [formCost, interpCost]) = {(Form.killed, Interp.direct), (Form.causedToDie, Interp.indirect)}

Weak optimality ((14), (15)): kill pairs with direct killing and cause to die with indirect killing, the M principle.

inductive Krifka2007b.Region : Type

The regions of the scale after strengthening ((18)–(20)): safely happy, mildly happy, mildly unhappy, safely unhappy.

• positive : Region
• plateauHigh : Region
• plateauLow : Region
• negative : Region

@[instance_reducible]

instance Krifka2007b.instDecidableEqRegion : DecidableEq Region

Equations

• Krifka2007b.instDecidableEqRegion x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Krifka2007b.instReprRegion : Repr Region

Equations

• Krifka2007b.instReprRegion = { reprPrec := Krifka2007b.instReprRegion.repr }

def Krifka2007b.instReprRegion.repr : Region → ℕ → Std.Format

Equations

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

def Krifka2007b.Region.flip : Region → Region

Mirror image of a region under the polarity flip.

Equations

• Krifka2007b.Region.positive.flip = Krifka2007b.Region.negative
• Krifka2007b.Region.negative.flip = Krifka2007b.Region.positive
• Krifka2007b.Region.plateauHigh.flip = Krifka2007b.Region.plateauLow
• Krifka2007b.Region.plateauLow.flip = Krifka2007b.Region.plateauHigh

@[simp]

theorem Krifka2007b.Region.flip_flip (r : Region) : r.flip.flip = r

def Krifka2007b.Region.above : Region → Bool

The regions above the border.

Equations

• Krifka2007b.Region.positive.above = true
• Krifka2007b.Region.plateauHigh.above = true
• Krifka2007b.Region.plateauLow.above = false
• Krifka2007b.Region.negative.above = false

def Krifka2007b.Region.markedness : Region → ℕ

The border regions are the non-stereotypical interpretations.

Equations

• Krifka2007b.Region.plateauHigh.markedness = 1
• Krifka2007b.Region.plateauLow.markedness = 1
• Krifka2007b.Region.positive.markedness = 0
• Krifka2007b.Region.negative.markedness = 0

def Krifka2007b.formAbove : Degree.AntonymForm → Bool

The forms literally true above the border (16).

Equations

• Krifka2007b.formAbove Degree.AntonymForm.positive = true
• Krifka2007b.formAbove Degree.AntonymForm.notNegative = true
• Krifka2007b.formAbove Degree.AntonymForm.notPositive = false
• Krifka2007b.formAbove Degree.AntonymForm.negative = false

def Krifka2007b.quadrupletPairs : Finset (Degree.AntonymForm × Region)

The pairs the literal semantics admits: a form and a region on the same side of the border.

Equations

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

def Krifka2007b.krifkaQuadruplet : Finset (Degree.AntonymForm × Region)

Krifka's assignment: the simple forms take the safe regions, the complex forms the border regions on their side.

Equations

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

theorem Krifka2007b.superoptimal_quadruplet : Pragmatics.Bidirectional.superoptimal quadrupletPairs (Pragmatics.Bidirectional.profile [fun (x : Degree.AntonymForm × Region) => x.2.markedness, fun (x : Degree.AntonymForm × Region) => x.1.complexity]) = krifkaQuadruplet ∧ Pragmatics.Bidirectional.superoptimal quadrupletPairs (Pragmatics.Bidirectional.profile [fun (x : Degree.AntonymForm × Region) => x.1.complexity, fun (x : Degree.AntonymForm × Region) => x.2.markedness]) = krifkaQuadruplet

Weak optimality over the quadruplet, with markedness and form complexity in either order, yields Krifka's assignment.