Van der Sandt & Maier (2003) — Denials in Discourse

[MvdS03]

Denials in Discourse. Michigan Linguistics and Philosophy Workshop, 2003.

Formalization of directed reverse anaphora (RA*) applied to the paper's worked examples, connecting:

• Semantics.ContentLayer — offensiveLayers (which layers are offensive)
• Data/Examples/VanDerSandtMaier2003.json — the paper's denial/correction discourse rows

Denial ≠ negation

The paper's central architectural claim: denial and negation are orthogonal. Negation is a semantic operator; denial is a discourse operation (non-monotonic correction of contextual information). A denial can use a positive sentence ("Mary IS happy" denying "Mary is unhappy", ex. 6), and a negative sentence can be a plain assertion. The DenialType taxonomy below classifies denials by the content layer the correction targets — one mechanism, three targets.

Layered DRT apparatus

The Layered-DRT machinery (LCond/LDRS/directedRA/denialUpdate) is single-paper substrate, defined locally here. It is orthogonal to the faithful model-theoretic DRS core (Semantics/Dynamic/DRS/): that core supplies K&R's model theory and subordination, whereas LDRT's content-layer/RA* algebra is a purely syntactic discourse-update operation (no model-theoretic interpretation is exercised by this paper). Condition formulas (LCond) are therefore opaque atoms — the paper's claims are about the layer bookkeeping, not truth conditions.

Layer naming convention

The paper's layer labels map to ContentLayer constructors as follows:

Paper	Code	Meaning
pr	.presupposition	Backgrounded precondition
fr (Frege)	.atIssue	Assertoric/at-issue content
imp	.implicature	Scalar implicature or connotation

Core mechanism

Denial is a non-monotonic discourse operation that selectively retracts content. The RA* algorithm: (1) identify offensive layers via offensiveLayers — those inconsistent with the correction; (2) move conditions at offensive layers under negation; (3) preserve conditions at non-offensive layers.

Verified examples

Example	Denial type	Off	RA* result
King of France (49)	Presuppositional	{pr, fr}	1 cond: ¬[pr+fr]
Possible/necessary (68)	Implicature	{imp}	3 conds: pr, fr + ¬[imp]
Lady/wife (69)	Connotation	{imp}	4 conds: pr, fr, fr + ¬[imp]

Denial taxonomy

[MvdS03]'s three denial types are not different operations but one mechanism (non-monotonic discourse correction) targeting different content layers. The fourth empirical category — register/connotation denials like "not a LAdy — my WIfe" (69) — maps to the implicature layer alongside scalar implicature.

inductive VanDerSandtMaier2003.DenialType : Type

The type of a denial, determined by which content layer the correction targets.

• propositional : DenialType

  Targets at-issue content; the presupposition survives. (5): "Mary is not happy."

• presuppositional : DenialType

  Targets presupposed content; the assertion falls with it. (30b): "The king of France is NOT bald — France does not have a king."

• implicature : DenialType

  Targets enrichment beyond truth conditions; literal meaning survives. (29b): "It's not POSSIBLE — it's NECESSARY."

@[implicit_reducible]

instance VanDerSandtMaier2003.instDecidableEqDenialType : DecidableEq DenialType

Equations

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

@[implicit_reducible]

instance VanDerSandtMaier2003.instReprDenialType : Repr DenialType

Equations

• VanDerSandtMaier2003.instReprDenialType = { reprPrec := VanDerSandtMaier2003.instReprDenialType.repr }

def VanDerSandtMaier2003.instReprDenialType.repr : DenialType → ℕ → Std.Format

Equations

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

def VanDerSandtMaier2003.DenialType.targetLayer : DenialType → Semantics.ContentLayer.ContentLayer

Map a denial type to the content layer it targets.

Equations

• VanDerSandtMaier2003.DenialType.propositional.targetLayer = Semantics.ContentLayer.ContentLayer.atIssue
• VanDerSandtMaier2003.DenialType.presuppositional.targetLayer = Semantics.ContentLayer.ContentLayer.presupposition
• VanDerSandtMaier2003.DenialType.implicature.targetLayer = Semantics.ContentLayer.ContentLayer.implicature

theorem VanDerSandtMaier2003.DenialType.targetLayer_injective : Function.Injective targetLayer

No two denial types target the same layer: the taxonomy is exactly the layer structure.

Layered DRT (LDRT) substrate

[MvdS03] extend DRT with content layers: each condition carries a label (pr, fr, imp) marking its discourse role.

inductive VanDerSandtMaier2003.LCond : Type

A condition formula. Opaque atoms (Nat-indexed predicate over Nat-indexed referents) closed under negation and boxing; never interpreted semantically — the paper reasons over the layer tags, not truth conditions.

• atom (pred : ℕ) (args : List ℕ) : LCond
• neg (c : LCond) : LCond
• box (drefs : List ℕ) (conds : List LCond) : LCond

structure VanDerSandtMaier2003.TaggedCondition : Type

A condition tagged with its content layer.

• layer : Semantics.ContentLayer.ContentLayer

  The content layer this condition contributes to.

• condition : LCond

  The underlying condition formula.

structure VanDerSandtMaier2003.LDRS : Type

A Layered DRS: a DRS whose conditions carry content-layer tags. A standard DRS is the special case where every condition is atIssue.

• drefs : List ℕ

  Universe: discourse referent indices.

• conditions : List TaggedCondition

  Layered conditions.

def VanDerSandtMaier2003.LDRS.merge (k1 k2 : LDRS) : LDRS

LDRS merge: combine two layered DRSs, preserving layer tags.

Equations

• k1.merge k2 = { drefs := k1.drefs ++ k2.drefs, conditions := k1.conditions ++ k2.conditions }

def VanDerSandtMaier2003.LDRS.offensiveConditions (k : LDRS) (offLayers : List Semantics.ContentLayer.ContentLayer) : List TaggedCondition

The offensive conditions of an LDRS w.r.t. a correction: those whose layer is in the offensive set. In denial, these are retracted.

Equations

• k.offensiveConditions offLayers = List.filter (fun (x : VanDerSandtMaier2003.TaggedCondition) => offLayers.contains x.layer) k.conditions

def VanDerSandtMaier2003.LDRS.survivingConditions (k : LDRS) (offLayers : List Semantics.ContentLayer.ContentLayer) : List TaggedCondition

The surviving conditions after denial: those NOT at offensive layers.

Equations

• k.survivingConditions offLayers = List.filter (fun (x : VanDerSandtMaier2003.TaggedCondition) => !offLayers.contains x.layer) k.conditions

Assertion vs. denial: monotonicity

The paper's deepest architectural claim: assertion is monotonic (merge only adds conditions), denial is non-monotonic (surviving conditions are a subset). Denial is the only operation that removes information from the discourse context.

theorem VanDerSandtMaier2003.LDRS.offensive_surviving_partition (k : LDRS) (offLayers : List Semantics.ContentLayer.ContentLayer) : (k.offensiveConditions offLayers).length + (k.survivingConditions offLayers).length = k.conditions.length

Offensive + surviving = all conditions (partition).

theorem VanDerSandtMaier2003.merge_monotonic (k1 k2 : LDRS) : k1.conditions.length ≤ (k1.merge k2).conditions.length

Assertion (merge) is monotonic: the result has at least as many conditions as the original LDRS.

theorem VanDerSandtMaier2003.denial_nonmonotonic (k : LDRS) (offLayers : List Semantics.ContentLayer.ContentLayer) : (k.survivingConditions offLayers).length ≤ k.conditions.length

Denial (surviving conditions) is non-monotonic: the result has at most as many conditions as the original LDRS.

Directed reverse anaphora (RA*)

[MvdS03]: given the offensive layers (computed by offensiveLayers), RA* partitions the conditions — surviving conditions remain in the main DRS, offensive conditions are moved under a single negation.

def VanDerSandtMaier2003.LDRS.directedRA (k : LDRS) (offLayers : List Semantics.ContentLayer.ContentLayer) : LDRS

Directed reverse anaphora (RA*): move offensive-layer conditions under negation, preserving non-offensive conditions.

Equations

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

def VanDerSandtMaier2003.LDRS.denialUpdate (state correction : LDRS) (offLayers : List Semantics.ContentLayer.ContentLayer) : LDRS

Denial pipeline: merge correction, then apply RA*. In an assertion-denial-correction sequence, the correction is merged with the discourse state, then RA* retracts the offensive layers.

Equations

• state.denialUpdate correction offLayers = (state.merge correction).directedRA offLayers

theorem VanDerSandtMaier2003.LDRS.directedRA_preserves_drefs (k : LDRS) (offLayers : List Semantics.ContentLayer.ContentLayer) : (k.directedRA offLayers).drefs = k.drefs

RA* preserves discourse referents — denial retracts conditions, not referent introductions, so drefs introduced by σ₁ remain available for anaphora even after denial ("A man jumped off the bridge. He didn't jump, he was pushed.").

§1. Presuppositional denial — King of France (§3.5, ex. 49)

σ₁: "The King of France walks in the park." σ₂: "No, he doesn't," σ₃: "France doesn't have a king."

The correction targets the existence presupposition of the definite. Off = {pr, fr}: both layers conflict with "no king".

The row vdsm2003_ex30b_king uses a different sentence (ex. 30b) but the same scenario and denial type — presuppositional; the §5 transfer theorem connects the Off computation to every row tagged with this scenario.

@[implicit_reducible]

instance VanDerSandtMaier2003.instDecidableEqKFW : DecidableEq VanDerSandtMaier2003.KFW✝

Equations

• VanDerSandtMaier2003.instDecidableEqKFW x✝ y✝ = if h : VanDerSandtMaier2003.KFW.ctorIdx✝ x✝ = VanDerSandtMaier2003.KFW.ctorIdx✝ y✝ then isTrue ⋯ else isFalse ⋯

def VanDerSandtMaier2003.instReprKFW.repr : VanDerSandtMaier2003.KFW✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance VanDerSandtMaier2003.instReprKFW : Repr VanDerSandtMaier2003.KFW✝

Equations

• VanDerSandtMaier2003.instReprKFW = { reprPrec := VanDerSandtMaier2003.instReprKFW.repr }

theorem VanDerSandtMaier2003.kf_off : Semantics.ContentLayer.offensiveLayers VanDerSandtMaier2003.kfLayered✝ (fun (w : VanDerSandtMaier2003.KFW✝) => w == VanDerSandtMaier2003.KFW.noKing✝) VanDerSandtMaier2003.kfWorlds✝ = [Semantics.ContentLayer.ContentLayer.presupposition, Semantics.ContentLayer.ContentLayer.atIssue]

Off: "no king" conflicts with both pr (king exists) and fr (king walks).

theorem VanDerSandtMaier2003.kf_ra_length : (VanDerSandtMaier2003.kfAssertion✝.directedRA [Semantics.ContentLayer.ContentLayer.presupposition, Semantics.ContentLayer.ContentLayer.atIssue]).conditions.length = 1

After RA* with Off = {pr, fr}: no conditions survive (both offensive); all material moves under a single negation wrapper.

theorem VanDerSandtMaier2003.kf_ra_layers : List.map (fun (x : TaggedCondition) => x.layer) (VanDerSandtMaier2003.kfAssertion✝.directedRA [Semantics.ContentLayer.ContentLayer.presupposition, Semantics.ContentLayer.ContentLayer.atIssue]).conditions = [Semantics.ContentLayer.ContentLayer.atIssue]

The sole surviving condition is at fr level (the negation wrapper is assertoric: "it is not the case that ...").

§2. Implicature denial — Possible/Necessary (§4.4, ex. 68)

σ₁: "It is possible the Pope is right." σ₂: "No, it's not POssible," σ₃: "it's NECessary that he's right."

The correction targets the scalar implicature ¬□p. Off = {imp}: only the implicature conflicts with correction □p. At-issue content ◇p survives (□p entails ◇p).

@[implicit_reducible]

instance VanDerSandtMaier2003.instDecidableEqModalW : DecidableEq VanDerSandtMaier2003.ModalW✝

Equations

• VanDerSandtMaier2003.instDecidableEqModalW x✝ y✝ = if h : VanDerSandtMaier2003.ModalW.ctorIdx✝ x✝ = VanDerSandtMaier2003.ModalW.ctorIdx✝ y✝ then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance VanDerSandtMaier2003.instReprModalW : Repr VanDerSandtMaier2003.ModalW✝

Equations

• VanDerSandtMaier2003.instReprModalW = { reprPrec := VanDerSandtMaier2003.instReprModalW.repr }

def VanDerSandtMaier2003.instReprModalW.repr : VanDerSandtMaier2003.ModalW✝ → ℕ → Std.Format

Equations

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

theorem VanDerSandtMaier2003.modal_off : Semantics.ContentLayer.offensiveLayers VanDerSandtMaier2003.modalLayered✝ (fun (w : VanDerSandtMaier2003.ModalW✝) => w == VanDerSandtMaier2003.ModalW.nec✝) VanDerSandtMaier2003.modalWorlds✝ = [Semantics.ContentLayer.ContentLayer.implicature]

Off: correction "necessary" (□p) conflicts only with imp (¬□p).

theorem VanDerSandtMaier2003.modal_ra_length : (VanDerSandtMaier2003.modalAssertion✝.directedRA [Semantics.ContentLayer.ContentLayer.implicature]).conditions.length = 3

After RA* with Off = {imp}: pr and fr survive; imp moves under negation. Result: 2 surviving + 1 negation wrapper = 3 conditions.

theorem VanDerSandtMaier2003.modal_ra_layers : List.map (fun (x : TaggedCondition) => x.layer) (VanDerSandtMaier2003.modalAssertion✝.directedRA [Semantics.ContentLayer.ContentLayer.implicature]).conditions = [Semantics.ContentLayer.ContentLayer.presupposition, Semantics.ContentLayer.ContentLayer.atIssue, Semantics.ContentLayer.ContentLayer.atIssue]

Surviving layers: pr, fr at top level; negated imp tagged fr.

§3. Connotation denial — Lady/Wife (§4.4, ex. 69)

σ₁: "Now, THAT's a nice lady." σ₂: "Yes, she is," σ₃: "but she's not a LAdy," σ₄: "she's my WIfe."

The correction targets the connotation of "a lady" (implicature: a stranger, not a close relative). The literal predication (lady, nice) and presupposition (pointing) survive; only the stranger implicature is retracted. Off = {imp}.

The paper's derivation has 4 utterances; σ₂ (affirmation) is monotonic merge and omitted; Off depends only on σ₁ + σ₄. The row vdsm2003_ex13_lady uses a related sentence (ex. 13) but the same scenario and denial type.

@[implicit_reducible]

instance VanDerSandtMaier2003.instDecidableEqLadyW : DecidableEq VanDerSandtMaier2003.LadyW✝

Equations

• VanDerSandtMaier2003.instDecidableEqLadyW x✝ y✝ = if h : VanDerSandtMaier2003.LadyW.ctorIdx✝ x✝ = VanDerSandtMaier2003.LadyW.ctorIdx✝ y✝ then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance VanDerSandtMaier2003.instReprLadyW : Repr VanDerSandtMaier2003.LadyW✝

Equations

• VanDerSandtMaier2003.instReprLadyW = { reprPrec := VanDerSandtMaier2003.instReprLadyW.repr }

def VanDerSandtMaier2003.instReprLadyW.repr : VanDerSandtMaier2003.LadyW✝ → ℕ → Std.Format

Equations

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

theorem VanDerSandtMaier2003.lady_off : Semantics.ContentLayer.offensiveLayers VanDerSandtMaier2003.ladyLayered✝ (fun (w : VanDerSandtMaier2003.LadyW✝) => w == VanDerSandtMaier2003.LadyW.ladyWife✝ || w == VanDerSandtMaier2003.LadyW.notLadyWife✝) VanDerSandtMaier2003.ladyWorlds✝ = [Semantics.ContentLayer.ContentLayer.implicature]

Off: correction "wife" conflicts only with imp (stranger). Crucially, lady (fr) is consistent with wife — Off does NOT retract the literal predication.

theorem VanDerSandtMaier2003.lady_ra_length : (VanDerSandtMaier2003.ladyAssertion✝.directedRA [Semantics.ContentLayer.ContentLayer.implicature]).conditions.length = 4

After RA*: pr, fr (lady), fr (nice) survive; imp (stranger) moves under negation. Result: 3 surviving + 1 negated = 4.

theorem VanDerSandtMaier2003.lady_ra_layers : List.map (fun (x : TaggedCondition) => x.layer) (VanDerSandtMaier2003.ladyAssertion✝.directedRA [Semantics.ContentLayer.ContentLayer.implicature]).conditions = [Semantics.ContentLayer.ContentLayer.presupposition, Semantics.ContentLayer.ContentLayer.atIssue, Semantics.ContentLayer.ContentLayer.atIssue, Semantics.ContentLayer.ContentLayer.atIssue]

Surviving layers: pr, fr, fr at top level; negated imp as fr.

§4. Discourse pipeline: assertion → denial

Full pipeline for the modal example: assertion adds content (monotonic merge), denial selectively retracts (non-monotonic RA*) — the paper's central claim that assertion and denial are dual discourse operations, one monotonic and one not.

theorem VanDerSandtMaier2003.assertion_grows : VanDerSandtMaier2003.φ₁✝.conditions.length > VanDerSandtMaier2003.modalBackground✝.conditions.length

theorem VanDerSandtMaier2003.denial_result_length : VanDerSandtMaier2003.φ₃✝.conditions.length = 4

Denial update: 4 conditions = 2 surviving (pr + ◇right) + 1 correction (□right) + 1 negated wrapper (¬[¬□right]).

theorem VanDerSandtMaier2003.denial_result_layers : List.map (fun (x : TaggedCondition) => x.layer) VanDerSandtMaier2003.φ₃✝.conditions = [Semantics.ContentLayer.ContentLayer.presupposition, Semantics.ContentLayer.ContentLayer.atIssue, Semantics.ContentLayer.ContentLayer.atIssue, Semantics.ContentLayer.ContentLayer.atIssue]

All surviving content is at pr or fr level; no imp content remains.

theorem VanDerSandtMaier2003.implicature_retracted : List.count Semantics.ContentLayer.ContentLayer.implicature (List.map (fun (x : TaggedCondition) => x.layer) VanDerSandtMaier2003.φ₃✝.conditions) = 0

The imp layer has been fully retracted from the top level.

§5. Off → row transfer

The Off computations above agree with the paper's denial-type classification of its rows (Data/Examples/VanDerSandtMaier2003.json): for every row whose discourse scenario is formalized as a LayeredProp above, the computed offensive layers include the layer targeted by the row's denial type.

def VanDerSandtMaier2003.denialTypeOf (row : Data.Examples.LinguisticExample) : Option DenialType

Denial-type adapter: the row's denial_type feature as a DenialType.

Equations

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

theorem VanDerSandtMaier2003.off_contains_target_layer (row : Data.Examples.LinguisticExample) : row ∈ Examples.all → ∀ d ∈ denialTypeOf row, ∀ off ∈ VanDerSandtMaier2003.scenarioOff✝ row, off.contains d.targetLayer = true

Transfer: the Off computation of every formalized scenario contains the target layer of each row classified under that scenario.

§6. Denial ≠ negation (§2.1)

[MvdS03] §2.1: denial and negation are orthogonal. Denial is a discourse operation (non-monotonic correction); negation is a semantic operator. A denial can use a positive sentence, and a negative sentence can be a plain assertion.

theorem VanDerSandtMaier2003.positive_denial_propositional (row : Data.Examples.LinguisticExample) : row ∈ Examples.all → row.feature? "surface_polarity" = some "positive" → denialTypeOf row = some DenialType.propositional

Positive denial is propositional: every row whose denial utterance is syntactically positive (ex. 6, where the denial IS the correction) targets fr, like negative propositional denials. The mechanism is the same regardless of surface polarity.

theorem VanDerSandtMaier2003.same_surface_different_types : ∃ r₁ ∈ Examples.all, ∃ r₂ ∈ Examples.all, r₁.discourseSegments[1]? = r₂.discourseSegments[1]? ∧ denialTypeOf r₁ = some DenialType.propositional ∧ denialTypeOf r₂ = some DenialType.presuppositional

The same surface negation can correspond to different denial types, disambiguated by the correction (§2.3: "still" denials, ex. 19–20): two rows share the denial utterance (second discourse segment) but target different layers.