Umbach (2004): On the Notion of Contrast in Information Structure and Discourse Structure

This file formalizes [Umb04]'s decomposition of contrast. The alternatives a focus evokes must be comparable, similar and dissimilar at once: following [Lan84]'s conditions on coordination, no alternative subsumes another, SemanticallyIndependent, and a common integrator subsumes them all, CommonIntegrator, together WellFormedAlts, which rules out drink beside martini, (9a) and (10a), not_wellFormedAlts_of_subset, and keeps the singular individuals out of the alternatives of a focused coordination, Krifka's problem. This is the contrast of any focus, in the sense of [Roo92]. A contrastive focus in the sense of [Cha76] and [EK98] adds exclusion, of which there are two varieties with different presuppositions, (14): a contrastive focus presupposes that some alternative satisfies the predicate and asserts that it is the focused one, excluding the others instead of it, instead, whereas an only-phrase presupposes the focused alternative and excludes the others in addition to it, inAddition, [Hor69]. The two convey the same total content, instead_content_eq_inAddition_content, and differ in what they presuppose, presupposition_inAddition_eq_assertion_instead. In discourse, but is focus-sensitive, (16), and answers a conjunctive question by confirming one part and denying the other, (17), the confirm+deny condition, ConfirmDeny: such an answer resolves the conjunctive question, mem_polar_inf_polar_of_confirmDeny, and its content is that of the corresponding only-phrase, (19) and (20), confirmDeny_content_eq_inAddition. CONTRAST and CORRECTION, (24) and (25), differ as the two exclusions do: the contrastive but excludes the second alternative in addition to the first, contrastBut, the corrective but, German sondern, excludes the first alternative instead of the second, correctionBut, with the same assertion and different licensing contexts, contrastBut_content_eq_correctionBut_content, presupposition_contrastBut, presupposition_correctionBut.

Implementation notes

Alternatives are propositions, sets of worlds, and a predicate over a set of alternatives is a function to propositions; the presupposition of a contrastive focus is taken in the strengthened form of footnote 8, that exactly one alternative satisfies the predicate. The implicit question of a but-sentence is the meet of the polar questions of its conjuncts, following [Rob98]'s implicit questions. The double-contrast cases (22) and the it-cleft data are recorded as rows only. The examples are the rows of Data.Examples.Umbach2004.

TODO

Footnote 12 observes that the contrastive counterfactual (24c), read as a no-yes sequence, presupposes the second conjunct and prefers the yes-no reading; presupposition_contrastBut follows the main text.

References

• [Umb04]
• [Lan84]
• [Roo92]
• [Cha76]
• [EK98]
• [Hor69]
• [Rob98]

Similarity plus dissimilarity

def Umbach2004.SemanticallyIndependent {W : Type u_1} (a b : Set W) : Prop

Two alternatives are semantically independent when neither subsumes the other.

Equations

• Umbach2004.SemanticallyIndependent a b = (¬a ⊆ b ∧ ¬b ⊆ a)

def Umbach2004.CommonIntegrator {W : Type u_1} (alts : Set (Set W)) (integ : Set W) : Prop

A common integrator subsumes every alternative.

Equations

• Umbach2004.CommonIntegrator alts integ = ∀ a ∈ alts, a ⊆ integ

def Umbach2004.WellFormedAlts {W : Type u_1} (alts : Set (Set W)) (integ : Set W) : Prop

A well-formed alternative set is similar, under a common integrator, and dissimilar, pairwise semantically independent.

Equations

• Umbach2004.WellFormedAlts alts integ = (Umbach2004.CommonIntegrator alts integ ∧ alts.Pairwise Umbach2004.SemanticallyIndependent)

theorem Umbach2004.not_semanticallyIndependent_of_subset {W : Type u_1} {a b : Set W} (h : a ⊆ b) : ¬SemanticallyIndependent a b

An alternative subsuming another is not independent of it.

theorem Umbach2004.not_wellFormedAlts_of_subset {W : Type u_1} {alts : Set (Set W)} {a b : Set W} (ha : a ∈ alts) (hb : b ∈ alts) (hne : a ≠ b) (h : a ⊆ b) (integ : Set W) : ¬WellFormedAlts alts integ

(9a), (10a): an alternative set containing an alternative and one it subsumes is not well-formed under any integrator.

theorem Umbach2004.wellFormedAlts_pair_of_disjoint {W : Type u_1} {a b : Set W} (ha : a.Nonempty) (hb : b.Nonempty) (hab : Disjoint a b) : WellFormedAlts {a, b} (a ∪ b)

(9b): two disjoint non-empty alternatives under their union are well-formed.

Two varieties of exclusion

structure Umbach2004.Exclusion (W : Type u_3) : Type u_3

A presupposition with an assertion.

• presupposition : Set W
• assertion : Set W

def Umbach2004.Exclusion.content {W : Type u_1} (e : Exclusion W) : Set W

The total content of an exclusion.

Equations

• e.content = e.presupposition ∩ e.assertion

def Umbach2004.noOther {W : Type u_1} {α : Type u_2} (P : α → Set W) (A : Set α) (a : α) : Set W

The alternatives other than the focused one satisfy the predicate nowhere.

Equations

• Umbach2004.noOther P A a = ⋂ x ∈ A \ {a}, (P x)ᶜ

def Umbach2004.instead {W : Type u_1} {α : Type u_2} (P : α → Set W) (A : Set α) (a : α) : Exclusion W

(14a): a contrastive focus presupposes that exactly one alternative satisfies the predicate and asserts that it is the focused one, excluding the others instead of it.

Equations

• Umbach2004.instead P A a = { presupposition := ⋃ x ∈ A, P x ∩ Umbach2004.noOther P A x, assertion := P a }

def Umbach2004.inAddition {W : Type u_1} {α : Type u_2} (P : α → Set W) (A : Set α) (a : α) : Exclusion W

(14b): an only-phrase presupposes the focused alternative and asserts that no other alternative satisfies the predicate, excluding the others in addition to it.

Equations

• Umbach2004.inAddition P A a = { presupposition := P a, assertion := Umbach2004.noOther P A a }

theorem Umbach2004.instead_content_eq_inAddition_content {W : Type u_1} {α : Type u_2} {P : α → Set W} {A : Set α} {a : α} (ha : a ∈ A) : (instead P A a).content = (inAddition P A a).content

The two exclusions convey the same content: the focused alternative and no other.

theorem Umbach2004.presupposition_inAddition_eq_assertion_instead {W : Type u_1} {α : Type u_2} {P : α → Set W} {A : Set α} {a : α} : (inAddition P A a).presupposition = (instead P A a).assertion

The only-phrase presupposes what the contrastive focus asserts, that the focused alternative satisfies the predicate.

The discourse relation CONTRAST

def Umbach2004.ConfirmDeny {W : Type u_1} (q₁ q₂ c₁ c₂ : Set W) : Prop

(17): the confirm+deny condition on a but-sentence answering the conjunctive question of q₁ and q₂: the first conjunct confirms q₁ and the second denies q₂.

Equations

• Umbach2004.ConfirmDeny q₁ q₂ c₁ c₂ = (c₁ ⊆ q₁ ∧ c₂ ⊆ q₂ᶜ)

theorem Umbach2004.not_confirmDeny_of_confirm_confirm {W : Type u_1} {q₁ q₂ c₁ c₂ : Set W} (h₂ : c₂ ⊆ q₂) (hne : c₂.Nonempty) : ¬ConfirmDeny q₁ q₂ c₁ c₂

(17b–d): confirming or denying both parts violates the condition whenever the parts hold somewhere; a but-sentence is no answer to a question it confirms twice.

theorem Umbach2004.mem_polar_inf_polar_of_confirmDeny {W : Type u_1} {q₁ q₂ c₁ c₂ : Set W} (h : ConfirmDeny q₁ q₂ c₁ c₂) : c₁ ∩ c₂ ∈ Question.polar q₁ ⊓ Question.polar q₂

A confirm+deny answer resolves the implicit conjunctive question, the meet of the two polar questions, (18).

theorem Umbach2004.confirmDeny_content_eq_inAddition {W : Type u_1} {α : Type u_2} {P : α → Set W} {a b : α} (hab : a ≠ b) : P a ∩ (P b)ᶜ = (inAddition P {a, b} a).content

(19), (20): the content of a confirm+deny but-sentence is the content of the only-phrase over the two alternatives, John cleaned the ROOM but not the DISHES and John only cleaned the ROOM.

CONTRAST and CORRECTION

def Umbach2004.contrastBut {W : Type u_1} {α : Type u_2} (P : α → Set W) (a b : α) : Exclusion W

(24a): the contrastive but, John didn't go to Berlin but he went to Paris, confirms the second alternative and excludes the first in addition to it.

Equations

• Umbach2004.contrastBut P a b = Umbach2004.inAddition P {a, b} a

def Umbach2004.correctionBut {W : Type u_1} {α : Type u_2} (P : α → Set W) (a b : α) : Exclusion W

(25a): the corrective but, German sondern, John didn't go to Berlin but to Paris, excludes the first alternative instead of the second.

Equations

• Umbach2004.correctionBut P a b = Umbach2004.instead P {a, b} a

theorem Umbach2004.contrastBut_content_eq_correctionBut_content {W : Type u_1} {α : Type u_2} {P : α → Set W} {a b : α} : (contrastBut P a b).content = (correctionBut P a b).content

Contrast and correction convey the same assertion, that John did not go to Berlin and did go to Paris.

theorem Umbach2004.presupposition_contrastBut {W : Type u_1} {α : Type u_2} {P : α → Set W} (a b : α) : (contrastBut P a b).presupposition = P a

(24c): the contexts licensing a contrast are those where the confirmed alternative holds, whether or not the denied one does too.

theorem Umbach2004.presupposition_correctionBut {W : Type u_1} {α : Type u_2} {P : α → Set W} {a b : α} (hab : a ≠ b) : (correctionBut P a b).presupposition = symmDiff (P a) (P b)

(25c): the contexts licensing a correction are those where exactly one of the two alternatives holds, the denied one instead of the confirmed one or the other way around.