Backgrounded Constituents Are Islands

@cite{kratzer-selkirk-2020} @cite{lu-pan-degen-2025} @cite{roberts-2012} @cite{goldberg-2006}

Formalization of the discourse-backgroundedness account of manner-of-speaking (MoS) island effects, following @cite{lu-pan-degen-2025}.

Core Argument

MoS verbs (whisper, shout, etc.) decompose into SAY + MANNER. The manner component activates a salient alternative set that addresses the QUD, foregrounding the verb and — by the single-QUD-at-a-time constraint — backgrounding the complement. Backgrounded constituents resist wh-extraction, producing the island effect.

Formal Strategy

Communication events have two semantic dimensions: manner and content. The active QUD (from Core/QUD.lean) partitions events along one dimension, foregrounding it and backgrounding the other. We derive:

1. Manner QUD → content is invisible to the partition → content is backgrounded
2. Content QUD → manner is invisible → content is foregrounded
3. Verb with manner weight → manner QUD is default → island effect
4. Prosodic focus on embedded object → overrides to content QUD → amelioration
5. Adding manner adverb to bridge verb → acquires manner weight → replicates island

Grounding

• Paper def (3) "foregrounded" = QUD projection (Core/QUD.lean : QUD.ofDecEq)
• Paper "backgrounded" = K&S DiscourseStatus.given (Core/InformationStructure.lean)
• Rooth FIP / Q-A congruence (imported from Focus/Interpretation.lean) = QUD cell membership; qaCongruentWeak derives that extracted fillers are focused (§4 Route 2)

§1. Verb Decomposition

MoS verbs are lexically composed of a light verb SAY and a manner component:

whisper = SAY + [whispering manner]
shout = SAY + [shouting manner]
say = SAY (no manner — bridge verb)

The manner component is what makes MoS verbs lexically "heavier" and activates manner alternatives that can address the QUD. Bridge verbs like say lack this component and so do not activate manner alternatives by default.

structure Semantics.Focus.BackgroundedIslands.MannerComponent : Type

A manner-of-speaking component. The specific manner (whispering, shouting, etc.) is what generates the alternative set: {say in manner m₁, say in manner m₂,...}.

• name : String

def Semantics.Focus.BackgroundedIslands.instDecidableEqMannerComponent.decEq (x✝ x✝¹ : MannerComponent) : Decidable (x✝ = x✝¹)

Equations

• Semantics.Focus.BackgroundedIslands.instDecidableEqMannerComponent.decEq { name := a } { name := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.Focus.BackgroundedIslands.instDecidableEqMannerComponent : DecidableEq MannerComponent

Equations

• Semantics.Focus.BackgroundedIslands.instDecidableEqMannerComponent = Semantics.Focus.BackgroundedIslands.instDecidableEqMannerComponent.decEq

def Semantics.Focus.BackgroundedIslands.instReprMannerComponent.repr : MannerComponent → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Focus.BackgroundedIslands.instReprMannerComponent : Repr MannerComponent

Equations

• Semantics.Focus.BackgroundedIslands.instReprMannerComponent = { reprPrec := Semantics.Focus.BackgroundedIslands.instReprMannerComponent.repr }

structure Semantics.Focus.BackgroundedIslands.VerbDecomp : Type

Lexical decomposition of a communication verb.

MoS verbs have manner = some _; bridge verbs have manner = none. The mannerAdverb field captures the "say + adverb" construction from Experiment 3: adding a manner adverb to say gives it manner weight.

• lightVerb : String

  The light verb component (always SAY for communication verbs)

• manner : Option MannerComponent

  Lexical manner component — present for MoS verbs, absent for bridge verbs

• mannerAdverb : Option String

  Manner adverb (for "say softly" constructions)

@[implicit_reducible]

instance Semantics.Focus.BackgroundedIslands.instReprVerbDecomp : Repr VerbDecomp

Equations

• Semantics.Focus.BackgroundedIslands.instReprVerbDecomp = { reprPrec := Semantics.Focus.BackgroundedIslands.instReprVerbDecomp.repr }

def Semantics.Focus.BackgroundedIslands.instReprVerbDecomp.repr : VerbDecomp → ℕ → Std.Format

Equations

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

def Semantics.Focus.BackgroundedIslands.VerbDecomp.hasMannerWeight (v : VerbDecomp) : Prop

A verb has manner weight if it has either a lexical manner component (MoS verbs) or a manner adverb ("say softly"). This is the property that determines default QUD selection and therefore backgroundedness.

Equations

• v.hasMannerWeight = (v.manner ≠ none ∨ v.mannerAdverb ≠ none)

@[implicit_reducible]

instance Semantics.Focus.BackgroundedIslands.VerbDecomp.instDecidableHasMannerWeight (v : VerbDecomp) : Decidable v.hasMannerWeight

Equations

• v.instDecidableHasMannerWeight = Semantics.Focus.BackgroundedIslands.VerbDecomp.instDecidableHasMannerWeight._aux_1 v

def Semantics.Focus.BackgroundedIslands.whisperDecomp : VerbDecomp

Equations

• Semantics.Focus.BackgroundedIslands.whisperDecomp = { manner := some { name := "whispering" } }

def Semantics.Focus.BackgroundedIslands.shoutDecomp : VerbDecomp

Equations

• Semantics.Focus.BackgroundedIslands.shoutDecomp = { manner := some { name := "shouting" } }

def Semantics.Focus.BackgroundedIslands.sayDecomp : VerbDecomp

Equations

• Semantics.Focus.BackgroundedIslands.sayDecomp = { }

def Semantics.Focus.BackgroundedIslands.saySoftlyDecomp : VerbDecomp

Equations

• Semantics.Focus.BackgroundedIslands.saySoftlyDecomp = { mannerAdverb := some "softly" }

§2. Two-Dimensional Communication Events and QUD Projections

A communication event has two semantic dimensions: the manner of communication (how it was said) and the propositional content (what was said). The QUD determines which dimension is "at issue."

The paper's definition (3) — FOREGROUNDED iff the alternative set relative to C is a subset of Q-alternatives determined by the QUD — corresponds formally to whether the QUD projects onto that dimension: if the QUD partitions events by manner, then manner is foregrounded (it distinguishes Q-alternatives) and content is backgrounded (it doesn't).

inductive Semantics.Focus.BackgroundedIslands.CommDimension : Type

Dimension of a communication utterance that the QUD can target.

• manner : CommDimension

  QUD asks about manner: "How/In what way did John say it?"

• content : CommDimension

  QUD asks about content: "What did John say?"

@[implicit_reducible]

instance Semantics.Focus.BackgroundedIslands.instDecidableEqCommDimension : DecidableEq CommDimension

Equations

• Semantics.Focus.BackgroundedIslands.instDecidableEqCommDimension x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Focus.BackgroundedIslands.instReprCommDimension.repr : CommDimension → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Focus.BackgroundedIslands.instReprCommDimension : Repr CommDimension

Equations

• Semantics.Focus.BackgroundedIslands.instReprCommDimension = { reprPrec := Semantics.Focus.BackgroundedIslands.instReprCommDimension.repr }

structure Semantics.Focus.BackgroundedIslands.CommEvent (Manner Content : Type) : Type

A communication event has two semantic dimensions. This mirrors the verb decomposition: MoS verbs make both dimensions available, while bridge verbs foreground only content.

• manner : Manner
• content : Content

@[implicit_reducible]

instance Semantics.Focus.BackgroundedIslands.instBEqCommEvent {Manner Content : Type} [BEq Manner] [BEq Content] : BEq (CommEvent Manner Content)

Equations

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

def Semantics.Focus.BackgroundedIslands.mannerQUD {Manner Content : Type} [DecidableEq Manner] : QUD (CommEvent Manner Content)

The manner QUD: partitions communication events by HOW something was said. "In what manner did John say that Mary was in the courtyard?"

Under this QUD, events with the same manner are equivalent regardless of content — content variation is invisible, hence content is backgrounded.

Built using QUD.ofDecEq from Core/QUD.lean.

Equations

• Semantics.Focus.BackgroundedIslands.mannerQUD = QUD.ofDecEq (fun (x : Semantics.Focus.BackgroundedIslands.CommEvent Manner Content) => x.manner) "manner"

def Semantics.Focus.BackgroundedIslands.contentQUD {Manner Content : Type} [DecidableEq Content] : QUD (CommEvent Manner Content)

The content QUD: partitions communication events by WHAT was said. "What did John say?"

Under this QUD, events with the same content are equivalent regardless of manner — manner variation is invisible, hence manner is backgrounded.

Built using QUD.ofDecEq from Core/QUD.lean.

Equations

• Semantics.Focus.BackgroundedIslands.contentQUD = QUD.ofDecEq (fun (x : Semantics.Focus.BackgroundedIslands.CommEvent Manner Content) => x.content) "content"

§3. Core Theorems: QUD Determines Backgroundedness

These theorems formalize the paper's central claim: the QUD determines which dimension of a communication event is foregrounded (participates in the QUD partition) and which is backgrounded (invisible to the partition).

theorem Semantics.Focus.BackgroundedIslands.manner_qud_ignores_content {Manner Content : Type} [DecidableEq Manner] (e1 e2 : CommEvent Manner Content) (h : e1.manner = e2.manner) : mannerQUD.r e1 e2

Manner QUD ignores content: Under the manner QUD, events with the same manner are equivalent regardless of their content.

This is the formal heart of the paper: content is invisible to the manner QUD partition, which is exactly what "backgrounded" means — the content doesn't participate in distinguishing Q-alternatives.

theorem Semantics.Focus.BackgroundedIslands.content_qud_ignores_manner {Manner Content : Type} [DecidableEq Content] (e1 e2 : CommEvent Manner Content) (h : e1.content = e2.content) : contentQUD.r e1 e2

Content QUD ignores manner: Under the content QUD, events with the same content are equivalent regardless of manner.

theorem Semantics.Focus.BackgroundedIslands.backgroundedness_means_qud_invisible {Manner Content : Type} [DecidableEq Manner] (e : CommEvent Manner Content) (c' : Content) : mannerQUD.r e { manner := e.manner, content := c' }

Backgroundedness = QUD invisibility: Varying the content of a communication event does not change its QUD cell under the manner QUD.

Formally: for any event e and any alternative content c', the event ⟨e.manner, c'⟩ is in the same manner-QUD cell as e. This means the content dimension is "invisible" to the partition — it is backgrounded.

This directly formalizes the paper's claim that elements in MoS verb complements are discourse-backgrounded.

theorem Semantics.Focus.BackgroundedIslands.backgrounded_content_same_cell {Manner Content : Type} [DecidableEq Manner] [BEq Manner] [BEq Content] (e : CommEvent Manner Content) (c' : Content) : { manner := e.manner, content := c' } ∈ mannerQUD.cell e

Backgrounded content is in the same QUD cell (set-membership version).

theorem Semantics.Focus.BackgroundedIslands.foregrounding_is_qud_projection_manner {Manner Content : Type} [DecidableEq Manner] (e1 e2 : CommEvent Manner Content) (h : mannerQUD.r e1 e2) : e1.manner = e2.manner

Foregrounding is QUD projection (manner direction): events in the same manner-QUD cell must agree on manner. That is, manner distinguishes Q-alternatives — it is foregrounded.

This is the converse of manner_qud_ignores_content: while content is invisible to the manner QUD, manner is NOT invisible — it's what the partition is about.

theorem Semantics.Focus.BackgroundedIslands.foregrounding_is_qud_projection_content {Manner Content : Type} [DecidableEq Content] (e1 e2 : CommEvent Manner Content) (h : contentQUD.r e1 e2) : e1.content = e2.content

Foregrounding is QUD projection (content direction): events in the same content-QUD cell must agree on content.

theorem Semantics.Focus.BackgroundedIslands.manner_content_qud_distinct {Manner Content : Type} [DecidableEq Manner] [DecidableEq Content] (e1 e2 : CommEvent Manner Content) (h_same_manner : e1.manner = e2.manner) (h_diff_content : e1.content ≠ e2.content) : mannerQUD.r e1 e2 ∧ ¬contentQUD.r e1 e2

Manner QUD and content QUD are genuinely distinct partitions. Events can be equivalent under one QUD but not the other. This is what makes the foregrounding/backgrounding complementarity non-trivial: you can't foreground both dimensions under a single QUD.

Formally: if two events share manner but differ in content, they are equivalent under the manner QUD but NOT under the content QUD.

§4. Deriving the Extraction Constraint

@cite{erteschik-shir-1973} @cite{roberts-1996} @cite{goldberg-2006}

The backgroundedness constraint on extraction — that backgrounded constituents resist wh-extraction — is not stipulated but derived from the QUD partition via two converging routes.

Route 1: Question relevance (@cite{roberts-1996})

Extraction creates a wh-question about the gap:

"What₁ did John whisper that Mary gave t₁ to Bill?"

Under the manner QUD, content variation is invisible (§3): all fillers produce events in the same QUD cell. The extraction question cannot be answered informatively — it is QUD-irrelevant, hence infelicitous.

Route 2: Information-structural clash (@cite{erteschik-shir-1973})

Wh-extraction creates a content QUD: "What₁ did John whisper t₁?" partitions events by the filler's value. By @cite{rooth-1992}'s Q-A congruence constraint (26d) — formalized as qaCongruentWeak in Focus/Interpretation.lean — the question's Hamblin denotation (the set of propositions obtained by varying the filler) must be ⊆ the answer's focus alternatives. Since focus alternatives are generated by substitution at the focused position, the filler position IS the focused position. So the extracted filler is [FoC].

But the extraction site is inside a backgrounded clause ([G]-marked under the verb's default manner QUD). A [FoC] element inside a [G] clause creates a clash: the filler addresses the extraction QUD but belongs to a dimension the verb's QUD ignores.

The underlying mechanism is QUD conflict: the extraction QUD (content) and the verb's default QUD (manner) assign incompatible statuses to the complement. The extraction QUD needs the filler to be focused; the verb's QUD backgrounds the entire complement.

Both routes derive the same prediction from the same QUD property (manner_qud_ignores_content): extraction from backgrounded clauses is degraded, and the degradation disappears when the QUD shifts to target content (prosodic amelioration).

def Semantics.Focus.BackgroundedIslands.contentQuestionRelevant {Manner Content : Type} (qud : QUD (CommEvent Manner Content)) : Prop

Whether a wh-question about the content of a communication event is relevant to a given QUD (@cite{roberts-1996}): different content values must produce events in different QUD cells. If not, the extraction question is vacuous — every filler gives the same QUD-level answer.

Equations

• Semantics.Focus.BackgroundedIslands.contentQuestionRelevant qud = ∃ (m : Manner) (c₁ : Content) (c₂ : Content), ¬qud.r { manner := m, content := c₁ } { manner := m, content := c₂ }

theorem Semantics.Focus.BackgroundedIslands.content_question_irrelevant_under_manner {Manner Content : Type} [DecidableEq Manner] : ¬contentQuestionRelevant mannerQUD

Under the manner QUD, content extraction questions are QUD-irrelevant: varying content never changes the QUD cell.

theorem Semantics.Focus.BackgroundedIslands.content_question_relevant_under_content {Manner Content : Type} [DecidableEq Content] (m : Manner) (c₁ c₂ : Content) (hne : c₁ ≠ c₂) : contentQuestionRelevant contentQUD

Under the content QUD, content extraction questions ARE QUD-relevant: different content values produce events in different QUD cells.

def Semantics.Focus.BackgroundedIslands.extractionQUD {Manner Content : Type} [DecidableEq Content] : QUD (CommEvent Manner Content)

The QUD established by wh-extraction from a communication verb's complement. "What₁ did John whisper t₁?" partitions events by the filler (= content dimension). (@cite{roberts-2012}: wh-questions establish QUDs.)

Equations

• Semantics.Focus.BackgroundedIslands.extractionQUD = Semantics.Focus.BackgroundedIslands.contentQUD

theorem Semantics.Focus.BackgroundedIslands.extraction_filler_varies {Manner Content : Type} [DecidableEq Content] (m : Manner) (c₁ c₂ : Content) (hne : c₁ ≠ c₂) : ¬extractionQUD.r { manner := m, content := c₁ } { manner := m, content := c₂ }

The extraction QUD partitions by content: different fillers produce different QUD cells. This is what makes the filler the focused element — it is the variable that distinguishes alternatives.

Combined with qaCongruentWeak from Focus/Interpretation.lean (@cite{rooth-1992} (26d): [ψ]° ⊆ [α]^f), this derives that extracted elements are [FoC]-marked: the question's alternatives (varying the filler) must be focus alternatives of the answer (varying the focused position), so filler position = focused position.

theorem Semantics.Focus.BackgroundedIslands.extraction_filler_is_focus_alternative {Manner Content : Type} {W : Type u_1} (den : CommEvent Manner Content → Set W) (m : Manner) (answerFocus extractionQ : FocusInterpretation.PropFocusValue W) (hq : ∀ (c : Content), den { manner := m, content := c } ∈ extractionQ) (hqa : FocusInterpretation.qaCongruentWeak answerFocus extractionQ) (c : Content) : den { manner := m, content := c } ∈ answerFocus

Q-A congruence applied to extraction (@cite{rooth-1992} (26d)): if Q-A congruence holds between the extraction question and the answer's focus value, then every filler produces a focus alternative of the answer.

This is the formal content of "the filler position = the focused position": the Hamblin question's alternatives (obtained by varying the filler) must be focus alternatives of the answer (obtained by varying the focused position), so these two positions coincide.

The theorem directly uses qaCongruentWeak from Focus/Interpretation.lean. Combined with extraction_filler_varies (different fillers → different QUD cells → non-trivial Hamblin alternatives), this derives that extraction foregrounds the filler.

def Semantics.Focus.BackgroundedIslands.extractedFillerStatus : Features.InformationStructure.FocusMark

The discourse status of the extracted filler: focused.

Derived from QUD structure + Q-A congruence, not stipulated:

1. Wh-extraction creates a content-QUD (extractionQUD, @cite{roberts-2012})
2. The filler distinguishes the extraction QUD's cells (extraction_filler_varies)
3. extraction_filler_is_focus_alternative (above) uses qaCongruentWeak (@cite{rooth-1992} (26d)) to show: if the extraction question's alternatives ⊆ the answer's focus value, then every filler is a focus alternative. Focus alternatives are generated at the focused position, so filler = focused.
4. Foreground = [FoC] in @cite{kratzer-selkirk-2020}'s two-feature system

Equations

• Semantics.Focus.BackgroundedIslands.extractedFillerStatus = Features.InformationStructure.FocusMark.focused

theorem Semantics.Focus.BackgroundedIslands.backgrounded_extraction_clashes : Comparability.extractionISClash extractedFillerStatus Features.BinaryGivenness.given

Extraction from a backgrounded clause creates an IS clash: the extracted filler is [FoC] (derived from extractedFillerStatus) but the clause is [G] (derived from the verb's default QUD).

Uses extractionISClash from Core/InformationStructure.lean, which unifies @cite{abeille-et-al-2020}'s FBC with @cite{erteschik-shir-1973}'s Dominance Condition.

theorem Semantics.Focus.BackgroundedIslands.atissue_extraction_compatible : ¬Comparability.extractionISClash extractedFillerStatus Features.BinaryGivenness.new

Extraction from an at-issue clause does NOT create a clash.

§5. Default QUD Selection: From Verbs to Backgroundedness

MoS verbs, due to their manner component, activate manner alternatives and make the manner QUD salient by default. Bridge verbs like say, lacking a manner component, default to the content QUD.

This follows from @cite{roberts-1996}: the QUD is determined by what alternatives are salient, and manner components activate manner alternatives.

def Semantics.Focus.BackgroundedIslands.defaultDimension (v : VerbDecomp) : CommDimension

Default QUD dimension based on verb properties. Verbs with manner weight activate the manner QUD (backgrounding content); verbs without manner weight activate the content QUD (foregrounding content).

Equations

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

def Semantics.Focus.BackgroundedIslands.complementStatus (dim : CommDimension) : Features.BinaryGivenness

Givenness of the complement content under a given QUD.

Under manner QUD: content is backgrounded (K&S [G]-marked, given). Under content QUD: content is foregrounded (new / at-issue).

Equations

• Semantics.Focus.BackgroundedIslands.complementStatus Semantics.Focus.BackgroundedIslands.CommDimension.manner = Features.BinaryGivenness.given
• Semantics.Focus.BackgroundedIslands.complementStatus Semantics.Focus.BackgroundedIslands.CommDimension.content = Features.BinaryGivenness.new

def Semantics.Focus.BackgroundedIslands.verbFocus (dim : CommDimension) : Features.InformationStructure.FocusMark

Focus marking of the matrix verb under a given QUD.

Under manner QUD: verb is foregrounded ([FoC], addresses QUD). Under content QUD: verb is non-focused.

Equations

• Semantics.Focus.BackgroundedIslands.verbFocus Semantics.Focus.BackgroundedIslands.CommDimension.manner = Features.InformationStructure.FocusMark.focused
• Semantics.Focus.BackgroundedIslands.verbFocus Semantics.Focus.BackgroundedIslands.CommDimension.content = Features.InformationStructure.FocusMark.nonFocused

def Semantics.Focus.BackgroundedIslands.verbGivenness (dim : CommDimension) : Features.BinaryGivenness

Givenness of the matrix verb under a given QUD.

Under manner QUD: verb is at-issue (new — addresses the QUD). Under content QUD: verb is backgrounded (given).

Equations

• Semantics.Focus.BackgroundedIslands.verbGivenness Semantics.Focus.BackgroundedIslands.CommDimension.manner = Features.BinaryGivenness.new
• Semantics.Focus.BackgroundedIslands.verbGivenness Semantics.Focus.BackgroundedIslands.CommDimension.content = Features.BinaryGivenness.given

§6. The MoS Island Effect: Main Derivation

The full derivation chain:

1. MoS verb has manner weight (lexical decomposition, §1)
2. Manner weight → default QUD dimension is manner (§5 defaultDimension)
3. Manner QUD → complement is backgrounded (§5 complementStatus)
4. Backgrounded → extraction question QUD-irrelevant (§4 Route 1)
5. Backgrounded → extraction creates information-structural clash (§4 Route 2)

Steps 4 and 5 are derived in §4 from manner_qud_ignores_content. DiscourseStatus.rank from Core/InformationStructure.lean provides the ordinal ranking consistent with this derivation.

theorem Semantics.Focus.BackgroundedIslands.mos_island_effect (v : VerbDecomp) (h : v.hasMannerWeight) : complementStatus (defaultDimension v) = Features.BinaryGivenness.given

MoS Island Effect: MoS verbs default-background their complements.

theorem Semantics.Focus.BackgroundedIslands.bridge_verb_transparent (v : VerbDecomp) (h : ¬v.hasMannerWeight) : complementStatus (defaultDimension v) = Features.BinaryGivenness.new

Bridge Verb Transparency: Bridge verbs default to the content QUD.

theorem Semantics.Focus.BackgroundedIslands.qud_conflict (v : VerbDecomp) (h : v.hasMannerWeight) : complementStatus (defaultDimension v) = Features.BinaryGivenness.given ∧ complementStatus CommDimension.content = Features.BinaryGivenness.new

QUD conflict (§4 Route 2): the extraction QUD and the verb's default QUD assign incompatible statuses to the complement content.

• Extraction QUD (content) → content is at-issue, filler is focused
• Verb's default QUD (manner) → content is backgrounded

The IS clash arises because the verb's manner QUD backgrounds the entire complement, but extraction needs the filler to be focused within it.

theorem Semantics.Focus.BackgroundedIslands.mos_extraction_clashes (v : VerbDecomp) (h : v.hasMannerWeight) : Comparability.extractionISClash extractedFillerStatus (complementStatus (defaultDimension v))

MoS verbs trigger the information-structural clash (§4 Route 2): filler is [FoC] (derived via extractedFillerStatus), complement is [G].

theorem Semantics.Focus.BackgroundedIslands.bridge_no_extraction_clash (v : VerbDecomp) (h : ¬v.hasMannerWeight) : ¬Comparability.extractionISClash extractedFillerStatus (complementStatus (defaultDimension v))

Bridge verbs do NOT trigger the clash: complement is [new], not [G].

§7. Prosodic Amelioration (Experiments 1 & 3b)

Prosodic focus ([FoC]) on the embedded object overrides the default manner QUD, forcing the content QUD. Under the content QUD, content extraction questions are QUD-relevant (§4 content_question_relevant_under_content), restoring extraction felicity.

This is predicted by the backgroundedness account and NOT by the subjacency or frequency accounts: prosody changes information structure without changing syntactic structure or verb-frame frequency.

def Semantics.Focus.BackgroundedIslands.activeDimension (v : VerbDecomp) (embeddedObjectFocused : Bool) : CommDimension

Active QUD dimension after prosodic manipulation.

Prosodic [FoC] on the embedded object makes the content dimension salient, overriding the default manner QUD. This models the capitalization/bolding manipulation in Experiments 1 and 3b.

Equations

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

theorem Semantics.Focus.BackgroundedIslands.prosodic_focus_ameliorates (v : VerbDecomp) : activeDimension v true = CommDimension.content

Prosodic Amelioration Theorem: Focusing the embedded object always results in the content QUD, regardless of verb type.

This captures Experiments 1 and 3b: prosodic focus on the embedded object ameliorates the island effect for both MoS verbs and say+adverb.

theorem Semantics.Focus.BackgroundedIslands.focused_complement_not_backgrounded (v : VerbDecomp) : complementStatus (activeDimension v true) = Features.BinaryGivenness.new

Under prosodic focus, complement is not backgrounded.

theorem Semantics.Focus.BackgroundedIslands.prosodic_focus_resolves_clash (v : VerbDecomp) : ¬Comparability.extractionISClash extractedFillerStatus (complementStatus (activeDimension v true))

Prosodic focus resolves the information-structural clash: under embedded focus, the complement is [new] (not [G]), so the filler's [FoC] status no longer clashes. This is why prosodic amelioration works.

theorem Semantics.Focus.BackgroundedIslands.unfocused_mos_complement_backgrounded (v : VerbDecomp) (h : v.hasMannerWeight) : complementStatus (activeDimension v false) = Features.BinaryGivenness.given

Without prosodic focus, MoS verb complements ARE backgrounded.

theorem Semantics.Focus.BackgroundedIslands.amelioration_improves_extraction : (complementStatus CommDimension.manner).rank > (complementStatus CommDimension.content).rank

Amelioration improves extraction: Extraction from prosodically focused complement is better than extraction from default-backgrounded complement. Stated as complementStatus .manner > complementStatus .content on BinaryGivenness.rank because BinaryGivenness orders by salience (.given = 1 > .new = 0) — content is at-issue (.new, lower givenness rank), manner is backgrounded (.given, higher rank), and "more backgrounded" predicts "harder extraction".

theorem Semantics.Focus.BackgroundedIslands.mos_focus_sensitivity (v : VerbDecomp) (h : v.hasMannerWeight) : (complementStatus (activeDimension v false)).rank > (complementStatus (activeDimension v true)).rank

Focus sensitivity for MoS verbs: Prosodic focus changes the extraction prediction for MoS verbs from degraded (backgrounded) to acceptable (new). Direction note: see amelioration_improves_extraction — BinaryGivenness ranks given > new, so the more-backgrounded-default outranks the prosodically-focused alternative.

§8. Say + Adverb Replication (Experiment 3)

The paper's key novel prediction: adding a manner adverb to say gives it manner weight, shifting the default QUD to manner and replicating the MoS island effect.

"say softly" = say + manner adverb → manner weight → manner QUD → island
"say" = say (no modifier) → no manner weight → content QUD → no island

This uniquely distinguishes the backgroundedness account:

• Subjacency: same CP structure ± adverb → no contrast predicted
• Frequency: would need to check corpus counts; n.s. in the data
• Backgroundedness: manner adverb adds manner weight → predicts contrast ✓

theorem Semantics.Focus.BackgroundedIslands.say_no_manner_weight : ¬sayDecomp.hasMannerWeight

say has no manner weight.

theorem Semantics.Focus.BackgroundedIslands.say_softly_has_manner_weight : saySoftlyDecomp.hasMannerWeight

say softly has manner weight (from the adverb).

theorem Semantics.Focus.BackgroundedIslands.whisper_has_manner_weight : whisperDecomp.hasMannerWeight

whisper has manner weight (from lexical decomposition).

theorem Semantics.Focus.BackgroundedIslands.shout_has_manner_weight : shoutDecomp.hasMannerWeight

shout has manner weight (from lexical decomposition).

theorem Semantics.Focus.BackgroundedIslands.say_adverb_replicates_mos : complementStatus (defaultDimension saySoftlyDecomp) = complementStatus (defaultDimension whisperDecomp)

Say+Adverb Replication Theorem: Adding a manner adverb to say produces the same complement backgroundedness as MoS verbs.

say softly and whisper both have manner weight, so they both default to the manner QUD, backgrounding their complements identically.

theorem Semantics.Focus.BackgroundedIslands.say_vs_say_softly_status : complementStatus (defaultDimension sayDecomp) ≠ complementStatus (defaultDimension saySoftlyDecomp)

say and say softly differ in complement backgroundedness.

theorem Semantics.Focus.BackgroundedIslands.say_vs_say_softly_acceptability : (complementStatus (defaultDimension saySoftlyDecomp)).rank > (complementStatus (defaultDimension sayDecomp)).rank

say extraction is better than say softly extraction. Stated as say softly > say on BinaryGivenness.rank because rank orders by salience: say softly's complement is .given (rank 1, more backgrounded), say's complement is .new (rank 0, at-issue); higher rank = more backgrounded = harder extraction.

theorem Semantics.Focus.BackgroundedIslands.say_adverb_focus_sensitive : (complementStatus (activeDimension saySoftlyDecomp false)).rank > (complementStatus (activeDimension saySoftlyDecomp true)).rank

The say+adverb island is also focus-sensitive (like the MoS island). Direction: prosodically focused complement is .new (rank 0); the unfocused default is .given (rank 1).

§9. Theory Comparison

Three accounts of the MoS island effect make different predictions. Only the backgroundedness account correctly predicts all five experiments' results.

inductive Semantics.Focus.BackgroundedIslands.MoSAccount : Type

Accounts of the MoS island effect.

• subjacency : MoSAccount

  Structural: MoS verbs select complex-NP complements.

• verbFrameFrequency : MoSAccount

  Processing: low verb-frame frequency → high surprisal.

• backgroundedness : MoSAccount

  Discourse: backgrounded complements resist extraction.

@[implicit_reducible]

instance Semantics.Focus.BackgroundedIslands.instDecidableEqMoSAccount : DecidableEq MoSAccount

Equations

• Semantics.Focus.BackgroundedIslands.instDecidableEqMoSAccount x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.Focus.BackgroundedIslands.instReprMoSAccount : Repr MoSAccount

Equations

• Semantics.Focus.BackgroundedIslands.instReprMoSAccount = { reprPrec := Semantics.Focus.BackgroundedIslands.instReprMoSAccount.repr }

def Semantics.Focus.BackgroundedIslands.instReprMoSAccount.repr : MoSAccount → ℕ → Std.Format

Equations

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

structure Semantics.Focus.BackgroundedIslands.Prediction : Type

Testable predictions of each account.

The three accounts make divergent predictions for three key manipulations, allowing empirical discrimination.

• focusSensitive : Bool

  Does prosodic focus affect extraction acceptability? (Tested in Experiments 1, 2a, 3b)

• sayAdverbCreatesIsland : Bool

  Does say + manner adverb create an island? (Tested in Experiment 3a)

• frequencyCorrelation : Bool

  Does verb-frame frequency correlate with acceptability? (Tested in all experiments)

def Semantics.Focus.BackgroundedIslands.instDecidableEqPrediction.decEq (x✝ x✝¹ : Prediction) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Semantics.Focus.BackgroundedIslands.instDecidableEqPrediction : DecidableEq Prediction

Equations

• Semantics.Focus.BackgroundedIslands.instDecidableEqPrediction = Semantics.Focus.BackgroundedIslands.instDecidableEqPrediction.decEq

def Semantics.Focus.BackgroundedIslands.instReprPrediction.repr : Prediction → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Focus.BackgroundedIslands.instReprPrediction : Repr Prediction

Equations

• Semantics.Focus.BackgroundedIslands.instReprPrediction = { reprPrec := Semantics.Focus.BackgroundedIslands.instReprPrediction.repr }

def Semantics.Focus.BackgroundedIslands.accountPredictions : MoSAccount → Prediction

Predictions of each account.

Equations

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

def Semantics.Focus.BackgroundedIslands.empiricalResults : Prediction

Empirical results from @cite{lu-pan-degen-2025}.

Equations

• Semantics.Focus.BackgroundedIslands.empiricalResults = { focusSensitive := true, sayAdverbCreatesIsland := true, frequencyCorrelation := false }

def Semantics.Focus.BackgroundedIslands.accountScore (a : MoSAccount) : ℕ

Score: number of correct predictions.

Equations

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

theorem Semantics.Focus.BackgroundedIslands.backgroundedness_perfect_score : accountScore MoSAccount.backgroundedness = 3

The backgroundedness account matches all empirical results (3/3).

theorem Semantics.Focus.BackgroundedIslands.subjacency_score : accountScore MoSAccount.subjacency = 1

The subjacency account scores 1/3 (only no-frequency-correlation).

theorem Semantics.Focus.BackgroundedIslands.frequency_score : accountScore MoSAccount.verbFrameFrequency = 0

The frequency account scores 0/3 (all predictions wrong).

theorem Semantics.Focus.BackgroundedIslands.backgroundedness_dominates : accountScore MoSAccount.backgroundedness > accountScore MoSAccount.subjacency ∧ accountScore MoSAccount.backgroundedness > accountScore MoSAccount.verbFrameFrequency

The backgroundedness account strictly dominates both alternatives.

§10. Grounding in Linglib Infrastructure

These theorems connect the paper's theoretical definitions to existing linglib formalization, establishing that this is not an isolated theory but a natural extension of the QUD and information-structure framework.

theorem Semantics.Focus.BackgroundedIslands.foregrounding_iff_qud_manner {Manner Content : Type} [DecidableEq Manner] (e1 e2 : CommEvent Manner Content) : mannerQUD.r e1 e2 ↔ e1.manner = e2.manner

Foregrounding = QUD cell membership (biconditional, manner direction).

The paper defines (def 3): "C is foregrounded iff Alt(C) ⊆ Q-alternatives."

In our formalization: a dimension is foregrounded under a QUD iff the QUD projects onto it — same-cell events agree on that dimension, and conversely, agreeing on that dimension suffices for same-cell membership.

This biconditional shows that our QUD.ofDecEq model exactly captures the paper's notion of foregrounding.

theorem Semantics.Focus.BackgroundedIslands.foregrounding_iff_qud_content {Manner Content : Type} [DecidableEq Content] (e1 e2 : CommEvent Manner Content) : contentQUD.r e1 e2 ↔ e1.content = e2.content

Foregrounding = QUD cell membership (biconditional, content direction).

theorem Semantics.Focus.BackgroundedIslands.qud_complementarity : (verbFocus CommDimension.manner = Features.InformationStructure.FocusMark.focused ∧ complementStatus CommDimension.manner = Features.BinaryGivenness.given) ∧ verbGivenness CommDimension.content = Features.BinaryGivenness.given ∧ complementStatus CommDimension.content = Features.BinaryGivenness.new

QUD complementarity: Under manner QUD, manner is foregrounded ([FoC]) and content is backgrounded ([G]). Under content QUD, vice versa.

This connects to @cite{kratzer-selkirk-2020}'s insight that [FoC] and [G] are mutually exclusive features — you can't foreground and background the same dimension simultaneously. Extended here to cross-dimensional complementarity: foregrounding one dimension of a communication event necessarily backgrounds the other, given the single-QUD-at-a-time constraint.

theorem Semantics.Focus.BackgroundedIslands.backgroundedness_is_given : complementStatus CommDimension.manner = Features.BinaryGivenness.given

Backgroundedness = BinaryGivenness.given: The paper's notion of "backgrounded" maps directly to Kratzer & Selkirk's [G]-marked status, which is the Prince hearer-status given value in the new substrate.

theorem Semantics.Focus.BackgroundedIslands.foregrounding_is_focused : verbFocus CommDimension.manner = Features.InformationStructure.FocusMark.focused

Foregrounding = FocusMark.focused: The paper's notion of "foregrounded" maps to Kratzer & Selkirk's [FoC]-marked status, which is the binary-focus axis value in the new substrate.

§11. Gradient Manner Weight: Lexical vs. Compositional

@cite{lu-pan-degen-2025} Experiment 2a shows a residual difference between MoS verbs and say even under identical prosodic manipulation: MoS verb complements are more opaque to extraction than say complements (β = −0.08, p < 0.001), and this holds even when both are prosodically foregrounded.

We extend the binary model to distinguish the source of manner weight. Lexical manner (inherent to the verb root) produces stronger default backgroundedness than compositional manner (added by adverbial modification). This is a theoretical extension, not directly stated in the paper, but it accounts for the residual MoS > say+adverb difference the paper leaves as an open question (Experiment 2a discussion, p. 641).

inductive Semantics.Focus.BackgroundedIslands.MannerWeightSource : Type

Source of manner weight in a communication verb.

Lexical manner weight (MoS verbs) is stronger than compositional manner weight (say+adverb) because lexical manner is part of the verb's root meaning and therefore more reliably activates manner alternatives.

• lexical : MannerWeightSource

  Manner encoded in the verb root (MoS verbs: whisper, shout, ...). Automatically activates manner alternatives in all contexts.

• compositional : MannerWeightSource

  Manner added by adverbial modification (say softly, say loudly). Activates manner alternatives only when the adverb is salient.

• none : MannerWeightSource

  No manner component (bridge verbs: say, tell).

@[implicit_reducible]

instance Semantics.Focus.BackgroundedIslands.instDecidableEqMannerWeightSource : DecidableEq MannerWeightSource

Equations

• Semantics.Focus.BackgroundedIslands.instDecidableEqMannerWeightSource x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.Focus.BackgroundedIslands.instReprMannerWeightSource : Repr MannerWeightSource

Equations

• Semantics.Focus.BackgroundedIslands.instReprMannerWeightSource = { reprPrec := Semantics.Focus.BackgroundedIslands.instReprMannerWeightSource.repr }

def Semantics.Focus.BackgroundedIslands.instReprMannerWeightSource.repr : MannerWeightSource → ℕ → Std.Format

Equations

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

def Semantics.Focus.BackgroundedIslands.VerbDecomp.mannerWeightSource (v : VerbDecomp) : MannerWeightSource

Derive manner weight source from verb decomposition.

Equations

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

def Semantics.Focus.BackgroundedIslands.MannerWeightSource.rank : MannerWeightSource → Fin 3

Ordinal ranking of manner weight strength. Captures the prediction that lexical > compositional > none in default backgrounding of complements.

Equations

• Semantics.Focus.BackgroundedIslands.MannerWeightSource.none.rank = 0
• Semantics.Focus.BackgroundedIslands.MannerWeightSource.compositional.rank = 1
• Semantics.Focus.BackgroundedIslands.MannerWeightSource.lexical.rank = 2

theorem Semantics.Focus.BackgroundedIslands.whisper_lexical : whisperDecomp.mannerWeightSource = MannerWeightSource.lexical

theorem Semantics.Focus.BackgroundedIslands.shout_lexical : shoutDecomp.mannerWeightSource = MannerWeightSource.lexical

theorem Semantics.Focus.BackgroundedIslands.say_softly_compositional : saySoftlyDecomp.mannerWeightSource = MannerWeightSource.compositional

theorem Semantics.Focus.BackgroundedIslands.say_none_source : sayDecomp.mannerWeightSource = MannerWeightSource.none

theorem Semantics.Focus.BackgroundedIslands.MannerWeightSource.rank_injective (a b : MannerWeightSource) (h : a.rank = b.rank) : a = b

MannerWeightSource.rank is injective: distinct sources have distinct ranks. Subsumes the pairwise chain lexical_rank_gt_compositional / compositional_rank_gt_none.

theorem Semantics.Focus.BackgroundedIslands.manner_weight_source_consistent (v : VerbDecomp) : v.mannerWeightSource ≠ MannerWeightSource.none ↔ v.hasMannerWeight

Any manner weight (lexical or compositional) yields hasMannerWeight. The binary and gradient models are consistent.

§12. Backgroundedness–Projectivity Dissociation

@cite{tonhauser-beaver-degen-2018} show that projectivity and at-issueness are anti-correlated (r = .85–.99): content that is not at-issue tends to project. Backgroundedness, in the sense of @cite{lu-pan-degen-2025}, implies low at-issueness and therefore predicts projectivity.

But the converse fails: projectivity does not imply backgroundedness. The complements of factive verbs like notice and discover are projective (presupposed) but NOT discourse-backgrounded — they can be at-issue and are extractable. This dissociation is what makes backgroundedness, not projectivity, the correct predictor of extraction resistance.

structure Semantics.Focus.BackgroundedIslands.ExtractionProfile : Type

The three properties relevant to extraction: backgroundedness, projectivity, and extraction resistance. Backgroundedness determines extraction resistance; projectivity is independent. Consistency with the §16 prediction API is verified per-profile by mos_profile_consistent, factive_profile_consistent, and bridge_profile_consistent below §15.

• backgrounded : Bool

  Content is discourse-backgrounded (not at-issue per QUD)

• projective : Bool

  Content projects under operators (negation, modals, conditionals)

• resistsExtraction : Bool

  Extraction from the clause is degraded

@[implicit_reducible]

instance Semantics.Focus.BackgroundedIslands.instDecidableEqExtractionProfile : DecidableEq ExtractionProfile

Equations

• Semantics.Focus.BackgroundedIslands.instDecidableEqExtractionProfile = Semantics.Focus.BackgroundedIslands.instDecidableEqExtractionProfile.decEq

def Semantics.Focus.BackgroundedIslands.instDecidableEqExtractionProfile.decEq (x✝ x✝¹ : ExtractionProfile) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Semantics.Focus.BackgroundedIslands.instReprExtractionProfile : Repr ExtractionProfile

Equations

• Semantics.Focus.BackgroundedIslands.instReprExtractionProfile = { reprPrec := Semantics.Focus.BackgroundedIslands.instReprExtractionProfile.repr }

def Semantics.Focus.BackgroundedIslands.instReprExtractionProfile.repr : ExtractionProfile → ℕ → Std.Format

Equations

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

def Semantics.Focus.BackgroundedIslands.mosComplementProfile : ExtractionProfile

MoS verb complement: backgrounded → projective → resists extraction.

Backgroundedness is derived from the formal model (§6 mos_island_effect). Projectivity follows from the anti-correlation with at-issueness (@cite{tonhauser-beaver-degen-2018}): backgrounded content is not at-issue, and not-at-issue content projects. Extraction resistance follows from backgroundedness (§6 DiscourseStatus.rank_injective).

Equations

• Semantics.Focus.BackgroundedIslands.mosComplementProfile = { backgrounded := true, projective := true, resistsExtraction := true }

def Semantics.Focus.BackgroundedIslands.factiveComplementProfile : ExtractionProfile

Factive verb complement (notice, discover): projective but NOT backgrounded → does NOT resist extraction.

This is the key dissociation: notice and annoy have similar projectivity levels but very different backgroundedness levels (@cite{tonhauser-beaver-degen-2018}): annoy complements are backgrounded, notice complements are not. Backgroundedness, not projectivity, determines extraction resistance.

Equations

• Semantics.Focus.BackgroundedIslands.factiveComplementProfile = { backgrounded := false, projective := true, resistsExtraction := false }

def Semantics.Focus.BackgroundedIslands.bridgeComplementProfile : ExtractionProfile

Bridge verb complement (say): not projective, not backgrounded, does not resist extraction. Derived: bridge_verb_transparent gives complementStatus = .new → not backgrounded → no extraction resistance.

Equations

• Semantics.Focus.BackgroundedIslands.bridgeComplementProfile = { backgrounded := false, projective := false, resistsExtraction := false }

theorem Semantics.Focus.BackgroundedIslands.projectivity_does_not_determine_extraction : mosComplementProfile.projective = factiveComplementProfile.projective ∧ mosComplementProfile.resistsExtraction ≠ factiveComplementProfile.resistsExtraction

Projectivity does not determine extraction resistance. MoS and factive complements are both projective, but only MoS complements resist extraction.

theorem Semantics.Focus.BackgroundedIslands.mos_backgrounded_iff_resists : mosComplementProfile.backgrounded = mosComplementProfile.resistsExtraction

MoS: backgrounded ↔ resists extraction.

theorem Semantics.Focus.BackgroundedIslands.factive_backgrounded_iff_resists : factiveComplementProfile.backgrounded = factiveComplementProfile.resistsExtraction

Factive: not backgrounded ↔ does not resist extraction.

theorem Semantics.Focus.BackgroundedIslands.bridge_backgrounded_iff_resists : bridgeComplementProfile.backgrounded = bridgeComplementProfile.resistsExtraction

Bridge: not backgrounded ↔ does not resist extraction.

§13. Negation Test (Diagnostic for Backgroundedness)

The negation test (@cite{erteschik-shir-1973}, @cite{ambridge-goldberg-2008}, @cite{lu-pan-degen-2025} p. 630): backgrounded content is unaffected by matrix sentential negation.

(7a) John didn't whisper that Mary was in the courtyard. → Mary was in the courtyard (complement PROJECTS under negation)

(7b) John didn't say that Mary was in the courtyard. → Mary may or may not have been in the courtyard (complement IN SCOPE)

Under the manner QUD, complement content is backgrounded and projects out of negation scope. Under the content QUD, complement content is at-issue and falls within negation scope. The negation test is thus a consequence of the QUD-determined backgroundedness, not an independent diagnostic.

def Semantics.Focus.BackgroundedIslands.projectsUnderNegation : Features.BinaryGivenness → Prop

Whether content projects under sentential negation, based on its givenness. Backgrounded (given) content projects out of negation scope; at-issue (new) content falls within scope.

Equations

• Semantics.Focus.BackgroundedIslands.projectsUnderNegation Features.BinaryGivenness.given = True
• Semantics.Focus.BackgroundedIslands.projectsUnderNegation Features.BinaryGivenness.new = False

@[implicit_reducible]

instance Semantics.Focus.BackgroundedIslands.instDecidableProjectsUnderNegation (s : Features.BinaryGivenness) : Decidable (projectsUnderNegation s)

Equations

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

theorem Semantics.Focus.BackgroundedIslands.mos_complement_projects_under_negation (v : VerbDecomp) (h : v.hasMannerWeight) : projectsUnderNegation (complementStatus (defaultDimension v))

MoS verb complements project under negation.

theorem Semantics.Focus.BackgroundedIslands.bridge_complement_in_negation_scope (v : VerbDecomp) (h : ¬v.hasMannerWeight) : ¬projectsUnderNegation (complementStatus (defaultDimension v))

Bridge verb complements do NOT project under negation.

theorem Semantics.Focus.BackgroundedIslands.prosodic_focus_overrides_negation (v : VerbDecomp) : ¬projectsUnderNegation (complementStatus (activeDimension v true))

Prosodic focus overrides: with embedded focus, even MoS verb complements fall within negation scope (complement becomes at-issue).

§14. Complementizer Restriction (Open Problem)

MoS verbs require an overt complementizer that; bridge verbs allow null that:

(22a) John said (that) Mary is in the courtyard.       ✓
(22b) John whispered *(that) Mary is in the courtyard.  ✗

@cite{lu-pan-degen-2025} (§5) explicitly note that the backgroundedness account does not explain this contrast: "the backgroundedness account does not make any prediction about the overtness of the complementizer."

The subjacency account handles it naturally: if MoS verbs select an appositive CP (not directly syntactically selected), a null complementizer is unavailable because null complementizers require syntactic selection.

This remains an open problem and a genuine empirical advantage of the structural account that the discourse account does not currently capture.

§15. Gradient At-Issueness: From Binary to Continuous

@cite{tonhauser-beaver-degen-2018} @cite{lu-pan-degen-2025}

The binary model (§5) treats backgroundedness as all-or-nothing: complement status is either .given or .new. But @cite{lu-pan-degen-2025} Experiment 2a shows a residual difference: MoS verbs (50–58) are more degraded than say+adverb (53), which is more degraded than say (73–80), even under identical prosodic conditions. The binary model predicts MoS = say+adverb (both .given) and cannot express this gradient.

We lift the model to gradient at-issueness using Rat01 from Core/Discourse/AtIssueness.lean. MannerWeightSource determines not just whether the complement is backgrounded, but how backgrounded. Lexical manner (inherent to verb root) produces stronger backgroundedness than compositional manner (from adverb modification).

This connects to @cite{tonhauser-beaver-degen-2018}'s Gradient Projection Principle: at-issueness and projectivity are anti-correlated (r = .85–.99) and both are gradient, not binary. The three-way ordering derived here (lexical < compositional < none in at-issueness) is a strictly finer prediction than the binary model's two-way split.

def Semantics.Focus.BackgroundedIslands.complementAtIssueness : MannerWeightSource → Core.Discourse.AtIssueness.AtIssuenessDegree

Gradient complement at-issueness based on manner weight source.

• Lexical manner weight (MoS verbs) → 0 (maximally backgrounded)
• Compositional manner weight (say+adverb) → 1/3 (partially backgrounded)
• No manner weight (bridge verbs) → 1 (fully at-issue)

The intermediate value 1/3 is below defaultThreshold (1/2), ensuring the binary model is recoverable: both lexical and compositional map to "not at-issue" under threshold semantics.

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Focus.BackgroundedIslands.complementAtIssueness Semantics.Focus.BackgroundedIslands.MannerWeightSource.none = ⟨1, Semantics.Focus.BackgroundedIslands.complementAtIssueness._proof_3⟩

theorem Semantics.Focus.BackgroundedIslands.lexical_lt_compositional_atissueness : ↑(complementAtIssueness MannerWeightSource.lexical) < ↑(complementAtIssueness MannerWeightSource.compositional)

Lexical manner weight yields strictly lower complement at-issueness than compositional. Matches Exp 2a's residual MoS > say+adverb difference (β = −0.08, p < 0.001).

theorem Semantics.Focus.BackgroundedIslands.compositional_lt_none_atissueness : ↑(complementAtIssueness MannerWeightSource.compositional) < ↑(complementAtIssueness MannerWeightSource.none)

Compositional manner weight yields strictly lower complement at-issueness than no manner weight.

theorem Semantics.Focus.BackgroundedIslands.bridge_above_threshold : ↑(complementAtIssueness MannerWeightSource.none) > 1 / 2

Bridge verbs (at-issueness = 1) are above the default threshold (1/2).

theorem Semantics.Focus.BackgroundedIslands.compositional_below_threshold : ↑(complementAtIssueness MannerWeightSource.compositional) < 1 / 2

Say+adverb (at-issueness = 1/3) is below the default threshold (1/2).

theorem Semantics.Focus.BackgroundedIslands.lexical_below_threshold : ↑(complementAtIssueness MannerWeightSource.lexical) < 1 / 2

MoS verbs (at-issueness = 0) are below the default threshold (1/2).

theorem Semantics.Focus.BackgroundedIslands.gradient_distinguishes_lexical_compositional : complementStatus (defaultDimension whisperDecomp) = complementStatus (defaultDimension saySoftlyDecomp) ∧ ↑(complementAtIssueness whisperDecomp.mannerWeightSource) < ↑(complementAtIssueness saySoftlyDecomp.mannerWeightSource)

Gradient distinguishes what binary cannot: The binary model predicts identical complement status for MoS verbs and say+adverb (both .given), but the gradient model assigns strictly different at-issueness degrees. This accounts for the residual difference in Exp 2a (β = −0.08, p < 0.001) and the per-verb correlation in Exp 2b (β = −0.44, p = 0.014, across 13 verbs including say; MoS-only β = −0.38, p = 0.076).

§16. General Island Prediction API

Given an at-issueness degree for any complement type, derive extraction predictions automatically. This decouples island prediction from manner-of- speaking specifically: any complement whose at-issueness can be estimated (factive, relative clause, purpose clause, etc.) gets predictions for free.

The key result is predictIsland_monotone: extraction rank is monotone in at-issueness, making at-issueness a sufficient statistic for extraction acceptability.

structure Semantics.Focus.BackgroundedIslands.IslandPrediction : Type

Bundled extraction prediction for an arbitrary complement type.

• isIsland : Bool

  Whether the complement constitutes an island (extraction degraded).

• status : Features.BinaryGivenness

  Givenness: .given (backgrounded) or .new (at-issue).

• rank : Fin 2

  Ordinal extraction acceptability (0 = most degraded, 1 = best). Note: this is the ACCEPTABILITY rank, opposite in direction from BinaryGivenness.rank (which orders by salience: given > new). Backgrounded complements (.given) are harder to extract from, so they get acceptability 0; at-issue complements (.new) get acceptability 1.

def Semantics.Focus.BackgroundedIslands.instDecidableEqIslandPrediction.decEq (x✝ x✝¹ : IslandPrediction) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Semantics.Focus.BackgroundedIslands.instDecidableEqIslandPrediction : DecidableEq IslandPrediction

Equations

• Semantics.Focus.BackgroundedIslands.instDecidableEqIslandPrediction = Semantics.Focus.BackgroundedIslands.instDecidableEqIslandPrediction.decEq

def Semantics.Focus.BackgroundedIslands.instReprIslandPrediction.repr : IslandPrediction → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Focus.BackgroundedIslands.instReprIslandPrediction : Repr IslandPrediction

Equations

• Semantics.Focus.BackgroundedIslands.instReprIslandPrediction = { reprPrec := Semantics.Focus.BackgroundedIslands.instReprIslandPrediction.repr }

def Semantics.Focus.BackgroundedIslands.predictIsland (d : Core.Discourse.AtIssueness.AtIssuenessDegree) (θ : Core.Discourse.AtIssueness.AtIssuenessThreshold := Core.Discourse.AtIssueness.defaultThreshold) : IslandPrediction

Derive island predictions from at-issueness degree and threshold. Complements below threshold are backgrounded (islands); those above are at-issue (transparent to extraction).

Equations

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

def Semantics.Focus.BackgroundedIslands.factiveComplementAI : Core.Discourse.AtIssueness.AtIssuenessDegree

Factive complement at-issueness: above threshold (presupposed content is backgrounded qua presupposition, but the propositional content is at-issue — the complement of "know" addresses the QUD).

Equations

• Semantics.Focus.BackgroundedIslands.factiveComplementAI = ⟨3 / 4, Semantics.Focus.BackgroundedIslands.factiveComplementAI._proof_1⟩

theorem Semantics.Focus.BackgroundedIslands.predict_mos : (predictIsland (complementAtIssueness MannerWeightSource.lexical)).isIsland = true

MoS verbs (lexical manner weight) predict islands.

theorem Semantics.Focus.BackgroundedIslands.predict_bridge : (predictIsland (complementAtIssueness MannerWeightSource.none)).isIsland = false

Bridge verbs (no manner weight) predict no island.

theorem Semantics.Focus.BackgroundedIslands.predict_factive : (predictIsland factiveComplementAI).isIsland = false

Factive complements (at-issueness 3/4 > threshold 1/2) predict no island.

theorem Semantics.Focus.BackgroundedIslands.mos_rank_le_factive : (predictIsland (complementAtIssueness MannerWeightSource.lexical)).rank ≤ (predictIsland factiveComplementAI).rank

MoS extraction rank ≤ factive extraction rank.

theorem Semantics.Focus.BackgroundedIslands.factive_rank_le_bridge : (predictIsland factiveComplementAI).rank ≤ (predictIsland (complementAtIssueness MannerWeightSource.none)).rank

Factive extraction rank ≤ bridge extraction rank.

theorem Semantics.Focus.BackgroundedIslands.predictIsland_monotone (d₁ d₂ : Core.Discourse.AtIssueness.AtIssuenessDegree) (θ : Core.Discourse.AtIssueness.AtIssuenessThreshold) (h : ↑d₁ ≤ ↑d₂) : (predictIsland d₁ θ).rank ≤ (predictIsland d₂ θ).rank

Sufficient statistic theorem: extraction rank is monotone in at-issueness. If complement A has at-issueness ≤ complement B, then A's extraction rank is ≤ B's. This makes at-issueness the only input needed for extraction predictions — syntax, frequency, and projectivity are irrelevant once at-issueness is known.

theorem Semantics.Focus.BackgroundedIslands.mos_profile_consistent : (predictIsland (complementAtIssueness MannerWeightSource.lexical)).isIsland = mosComplementProfile.resistsExtraction

MoS profile consistent with predictIsland: both say island.

theorem Semantics.Focus.BackgroundedIslands.factive_profile_consistent : (predictIsland factiveComplementAI).isIsland = factiveComplementProfile.resistsExtraction

Factive profile consistent with predictIsland: both say no island.

theorem Semantics.Focus.BackgroundedIslands.bridge_profile_consistent : (predictIsland (complementAtIssueness MannerWeightSource.none)).isIsland = bridgeComplementProfile.resistsExtraction

Bridge profile consistent with predictIsland: both say no island.