@cite{alexandropoulou-gotzner-2024-jos} — The Interpretation of Relative and Absolute Adjectives Under Negation

@cite{alexandropoulou-gotzner-2024-jos}

In: Journal of Semantics 41(3), pp. 373–399.

Thesis

@cite{alexandropoulou-gotzner-2024-jos} (JoS) tests the @cite{horn-1989} R- implicature account vs. @cite{krifka-2007b}'s complexity-based account of negative strengthening across three distinct cases of negated antonymic adjectives:

1. Weak relative (e.g. not large vs. not small): both Horn and Krifka predict negative strengthening — asymmetric interpretation.
2. Weak absolute (e.g. not clean vs. not dirty): both predict symmetric interpretation, since contradictory antonyms partition the scale exhaustively (no gap for an implicature to exploit).
3. Strong gradable (e.g. not gigantic vs. not tiny, not pristine vs. not filthy): Horn predicts asymmetric strengthening (since strong adjectives are contrary, with a gap). The JoS experimental findings on strong adjectives are presented as prima facie challenges to Horn's account, while not endorsing any specific alternative. Per JoS footnote 2, Krifka's account is explicitly restricted to informationally weak adjectives and does not commit to a prediction for the strong case.

Companion paper

The Glossa companion @cite{alexandropoulou-gotzner-2024} formalised in AlexandropoulouGotzner2024.lean extends this work by isolating the role of overt contextual competition in surfacing the asymmetric pattern. The Glossa paper builds on the JoS findings as established results.

Substrate consumed

• Theories/Semantics/Gradability/Theory.lean — ThresholdPair, positiveMeaning', contraryNegMeaning, notContraryNegMeaning.
• Theories/Semantics/Gradability/AntonymQuadruplet.lean — AntonymForm (the four-form quadruplet enum, theory-neutral substrate).
• Theories/Semantics/Gradability/AntonymPrediction.lean — AntonymForm.contradictoryDenot, AntonymForm.strengthenedDenot, predictionForAntonymy, predictionForEntry, anchor theorems.
• Theories/Semantics/Degree/Basic.lean — antonymMeaning.
• Features/Antonymy.lean — NegationType, Asymmetry.
• Fragments/English/Predicates/Adjectival.lean — lexical entries (transitively, via the Glossa companion file).

What this file makes Lean-checkable

• A typed three-case taxonomy (AGCase).
• Horn 1989's predicted asymmetry direction per cell as a total function AGCase → Asymmetry.
• Krifka 2007's predicted asymmetry direction per cell as AGCase → Option Asymmetry, with none for strongGradable reflecting the paper-faithful commitment that Krifka does not extend to strong adjectives.
• The JoS empirical observations as a third such function.
• A theorem witnessing that Horn's prediction differs from the JoS observation on the strongGradable cell — the paper's headline negative result, made Lean-checkable.
• The Krifka 2007 hidden-agreement bridge: A&G's lexical commitment to contrary semantics for "not positive" coincides definitionally with the output of Krifka's pragmatic strengthening procedure on the same input.

What this file does not formalise

The full Horn 1989 R-implicature derivation, the full Krifka 2007 complexity calculus, the experimental rating distributions, the participant population metadata, or the statistical analysis. The prediction signatures are simple total functions encoding the qualitative direction each theory predicts; the strength of the falsification claim rides on whether those direction encodings match the prose of each cited paper, not on a Lean-internal derivation of the predictions from first principles.

inductive AlexandropoulouGotzner2024JoS.AGCase : Type

The JoS paper's three distinct cases of negated antonymic adjectives.

• weakRelative : AGCase
• weakAbsolute : AGCase
• strongGradable : AGCase

@[implicit_reducible]

instance AlexandropoulouGotzner2024JoS.instReprAGCase : Repr AGCase

Equations

• AlexandropoulouGotzner2024JoS.instReprAGCase = { reprPrec := AlexandropoulouGotzner2024JoS.instReprAGCase.repr }

def AlexandropoulouGotzner2024JoS.instReprAGCase.repr : AGCase → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance AlexandropoulouGotzner2024JoS.instDecidableEqAGCase : DecidableEq AGCase

Equations

• AlexandropoulouGotzner2024JoS.instDecidableEqAGCase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

Asymmetry (asymmetric/symmetric direction enum), predictionForAntonymy (NegationType → Asymmetry skeleton), and predictionForEntry (GradableAdjEntry → Asymmetry projection) are now substrate, in Features/Antonymy.lean and Theories/Semantics/Gradability/AntonymPrediction.lean respectively. The substrate-anchor theorems Semantics.Gradability.contradictoryDenot_synonymy and Semantics.Gradability.strengthenedDenot_breaks_synonymy make the .contrary → .asymmetric / .contradictory → .symmetric mapping Lean-checkable from the canonical denotations.

def AlexandropoulouGotzner2024JoS.AGCase.representative : AGCase → Semantics.Gradability.GradableAdjEntry

Each AGCase is represented by a canonical Fragment lexical entry. The prediction signatures below derive their per-case answers by reading antonymRelation off this representative — the Fragment is the single source of truth, not a parallel hardcoded enum in this file.

Equations

• AlexandropoulouGotzner2024JoS.AGCase.weakRelative.representative = Fragments.English.Predicates.Adjectival.large
• AlexandropoulouGotzner2024JoS.AGCase.weakAbsolute.representative = Fragments.English.Predicates.Adjectival.clean
• AlexandropoulouGotzner2024JoS.AGCase.strongGradable.representative = Fragments.English.Predicates.Adjectival.gigantic

def AlexandropoulouGotzner2024JoS.hornPrediction (c : AGCase) : Features.Asymmetry

Horn 1989's R-implicature account predicts asymmetric interpretation whenever an extension gap is available between the contrary antonyms, and symmetric interpretation when the antonyms are contradictory. The per-case answer is derived by reading off the representative Fragment entry's antonymRelation via predictionForEntry. Total over all three cases (Horn extends to strong adjectives).

Equations

• AlexandropoulouGotzner2024JoS.hornPrediction c = Semantics.Gradability.predictionForEntry c.representative

def AlexandropoulouGotzner2024JoS.krifkaPrediction : AGCase → Option Features.Asymmetry

Krifka 2007's complexity-based account predicts via the same antonymy skeleton as Horn for the weak cases — derived from the Fragment via predictionForEntry — but is silent on the strong-gradable case (per JoS footnote 2: Krifka focuses on informationally weak adjectives only and does not extend his account explicitly to strong gradable adjectives). The strong-case none is the paper-faithful encoding of that scope restriction.

Equations

• AlexandropoulouGotzner2024JoS.krifkaPrediction AlexandropoulouGotzner2024JoS.AGCase.strongGradable = none
• AlexandropoulouGotzner2024JoS.krifkaPrediction x✝ = some (Semantics.Gradability.predictionForEntry x✝.representative)

def AlexandropoulouGotzner2024JoS.agObserved : AGCase → Features.Asymmetry

The JoS paper's reported experimental findings, abstracting from response-distribution detail to the qualitative asymmetry direction. The strong-gradable cell encodes the paper's headline negative result: the observed pattern does NOT match Horn's predicted asymmetric behavior.

Equations

• AlexandropoulouGotzner2024JoS.agObserved AlexandropoulouGotzner2024JoS.AGCase.weakRelative = Features.Asymmetry.asymmetric
• AlexandropoulouGotzner2024JoS.agObserved AlexandropoulouGotzner2024JoS.AGCase.weakAbsolute = Features.Asymmetry.symmetric
• AlexandropoulouGotzner2024JoS.agObserved AlexandropoulouGotzner2024JoS.AGCase.strongGradable = Features.Asymmetry.symmetric

theorem AlexandropoulouGotzner2024JoS.hornPrediction_ne_observed_on_strong : hornPrediction AGCase.strongGradable ≠ agObserved AGCase.strongGradable

The JoS paper's headline negative result: Horn 1989's account predicts asymmetric interpretation for negated strong gradable adjectives, but the empirical observations are not asymmetric in the predicted way.

Theorem-as-stated form (mathlib idiom: name describes the proved proposition): hornPrediction .strongGradable ≠ agObserved .strongGradable. Reading: the JoS paper's "prima facie present challenges for Horn's (1989) analysis" claim about strong antonymic adjectives.

theorem AlexandropoulouGotzner2024JoS.horn_agrees_on_weak_cases : hornPrediction AGCase.weakRelative = agObserved AGCase.weakRelative ∧ hornPrediction AGCase.weakAbsolute = agObserved AGCase.weakAbsolute

Horn and the JoS observations agree on the weak relative and weak absolute cases. The disagreement is localised to the strong-gradable cell.

theorem AlexandropoulouGotzner2024JoS.krifka_silent_on_strong_gradable : krifkaPrediction AGCase.strongGradable = none

Krifka's account is silent on the strong-gradable case (per JoS fn 2). There is therefore no Krifka prediction to falsify on this cell — the silence itself is the position the paper attributes to Krifka.

theorem AlexandropoulouGotzner2024JoS.krifka_agrees_with_horn_where_committed : krifkaPrediction AGCase.weakRelative = some (hornPrediction AGCase.weakRelative) ∧ krifkaPrediction AGCase.weakAbsolute = some (hornPrediction AGCase.weakAbsolute)

On the cells where Krifka does commit, his prediction matches Horn's (and matches the JoS observations). The two theories diverge only in whether they extend to the strong case, not in what they predict on the cells where they both speak.

Both A&G and Krifka 2007 use the same ThresholdPair substrate for the effective (post-strengthening) semantics of negated contrary antonyms. A&G commit to this two-threshold structure as a lexical fact; Krifka derives it pragmatically from a contradictory base via the M-principle.

The two views are empirically indistinguishable at the level of their
composed output: A&G's `antonymMeaning d tp.pos` (the literal denotation
of "not positive" projected through the positive threshold) **is**
`AntonymForm.strengthenedDenot tp .notPositive d` definitionally.

The `Iff.rfl` proofs below are **intentional** and load-bearing: their
fragility under substrate change *is* the point. If `contradictoryNeg`
ever stops being a `def`-equal alias for `antonymMeaning` (e.g. through
a regression of the Bool→Prop substrate evolution in
`Theories/Semantics/Gradability/Theory.lean`), these theorems will
break loudly — surfacing the substrate drift at the cross-paper bridge
rather than letting it propagate silently. 

theorem AlexandropoulouGotzner2024JoS.ag_negative_strengthening_eq_krifka {max : ℕ} (d : Core.Scale.Degree max) (tp : Semantics.Gradability.ThresholdPair max) : Semantics.Degree.antonymMeaning d tp.pos ↔ Semantics.Gradability.AntonymForm.strengthenedDenot tp Semantics.Gradability.AntonymForm.notPositive d

The bridge theorem. A&G's lexical "not positive" semantics coincides with the output of Krifka 2007's pragmatic strengthening procedure on the notPositive form. Both sides reduce to d ≤ tp.pos definitionally after the substrate's def-to-abbrev migration on Theory.lean::contradictoryNeg.

theorem AlexandropoulouGotzner2024JoS.ag_quadruplet_eq_krifka_strengthened {max : ℕ} (d : Core.Scale.Degree max) (tp : Semantics.Gradability.ThresholdPair max) : (Semantics.Gradability.positiveMeaning' d tp ↔ Semantics.Gradability.AntonymForm.strengthenedDenot tp Semantics.Gradability.AntonymForm.positive d) ∧ (Semantics.Degree.antonymMeaning d tp.pos ↔ Semantics.Gradability.AntonymForm.strengthenedDenot tp Semantics.Gradability.AntonymForm.notPositive d) ∧ (Semantics.Gradability.contraryNegMeaning d tp ↔ Semantics.Gradability.AntonymForm.strengthenedDenot tp Semantics.Gradability.AntonymForm.negative d) ∧ (Semantics.Gradability.notContraryNegMeaning d tp ↔ Semantics.Gradability.AntonymForm.strengthenedDenot tp Semantics.Gradability.AntonymForm.notNegative d)

The bridge generalises to the full quadruplet structure: A&G's lexical semantics for each of the four forms (positive / not-positive / negative / not-negative) coincides with Krifka 2007's strengthenedQuad output on the corresponding form.