@cite{umbach-2004} — On the Notion of Contrast @cite{umbach-2004}

Umbach, Carla (2004). On the Notion of Contrast in Information Structure and Discourse Structure. Journal of Semantics 21(2): 155–175.

Core thesis

Contrast is similarity plus dissimilarity. This single notion unifies three levels at which "contrast" appears:

1. Focus alternatives (§2.2): all focus evokes alternatives that are similar (common integrator) and dissimilar (semantically independent). This is contrast in the broadest sense — a prerequisite for any coordination by and or but.

2. Contrastive focus (§2.3): adds exclusion on top of similarity+dissimilarity. Exhaustive interpretation entails that no other alternative satisfies the predicate.

3. Discourse relations (§3): CONTRAST and CORRECTION both require similarity+dissimilarity but differ in exclusion type:

   • CONTRAST: excludes additional alternatives (confirm+deny)
   • CORRECTION: excludes by substitution (German sondern)

Key contributions formalized

• Alternative set well-formedness: semanticallyIndependent, commonIntegrator, wellFormedAlts (defined in Core, exercised here)
• Confirm+deny condition on "but" (§3.1)
• Exclusion variety taxonomy connecting only-phrases ↔ CONTRAST and contrastive focus ↔ CORRECTION (§2.3, §3.2)
• Bridge: comparison with @cite{merin-1999} DTS account of "but"

Connection to existing formalization

• Focus alternatives & FIP: Semantics.FocusInterpretation (@cite{rooth-1992})
• QUD / implicit questions: Core.Question, Core.Question.isPartialAnswer (@cite{roberts-2012})
• DTS "but": DTS.But (@cite{merin-1999})
• Coherence relations: Core.Discourse.Coherence (@cite{kehler-2002})
• Focus particles: Fragments.English.FocusParticles

A 6-world model sufficient for all examples.

Worlds encode who went where (Berlin/Paris/London examples from §3.2) and what John had to drink (beer/martini examples from §2.2).

inductive Umbach2004.W : Type

• jBerlin : W
• jParis : W
• jBoth : W
• jBeer : W
• jMartini : W
• jBeerMartini : W

@[implicit_reducible]

instance Umbach2004.instDecidableEqW : DecidableEq W

Equations

• Umbach2004.instDecidableEqW x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Umbach2004.instReprW.repr : W → ℕ → Std.Format

Equations

• Umbach2004.instReprW.repr Umbach2004.W.jBerlin prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Umbach2004.W.jBerlin")).group prec✝
• Umbach2004.instReprW.repr Umbach2004.W.jParis prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Umbach2004.W.jParis")).group prec✝
• Umbach2004.instReprW.repr Umbach2004.W.jBoth prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Umbach2004.W.jBoth")).group prec✝
• Umbach2004.instReprW.repr Umbach2004.W.jBeer prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Umbach2004.W.jBeer")).group prec✝
• Umbach2004.instReprW.repr Umbach2004.W.jMartini prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Umbach2004.W.jMartini")).group prec✝
• Umbach2004.instReprW.repr Umbach2004.W.jBeerMartini prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Umbach2004.W.jBeerMartini")).group prec✝

@[implicit_reducible]

instance Umbach2004.instReprW : Repr W

Equations

• Umbach2004.instReprW = { reprPrec := Umbach2004.instReprW.repr }

def Umbach2004.instInhabitedW.default : W

Equations

• Umbach2004.instInhabitedW.default = Umbach2004.W.jBerlin

@[implicit_reducible]

instance Umbach2004.instInhabitedW : Inhabited W

Equations

• Umbach2004.instInhabitedW = { default := Umbach2004.instInhabitedW.default }

def Umbach2004.wentBerlin : Set W

Equations

• Umbach2004.wentBerlin = {Umbach2004.W.jBerlin, Umbach2004.W.jBoth}

def Umbach2004.wentParis : Set W

Equations

• Umbach2004.wentParis = {Umbach2004.W.jParis, Umbach2004.W.jBoth}

def Umbach2004.hadBeer : Set W

Equations

• Umbach2004.hadBeer = {Umbach2004.W.jBeer, Umbach2004.W.jBeerMartini}

def Umbach2004.hadMartini : Set W

Equations

• Umbach2004.hadMartini = {Umbach2004.W.jMartini, Umbach2004.W.jBeerMartini}

def Umbach2004.hadDrink : Set W

"had a drink" — subsumes both beer and martini.

Equations

• Umbach2004.hadDrink = {Umbach2004.W.jBeer, Umbach2004.W.jMartini, Umbach2004.W.jBeerMartini}

def Umbach2004.wentSomewhere : Set W

"went somewhere" — common integrator for Berlin/Paris.

Equations

• Umbach2004.wentSomewhere = {Umbach2004.W.jBerlin, Umbach2004.W.jParis, Umbach2004.W.jBoth}

The core formal claim: alternatives must be pairwise semantically independent (dissimilar) and share a common integrator (similar). This explains coordination acceptability judgments.

theorem Umbach2004.beer_martini_independent : Semantics.Focus.Comparability.semanticallyIndependent hadBeer hadMartini

Beer and martini are semantically independent: neither entails the other. Having a beer does not entail having a martini (witness: W.jBeer), and vice versa (witness: W.jMartini).

theorem Umbach2004.drink_integrates_beer_martini : Semantics.Focus.Comparability.commonIntegrator [hadBeer, hadMartini] hadDrink

"drink" is a common integrator for {beer, martini}: every world where beer or martini is true is also a world where drink is true.

theorem Umbach2004.beer_martini_wellformed : Semantics.Focus.Comparability.wellFormedAlts [hadBeer, hadMartini] hadDrink

{beer, martini} is a well-formed alternative set under "drink".

theorem Umbach2004.drink_subsumes_martini : hadMartini ⊆ hadDrink

"drink" subsumes "martini": hadMartini ⊆ hadDrink. This violates semantic independence, explaining why #John had a drink and Mary had a martini is odd (@cite{umbach-2004} §2.2, ex. 9a).

theorem Umbach2004.drink_martini_not_independent : ¬Semantics.Focus.Comparability.semanticallyIndependent hadDrink hadMartini

theorem Umbach2004.drink_martini_not_wellformed (integ : Set W) : ¬Semantics.Focus.Comparability.wellFormedAlts [hadDrink, hadMartini] integ

{drink, martini} is NOT a well-formed alternative set (under any integrator).

theorem Umbach2004.berlin_paris_independent : Semantics.Focus.Comparability.semanticallyIndependent wentBerlin wentParis

theorem Umbach2004.somewhere_integrates : Semantics.Focus.Comparability.commonIntegrator [wentBerlin, wentParis] wentSomewhere

@cite{umbach-2004} §2.1 builds directly on @cite{rooth-1992}'s alternative semantics: all focus evokes alternatives, and Umbach's similarity+dissimilarity refines what counts as a well-formed alternative set.

The FIP (Γ ⊆ ⟦α⟧f) constrains the contrast set Γ to be a subset of focus alternatives. Umbach adds that alternatives within Γ must be pairwise semantically independent (dissimilarity) and share a common integrator (similarity). This is strictly more constraining than FIP alone.

theorem Umbach2004.wellformed_implies_fip_compatible {W : Type} (alts : List (Set W)) (integ : Set W) (focusValue : Semantics.FocusInterpretation.PropFocusValue W) (_hwf : Semantics.Focus.Comparability.wellFormedAlts alts integ) (gamma : Set (Set W)) (hgamma : ∀ a ∈ alts, a ∈ gamma) (hfip : Semantics.FocusInterpretation.fip gamma focusValue) (a : Set W) : a ∈ alts → a ∈ focusValue

Well-formed alternatives satisfy Rooth's FIP: if the focus value admits each alternative as a focus alternative, the well-formedness constraints layer on top of FIP without contradicting it.

Concretely: if ⟦α⟧f includes all members of the alternative set (Γ ⊆ ⟦α⟧f), and the alternatives are well-formed in Umbach's sense, then FIP is satisfied. Umbach's conditions refine, not replace, Rooth.

@cite{umbach-2004} (§2.3 UNVERIFIED) distinguishes two varieties of exclusion that cross-cut information structure and discourse structure: only-phrases exclude additional alternatives (mapping to the CONTRAST discourse relation), while contrastive focus excludes by substitution (mapping to the CORRECTION discourse relation). The two-cell IS taxonomy is recoverable from Core.Discourse.Coherence.CoherenceRelation's .contrast and .correction cases — Umbach's own decomposition makes the IS-side enum redundant once the discourse-side cases exist. The prior ExclusionVariety substrate enum was deleted in the 0.230.488 cleanup.

theorem Umbach2004.only_fragment_exclusion : Fragments.English.FocusParticles.only_.exclusionVariety = some Core.Discourse.Coherence.CoherenceRelation.contrast

The English "only" Fragment entry carries the contrast (= additional) exclusion.

@cite{umbach-2004} §3.1: a but-sentence responds to an implicit question with "yes...but no...". One conjunct confirms a sub-question, the other denies its counterpart. This is the confirm+deny condition.

Example (§3.1, ex. 17e): "John cleaned up his room, but he didn't wash the dishes" — confirms "Did John clean his room?" (yes) and denies "Did he wash the dishes?" (no).

The confirm+deny condition distinguishes but from and: both require similarity+dissimilarity in their conjuncts, but only but requires one conjunct to confirm and one to deny.

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

The confirm+deny condition on a but-sentence. Given two sub-questions q₁, q₂ (derived from focus in the conjuncts), the first conjunct confirms q₁ and the second denies q₂.

Equations

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

inductive Umbach2004.CDWorld : Type

A 4-world model for the confirm+deny examples.

• roomOnly : CDWorld
• dishesOnly : CDWorld
• both : CDWorld
• neither : CDWorld

@[implicit_reducible]

instance Umbach2004.instDecidableEqCDWorld : DecidableEq CDWorld

Equations

• Umbach2004.instDecidableEqCDWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Umbach2004.instReprCDWorld.repr : CDWorld → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Umbach2004.instReprCDWorld.repr Umbach2004.CDWorld.both prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Umbach2004.CDWorld.both")).group prec✝
• Umbach2004.instReprCDWorld.repr Umbach2004.CDWorld.neither prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Umbach2004.CDWorld.neither")).group prec✝

@[implicit_reducible]

instance Umbach2004.instReprCDWorld : Repr CDWorld

Equations

• Umbach2004.instReprCDWorld = { reprPrec := Umbach2004.instReprCDWorld.repr }

def Umbach2004.cleanedRoom : Set CDWorld

Equations

• Umbach2004.cleanedRoom = {Umbach2004.CDWorld.roomOnly, Umbach2004.CDWorld.both}

def Umbach2004.washedDishes : Set CDWorld

Equations

• Umbach2004.washedDishes = {Umbach2004.CDWorld.dishesOnly, Umbach2004.CDWorld.both}

def Umbach2004.didntWashDishes : Set CDWorld

Equations

• Umbach2004.didntWashDishes = {Umbach2004.CDWorld.roomOnly, Umbach2004.CDWorld.neither}

theorem Umbach2004.ex17e_confirm_deny : confirmDeny cleanedRoom washedDishes cleanedRoom didntWashDishes

"John cleaned up his room, but he didn't wash the dishes" (§3.1, ex. 17e) satisfies confirm+deny: the first conjunct confirms the room question, the second denies the dishes question.

theorem Umbach2004.room_dishes_independent : Semantics.Focus.Comparability.semanticallyIndependent cleanedRoom washedDishes

Semantic independence of the sub-questions: cleaning the room does not entail washing the dishes, and vice versa.

@cite{umbach-2004} §3.1 formulates confirm+deny in terms of implicit questions (QUDs): "A but B" responds to an implicit conjunctive question "Did X do A, and did X do B?" where one sub-answer confirms and the other denies. This connects to Core.Question.fromSetoid (@cite{roberts-2012}): the implicit conjunctive question is the partition by joint (room, dishes) values, and confirm+deny picks one cell.

def Umbach2004.roomDishesEquiv : Setoid CDWorld

Equivalence: two worlds agree on both cleanedRoom and washedDishes. The four cells of this partition are the four combinations of yes/no answers to the conjunctive question.

Equations

• Umbach2004.roomDishesEquiv = Setoid.ker fun (w : Umbach2004.CDWorld) => (w ∈ Umbach2004.cleanedRoom, w ∈ Umbach2004.washedDishes)

def Umbach2004.roomDishesQUD : Core.Question CDWorld

The implicit conjunctive question behind a but-sentence: "Did John clean his room? And did he wash the dishes?" Built as the inquisitive content of the (room, dishes) partition.

Equations

• Umbach2004.roomDishesQUD = Core.Question.fromSetoid Umbach2004.roomDishesEquiv

theorem Umbach2004.roomDishes_inquisitive : roomDishesQUD.isInquisitive

The implicit question behind CONTRAST is genuinely inquisitive: it has multiple alternatives (all four combinations are nontrivial).

def Umbach2004.roomYesDishesNo : Set CDWorld

The "room yes, dishes no" cell — the equivalence class of .roomOnly under roomDishesEquiv.

Equations

• Umbach2004.roomYesDishesNo = {x : Umbach2004.CDWorld | Umbach2004.roomDishesEquiv x Umbach2004.CDWorld.roomOnly}

theorem Umbach2004.confirm_deny_is_partial_answer : roomDishesQUD.partiallyAnswers roomYesDishesNo

The "room yes, dishes no" alternative partially answers the QUD: the confirm+deny pattern corresponds to one cell of the implicit conjunctive question.

@cite{umbach-2004} §3.1 distinguishes two kinds of CONTRAST:

• Single contrast ("but"): one conjunct confirms, one denies. "John cleaned his room, but he didn't wash the dishes."

• Double contrast ("although"/"while"): both conjuncts deny parts of a conjunctive expectation. "Although John cleaned his room, he didn't wash the dishes."

In double contrast, both conjuncts bear contrastive focus and neither is presented as a simple confirmation.

@[reducible, inline]

abbrev Umbach2004.singleContrast {W : Type} (q₁ q₂ c₁ c₂ : Set W) : Prop

Single contrast: confirm+deny — one conjunct confirms, one denies. "John cleaned his room, but he didn't wash the dishes." Lexicalized by English "but", German aber.

Equations

• Umbach2004.singleContrast q₁ q₂ c₁ c₂ = Umbach2004.confirmDeny q₁ q₂ c₁ c₂

inductive Umbach2004.ContrastMultiplicity : Type

Contrast multiplicity: single vs double. @cite{umbach-2004} §3.1: single contrast ("but") has one contrastive focus (confirm+deny); double contrast ("although"/"while") has two contrastive foci (both conjuncts bear contrastive marking).

The distinction is prosodic/information-structural: "although" marks both conjuncts as contrastive, while "but" marks only the second.

• single : ContrastMultiplicity

  One contrastive focus: "A, but B" (confirm+deny, asymmetric).

• double : ContrastMultiplicity

  Two contrastive foci: "Although A, B" (deny+deny, symmetric).

@[implicit_reducible]

instance Umbach2004.instDecidableEqContrastMultiplicity : DecidableEq ContrastMultiplicity

Equations

• Umbach2004.instDecidableEqContrastMultiplicity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Umbach2004.instReprContrastMultiplicity.repr : ContrastMultiplicity → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Umbach2004.instReprContrastMultiplicity : Repr ContrastMultiplicity

Equations

• Umbach2004.instReprContrastMultiplicity = { reprPrec := Umbach2004.instReprContrastMultiplicity.repr }

The discourse relations CONTRAST and CORRECTION both require similarity+dissimilarity but differ in exclusion type and in the implicit question they respond to.

• CONTRAST (§3.2, ex. 24a): "John didn't go to Berlin but he went to Paris." Implicit Q: "Did John go to Berlin, and also to Paris?" Counterfactual: either both or only Paris.

• CORRECTION (§3.2, ex. 25a): "John didn't go to Berlin but to Paris." Implicit Q: "Did John go to Berlin?" Counterfactual: Berlin instead of Paris.

German lexicalizes: aber (contrast) vs sondern (correction).

def Umbach2004.contrastImplicitQ {W : Type} (q₁ q₂ : Set W) : Set W

CONTRAST responds to a conjunctive implicit question: "Did X do A, and did X also do B?" Answer: "yes A, but no B." Both alternatives could in principle be true.

Equations

• Umbach2004.contrastImplicitQ q₁ q₂ = q₁ ∩ q₂

def Umbach2004.correctionImplicitQ {W : Type} (q₁ : Set W) : Set W

CORRECTION responds to a simple question about the denied item: "Did X do A?" Answer: "No A, but B instead." The alternatives are mutually exclusive.

Equations

• Umbach2004.correctionImplicitQ q₁ = q₁

theorem Umbach2004.contrast_allows_both : W.jBoth ∈ contrastImplicitQ wentBerlin wentParis

In the contrastive case (ex. 24a), the counterfactual allows both alternatives to be true.

theorem Umbach2004.correction_excludes_first : W.jParis ∉ wentBerlin ∧ W.jParis ∈ wentParis

In the corrective case (ex. 25a), the assertion is that Berlin is false and Paris holds instead.

Two accounts of "but" are now formalized in linglib:

1. @cite{merin-1999} (in DTS.But): "A but B" is felicitous iff A is positively relevant and B is negatively relevant to an issue H, with B "winning" (A∧B negatively relevant). This yields unexpectedness as the core meaning: P(B|A) < P(B).

2. @cite{umbach-2004} (this file): "A but B" requires similarity+dissimilarity in the focused alternatives of the conjuncts, plus the confirm+deny condition: one conjunct confirms and one denies a sub-question. This yields exclusion of an alternative.

Key difference

Merin: "but" signals that A raises expectations that B defeats. The mechanism is probabilistic relevance — no reference to alternatives or focus.

Umbach: "but" is focus-sensitive — the contrast is determined by the focused elements in the conjuncts. The mechanism is alternative-based exclusion — the hearer must reconstruct what is being excluded, and the exclusion type determines whether the relation is CONTRAST (additional: "in addition to") or CORRECTION (substitution: "instead of").

Where they agree

Both predict that "A but B" requires A and B to be in some sense opposed. Merin captures this as opposite relevance signs; Umbach captures it as the deny component of confirm+deny.

Where they diverge

Merin's account does not predict the focus-sensitivity of "but": if the issue H is held constant, the relevance of A and B depends only on their truth-conditional content, not on what is focused. Umbach's account directly predicts that shifting focus in the second conjunct changes the contrast (§3.1, ex. 16a vs 16b).

@cite{merin-1999} Theorem 8 (CIP + contrariness → unexpectedness) is in DTS.But.cip_contrariness_implies_unexpectedness.

theorem Umbach2004.and_but_distinct : Fragments.English.FunctionWords.and_.form ≠ Fragments.English.FunctionWords.but.form

Both accounts treat "but" as semantically distinct from "and". The Fragment entries distinguish them morphologically; the theory layer explains why.

theorem Umbach2004.contrast_correction_structurally_distinct : Core.Discourse.Coherence.CoherenceRelation.contrast ≠ Core.Discourse.Coherence.CoherenceRelation.correction

Both accounts agree that CONTRAST and CORRECTION are distinct. Merin distinguishes them by relevance sign (contrariness vs non-contrariness of issues); Umbach distinguishes them by exclusion type.

@cite{umbach-2004} Conclusion (Table 1 UNVERIFIED): the notion of contrast decomposes into three nested layers, each adding a requirement:

similarity + dissimilarity       → all focus / all coordination
  + exclusion (in addition to)   → only-phrases / CONTRAST
  + exclusion (instead of)       → contrastive focus / CORRECTION

The taxonomy is represented in linglib's type system:

• semanticallyIndependent + commonIntegrator = similarity+dissimilarity
• CoherenceRelation.contrast = only-phrases / CONTRAST (additional)
• CoherenceRelation.correction = contrastive focus / CORRECTION (substitution)

Both polarity-switch contexts and exclusion varieties are populated directly with Core.Discourse.Coherence.CoherenceRelation's .contrast and .correction cases — the prior IS-vocabulary parallel enums (PolaritySwitchContext, ExclusionVariety) were deleted in the 0.230.488 cleanup as duplicates of the discourse-side primitive.

theorem Umbach2004.contrast_levels : Core.Discourse.Coherence.CoherenceRelation.contrast.toClass = Core.Discourse.Coherence.CoherenceClass.resemblance ∧ Core.Discourse.Coherence.CoherenceRelation.correction.toClass = Core.Discourse.Coherence.CoherenceClass.resemblance ∧ Core.Discourse.Coherence.CoherenceRelation.contrast ≠ Core.Discourse.Coherence.CoherenceRelation.correction

The two non-vacuous levels of contrast correspond to progressively more constrained discourse configurations:

1. CONTRAST: exclusion of additional alternatives (only)
2. CORRECTION: exclusion by substitution (contrastive focus)