Denial in Discourse

@cite{van-der-sandt-maier-2003}

Theory-neutral empirical data on denial: how correction sequences selectively retract different content layers of the denied sentence.

Central Claim: Denial ≠ Negation

@cite{van-der-sandt-maier-2003} argue that denial and negation are orthogonal concepts:

• Negation is a semantic operator (a logical connective on propositions)
• Denial is a discourse operation (non-monotonic correction of contextual information)

A denial can use a POSITIVE sentence: "Mary IS happy" denies "Mary is unhappy" (§2.1, ex. 6). And a negative sentence can be a plain assertion, not a denial: "Mary is unhappy" uttered in isolation (§2.1, ex. 2). What makes something a denial is its discourse function (correcting prior information), not its syntactic form.

Three Denial Types

When denial DOES use negation, the correction determines which content layer is retracted:

Denial type	Layer targeted	Paper example
Propositional	fr (at-issue)	"Mary is NOT happy" (5)
Presuppositional	pr	"...NOT bald — there is no king" (30b)
Implicature	imp	"Not POSSIBLE — NECESSARY" (29b)

The paper also identifies a fourth empirical category — register/ connotation denials like "not a steed — a horse" (14) and "didn't kick the bucket — passed away" (15) — which maps to the imp layer alongside scalar implicature.

Scope

This module captures theory-neutral denial data and the DenialType → ContentLayer mapping. The directed reverse anaphora (RA*) mechanism is formalized in Theories.Semantics.Dynamic.DRT.Basic (LDRS.directedRA), with worked examples and Off→DenialDatum agreement proofs in Phenomena.Negation.Studies.VanDerSandtMaier2003.

inductive Phenomena.Negation.Denial.DenialType : Type

The type of denial, determined by which content layer is targeted.

Each type corresponds to a ContentLayer via targetLayer. This is the central claim of: the different denial types are not different operations, but one mechanism (non-monotonic discourse correction) targeting different layers.

• propositional : DenialType

  Propositional denial: targets at-issue content. The presupposition survives; the assertion is retracted. (5): "Mary is not happy." (8): "The king of France is not bald — he has a full head of hair."

• presuppositional : DenialType

  Presuppositional denial: targets presupposed content. The presupposition is retracted; the assertion falls with it. (30b): "The king of France is not bald — France does not have a king." (10): "John did not stop smoking — he never smoked."

• implicature : DenialType

  Implicature denial: targets enrichment beyond truth conditions. Literal meaning survives; the implicature or connotation is retracted. (29b): "It's not POSSIBLE — it's NECESSARY." (14): "That is not a steed — it's a horse."

instance Phenomena.Negation.Denial.instDecidableEqDenialType : DecidableEq DenialType

Equations

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

def Phenomena.Negation.Denial.instReprDenialType.repr : DenialType → ℕ → Std.Format

Equations

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

instance Phenomena.Negation.Denial.instReprDenialType : Repr DenialType

Equations

• Phenomena.Negation.Denial.instReprDenialType = { reprPrec := Phenomena.Negation.Denial.instReprDenialType.repr }

instance Phenomena.Negation.Denial.instBEqDenialType : BEq DenialType

Equations

• Phenomena.Negation.Denial.instBEqDenialType = { beq := Phenomena.Negation.Denial.instBEqDenialType.beq }

def Phenomena.Negation.Denial.instBEqDenialType.beq : DenialType → DenialType → Bool

Equations

• Phenomena.Negation.Denial.instBEqDenialType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Negation.Denial.DenialType.targetLayer : DenialType → Core.Semantics.ContentLayer.ContentLayer

Map denial type to the content layer it targets.

Equations

• Phenomena.Negation.Denial.DenialType.propositional.targetLayer = Core.Semantics.ContentLayer.ContentLayer.atIssue
• Phenomena.Negation.Denial.DenialType.presuppositional.targetLayer = Core.Semantics.ContentLayer.ContentLayer.presupposition
• Phenomena.Negation.Denial.DenialType.implicature.targetLayer = Core.Semantics.ContentLayer.ContentLayer.implicature

theorem Phenomena.Negation.Denial.denial_types_target_distinct_layers : DenialType.propositional.targetLayer ≠ DenialType.presuppositional.targetLayer ∧ DenialType.propositional.targetLayer ≠ DenialType.implicature.targetLayer ∧ DenialType.presuppositional.targetLayer ≠ DenialType.implicature.targetLayer

Each denial type targets a distinct layer.

theorem Phenomena.Negation.Denial.targetLayer_injective (d₁ d₂ : DenialType) (h : d₁.targetLayer = d₂.targetLayer) : d₁ = d₂

The mapping from denial types to content layers is injective: no two denial types target the same layer.

structure Phenomena.Negation.Denial.DenialDatum : Type

A denial datum: an assertion-denial-correction triple.

Records the empirical pattern where a speaker asserts S, a hearer denies with a correction C, and the denial selectively retracts one content layer while preserving others.

Note: denial and correction may be the same sentence in positive denials (where the correcting utterance is itself affirmative).

• assertion : String

  The original assertion being denied

• denial : String

  The denial utterance (may be negative or positive)

• correction : String

  The correction that follows or constitutes the denial

• denialType : DenialType

  Which content layer the correction targets

• retractedContent : String

  What content is retracted by the denial

• survivingContent : String

  What content survives the denial

• exampleNum : String

  Paper example number, if from

• notes : String

def Phenomena.Negation.Denial.instReprDenialDatum.repr : DenialDatum → ℕ → Std.Format

Equations

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

instance Phenomena.Negation.Denial.instReprDenialDatum : Repr DenialDatum

Equations

• Phenomena.Negation.Denial.instReprDenialDatum = { reprPrec := Phenomena.Negation.Denial.instReprDenialDatum.repr }

def Phenomena.Negation.Denial.maryHappy_positive : DenialDatum

Positive denial: denial does not require negation.

§2.1, ex. 6: "Mary IS happy" can deny "Mary is unhappy." The correcting utterance is syntactically positive. This demonstrates the paper's central architectural claim: denial is a discourse operation (non-monotonic correction), not a syntactic one (negation).

Equations

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

def Phenomena.Negation.Denial.maryNotHappy : DenialDatum

Propositional denial: negation targets the assertion (at-issue content). §2.2, ex. 5.

Equations

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

def Phenomena.Negation.Denial.kingBald_presuppositional : DenialDatum

Presuppositional denial of the king of France. §2.4, ex. 30b.

Equations

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

def Phenomena.Negation.Denial.stop_presuppositional : DenialDatum

Presuppositional denial of "stop" (prior-state presupposition). §2.2, ex. 10.

Equations

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

def Phenomena.Negation.Denial.know_presuppositional : DenialDatum

Presuppositional denial of "know" (factive presupposition). §2.2, ex. 9.

Equations

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

def Phenomena.Negation.Denial.possible_necessary : DenialDatum

Scalar implicature denial: "possible" implicates "not necessary." §2.2, ex. 11 / §2.4, ex. 29b.

"Possible" literally means ◇p; the scalar implicature is ¬□p (not necessary). The correction "it is necessary" retracts the implicature while preserving the literal meaning (□p entails ◇p).

Equations

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

def Phenomena.Negation.Denial.several_all : DenialDatum

Scalar implicature denial with "several." §2.3, ex. 21.

"Several" implicates "not all." The correction "all" retracts the upper-bound implicature.

Equations

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

def Phenomena.Negation.Denial.good_excellent : DenialDatum

Gradable adjective implicature denial: "good" implicates "not excellent." §2.2, ex. 12.

Equations

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

def Phenomena.Negation.Denial.lady_wife : DenialDatum

Connotation denial: "lady" connotes a social role beyond "woman/wife." §2.2, ex. 13.

Equations

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

def Phenomena.Negation.Denial.steed_horse : DenialDatum

Register denial: "steed" connotes formality/literary register. §2.2, ex. 14.

Equations

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

The same surface negation can correspond to different denial types, disambiguated by the correction. The paper's §2.3 example (19)/(20) demonstrates this with "still":

• (19) "John does NOT still live in Paris — he did live there but has moved" = propositional denial (targets fr: "John lives in Paris now")
• (20) "John does NOT still live in Paris — he has never set foot in France" = presuppositional denial (targets pr: "John lived in Paris before")

def Phenomena.Negation.Denial.still_propositional : DenialDatum

Propositional reading of "still" denial. §2.3, ex. 19.

Equations

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

def Phenomena.Negation.Denial.still_presuppositional : DenialDatum

Presuppositional reading of "still" denial. §2.3, ex. 20.

Equations

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

theorem Phenomena.Negation.Denial.still_denial_same_surface : still_propositional.denial = still_presuppositional.denial

Same surface negation, different denial types.

theorem Phenomena.Negation.Denial.still_denial_different_layers : still_propositional.denialType ≠ still_presuppositional.denialType

But they target different layers.

def Phenomena.Negation.Denial.propositionalDenials : List DenialDatum

Equations

• Phenomena.Negation.Denial.propositionalDenials = [Phenomena.Negation.Denial.maryHappy_positive, Phenomena.Negation.Denial.maryNotHappy, Phenomena.Negation.Denial.still_propositional]

def Phenomena.Negation.Denial.presuppositionalDenials : List DenialDatum

Equations

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

def Phenomena.Negation.Denial.implicatureDenials : List DenialDatum

Equations

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

def Phenomena.Negation.Denial.allDenialData : List DenialDatum

Equations

• Phenomena.Negation.Denial.allDenialData = Phenomena.Negation.Denial.propositionalDenials ++ Phenomena.Negation.Denial.presuppositionalDenials ++ Phenomena.Negation.Denial.implicatureDenials