van der Sandt and Maier (2003): Denials in Discourse

This file formalizes [vdSM03]'s account of denial as a non-monotonic correction operation on the discourse record, independent of the semantic operator of negation, against [Hor85]'s metalinguistic negation. A denial leaves a negated star condition in the discourse representation, and reverse anaphora moves the material objected to under that negation, (2); removing the whole contribution of the previous utterance fails on [Str52]'s pushed man, (3), on multiple presuppositions, (4), and on an acknowledged part of the utterance, (5). Layered DRT distributes the information an utterance conveys over layers, each condition labelled with the Frege, presupposition or implicature layer of the sentence it comes from, Label, Condition, LDRS, and the content of a set of layers ignores every other, content, (13). Directed reverse anaphora then targets the offensive layers alone, a smallest set of layers whose content is inconsistent with the Frege content of the correction, IsOff, (18), and moves their conditions under the negation of the denial, directedRA, (19): the resulting record keeps the conditions of every other layer and entails the negation of the offensive content, content_directedRA, so the offensive content is retracted, disjoint_content_directedRA, while assertion, the merge of representations, only strengthens the record, content_append_subset. The worked examples are the implicature denials of the possibly right Pope, (20), popeOff, pope_content_directedRA, and of the lady who is a wife, (21), ladyOff, lady_nice_survives.

Implementation notes

The paper interprets layered representations by partial embeddings and closes open layers into singular propositions through the utterance context, (15) and (16); here a condition carries the proposition it expresses once anchored, so an LDRS is a list of labelled propositions and the L-content is the intersection of the conditions bearing a label in L. Offensiveness is minimal disjointness, which need not be unique. The finer targeting of footnote 10, moving only the smallest inconsistent sub-DRS, is not formalized: at the granularity of layers the denial of one of two presuppositions of the same sentence, (4), retracts both, kingQuit_quit_lost, the limitation the paper records there. The examples are the rows of Data.Examples.VanDerSandtMaier2003.

References

• [vdSM03]
• [vdS91]
• [vdS92]
• [Geu98]
• [Hor85]
• [Hor89]
• [Lev00]
• [Str52]
• [KR93]

Layered DRT

inductive VanDerSandtMaier2003.ContentLayer : Type

The layer of a semantic contribution carrying a condition: a backgrounded precondition, the proffered content, or an enrichment beyond the truth conditions — the paper's pr, fr and imp layers.

• presupposition : ContentLayer
• atIssue : ContentLayer
• implicature : ContentLayer

@[instance_reducible]

instance VanDerSandtMaier2003.instDecidableEqContentLayer : DecidableEq ContentLayer

Equations

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

@[instance_reducible]

instance VanDerSandtMaier2003.instReprContentLayer : Repr ContentLayer

Equations

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

def VanDerSandtMaier2003.instReprContentLayer.repr : ContentLayer → ℕ → Std.Format

Equations

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

inductive VanDerSandtMaier2003.Label : Type

A layer label, (6), names the background or a content layer of the i-th sentence.

• background : Label
• of (layer : ContentLayer) (i : ℕ) : Label

@[instance_reducible]

instance VanDerSandtMaier2003.instDecidableEqLabel : DecidableEq Label

Equations

• VanDerSandtMaier2003.instDecidableEqLabel = VanDerSandtMaier2003.instDecidableEqLabel.decEq

def VanDerSandtMaier2003.instDecidableEqLabel.decEq (x✝ x✝¹ : Label) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• VanDerSandtMaier2003.instDecidableEqLabel.decEq VanDerSandtMaier2003.Label.background VanDerSandtMaier2003.Label.background = isTrue ⋯
• VanDerSandtMaier2003.instDecidableEqLabel.decEq VanDerSandtMaier2003.Label.background (VanDerSandtMaier2003.Label.of layer i) = isFalse ⋯
• VanDerSandtMaier2003.instDecidableEqLabel.decEq (VanDerSandtMaier2003.Label.of layer i) VanDerSandtMaier2003.Label.background = isFalse ⋯

def VanDerSandtMaier2003.instReprLabel.repr : Label → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance VanDerSandtMaier2003.instReprLabel : Repr Label

Equations

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

@[reducible, inline]

abbrev VanDerSandtMaier2003.fr (i : ℕ) : Label

The Frege layer of sentence i.

Equations

• VanDerSandtMaier2003.fr i = VanDerSandtMaier2003.Label.of VanDerSandtMaier2003.ContentLayer.atIssue i

@[reducible, inline]

abbrev VanDerSandtMaier2003.pr (i : ℕ) : Label

The presupposition layer of sentence i.

Equations

• VanDerSandtMaier2003.pr i = VanDerSandtMaier2003.Label.of VanDerSandtMaier2003.ContentLayer.presupposition i

@[reducible, inline]

abbrev VanDerSandtMaier2003.imp (i : ℕ) : Label

The implicature layer of sentence i.

Equations

• VanDerSandtMaier2003.imp i = VanDerSandtMaier2003.Label.of VanDerSandtMaier2003.ContentLayer.implicature i

structure VanDerSandtMaier2003.Condition (W : Type u_2) : Type u_2

A labelled condition, (8), pairs its labels with the proposition it expresses once its reference markers are anchored in the context.

• labels : Finset Label
• content : Set W

@[reducible, inline]

abbrev VanDerSandtMaier2003.LDRS (W : Type u_2) : Type u_2

A layered DRS lists its labelled conditions.

Equations

• VanDerSandtMaier2003.LDRS W = List (VanDerSandtMaier2003.Condition W)

def VanDerSandtMaier2003.content {W : Type u_1} (ϕ : LDRS W) (L : Finset Label) : Set W

By (11b) and (13), the L-content of a representation, the conditions bearing a label in L, every other condition being ignored.

Equations

• VanDerSandtMaier2003.content ϕ L = ⋂ c ∈ List.filter (fun (c : VanDerSandtMaier2003.Condition W) => decide (c.labels ∩ L).Nonempty) ϕ, c.content

theorem VanDerSandtMaier2003.mem_content_iff {W : Type u_1} {ϕ : LDRS W} {L : Finset Label} {w : W} : w ∈ content ϕ L ↔ ∀ c ∈ ϕ, (c.labels ∩ L).Nonempty → w ∈ c.content

theorem VanDerSandtMaier2003.content_append {W : Type u_1} (ϕ ψ : LDRS W) (L : Finset Label) : content (ϕ ++ ψ) L = content ϕ L ∩ content ψ L

theorem VanDerSandtMaier2003.content_append_subset {W : Type u_1} (ϕ ψ : LDRS W) (L : Finset Label) : content (ϕ ++ ψ) L ⊆ content ϕ L

Assertion is monotonic: merging a representation into the record only strengthens the record's content.

Directed reverse anaphora

def VanDerSandtMaier2003.IsOff {W : Type u_1} (ϕ : LDRS W) (K L : Finset Label) : Prop

In (18), L is offensive against the correction layers K, a smallest set of layers whose content is inconsistent with the content of K.

Equations

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

def VanDerSandtMaier2003.surviving {W : Type u_1} (ϕ : LDRS W) (off : Finset Label) : LDRS W

The conditions bearing no offensive label.

Equations

• VanDerSandtMaier2003.surviving ϕ off = List.filter (fun (c : VanDerSandtMaier2003.Condition W) => decide (c.labels ∩ off = ∅)) ϕ

def VanDerSandtMaier2003.directedRA {W : Type u_1} (ϕ : LDRS W) (off : Finset Label) (i : ℕ) : LDRS W

Directed reverse anaphora for the denial σ i, (19), moves the conditions bearing an offensive label move under a negation in the denial's Frege layer, the others stay.

Equations

• VanDerSandtMaier2003.directedRA ϕ off i = VanDerSandtMaier2003.surviving ϕ off ++ [{ labels := {VanDerSandtMaier2003.fr i}, content := (VanDerSandtMaier2003.content ϕ off)ᶜ }]

theorem VanDerSandtMaier2003.content_directedRA {W : Type u_1} (ϕ : LDRS W) (off : Finset Label) {i : ℕ} {L : Finset Label} (hi : fr i ∈ L) : content (directedRA ϕ off i) L = content (surviving ϕ off) L ∩ (content ϕ off)ᶜ

The record after directed reverse anaphora, read at layers including the denial's Frege layer: the surviving conditions together with the negation of the offensive content.

theorem VanDerSandtMaier2003.disjoint_content_directedRA {W : Type u_1} (ϕ : LDRS W) (off : Finset Label) {i : ℕ} {L : Finset Label} (hi : fr i ∈ L) : Disjoint (content (directedRA ϕ off i) L) (content ϕ off)

Denial is non-monotonic: the offensive content is retracted from the record.

theorem VanDerSandtMaier2003.content_directedRA_subset {W : Type u_1} {ϕ : LDRS W} {off : Finset Label} {i : ℕ} {L : Finset Label} (hi : fr i ∈ L) {c : Condition W} (hc : c ∈ ϕ) (hoff : c.labels ∩ off = ∅) (hL : (c.labels ∩ L).Nonempty) : content (directedRA ϕ off i) L ⊆ c.content

A condition bearing no offensive label survives directed reverse anaphora.

The possibly right Pope, (20)

inductive VanDerSandtMaier2003.PopeW : Type

The worlds of (20) make the Pope possibly but not necessarily right, or necessarily right.

• possNotNec : PopeW
• nec : PopeW

@[instance_reducible]

instance VanDerSandtMaier2003.instDecidableEqPopeW : DecidableEq PopeW

Equations

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

def VanDerSandtMaier2003.instReprPopeW.repr : PopeW → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance VanDerSandtMaier2003.instReprPopeW : Repr PopeW

Equations

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

@[instance_reducible]

instance VanDerSandtMaier2003.instFintypePopeW : Fintype PopeW

Equations

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

def VanDerSandtMaier2003.popeRecord : LDRS PopeW

ψ of (20) before reverse anaphora holds the background Pope, σ₁'s Frege content that he is possibly right and implicature that he is not necessarily right, and σ₃'s correction that he is necessarily right.

Equations

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

theorem VanDerSandtMaier2003.popeOff : IsOff popeRecord {fr 3} {imp 1}

Off(ψ, fr₃) = {imp₁} — the correction clashes with the implicature layer alone.

theorem VanDerSandtMaier2003.pope_content_directedRA : content (directedRA popeRecord {imp 1} 2) {Label.background, fr 1, fr 2, fr 3} = {PopeW.nec}

After directed reverse anaphora the record says the Pope is necessarily right, keeping σ₁'s Frege content and negating its implicature.

The lady who is a wife, (21)

inductive VanDerSandtMaier2003.LadyW : Type

In the worlds of (21), the woman pointed at is a nice stranger, a nice wife, or a wife who is not nice.

• niceStranger : LadyW
• niceWife : LadyW
• plainWife : LadyW

@[instance_reducible]

instance VanDerSandtMaier2003.instDecidableEqLadyW : DecidableEq LadyW

Equations

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

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

Equations

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

@[instance_reducible]

instance VanDerSandtMaier2003.instReprLadyW : Repr LadyW

Equations

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

@[instance_reducible]

instance VanDerSandtMaier2003.instFintypeLadyW : Fintype LadyW

Equations

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

def VanDerSandtMaier2003.ladyRecord : LDRS LadyW

ψ of (21) holds the background pointing, σ₁'s Frege content that she is a lady and nice, the latter acknowledged by σ₂, its implicature that she is a stranger, and σ₄'s correction that she is my wife.

Equations

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

theorem VanDerSandtMaier2003.ladyOff : IsOff ladyRecord {fr 4} {imp 1}

Off(ψ, fr₄) = {imp₁} — being my wife clashes with the stranger implicature alone.

theorem VanDerSandtMaier2003.lady_nice_survives : content (directedRA ladyRecord {imp 1} 3) {Label.background, fr 1, fr 2, fr 3, fr 4} ⊆ {LadyW.niceStranger, LadyW.niceWife}

The acknowledged content that she is nice survives the denial of the implicature.

Two presuppositions, (4)

@[reducible, inline]

abbrev VanDerSandtMaier2003.KingQuitW : Type

The worlds of (4) record whether France has a king and whether I quit smoking.

Equations

• VanDerSandtMaier2003.KingQuitW = (Bool × Bool)

def VanDerSandtMaier2003.kingQuitRecord : LDRS KingQuitW

ψ of (4) holds σ₁'s two presuppositions, that France has a king and that I quit smoking, its Frege content that the king knows it, and σ₂'s correction that France has no king.

Equations

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

theorem VanDerSandtMaier2003.kingQuit_quit_lost : surviving kingQuitRecord {pr 1} = [{ labels := {fr 1}, content := {w : KingQuitW | w.1 = true ∧ w.2 = true} }, { labels := {fr 2}, content := {w : KingQuitW | w.1 = false} }]

At the granularity of layers, denying the king moves the presupposition that I quit smoking under the negation as well: only the Frege conditions survive, the limitation of footnote 10.