@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:

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.
Contrastive focus (§2.3): adds exclusion on top of similarity+dissimilarity. Exhaustive interpretation entails that no other alternative satisfies the predicate.
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: Discourse.Issue, Discourse.partiallyAnswers (@cite{roberts-2012})
DTS "but": Theories.DTS.But (@cite{merin-1999})
Coherence relations: Core.Discourse.CoherenceRelation (@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).

source

inductive Phenomena.Focus.Studies.Umbach2004.W :

Type

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

Instances For

source

instance Phenomena.Focus.Studies.Umbach2004.instDecidableEqW :

DecidableEq W

Equations

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

source

def Phenomena.Focus.Studies.Umbach2004.instBEqW.beq :

W → W → Bool

Equations

Phenomena.Focus.Studies.Umbach2004.instBEqW.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

instance Phenomena.Focus.Studies.Umbach2004.instBEqW :

BEq W

Equations

Phenomena.Focus.Studies.Umbach2004.instBEqW = { beq := Phenomena.Focus.Studies.Umbach2004.instBEqW.beq }

source

def Phenomena.Focus.Studies.Umbach2004.instReprW.repr :

W → ℕ → Std.Format

Equations

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

Instances For

source

instance Phenomena.Focus.Studies.Umbach2004.instReprW :

Repr W

Equations

Phenomena.Focus.Studies.Umbach2004.instReprW = { reprPrec := Phenomena.Focus.Studies.Umbach2004.instReprW.repr }

source

instance Phenomena.Focus.Studies.Umbach2004.instInhabitedW :

Inhabited W

Equations

Phenomena.Focus.Studies.Umbach2004.instInhabitedW = { default := Phenomena.Focus.Studies.Umbach2004.instInhabitedW.default }

source

def Phenomena.Focus.Studies.Umbach2004.instInhabitedW.default :

Equations

Phenomena.Focus.Studies.Umbach2004.instInhabitedW.default = Phenomena.Focus.Studies.Umbach2004.W.jBerlin

Instances For

source

def Phenomena.Focus.Studies.Umbach2004.wentBerlin :

W → Bool

Equations

Instances For

source

def Phenomena.Focus.Studies.Umbach2004.wentParis :

W → Bool

Equations

Instances For

source

def Phenomena.Focus.Studies.Umbach2004.hadBeer :

W → Bool

Equations

Instances For

source

def Phenomena.Focus.Studies.Umbach2004.hadMartini :

W → Bool

Equations

Instances For

source

def Phenomena.Focus.Studies.Umbach2004.hadDrink :

W → Bool

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

Equations

Instances For

source

def Phenomena.Focus.Studies.Umbach2004.wentSomewhere :

W → Bool

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

Equations

Instances For

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

source

theorem Phenomena.Focus.Studies.Umbach2004.beer_martini_independent :

Core.InformationStructure.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).

source

theorem Phenomena.Focus.Studies.Umbach2004.drink_integrates_beer_martini :

Core.InformationStructure.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.

source

theorem Phenomena.Focus.Studies.Umbach2004.beer_martini_wellformed :

Core.InformationStructure.wellFormedAlts [hadBeer , hadMartini ] hadDrink

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

source

theorem Phenomena.Focus.Studies.Umbach2004.drink_subsumes_martini (w : W) :

hadMartini w = true → hadDrink w = true

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

source

theorem Phenomena.Focus.Studies.Umbach2004.drink_martini_not_independent :

¬Core.InformationStructure.semanticallyIndependent hadDrink hadMartini

source

theorem Phenomena.Focus.Studies.Umbach2004.drink_martini_not_wellformed (integ : W → Bool) :

¬Core.InformationStructure.wellFormedAlts [hadDrink , hadMartini ] integ

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

source

theorem Phenomena.Focus.Studies.Umbach2004.berlin_paris_independent :

Core.InformationStructure.semanticallyIndependent wentBerlin wentParis

source

theorem Phenomena.Focus.Studies.Umbach2004.somewhere_integrates :

Core.InformationStructure.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.

source

theorem Phenomena.Focus.Studies.Umbach2004.wellformed_implies_fip_compatible {W : Type} (alts : List (W → Bool)) (integ : W → Bool) (focusValue : Semantics.FocusInterpretation.PropFocusValue W) (_hwf : Core.InformationStructure.wellFormedAlts alts integ) (gamma : (W → Bool) → Bool) (hgamma : ∀ a ∈ alts, gamma a = true) (hfip : Semantics.FocusInterpretation.fip gamma focusValue) (a : W → Bool) :

a ∈ alts → focusValue a = true

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.

Two varieties of exclusion cross-cut information structure and discourse structure. The taxonomy is already defined in Core (ExclusionVariety); here we verify the parallel and connect to Fragment entries.

source

theorem Phenomena.Focus.Studies.Umbach2004.only_maps_to_contrast :

Core.InformationStructure.ExclusionVariety.additional.toCoherenceRelation = Core.Discourse.CoherenceRelation.CoherenceRelation.contrast

Only-phrases exclude additional alternatives: "Tonight, only RONALD went shopping" (§2.3, ex. 14b) excludes the possibility that someone in addition to Ronald went shopping. This maps to the CONTRAST discourse relation.

source

theorem Phenomena.Focus.Studies.Umbach2004.contrastive_focus_maps_to_correction :

Core.InformationStructure.ExclusionVariety.substitution.toCoherenceRelation = Core.Discourse.CoherenceRelation.CoherenceRelation.correction

Contrastive focus excludes by substitution: "Tonight, RONALD went shopping" (§2.3, ex. 13) excludes the possibility that someone instead of Ronald went shopping. This maps to the CORRECTION discourse relation.

source

theorem Phenomena.Focus.Studies.Umbach2004.only_fragment_exclusion :

Fragments.English.FocusParticles.only_.exclusionVariety = some Core.InformationStructure.ExclusionVariety.additional

The English "only" Fragment entry carries the additional variety.

source

theorem Phenomena.Focus.Studies.Umbach2004.exclusion_parallel :

Core.InformationStructure.ExclusionVariety.additional.toCoherenceRelation ≠ Core.InformationStructure.ExclusionVariety.substitution.toCoherenceRelation

The exclusion parallel: only and CONTRAST share the additional exclusion type, just as contrastive focus and CORRECTION share the substitution type. @cite{umbach-2004} §3.2: "the discourse relations of contrast and correction differ from each other in the same way a contrastive focus differs from an only-phrase."

@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.

source

def Phenomena.Focus.Studies.Umbach2004.confirmDeny {W : Type} (q₁ q₂ c₁ c₂ : W → Bool) :

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

Phenomena.Focus.Studies.Umbach2004.confirmDeny q₁ q₂ c₁ c₂ = ((∀ (w : W), c₁ w = true → q₁ w = true) ∧ ∀ (w : W), c₂ w = true → q₂ w = false)

Instances For

source

inductive Phenomena.Focus.Studies.Umbach2004.CDWorld :

Type

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

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

Instances For

source

instance Phenomena.Focus.Studies.Umbach2004.instDecidableEqCDWorld :

DecidableEq CDWorld

Equations

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

source

def Phenomena.Focus.Studies.Umbach2004.instBEqCDWorld.beq :

CDWorld → CDWorld → Bool

Equations

Phenomena.Focus.Studies.Umbach2004.instBEqCDWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

instance Phenomena.Focus.Studies.Umbach2004.instBEqCDWorld :

BEq CDWorld

Equations

Phenomena.Focus.Studies.Umbach2004.instBEqCDWorld = { beq := Phenomena.Focus.Studies.Umbach2004.instBEqCDWorld.beq }

source

def Phenomena.Focus.Studies.Umbach2004.instReprCDWorld.repr :

CDWorld → ℕ → Std.Format

Equations

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

Instances For

source

instance Phenomena.Focus.Studies.Umbach2004.instReprCDWorld :

Repr CDWorld

Equations

Phenomena.Focus.Studies.Umbach2004.instReprCDWorld = { reprPrec := Phenomena.Focus.Studies.Umbach2004.instReprCDWorld.repr }

source

def Phenomena.Focus.Studies.Umbach2004.cleanedRoom :

CDWorld → Bool

Equations

Instances For

source

def Phenomena.Focus.Studies.Umbach2004.washedDishes :

CDWorld → Bool

Equations

Instances For

source

def Phenomena.Focus.Studies.Umbach2004.didntWashDishes :

CDWorld → Bool

Equations

Instances For

source

theorem Phenomena.Focus.Studies.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.

source

theorem Phenomena.Focus.Studies.Umbach2004.room_dishes_independent :

Core.InformationStructure.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 Discourse.Issue.polar from @cite{roberts-2012}.

source

def Phenomena.Focus.Studies.Umbach2004.roomDishesQUD :

Discourse.Issue CDWorld

The implicit conjunctive question behind a but-sentence: "Did John clean his room? And did he wash the dishes?" Each sub-question is a polar question in the sense of @cite{roberts-2012}.

Equations

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

Instances For

source

theorem Phenomena.Focus.Studies.Umbach2004.roomDishes_inquisitive :

roomDishesQUD.isInquisitive = true

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

source

theorem Phenomena.Focus.Studies.Umbach2004.confirm_deny_is_partial_answer :

Discourse.partiallyAnswers (fun (w : CDWorld) => cleanedRoom w && !washedDishes w) roomDishesQUD [CDWorld.roomOnly , CDWorld.dishesOnly , CDWorld.both , CDWorld.neither ] = true

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.

source

@[reducible, inline]

abbrev Phenomena.Focus.Studies.Umbach2004.singleContrast {W : Type} (q₁ q₂ c₁ c₂ : W → Bool) :

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

Phenomena.Focus.Studies.Umbach2004.singleContrast q₁ q₂ c₁ c₂ = Phenomena.Focus.Studies.Umbach2004.confirmDeny q₁ q₂ c₁ c₂

Instances For

source

inductive Phenomena.Focus.Studies.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).

Instances For

source

instance Phenomena.Focus.Studies.Umbach2004.instDecidableEqContrastMultiplicity :

DecidableEq ContrastMultiplicity

Equations

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

source

def Phenomena.Focus.Studies.Umbach2004.instReprContrastMultiplicity.repr :

ContrastMultiplicity → ℕ → Std.Format

Equations

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

Instances For

source

instance Phenomena.Focus.Studies.Umbach2004.instReprContrastMultiplicity :

Repr ContrastMultiplicity

Equations

Phenomena.Focus.Studies.Umbach2004.instReprContrastMultiplicity = { reprPrec := Phenomena.Focus.Studies.Umbach2004.instReprContrastMultiplicity.repr }

source

def Phenomena.Focus.Studies.Umbach2004.instBEqContrastMultiplicity.beq :

ContrastMultiplicity → ContrastMultiplicity → Bool

Equations

Phenomena.Focus.Studies.Umbach2004.instBEqContrastMultiplicity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

instance Phenomena.Focus.Studies.Umbach2004.instBEqContrastMultiplicity :

BEq ContrastMultiplicity

Equations

Phenomena.Focus.Studies.Umbach2004.instBEqContrastMultiplicity = { beq := Phenomena.Focus.Studies.Umbach2004.instBEqContrastMultiplicity.beq }

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).

source

def Phenomena.Focus.Studies.Umbach2004.contrastImplicitQ {W : Type} (q₁ q₂ : W → Bool) :

W → Bool

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

Phenomena.Focus.Studies.Umbach2004.contrastImplicitQ q₁ q₂ w = (q₁ w && q₂ w)

Instances For

source

def Phenomena.Focus.Studies.Umbach2004.correctionImplicitQ {W : Type} (q₁ : W → Bool) :

W → Bool

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

Phenomena.Focus.Studies.Umbach2004.correctionImplicitQ q₁ = q₁

Instances For

source

theorem Phenomena.Focus.Studies.Umbach2004.contrast_allows_both :

contrastImplicitQ wentBerlin wentParis W.jBoth = true

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

source

theorem Phenomena.Focus.Studies.Umbach2004.correction_excludes_first :

wentBerlin W.jParis = false ∧ wentParis W.jParis = true

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

source

theorem Phenomena.Focus.Studies.Umbach2004.polarity_switch_bridge :

Core.InformationStructure.PolaritySwitchContext.contrast.toCoherenceRelation = Core.Discourse.CoherenceRelation.CoherenceRelation.contrast ∧ Core.InformationStructure.PolaritySwitchContext.correction.toCoherenceRelation = Core.Discourse.CoherenceRelation.CoherenceRelation.correction

The polarity-switch bridge: contrast and correction map to their corresponding coherence relations.

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

@cite{merin-1999} (in Theories.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).
@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 Theories.DTS.But.cip_contrariness_implies_unexpectedness.

source

theorem Phenomena.Focus.Studies.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.

source

theorem Phenomena.Focus.Studies.Umbach2004.contrast_correction_structurally_distinct :

Core.Discourse.CoherenceRelation.CoherenceRelation.contrast ≠ Core.Discourse.CoherenceRelation.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): 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 now represented in linglib's type system:

semanticallyIndependent + commonIntegrator = similarity+dissimilarity
ExclusionVariety.additional = only-phrases / CONTRAST
ExclusionVariety.substitution = contrastive focus / CORRECTION
PolaritySwitchContext.toCoherenceRelation bridges IS ↔ discourse
ExclusionVariety.toCoherenceRelation bridges focus ↔ discourse

source

The three levels of contrast correspond to progressively more constrained discourse configurations:

All focus triggers alternatives (similarity+dissimilarity)
CONTRAST adds exclusion of additional alternatives (only)
CORRECTION adds exclusion by substitution (contrastive focus)

Documentation

Linglib.Phenomena.Focus.Studies.Umbach2004

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

Core thesis #

Key contributions formalized #

Connection to existing formalization #

Key difference #

Where they agree #

Where they diverge #