Rett (2026): Semantic ambivalence and expletive negation

This file formalizes the paper's account of low expletive negation, negation that targets truth-conditional content without changing it. A scalar construction licenses it when it is fixed-point ambidirectional: the construction relates the informative bound of its argument, and an interval and its complement share that bound. The degrees an individual reaches and the degrees it does not both have the individual's height as their bound, sharesBounds_Iic, so a comparative with a negated standard is the comparative, tallerNeg_iff_taller, whereas a scale with a top gives the complement a second bound and blocks the pattern. The runtime of a negated event is the interval before it, preEvent, whose end before, until and since read as the event's start, before_preEvent_completive_iff; after gains nothing from it and while is not ambidirectional. The negated standard stays downward entailing, so negative polarity items survive. The paper's examples are rows, and en_rows records which constructions attest expletive negation.

Implementation notes

Degrees are a linear order and a degree relative denotes the ray of degrees an individual reaches; maximality relativized to a scale is the least upper bound on the positive scale and the greatest lower bound on the negative one, which is what a negated degree relative carries. Times carry a bottom, the paper's minus infinity, so that the pre-event interval is a closed interval of the substrate. The survey counts of Jin and Koenig, the high expletive negation of exclamations, the manner implicature effects and the negative verbs are discussed in the paper without a proposal formalized here.

References

• J. Rett, Semantic ambivalence and expletive negation (2026)
• J. Rett, Eliminating EARLIEST (2020)
• P. Cépeda, Negation and time: against expletive negation in temporal clauses (2018)
• Y. Jin, J.-P. Koenig, A cross-linguistic study of expletive negation (2021)
• C. Greco, Negative polarity items and expletive negation (2018)
• D. J. Napoli, M. Nespor, Negatives in comparatives (1976)
• C. Kennedy, L. McNally, Scale structure, degree modification, and the semantics of gradable predicates (2005)
• O. Heinämäki, Semantics of English temporal connectives (1974)

Ambivalence

def Rett2026.Ambivalent (p q : Prop) : Prop

Semantic ambivalence (4) is a sentence's ambiguity between two propositions each equivalent to the negation of the other.

Equations

• Rett2026.Ambivalent p q = (p ↔ ¬q)

theorem Rett2026.Ambivalent.symm {p q : Prop} (h : Ambivalent p q) : Ambivalent q p

Ambivalence is symmetric.

Degrees

def Rett2026.informativeBounds {D : Type u_2} [LinearOrder D] (X : Set D) : Set D

The informative bounds of a set of degrees are its greatest lower and least upper bounds, when it has them.

Equations

• Rett2026.informativeBounds X = {x : D | IsGLB X x ∨ IsLUB X x}

def Rett2026.SharesBounds {D : Type u_2} [LinearOrder D] (X : Set D) : Prop

A degree set is fixed-point ambidirectional when every informative bound of its complement is one of its own, so a relation to the informative bound is insensitive to negation.

Equations

• Rett2026.SharesBounds X = (Rett2026.informativeBounds Xᶜ ⊆ Rett2026.informativeBounds X)

theorem Rett2026.sharesBounds_Iic {D : Type u_2} [LinearOrder D] [DenselyOrdered D] [NoMaxOrder D] (a : D) : SharesBounds (Set.Iic a)

On an open scale, the degrees an individual does not reach share their only informative bound, the individual's degree, with those it reaches.

theorem Rett2026.not_sharesBounds_Iic {D : Type u_2} [LinearOrder D] [OrderTop D] {a : D} (ha : a < ⊤) : ¬SharesBounds (Set.Iic a)

On a scale with a top, the degrees an individual below the top does not reach acquire the top as a second informative bound, which is not a bound of the degrees it reaches.

def Rett2026.taller {E : Type u_1} {D : Type u_2} [LinearOrder D] (μ : E → D) (a b : E) : Prop

The comparative (47) holds when the least upper bound of the target's degrees exceeds that of the standard's.

Equations

• Rett2026.taller μ a b = ∃ (d' : D) (d : D), IsLUB (Set.Iic (μ a)) d' ∧ IsLUB (Set.Iic (μ b)) d ∧ d < d'

def Rett2026.tallerNeg {E : Type u_1} {D : Type u_2} [LinearOrder D] (μ : E → D) (a b : E) : Prop

The comparative with a negated standard (53) reads the standard's degree relative on the negative scale, so its informative bound is the greatest lower bound of the degrees the standard does not reach.

Equations

• Rett2026.tallerNeg μ a b = ∃ (d' : D) (d : D), IsLUB (Set.Iic (μ a)) d' ∧ IsGLB (Set.Ioi (μ b)) d ∧ d < d'

theorem Rett2026.taller_iff {E : Type u_1} {D : Type u_2} [LinearOrder D] (μ : E → D) (a b : E) : taller μ a b ↔ μ b < μ a

theorem Rett2026.tallerNeg_iff {E : Type u_1} {D : Type u_2} [LinearOrder D] (μ : E → D) (a b : E) [DenselyOrdered D] : tallerNeg μ a b ↔ μ b < μ a

theorem Rett2026.tallerNeg_iff_taller {E : Type u_1} {D : Type u_2} [LinearOrder D] (μ : E → D) (a b : E) [DenselyOrdered D] : tallerNeg μ a b ↔ taller μ a b

The comparative is fixed-point ambidirectional, since negating the standard changes nothing.

theorem Rett2026.taller_antitone {E : Type u_1} {D : Type u_2} [LinearOrder D] (μ : E → D) (a b : E) {c : E} (h : μ b ≤ μ a) : taller μ c a → taller μ c b

The comparative is downward entailing in its standard (80).

theorem Rett2026.tallerNeg_antitone {E : Type u_1} {D : Type u_2} [LinearOrder D] (μ : E → D) (a b : E) [DenselyOrdered D] {c : E} (h : μ b ≤ μ a) : tallerNeg μ c a → tallerNeg μ c b

So is the comparative with a negated standard, since the negation reverses the scale on which the entailment is computed but not the truth conditions.

Times

def Rett2026.until_ {T : Type u_1} [LinearOrder T] (A B : Set (NonemptyInterval T)) : Prop

A until B (73) holds when the last time of A precedes the first time of B.

Equations

• Rett2026.until_ A B = ∃ m ∈ Degree.maxOnScale Degree.Comparison.gt (Tense.timeTrace A), ∃ m' ∈ Degree.maxOnScale Degree.Comparison.lt (Tense.timeTrace B), m < m'

theorem Rett2026.until_iff_of_isLeast {T : Type u_1} [LinearOrder T] (A : Set (NonemptyInterval T)) {B : Set (NonemptyInterval T)} {m' : T} (h : IsLeast (Tense.timeTrace B) m') : until_ A B ↔ ∃ m ∈ Degree.maxOnScale Degree.Comparison.gt (Tense.timeTrace A), m < m'

def Rett2026.preEvent {T : Type u_1} [LinearOrder T] [OrderBot T] (s : T) : Set (NonemptyInterval T)

The runtime of a negated event is the interval from the beginning of time to the event's start.

Equations

• Rett2026.preEvent s = Set.Iic { fst := ⊥, snd := s, fst_le_snd := ⋯ }

theorem Rett2026.isLeast_timeTrace_preEvent {T : Type u_1} [LinearOrder T] [OrderBot T] (s : T) : IsLeast (Tense.timeTrace (preEvent s)) ⊥

theorem Rett2026.isGreatest_timeTrace_preEvent {T : Type u_1} [LinearOrder T] [OrderBot T] (s : T) : IsGreatest (Tense.timeTrace (preEvent s)) s

theorem Rett2026.isLeast_timeTrace_completive_preEvent {T : Type u_1} [LinearOrder T] [OrderBot T] (s : T) : IsLeast (Tense.timeTrace (Rett2020a.completive (preEvent s))) s

theorem Rett2026.not_before_preEvent {T : Type u_1} [LinearOrder T] (A : Set (NonemptyInterval T)) [OrderBot T] (s : T) : ¬Rett2020a.before A (preEvent s)

Uncoerced, before a negated event asks for a time before the beginning of time.

theorem Rett2026.before_preEvent_completive_iff {T : Type u_1} [LinearOrder T] (A : Set (NonemptyInterval T)) [OrderBot T] (s : T) : Rett2020a.before A (Rett2020a.completive (preEvent s)) ↔ ∃ t ∈ Tense.timeTrace A, t < s

Coerced to its end, the negated event gives before the starting-point reading of the event itself, since the two share their informative bound.

theorem Rett2026.before_ambidirectional {T : Type u_1} [LinearOrder T] (A : Set (NonemptyInterval T)) [OrderBot T] (i : NonemptyInterval T) : Rett2020a.before A (Set.Iic i) ↔ Rett2020a.before A (Rett2020a.completive (preEvent i.toProd.1))

Before is ambidirectional on the starting-point reading, since negating an embedded event changes nothing, and the endpoint reading of a telic event is lost.

theorem Rett2026.after_preEvent_iff {T : Type u_1} [LinearOrder T] (A : Set (NonemptyInterval T)) [OrderBot T] (s : T) : Rett2020a.after A (preEvent s) ↔ ∃ t ∈ Tense.timeTrace A, s < t

Uncoerced, after a negated event is the after-start reading of the event.

theorem Rett2026.after_preEvent_inchoative {T : Type u_1} [LinearOrder T] (A : Set (NonemptyInterval T)) [OrderBot T] (s : T) {t : T} (ht : t ∈ Tense.timeTrace A) (h : t ≠ ⊥) : Rett2020a.after A (Rett2020a.inchoative (preEvent s))

Coerced to its onset, after a negated event is trivially true of any main clause with a time, so nothing is gained and after licenses no expletive negation.

theorem Rett2026.until_preEvent_completive_iff {T : Type u_1} [LinearOrder T] (A : Set (NonemptyInterval T)) [OrderBot T] (i : NonemptyInterval T) : until_ A (Set.Iic i) ↔ until_ A (Rett2020a.completive (preEvent i.toProd.1))

Until treats its embedded clause as before does, so it is ambidirectional in the same way.

theorem Rett2026.since_preEvent_completive_iff {T : Type u_1} [LinearOrder T] (A : Set (NonemptyInterval T)) [OrderBot T] (s : T) : Heinamaki1974.since A (Rett2020a.completive (preEvent s)) ↔ Heinamaki1974.since A {NonemptyInterval.pure s}

Since a punctual event is since the negated event coerced to its end, as the two have the same single time.

def Rett2026.IsAmbidirectional {α : Type u_1} (f : Set α → Prop) (B : Set α) : Prop

A scalar construction f is ambidirectional at B when it returns the same result on B and on its complement, as maximality does when it picks the same boundary from both; this is the mechanism behind expletive negation.

Equations

• Rett2026.IsAmbidirectional f B = (f B ↔ f Bᶜ)

theorem Rett2026.after_not_ambidirectional {T : Type u_1} [LinearOrder T] (hab : ∃ (a : T) (b : T), a < b) : ¬∀ (A : Set (NonemptyInterval T)) (B : Set T), IsAmbidirectional (fun (X : Set T) => ∃ t ∈ Tense.timeTrace A, ∃ m ∈ Degree.maxOnScale Degree.Comparison.gt X, m < t) B

After is not ambidirectional under complementation, since with two times after the earlier of a punctual clause differs from after its complement.

theorem Rett2026.while_not_ambidirectional {T : Type u_1} [Inhabited T] : ¬∀ (A B : Set T), IsAmbidirectional (fun (X : Set T) => ∀ t ∈ A, t ∈ X) B

While demands total overlap, which the complement of the embedded interval cannot supply, so it is not ambidirectional and Hungarian amíg with negation reads only as until (74).

The paper's examples

inductive Rett2026.Construction : Type

The constructions of the paper's examples.

• before : Construction
• until : Construction
• since : Construction
• comparative : Construction
• closedScaleComparative : Construction
• differentialComparative : Construction
• equative : Construction
• preference : Construction
• negativeVerb : Construction
• exclamative : Construction
• surpriseNegation : Construction
• notSure : Construction

@[instance_reducible]

instance Rett2026.instDecidableEqConstruction : DecidableEq Construction

Equations

• Rett2026.instDecidableEqConstruction x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Rett2026.instFintypeConstruction : Fintype Construction

Equations

• Rett2026.instFintypeConstruction = { elems := { val := ↑Rett2026.Construction.enumList, nodup := Rett2026.Construction.enumList_nodup }, complete := Rett2026.instFintypeConstruction._proof_1 }

def Rett2026.Construction.labels : List (String × Construction)

The constructions by their paperFeatures labels.

Equations

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

def Rett2026.Construction.Scalar : Construction → Prop

The scalar relations the paper analyzes as fixed-point ambidirectional.

Equations

• Rett2026.Construction.before.Scalar = True
• Rett2026.Construction.until.Scalar = True
• Rett2026.Construction.since.Scalar = True
• Rett2026.Construction.comparative.Scalar = True
• Rett2026.Construction.equative.Scalar = True
• x✝.Scalar = False

@[instance_reducible]

instance Rett2026.instDecidablePredConstructionScalar : DecidablePred Construction.Scalar

Equations

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

structure Rett2026.Row : Type

An example records its construction and judgment.

• construction : Construction
• judgment : Judgment

def Rett2026.Row.ofDatum (e : Datum) : Option Row

A datum read into its row.

Equations

• Rett2026.Row.ofDatum e = do let __do_lift ← e.parse? "construction" Rett2026.Construction.labels pure { construction := __do_lift, judgment := e.judgment }

theorem Rett2026.isSome_ofDatum (e : Datum) : e ∈ Examples.all → (Row.ofDatum e).isSome = true

Every example is read.

def Rett2026.data : List Row

The paper's examples.

Equations

• Rett2026.data = List.filterMap Rett2026.Row.ofDatum Rett2026.Examples.all

theorem Rett2026.en_rows : (∀ (c : Construction), c.Scalar → ∃ d ∈ data, d.construction = c ∧ d.judgment = Judgment.acceptable) ∧ ∀ d ∈ data, d.construction = Construction.closedScaleComparative → d.judgment ≠ Judgment.acceptable

Expletive negation is attested in every scalar relation the paper analyzes, in a comparative with a relative adjective, and never in after or while, which have no row; the comparative with a closed-scale adjective rejects it.