Highlighting

@cite{roelofsen-vangool-2010} @cite{roelofsen-farkas-2015} @cite{simons-tonhauser-beaver-roberts-2010} @cite{krifka-2017}

A highlighted proposition is one that has been made salient by a recent utterance and that addresses the current question under discussion (QUD). The notion was introduced by @cite{roelofsen-vangool-2010} for disjunctive questions (the affirmative disjunct is highlighted and feeds the polarity particle response in @cite{roelofsen-farkas-2015}). It generalises in @cite{krifka-2017} and the verum-marker literature (e.g. @cite{martinez-vera-2026}) to a discourse-management primitive shared across focus, biased polar questions, and verum strategies.

What this module provides

• HighlightingContext W — bundles a set of salient propositions with the current QUD.
• AddressesQUD — a proposition is comparable to a QUD alternative, the simplest @cite{simons-tonhauser-beaver-roberts-2010} version of "contextually entails an answer".
• Highlighted — the conjunction salient ∧ addresses-QUD. This is exactly the @cite{martinez-vera-2026} (38) presupposition.
• @cite{roelofsen-farkas-2015} polarity particles agree/reverse with a commitment projection.

Consumers (verum studies, biased polar question studies, evidential discourse studies) import this file rather than re-stipulating the predicate locally.

Known unmigrated consumers (deferred)

This substrate landed alongside @cite{martinez-vera-2026}'s formalisation; existing files that use highlighting-shaped notions but have not yet been migrated:

• Theories/Semantics/Attitudes/Preferential.lean — HighlightingClauseType
  • highlightedValue for Pruitt-Roelofsen 2011 / Uegaki 2022 hope-whether.
• Phenomena/Dialogue/Studies/FarkasRoelofsen2017.lean — paper-side highlighted-alternative prose; F&R 2015 is the substrate's own anchor.
• Core/Question/Singleton.lean — IsSingleton documents itself in @cite{roelofsen-farkas-2015} terminology but is a different abstraction (property of a Question, not a discourse context).
• Theories/Semantics/Modality/BiasedPQ.lean — OriginalBias / ContextualEvidence cover adjacent ground (prior-discourse bias) with a different shape; bridge not yet written.

Migration to consume Highlighting.HighlightingContext is queued for follow-up work; landing the substrate first lets the new MartinezVera2026 study consume it without forcing an immediate four-file refactor.

structure Semantics.Highlighting.HighlightingContext (W : Type u_1) : Type u_1

A highlighting context: the set of propositions made salient by recent utterances, paired with the QUD they should address.

• salient : Set (Set W)

  Propositions made salient by recent utterances.

• qud : Core.Question W

  The current question under discussion.

def Semantics.Highlighting.AddressesQUD {W : Type u_1} (q : Core.Question W) (p : Set W) : Prop

A proposition p addresses a question q iff it is comparable to some alternative — entailing it or being entailed by it. The simplest Set-valued version of @cite{simons-tonhauser-beaver-roberts-2010}'s "contextually entails an answer".

Equations

• Semantics.Highlighting.AddressesQUD q p = ∃ a ∈ q.alt, p ⊆ a ∨ a ⊆ p

def Semantics.Highlighting.Highlighted {W : Type u_1} (c : HighlightingContext W) (p : Set W) : Prop

@cite{martinez-vera-2026} (38): proposition p is highlighted in context c iff it has been made salient by an utterance and addresses the current QUD.

Equations

• Semantics.Highlighting.Highlighted c p = (p ∈ c.salient ∧ Semantics.Highlighting.AddressesQUD c.qud p)

theorem Semantics.Highlighting.highlighted_imp_salient {W : Type u_1} {c : HighlightingContext W} {p : Set W} (h : Highlighted c p) : p ∈ c.salient

theorem Semantics.Highlighting.highlighted_imp_addressesQUD {W : Type u_1} {c : HighlightingContext W} {p : Set W} (h : Highlighted c p) : AddressesQUD c.qud p

@[implicit_reducible]

instance Semantics.Highlighting.instDecidableHighlightedOfMemSetSalientOfAddressesQUDQud {W : Type u_1} (c : HighlightingContext W) (p : Set W) [Decidable (p ∈ c.salient)] [Decidable (AddressesQUD c.qud p)] : Decidable (Highlighted c p)

Equations

• Semantics.Highlighting.instDecidableHighlightedOfMemSetSalientOfAddressesQUDQud c p = Semantics.Highlighting.instDecidableHighlightedOfMemSetSalientOfAddressesQUDQud._aux_1 c p

def Semantics.Highlighting.empty {W : Type u_1} : HighlightingContext W

The empty highlighting context: no salient propositions, the trivial QUD that is resolved by anything.

Equations

• Semantics.Highlighting.empty = { salient := ∅, qud := Core.Question.declarative Set.univ }

def Semantics.Highlighting.singleton {W : Type u_1} (p : Set W) : HighlightingContext W

A highlighting context built from a single salient proposition that declaratively resolves its own QUD.

Equations

• Semantics.Highlighting.singleton p = { salient := {p}, qud := Core.Question.declarative p }

def Semantics.Highlighting.addSalient {W : Type u_1} (c : HighlightingContext W) (p : Set W) : HighlightingContext W

Add a proposition to the salient set without touching the QUD.

Equations

• Semantics.Highlighting.addSalient c p = { salient := insert p c.salient, qud := c.qud }

@[simp]

theorem Semantics.Highlighting.mem_salient_addSalient {W : Type u_1} (c : HighlightingContext W) (p q : Set W) : q ∈ (addSalient c p).salient ↔ q = p ∨ q ∈ c.salient

@[simp]

theorem Semantics.Highlighting.qud_addSalient {W : Type u_1} (c : HighlightingContext W) (p : Set W) : (addSalient c p).qud = c.qud

@[simp]

theorem Semantics.Highlighting.salient_singleton {W : Type u_1} (p : Set W) : (singleton p).salient = {p}

@[simp]

theorem Semantics.Highlighting.qud_singleton {W : Type u_1} (p : Set W) : (singleton p).qud = Core.Question.declarative p

@cite{roelofsen-farkas-2015}: polarity particles

inductive Semantics.Highlighting.ResponseParticle : Type

@cite{roelofsen-farkas-2015}'s polarity-particle response slot.

agree (English yes, German ja, Romance sí/oui) confirms the highlighted proposition; reverse (English no, German nein, Romance no/non) commits to its (set-theoretic) complement.

The two-cell taxonomy is the cross-linguistic minimum; English/German elaborate it with intonation, Polish/Czech and Mandarin add further morphology — extensions live in study files, not here.

• agree : ResponseParticle
• reverse : ResponseParticle

@[implicit_reducible]

instance Semantics.Highlighting.instDecidableEqResponseParticle : DecidableEq ResponseParticle

Equations

• Semantics.Highlighting.instDecidableEqResponseParticle x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Highlighting.instReprResponseParticle.repr : ResponseParticle → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Highlighting.instReprResponseParticle : Repr ResponseParticle

Equations

• Semantics.Highlighting.instReprResponseParticle = { reprPrec := Semantics.Highlighting.instReprResponseParticle.repr }

@[implicit_reducible]

instance Semantics.Highlighting.instInhabitedResponseParticle : Inhabited ResponseParticle

Equations

• Semantics.Highlighting.instInhabitedResponseParticle = { default := Semantics.Highlighting.instInhabitedResponseParticle.default }

def Semantics.Highlighting.instInhabitedResponseParticle.default : ResponseParticle

Equations

• Semantics.Highlighting.instInhabitedResponseParticle.default = Semantics.Highlighting.ResponseParticle.agree

def Semantics.Highlighting.ResponseParticle.commitment {W : Type u_1} (r : ResponseParticle) (p : Set W) : Set W

The proposition committed to by a polarity-particle response, given a highlighted proposition p. agree projects to p; reverse projects to pᶜ (set-theoretic complement).

Equations

• Semantics.Highlighting.ResponseParticle.agree.commitment p = p
• Semantics.Highlighting.ResponseParticle.reverse.commitment p = pᶜ

@[simp]

theorem Semantics.Highlighting.ResponseParticle.commitment_agree {W : Type u_1} (p : Set W) : agree.commitment p = p

@[simp]

theorem Semantics.Highlighting.ResponseParticle.commitment_reverse {W : Type u_1} (p : Set W) : reverse.commitment p = pᶜ

theorem Semantics.Highlighting.ResponseParticle.commitment_inter_eq_empty {W : Type u_1} (p : Set W) : agree.commitment p ∩ reverse.commitment p = ∅

The two response particles disagree on every world: agree commits to p, reverse commits to pᶜ, and these partition Set.univ.