Evidence for a Discourse Account of Manner-of-Speaking Islands

[LPD25]

[LPD25] (Language 101(4): 627–659) reports five acceptability judgment experiments testing the causal relationship between discourse backgroundedness and the manner-of-speaking (MoS) island effect, and this file connects that data to the formal backgroundedness model (the backgroundedness sections below) and the lexical substrate (Semantics/Lexical/LevinClass).

Key findings (§0 data)

1. Prosodic focus on the embedded object ameliorates the MoS island (Exp 1)
2. The same manipulation creates island effects with the bridge verb say (Exp 2a)
3. MoS verbs default-background their complements more than say (Exp 2b)
4. Adding manner adverbs to say replicates the MoS island effect (Exp 3a)
5. The say+adverb island is also sensitive to prosodic manipulation (Exp 3b)
6. Verb-frame frequency does NOT predict the effect (all experiments)

Mean acceptability ratings and backgroundedness proportions are coded as Nat (× 100). Stimulus sentences live in Data/Examples/LuPanDegen2025.json (generated module Data.Examples.LuPanDegen2025).

Derivation chain (§2–§7)

Semantics/Lexical/LevinClass  →  mannerSpec = true for MoS verbs (§37.3)
         ↓
backgroundedness model (below)  →  mannerSpec ↔ hasMannerWeight → island
         ↓
mosIslandSources = [.discourse], mosIslandStrength = .weak

The MoS island is classified as weak (ameliorable) and discourse-sourced, and we derive both properties from the experimental data and the formal model.

Backgrounded constituents are islands

Discourse-backgroundedness account of manner-of-speaking (MoS) island effects. Communication events have manner and content dimensions; the active QUD partitions events along one dimension and backgrounds the other; backgrounded constituents resist wh-extraction.

Main definitions

• MannerComponent, VerbDecomp: lexical decomposition of communication verbs.
• hasMannerWeight: predicate on a VerbDecomp true exactly when the verb carries lexical or compositional manner content.
• CommEvent, QUDDimension, mannerQUD, contentQUD: two-dimensional events and their QUD projections.
• complementBackgrounded, verbForegrounded: discourse status under a given QUD.
• extractionQUD, qaCongruent_* lemmas: Q-A congruence applied to wh-extraction.
• MannerWeightSource, AtIssuenessDegree, complementAtIssueness: gradient manner weight and a rational at-issueness scale.
• IslandPrediction, predictIsland: extraction-prediction API derived from complementAtIssueness.
• ExtractionProfile: backgroundedness × projectivity × extraction- resistance triple, exhibiting the projectivity/extraction dissociation.

Main results

• mos_island_effect, bridge_no_island: contrasting predictions for MoS and bridge verbs.
• prosodic_amelioration, say_adverb_replication: prosodic focus ameliorates and say + adverb replicates the island effect.
• mos_complement_projects, bridge_complement_not_projects: complement projection under sentential negation.
• extraction_rank_monotone_in_atIssueness: extraction rank is monotone in the at-issueness degree.

References

• [LPD25], [KS20], [Rob12], [Gol06].

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

@[implicit_reducible]

instance LuPanDegen2025.instDecidableEqMannerComponent : DecidableEq MannerComponent

Equations

• LuPanDegen2025.instDecidableEqMannerComponent = LuPanDegen2025.instDecidableEqMannerComponent.decEq

def LuPanDegen2025.instDecidableEqMannerComponent.decEq (x✝ x✝¹ : MannerComponent) : Decidable (x✝ = x✝¹)

Equations

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

def LuPanDegen2025.instReprMannerComponent.repr : MannerComponent → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance LuPanDegen2025.instReprMannerComponent : Repr MannerComponent

Equations

• LuPanDegen2025.instReprMannerComponent = { reprPrec := LuPanDegen2025.instReprMannerComponent.repr }

structure LuPanDegen2025.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 LuPanDegen2025.instReprVerbDecomp : Repr VerbDecomp

Equations

• LuPanDegen2025.instReprVerbDecomp = { reprPrec := LuPanDegen2025.instReprVerbDecomp.repr }

def LuPanDegen2025.instReprVerbDecomp.repr : VerbDecomp → ℕ → Std.Format

Equations

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

def LuPanDegen2025.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 LuPanDegen2025.VerbDecomp.instDecidableHasMannerWeight (v : VerbDecomp) : Decidable v.hasMannerWeight

Equations

• v.instDecidableHasMannerWeight = LuPanDegen2025.VerbDecomp.instDecidableHasMannerWeight._aux_1 v

def LuPanDegen2025.whisperDecomp : VerbDecomp

Equations

• LuPanDegen2025.whisperDecomp = { manner := some { name := "whispering" } }

def LuPanDegen2025.shoutDecomp : VerbDecomp

Equations

• LuPanDegen2025.shoutDecomp = { manner := some { name := "shouting" } }

def LuPanDegen2025.sayDecomp : VerbDecomp

Equations

• LuPanDegen2025.sayDecomp = { }

def LuPanDegen2025.saySoftlyDecomp : VerbDecomp

Equations

• LuPanDegen2025.saySoftlyDecomp = { mannerAdverb := some "softly" }

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 LuPanDegen2025.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 LuPanDegen2025.instDecidableEqCommDimension : DecidableEq CommDimension

Equations

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

@[implicit_reducible]

instance LuPanDegen2025.instReprCommDimension : Repr CommDimension

Equations

• LuPanDegen2025.instReprCommDimension = { reprPrec := LuPanDegen2025.instReprCommDimension.repr }

def LuPanDegen2025.instReprCommDimension.repr : CommDimension → ℕ → Std.Format

Equations

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

structure LuPanDegen2025.CommEvent (Manner : Type u_1) (Content : Type u_2) : Type (max u_1 u_2)

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 LuPanDegen2025.instBEqCommEvent {Manner : Type u_1} {Content : Type u_2} [BEq Manner] [BEq Content] : BEq (CommEvent Manner Content)

Equations

• LuPanDegen2025.instBEqCommEvent = { beq := fun (e1 e2 : LuPanDegen2025.CommEvent Manner Content) => e1.manner == e2.manner && e1.content == e2.content }

def LuPanDegen2025.mannerQUD {Manner : Type u_1} {Content : Type u_2} [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

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

def LuPanDegen2025.contentQUD {Manner : Type u_1} {Content : Type u_2} [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

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

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 LuPanDegen2025.manner_qud_ignores_content {Manner : Type u_1} {Content : Type u_2} [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 LuPanDegen2025.content_qud_ignores_manner {Manner : Type u_1} {Content : Type u_2} [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 LuPanDegen2025.backgroundedness_means_qud_invisible {Manner : Type u_1} {Content : Type u_2} [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 LuPanDegen2025.backgrounded_content_same_cell {Manner : Type u_1} {Content : Type u_2} [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 LuPanDegen2025.foregrounding_is_qud_projection_manner {Manner : Type u_1} {Content : Type u_2} [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 LuPanDegen2025.foregrounding_is_qud_projection_content {Manner : Type u_1} {Content : Type u_2} [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 LuPanDegen2025.manner_content_qud_distinct {Manner : Type u_1} {Content : Type u_2} [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.

The extraction constraint

[erteschik-shir-1973] [Rob96] [Gol06]

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 ([Rob96])

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 ([erteschik-shir-1973])

Wh-extraction creates a content QUD: "What₁ did John whisper t₁?" partitions events by the filler's value. By [Roo92]'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 LuPanDegen2025.contentQuestionRelevant {Manner : Type u_1} {Content : Type u_2} (qud : QUD (CommEvent Manner Content)) : Prop

Whether a wh-question about the content of a communication event is relevant to a given QUD ([Rob96]): 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

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

theorem LuPanDegen2025.content_question_irrelevant_under_manner {Manner : Type u_1} {Content : Type u_2} [DecidableEq Manner] : ¬contentQuestionRelevant mannerQUD

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

theorem LuPanDegen2025.content_question_relevant_under_content {Manner : Type u_1} {Content : Type u_2} [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 LuPanDegen2025.extractionQUD {Manner : Type u_1} {Content : Type u_2} [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). ([Rob12]: wh-questions establish QUDs.)

Equations

• LuPanDegen2025.extractionQUD = LuPanDegen2025.contentQUD

theorem LuPanDegen2025.extraction_filler_varies {Manner : Type u_1} {Content : Type u_2} [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 ([Roo92] (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 LuPanDegen2025.extraction_filler_is_focus_alternative {Manner : Type u_1} {Content : Type u_2} {W : Type u_3} (den : CommEvent Manner Content → Set W) (m : Manner) (answerFocus extractionQ : Semantics.Focus.Interpretation.PropFocusValue W) (hq : ∀ (c : Content), den { manner := m, content := c } ∈ extractionQ) (hqa : Semantics.Focus.Interpretation.qaCongruentWeak answerFocus extractionQ) (c : Content) : den { manner := m, content := c } ∈ answerFocus

Q-A congruence applied to extraction ([Roo92] (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 LuPanDegen2025.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, [Rob12])
2. The filler distinguishes the extraction QUD's cells (extraction_filler_varies)
3. extraction_filler_is_focus_alternative (above) uses qaCongruentWeak ([Roo92] (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 [KS20]'s two-feature system

Equations

• LuPanDegen2025.extractedFillerStatus = Features.InformationStructure.FocusMark.focused

theorem LuPanDegen2025.backgrounded_extraction_clashes : Semantics.Focus.ExtractionClash.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 Semantics/Focus/Comparability.lean, which unifies [AHWG20]'s FBC with [erteschik-shir-1973]'s Dominance Condition.

theorem LuPanDegen2025.atissue_extraction_compatible : ¬Semantics.Focus.ExtractionClash.extractionISClash extractedFillerStatus Features.BinaryGivenness.new

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

Default QUD selection

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 [Rob96]: the QUD is determined by what alternatives are salient, and manner components activate manner alternatives.

def LuPanDegen2025.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

• LuPanDegen2025.defaultDimension v = if v.hasMannerWeight then LuPanDegen2025.CommDimension.manner else LuPanDegen2025.CommDimension.content

def LuPanDegen2025.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

• LuPanDegen2025.complementStatus LuPanDegen2025.CommDimension.manner = Features.BinaryGivenness.given
• LuPanDegen2025.complementStatus LuPanDegen2025.CommDimension.content = Features.BinaryGivenness.new

def LuPanDegen2025.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

• LuPanDegen2025.verbFocus LuPanDegen2025.CommDimension.manner = Features.InformationStructure.FocusMark.focused
• LuPanDegen2025.verbFocus LuPanDegen2025.CommDimension.content = Features.InformationStructure.FocusMark.nonFocused

def LuPanDegen2025.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

• LuPanDegen2025.verbGivenness LuPanDegen2025.CommDimension.manner = Features.BinaryGivenness.new
• LuPanDegen2025.verbGivenness LuPanDegen2025.CommDimension.content = Features.BinaryGivenness.given

The MoS island effect

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. BinaryGivenness.rank (Features/Givenness.lean) provides the ordinal ranking consistent with this derivation.

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

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

theorem LuPanDegen2025.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 LuPanDegen2025.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 LuPanDegen2025.mos_extraction_clashes (v : VerbDecomp) (h : v.hasMannerWeight) : Semantics.Focus.ExtractionClash.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 LuPanDegen2025.bridge_no_extraction_clash (v : VerbDecomp) (h : ¬v.hasMannerWeight) : ¬Semantics.Focus.ExtractionClash.extractionISClash extractedFillerStatus (complementStatus (defaultDimension v))

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

Prosodic amelioration

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

• LuPanDegen2025.activeDimension v embeddedObjectFocused = if embeddedObjectFocused = true then LuPanDegen2025.CommDimension.content else LuPanDegen2025.defaultDimension v

theorem LuPanDegen2025.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 LuPanDegen2025.focused_complement_not_backgrounded (v : VerbDecomp) : complementStatus (activeDimension v true) = Features.BinaryGivenness.new

Under prosodic focus, complement is not backgrounded.

theorem LuPanDegen2025.prosodic_focus_resolves_clash (v : VerbDecomp) : ¬Semantics.Focus.ExtractionClash.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 LuPanDegen2025.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 LuPanDegen2025.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 LuPanDegen2025.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.

Say-plus-adverb replication

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 LuPanDegen2025.say_no_manner_weight : ¬sayDecomp.hasMannerWeight

say has no manner weight.

theorem LuPanDegen2025.say_softly_has_manner_weight : saySoftlyDecomp.hasMannerWeight

say softly has manner weight (from the adverb).

theorem LuPanDegen2025.whisper_has_manner_weight : whisperDecomp.hasMannerWeight

whisper has manner weight (from lexical decomposition).

theorem LuPanDegen2025.shout_has_manner_weight : shoutDecomp.hasMannerWeight

shout has manner weight (from lexical decomposition).

theorem LuPanDegen2025.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 LuPanDegen2025.say_vs_say_softly_status : complementStatus (defaultDimension sayDecomp) ≠ complementStatus (defaultDimension saySoftlyDecomp)

say and say softly differ in complement backgroundedness.

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

Theory comparison

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

inductive LuPanDegen2025.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 LuPanDegen2025.instDecidableEqMoSAccount : DecidableEq MoSAccount

Equations

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

@[implicit_reducible]

instance LuPanDegen2025.instReprMoSAccount : Repr MoSAccount

Equations

• LuPanDegen2025.instReprMoSAccount = { reprPrec := LuPanDegen2025.instReprMoSAccount.repr }

def LuPanDegen2025.instReprMoSAccount.repr : MoSAccount → ℕ → Std.Format

Equations

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

structure LuPanDegen2025.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 LuPanDegen2025.instDecidableEqPrediction.decEq (x✝ x✝¹ : Prediction) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance LuPanDegen2025.instDecidableEqPrediction : DecidableEq Prediction

Equations

• LuPanDegen2025.instDecidableEqPrediction = LuPanDegen2025.instDecidableEqPrediction.decEq

@[implicit_reducible]

instance LuPanDegen2025.instReprPrediction : Repr Prediction

Equations

• LuPanDegen2025.instReprPrediction = { reprPrec := LuPanDegen2025.instReprPrediction.repr }

def LuPanDegen2025.instReprPrediction.repr : Prediction → ℕ → Std.Format

Equations

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

def LuPanDegen2025.accountPredictions : MoSAccount → Prediction

Predictions of each account.

Equations

• LuPanDegen2025.accountPredictions LuPanDegen2025.MoSAccount.subjacency = { focusSensitive := false, sayAdverbCreatesIsland := false, frequencyCorrelation := false }
• LuPanDegen2025.accountPredictions LuPanDegen2025.MoSAccount.verbFrameFrequency = { focusSensitive := false, sayAdverbCreatesIsland := false, frequencyCorrelation := true }
• LuPanDegen2025.accountPredictions LuPanDegen2025.MoSAccount.backgroundedness = { focusSensitive := true, sayAdverbCreatesIsland := true, frequencyCorrelation := false }

def LuPanDegen2025.empiricalResults : Prediction

Empirical results from [LPD25].

Equations

• LuPanDegen2025.empiricalResults = { focusSensitive := true, sayAdverbCreatesIsland := true, frequencyCorrelation := false }

def LuPanDegen2025.accountScore (a : MoSAccount) : ℕ

Score: number of correct predictions.

Equations

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

theorem LuPanDegen2025.backgroundedness_perfect_score : accountScore MoSAccount.backgroundedness = 3

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

theorem LuPanDegen2025.subjacency_score : accountScore MoSAccount.subjacency = 1

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

theorem LuPanDegen2025.frequency_score : accountScore MoSAccount.verbFrameFrequency = 0

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

theorem LuPanDegen2025.backgroundedness_dominates : accountScore MoSAccount.backgroundedness > accountScore MoSAccount.subjacency ∧ accountScore MoSAccount.backgroundedness > accountScore MoSAccount.verbFrameFrequency

The backgroundedness account strictly dominates both alternatives.

Grounding bridges

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 LuPanDegen2025.foregrounding_iff_qud_manner {Manner : Type u_1} {Content : Type u_2} [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 LuPanDegen2025.foregrounding_iff_qud_content {Manner : Type u_1} {Content : Type u_2} [DecidableEq Content] (e1 e2 : CommEvent Manner Content) : contentQUD.r e1 e2 ↔ e1.content = e2.content

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

theorem LuPanDegen2025.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 [KS20]'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 LuPanDegen2025.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 LuPanDegen2025.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.

Gradient manner weight: lexical vs. compositional

[LPD25] 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 LuPanDegen2025.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 LuPanDegen2025.instDecidableEqMannerWeightSource : DecidableEq MannerWeightSource

Equations

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

def LuPanDegen2025.instReprMannerWeightSource.repr : MannerWeightSource → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance LuPanDegen2025.instReprMannerWeightSource : Repr MannerWeightSource

Equations

• LuPanDegen2025.instReprMannerWeightSource = { reprPrec := LuPanDegen2025.instReprMannerWeightSource.repr }

def LuPanDegen2025.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 LuPanDegen2025.MannerWeightSource.rank : MannerWeightSource → Fin 3

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

Equations

• LuPanDegen2025.MannerWeightSource.none.rank = 0
• LuPanDegen2025.MannerWeightSource.compositional.rank = 1
• LuPanDegen2025.MannerWeightSource.lexical.rank = 2

theorem LuPanDegen2025.whisper_lexical : whisperDecomp.mannerWeightSource = MannerWeightSource.lexical

theorem LuPanDegen2025.shout_lexical : shoutDecomp.mannerWeightSource = MannerWeightSource.lexical

theorem LuPanDegen2025.say_softly_compositional : saySoftlyDecomp.mannerWeightSource = MannerWeightSource.compositional

theorem LuPanDegen2025.say_none_source : sayDecomp.mannerWeightSource = MannerWeightSource.none

theorem LuPanDegen2025.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 LuPanDegen2025.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.

Backgroundedness/projectivity dissociation

[TBD18] 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 [LPD25], 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 LuPanDegen2025.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

def LuPanDegen2025.instDecidableEqExtractionProfile.decEq (x✝ x✝¹ : ExtractionProfile) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance LuPanDegen2025.instDecidableEqExtractionProfile : DecidableEq ExtractionProfile

Equations

• LuPanDegen2025.instDecidableEqExtractionProfile = LuPanDegen2025.instDecidableEqExtractionProfile.decEq

def LuPanDegen2025.instReprExtractionProfile.repr : ExtractionProfile → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance LuPanDegen2025.instReprExtractionProfile : Repr ExtractionProfile

Equations

• LuPanDegen2025.instReprExtractionProfile = { reprPrec := LuPanDegen2025.instReprExtractionProfile.repr }

def LuPanDegen2025.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 ([TBD18]): backgrounded content is not at-issue, and not-at-issue content projects. Extraction resistance follows from backgroundedness (ranked by BinaryGivenness.rank).

Equations

• LuPanDegen2025.mosComplementProfile = { backgrounded := true, projective := true, resistsExtraction := true }

def LuPanDegen2025.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 ([TBD18]): annoy complements are backgrounded, notice complements are not. Backgroundedness, not projectivity, determines extraction resistance.

Equations

• LuPanDegen2025.factiveComplementProfile = { backgrounded := false, projective := true, resistsExtraction := false }

def LuPanDegen2025.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

• LuPanDegen2025.bridgeComplementProfile = { backgrounded := false, projective := false, resistsExtraction := false }

theorem LuPanDegen2025.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 LuPanDegen2025.mos_backgrounded_iff_resists : mosComplementProfile.backgrounded = mosComplementProfile.resistsExtraction

MoS: backgrounded ↔ resists extraction.

theorem LuPanDegen2025.factive_backgrounded_iff_resists : factiveComplementProfile.backgrounded = factiveComplementProfile.resistsExtraction

Factive: not backgrounded ↔ does not resist extraction.

theorem LuPanDegen2025.bridge_backgrounded_iff_resists : bridgeComplementProfile.backgrounded = bridgeComplementProfile.resistsExtraction

Bridge: not backgrounded ↔ does not resist extraction.

Negation test as a backgroundedness diagnostic

The negation test ([erteschik-shir-1973], [ambridge-goldberg-2008], [LPD25] 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 LuPanDegen2025.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

• LuPanDegen2025.projectsUnderNegation Features.BinaryGivenness.given = True
• LuPanDegen2025.projectsUnderNegation Features.BinaryGivenness.new = False

@[implicit_reducible]

instance LuPanDegen2025.instDecidableProjectsUnderNegation (s : Features.BinaryGivenness) : Decidable (projectsUnderNegation s)

Equations

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

theorem LuPanDegen2025.mos_complement_projects_under_negation (v : VerbDecomp) (h : v.hasMannerWeight) : projectsUnderNegation (complementStatus (defaultDimension v))

MoS verb complements project under negation.

theorem LuPanDegen2025.bridge_complement_in_negation_scope (v : VerbDecomp) (h : ¬v.hasMannerWeight) : ¬projectsUnderNegation (complementStatus (defaultDimension v))

Bridge verb complements do NOT project under negation.

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

Complementizer restriction

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

[LPD25] (§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.

Gradient at-issueness

[TBD18] [LPD25]

The binary model (§5) treats backgroundedness as all-or-nothing: complement status is either .given or .new. But [LPD25] 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 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 [TBD18]'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 LuPanDegen2025.complementAtIssueness : MannerWeightSource → 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

• LuPanDegen2025.complementAtIssueness LuPanDegen2025.MannerWeightSource.lexical = ⟨0, LuPanDegen2025.complementAtIssueness._proof_1⟩
• LuPanDegen2025.complementAtIssueness LuPanDegen2025.MannerWeightSource.compositional = ⟨1 / 3, LuPanDegen2025.complementAtIssueness._proof_2⟩
• LuPanDegen2025.complementAtIssueness LuPanDegen2025.MannerWeightSource.none = ⟨1, LuPanDegen2025.complementAtIssueness._proof_3⟩

theorem LuPanDegen2025.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 LuPanDegen2025.compositional_lt_none_atissueness : ↑(complementAtIssueness MannerWeightSource.compositional) < ↑(complementAtIssueness MannerWeightSource.none)

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

theorem LuPanDegen2025.bridge_above_threshold : ↑(complementAtIssueness MannerWeightSource.none) > 1 / 2

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

theorem LuPanDegen2025.compositional_below_threshold : ↑(complementAtIssueness MannerWeightSource.compositional) < 1 / 2

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

theorem LuPanDegen2025.lexical_below_threshold : ↑(complementAtIssueness MannerWeightSource.lexical) < 1 / 2

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

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

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

@[implicit_reducible]

instance LuPanDegen2025.instDecidableEqIslandPrediction : DecidableEq IslandPrediction

Equations

• LuPanDegen2025.instDecidableEqIslandPrediction = LuPanDegen2025.instDecidableEqIslandPrediction.decEq

def LuPanDegen2025.instDecidableEqIslandPrediction.decEq (x✝ x✝¹ : IslandPrediction) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance LuPanDegen2025.instReprIslandPrediction : Repr IslandPrediction

Equations

• LuPanDegen2025.instReprIslandPrediction = { reprPrec := LuPanDegen2025.instReprIslandPrediction.repr }

def LuPanDegen2025.instReprIslandPrediction.repr : IslandPrediction → ℕ → Std.Format

Equations

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

def LuPanDegen2025.predictIsland (d : Discourse.AtIssueness.AtIssuenessDegree) (θ : Discourse.AtIssueness.AtIssuenessThreshold := 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 LuPanDegen2025.factiveComplementAI : 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

• LuPanDegen2025.factiveComplementAI = ⟨3 / 4, LuPanDegen2025.factiveComplementAI._proof_1⟩

theorem LuPanDegen2025.predict_mos : (predictIsland (complementAtIssueness MannerWeightSource.lexical)).isIsland = true

MoS verbs (lexical manner weight) predict islands.

theorem LuPanDegen2025.predict_bridge : (predictIsland (complementAtIssueness MannerWeightSource.none)).isIsland = false

Bridge verbs (no manner weight) predict no island.

theorem LuPanDegen2025.predict_factive : (predictIsland factiveComplementAI).isIsland = false

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

theorem LuPanDegen2025.mos_rank_le_factive : (predictIsland (complementAtIssueness MannerWeightSource.lexical)).rank ≤ (predictIsland factiveComplementAI).rank

MoS extraction rank ≤ factive extraction rank.

theorem LuPanDegen2025.factive_rank_le_bridge : (predictIsland factiveComplementAI).rank ≤ (predictIsland (complementAtIssueness MannerWeightSource.none)).rank

Factive extraction rank ≤ bridge extraction rank.

theorem LuPanDegen2025.predictIsland_monotone (d₁ d₂ : Discourse.AtIssueness.AtIssuenessDegree) (θ : 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 LuPanDegen2025.mos_profile_consistent : (predictIsland (complementAtIssueness MannerWeightSource.lexical)).isIsland = mosComplementProfile.resistsExtraction

MoS profile consistent with predictIsland: both say island.

theorem LuPanDegen2025.factive_profile_consistent : (predictIsland factiveComplementAI).isIsland = factiveComplementProfile.resistsExtraction

Factive profile consistent with predictIsland: both say no island.

theorem LuPanDegen2025.bridge_profile_consistent : (predictIsland (complementAtIssueness MannerWeightSource.none)).isIsland = bridgeComplementProfile.resistsExtraction

Bridge profile consistent with predictIsland: both say no island.

§0. Experimental Data

Acceptability and backgroundedness aggregates from the five experiments.

Experiment 1: Discourse Effects on MoS Islands

Prosodic focus on the embedded object ameliorates the MoS island effect. N = 94 (after exclusions). Within-subjects: 2 focus conditions × 12 MoS verbs (whisper, mutter, shout, yell, scream, mumble, stammer, whine, groan, moan, shriek, murmur). Stimuli (9): exp1_verbfocus, exp1_embeddedfocus in Data.Examples.LuPanDegen2025. (Figure 4)

def LuPanDegen2025.exp1_acceptability_embeddedFocus : ℕ

Exp 1 mean acceptability (× 100). Figure 4b.

Equations

• LuPanDegen2025.exp1_acceptability_embeddedFocus = 68

def LuPanDegen2025.exp1_acceptability_verbFocus : ℕ

Equations

• LuPanDegen2025.exp1_acceptability_verbFocus = 57

def LuPanDegen2025.exp1_acceptability_goodFiller : ℕ

Equations

• LuPanDegen2025.exp1_acceptability_goodFiller = 79

def LuPanDegen2025.exp1_acceptability_badFiller : ℕ

Equations

• LuPanDegen2025.exp1_acceptability_badFiller = 14

def LuPanDegen2025.exp1_backgrounded_embeddedFocus : ℕ

Exp 1 backgroundedness proportion (× 100). Figure 4a.

Equations

• LuPanDegen2025.exp1_backgrounded_embeddedFocus = 14

def LuPanDegen2025.exp1_backgrounded_verbFocus : ℕ

Equations

• LuPanDegen2025.exp1_backgrounded_verbFocus = 76

theorem LuPanDegen2025.exp1_focus_changes_backgroundedness : exp1_backgrounded_embeddedFocus < exp1_backgrounded_verbFocus

Focus manipulation changed backgroundedness (manipulation check). β = −2.46, SE = 0.40, z = −6.14, p < 0.001.

theorem LuPanDegen2025.exp1_focus_ameliorates_island : exp1_acceptability_embeddedFocus > exp1_acceptability_verbFocus

Main result: Foregrounding the embedded object ameliorates the island. β = 0.23, SE = 0.03, t = 7.10, p < 0.001.

theorem LuPanDegen2025.exp1_island_degraded : exp1_acceptability_verbFocus < exp1_acceptability_goodFiller

MoS island sentences are degraded relative to grammatical fillers.

theorem LuPanDegen2025.exp1_ameliorated_still_degraded : exp1_acceptability_embeddedFocus < exp1_acceptability_goodFiller

Even ameliorated MoS islands remain below grammatical filler level.

Experiment 2a: MoS Verbs and Say

Both verb types show focus effects, but MoS verbs are overall more degraded. The same prosodic manipulation that ameliorates MoS islands can CREATE island-like effects for the bridge verb say. N = 97. 2 focus × 2 verb type. (Figure 7)

def LuPanDegen2025.exp2a_acc_mos_embeddedFocus : ℕ

Exp 2a acceptability (× 100). Figure 7b.

Equations

• LuPanDegen2025.exp2a_acc_mos_embeddedFocus = 58

def LuPanDegen2025.exp2a_acc_mos_verbFocus : ℕ

Equations

• LuPanDegen2025.exp2a_acc_mos_verbFocus = 50

def LuPanDegen2025.exp2a_acc_say_embeddedFocus : ℕ

Equations

• LuPanDegen2025.exp2a_acc_say_embeddedFocus = 80

def LuPanDegen2025.exp2a_acc_say_verbFocus : ℕ

Equations

• LuPanDegen2025.exp2a_acc_say_verbFocus = 73

def LuPanDegen2025.exp2a_acc_goodFiller : ℕ

Equations

• LuPanDegen2025.exp2a_acc_goodFiller = 85

def LuPanDegen2025.exp2a_acc_badFiller : ℕ

Equations

• LuPanDegen2025.exp2a_acc_badFiller = 16

def LuPanDegen2025.exp2a_bg_mos_embeddedFocus : ℕ

Exp 2a backgroundedness (× 100). Figure 7a.

Equations

• LuPanDegen2025.exp2a_bg_mos_embeddedFocus = 12

def LuPanDegen2025.exp2a_bg_mos_verbFocus : ℕ

Equations

• LuPanDegen2025.exp2a_bg_mos_verbFocus = 77

def LuPanDegen2025.exp2a_bg_say_embeddedFocus : ℕ

Equations

• LuPanDegen2025.exp2a_bg_say_embeddedFocus = 10

def LuPanDegen2025.exp2a_bg_say_verbFocus : ℕ

Equations

• LuPanDegen2025.exp2a_bg_say_verbFocus = 20

theorem LuPanDegen2025.exp2a_mos_focus_effect : exp2a_acc_mos_embeddedFocus > exp2a_acc_mos_verbFocus

MoS verbs show focus effect. β = 0.14, SE = 0.02, t = 9.14, p < 0.001.

theorem LuPanDegen2025.exp2a_say_focus_effect : exp2a_acc_say_embeddedFocus > exp2a_acc_say_verbFocus

Say also shows focus effect (can create island-like degradation). Focus × verb-type interaction NOT significant (β = 0.005, p = 0.509).

theorem LuPanDegen2025.exp2a_mos_lt_say : exp2a_acc_mos_verbFocus < exp2a_acc_say_verbFocus ∧ exp2a_acc_mos_embeddedFocus < exp2a_acc_say_embeddedFocus

MoS verbs are overall more degraded than say. β = −0.08, SE = 0.01, t = −5.49, p < 0.001.

theorem LuPanDegen2025.exp2a_mos_more_backgrounded : exp2a_bg_mos_verbFocus > exp2a_bg_say_verbFocus

MoS verb complements are more backgrounded than say complements. β = 0.59, SE = 0.14, z = 4.27, p < 0.001.

Experiment 2b: Default Backgroundedness

Without focus manipulation, MoS verbs default-background their complements more than say. This is the crucial baseline measurement. N = 94. MoS vs Say, no focus manipulation. (Figure 10)

def LuPanDegen2025.exp2b_acc_mos : ℕ

Exp 2b acceptability (× 100). Figure 10b.

Equations

• LuPanDegen2025.exp2b_acc_mos = 68

def LuPanDegen2025.exp2b_acc_say : ℕ

Equations

• LuPanDegen2025.exp2b_acc_say = 77

def LuPanDegen2025.exp2b_acc_goodFiller : ℕ

Equations

• LuPanDegen2025.exp2b_acc_goodFiller = 81

def LuPanDegen2025.exp2b_acc_badFiller : ℕ

Equations

• LuPanDegen2025.exp2b_acc_badFiller = 13

def LuPanDegen2025.exp2b_bg_mos : ℕ

Exp 2b backgroundedness (× 100). Figure 10a.

Equations

• LuPanDegen2025.exp2b_bg_mos = 62

def LuPanDegen2025.exp2b_bg_say : ℕ

Equations

• LuPanDegen2025.exp2b_bg_say = 28

theorem LuPanDegen2025.exp2b_mos_more_backgrounded : exp2b_bg_mos > exp2b_bg_say

MoS verbs default-background complements more than say. β = 0.96, SE = 0.16, z = 6.06, p < 0.001.

theorem LuPanDegen2025.exp2b_mos_less_acceptable : exp2b_acc_mos < exp2b_acc_say

MoS extraction is less acceptable than say extraction. β = −0.14, SE = 0.02, t = −9.26, p < 0.001.

theorem LuPanDegen2025.exp2b_backgroundedness_predicts_acceptability : exp2b_bg_mos > exp2b_bg_say ∧ exp2b_acc_mos < exp2b_acc_say

Core correlation: more backgrounded → less acceptable extraction. This is the key link between backgroundedness and islandhood.

theorem LuPanDegen2025.exp2b_say_near_grammatical : exp2b_acc_say < exp2b_acc_goodFiller

Say extraction approaches grammatical-filler level. β = −0.02, SE = 0.01, t = −1.83, p = 0.067 (n.s.).

Experiment 3a: Say + Manner Adverb Creates Islands

The paper's key novel prediction: adding manner adverbs to say replicates the MoS island effect. This is predicted ONLY by the backgroundedness account. N = 93. Say vs Say+Adverb. Stimuli (18): exp3a_say, exp3a_sayadverb in Data.Examples.LuPanDegen2025. (Figure 14)

def LuPanDegen2025.exp3a_acc_say : ℕ

Exp 3a acceptability (× 100). Figure 14.

Equations

• LuPanDegen2025.exp3a_acc_say = 77

def LuPanDegen2025.exp3a_acc_sayAdverb : ℕ

Equations

• LuPanDegen2025.exp3a_acc_sayAdverb = 53

def LuPanDegen2025.exp3a_acc_goodFiller : ℕ

Equations

• LuPanDegen2025.exp3a_acc_goodFiller = 80

def LuPanDegen2025.exp3a_acc_badFiller : ℕ

Equations

• LuPanDegen2025.exp3a_acc_badFiller = 11

theorem LuPanDegen2025.exp3a_adverb_creates_island : exp3a_acc_sayAdverb < exp3a_acc_say

KEY RESULT: Adding a manner adverb to say degrades extraction. β = −0.24, SE = 0.02, t = −12.4, p < 0.001.

Predicted by backgroundedness account (manner adverb adds manner weight). NOT predicted by subjacency (same CP structure ± adverb). NOT predicted by frequency (predicate-frame frequency n.s., p = 0.664).

theorem LuPanDegen2025.exp3a_adverb_degraded : exp3a_acc_sayAdverb < exp3a_acc_goodFiller

Say+adverb is substantially degraded relative to grammatical fillers.

theorem LuPanDegen2025.exp3a_say_near_grammatical : exp3a_acc_goodFiller - exp3a_acc_say < exp3a_acc_say - exp3a_acc_sayAdverb

Say alone patterns with grammatical fillers.

Experiment 3b: Discourse Effect on Say+Adverb Islands

Prosodic focus ameliorates the say+adverb island, confirming that the effect in Experiment 3a is discourse-driven, not a structural complexity artifact. N = 94. 2 focus conditions (adverb-focus vs embedded-focus). Stimuli (20): exp3b_adverbfocus, exp3b_embeddedfocus in Data.Examples.LuPanDegen2025. (Figure 17)

def LuPanDegen2025.exp3b_acc_embeddedFocus : ℕ

Exp 3b acceptability (× 100). Figure 17b.

Equations

• LuPanDegen2025.exp3b_acc_embeddedFocus = 68

def LuPanDegen2025.exp3b_acc_adverbFocus : ℕ

Equations

• LuPanDegen2025.exp3b_acc_adverbFocus = 50

def LuPanDegen2025.exp3b_acc_goodFiller : ℕ

Equations

• LuPanDegen2025.exp3b_acc_goodFiller = 78

def LuPanDegen2025.exp3b_acc_badFiller : ℕ

Equations

• LuPanDegen2025.exp3b_acc_badFiller = 15

def LuPanDegen2025.exp3b_bg_embeddedFocus : ℕ

Exp 3b backgroundedness (× 100). Figure 17a.

Equations

• LuPanDegen2025.exp3b_bg_embeddedFocus = 35

def LuPanDegen2025.exp3b_bg_adverbFocus : ℕ

Equations

• LuPanDegen2025.exp3b_bg_adverbFocus = 72

theorem LuPanDegen2025.exp3b_focus_changes_backgroundedness : exp3b_bg_embeddedFocus < exp3b_bg_adverbFocus

Focus manipulation changes backgroundedness in say+adverb construction. β = −3.99, SE = 0.74, z = −5.42, p < 0.001.

theorem LuPanDegen2025.exp3b_focus_ameliorates : exp3b_acc_embeddedFocus > exp3b_acc_adverbFocus

Foregrounding embedded object ameliorates the say+adverb island. β = 0.21, SE = 0.03, t = 6.90, p < 0.001.

Negative results: frequency does not predict

Verb-frame frequency and sentence complement ratio (SCR) are n.s. in every experiment that tested them, ruling out the verb-frame frequency account:

• Exp 1: freq β = −0.003, p = 0.874; SCR β = −0.0002, p = 0.987
• Exp 2b: freq β = −0.001, p = 0.981; SCR β = 0.008, p = 0.754
• Exp 3a: freq β = −0.005, p = 0.664; SCR β = −0.003, p = 0.793
• Exp 3b: freq β = 0.01, p = 0.712; SCR β = 0.01, p = 0.587

(0/8 tests significant; see frequencyMoS in §8 for the typed manipulation-level encoding.)

Cross-experiment generalizations

theorem LuPanDegen2025.focus_amelioration_consistent : exp1_acceptability_embeddedFocus > exp1_acceptability_verbFocus ∧ exp2a_acc_mos_embeddedFocus > exp2a_acc_mos_verbFocus ∧ exp2a_acc_say_embeddedFocus > exp2a_acc_say_verbFocus ∧ exp3b_acc_embeddedFocus > exp3b_acc_adverbFocus

Focus amelioration is consistent across all tested configurations.

theorem LuPanDegen2025.backgroundedness_anticorrelates_with_acceptability : (exp1_backgrounded_verbFocus > exp1_backgrounded_embeddedFocus ∧ exp1_acceptability_verbFocus < exp1_acceptability_embeddedFocus) ∧ (exp2b_bg_mos > exp2b_bg_say ∧ exp2b_acc_mos < exp2b_acc_say) ∧ exp3b_bg_adverbFocus > exp3b_bg_embeddedFocus ∧ exp3b_acc_adverbFocus < exp3b_acc_embeddedFocus

More backgrounded → lower extraction acceptability, consistently.

theorem LuPanDegen2025.mos_effect_not_verb_class_artifact : exp3a_acc_say > exp3a_acc_sayAdverb ∧ exp2b_acc_say > exp2b_acc_mos

The MoS island effect is NOT an artifact of verb-class confounds: the say+adverb construction replicates it with the same bridge verb.

Island source derivation

The MoS island effect is classified as a weak, discourse-sourced island. The source classification is DERIVED from the experimental evidence above, not stipulated in a global lookup table:

1. Not syntactic: prosodic focus ameliorates the effect (Exps 1, 3b). Syntactic constraints (PIC, subjacency) are insensitive to prosodic focus.
2. Not processing: verb-frame frequency is non-predictive (0/8 tests). Processing accounts predict frequency effects.
3. Discourse: say+adverb replicates the effect without structural change (Exp 3a). Only the backgroundedness account predicts this — adding a manner adverb to a bridge verb increases manner salience, shifting the QUD and backgrounding the complement.

def LuPanDegen2025.mosIslandSources : List IslandSource

MoS islands are discourse-sourced. Derived from three empirical dissociations (above) that rule out syntactic and processing sources.

Equations

• LuPanDegen2025.mosIslandSources = [IslandSource.discourse]

def LuPanDegen2025.mosIslandStrength : ConstraintStrength

MoS islands are weak: ameliorated by prosodic focus. Derived from Experiments 1 and 3b: embedded-focus conditions are significantly more acceptable than verb-focus conditions.

Equations

• LuPanDegen2025.mosIslandStrength = ConstraintStrength.weak

theorem LuPanDegen2025.weak_classification_justified : mosIslandStrength = ConstraintStrength.weak ∧ exp1_acceptability_embeddedFocus > exp1_acceptability_verbFocus ∧ exp3b_acc_embeddedFocus > exp3b_acc_adverbFocus

The strength classification is empirically supported: prosodic focus improves extraction across all tested configurations.

theorem LuPanDegen2025.mos_vs_wh_same_strength_different_source : mosIslandStrength = ConstraintStrength.weak ∧ mosIslandSources ≠ [IslandSource.syntactic]

MoS islands and wh-islands are both weak (ameliorable), but by DIFFERENT mechanisms: MoS by prosodic focus (information structure), wh-islands by D-linking (filler complexity). Same strength label, different sources, different amelioration strategies.

Stimulus rows

The example stimuli are typed rows in Data.Examples.LuPanDegen2025 (UNVERIFIED against the published item lists; reconstructed from the paper's in-text examples). Their judgment coding mirrors the mean-rating direction: island conditions (verb focus, say+adverb, adverb focus) are .marginal; ameliorated/bridge conditions are .acceptable.

theorem LuPanDegen2025.stimulus_judgments_track_island_conditions (row : Data.Examples.LinguisticExample) : row ∈ Examples.all → (row.feature? "island_condition" = some "true" ↔ row.judgment = Features.Judgment.marginal)

The stimulus rows' judgment coding matches the rating data: a row is .marginal iff it instantiates an island condition (the lower-rated member of its experimental contrast).

§1. Island Source Classification

The paper's core contribution is the double dissociation between discourse- sourced MoS islands (mosIslandSources, derived in §0 from the experimental evidence) and syntactically-sourced traditional islands. The traditional island classification is the baseline consensus view: these islands arise from structural constraints on movement (subjacency, PIC, Relativized Minimality).

def LuPanDegen2025.traditionalIslandSource : IslandSource

Traditional islands (wh, CNPC, adjunct, coordinate, subject, sentential subject) are syntactically sourced. This is the baseline consensus against which the paper shows MoS islands are categorically different.

Note: [HS10] argue that some of these (CNPC, wh-islands) have processing sources. That alternative classification is formalized in their study file, not here.

Equations

• LuPanDegen2025.traditionalIslandSource = IslandSource.syntactic

§2. Levin Class → Manner Weight Bridge

[Lev93] §37 classifies communication verbs into three subclasses:

• §37.7 say verbs (say, report, announce): mannerSpec = false
• §37.2 tell verbs (tell, inform, notify): mannerSpec = false
• §37.3 manner-of-speaking verbs (whisper, shout, mumble): mannerSpec = true

The mannerSpec meaning component is exactly the property that drives the MoS island effect: it indicates whether the verb's root specifies manner, which determines whether manner alternatives are activated, which determines QUD selection, which determines complement backgroundedness.

This section connects the Levin class infrastructure to the backgroundedness model, making the island prediction derivable from lexical classification by construction.

def LuPanDegen2025.levinClassToMannerWeight (lc : Semantics.Lexical.LevinClass) : Bool

Map Levin class manner specification to the backgroundedness model's manner weight. A verb with mannerSpec = true has lexical manner weight; one without has none. (Compositional manner weight from adverbs is not captured by Levin classes.)

Equations

• LuPanDegen2025.levinClassToMannerWeight lc = lc.meaningComponents.mannerSpec

theorem LuPanDegen2025.levin_mos_has_manner_weight : levinClassToMannerWeight Semantics.Lexical.LevinClass.mannerOfSpeaking = true

MoS verbs (§37.3) have manner weight by Levin classification.

theorem LuPanDegen2025.levin_say_no_manner_weight : levinClassToMannerWeight Semantics.Lexical.LevinClass.say = false

Bridge verbs (§37.7) lack manner weight by Levin classification.

theorem LuPanDegen2025.levin_class_predicts_island : (levinClassToMannerWeight Semantics.Lexical.LevinClass.mannerOfSpeaking = true ∧ complementStatus (defaultDimension { manner := some { name := "manner" } }) = Features.BinaryGivenness.given) ∧ levinClassToMannerWeight Semantics.Lexical.LevinClass.say = false ∧ complementStatus (defaultDimension { }) = Features.BinaryGivenness.new

Full derivation from Levin class to island prediction: the Levin mannerSpec feature determines manner weight, which determines the default QUD, which determines complement backgroundedness, which determines extraction acceptability.

This makes the MoS island prediction a consequence of lexical classification, not an independent stipulation.

theorem LuPanDegen2025.levin_manner_is_only_difference : levinClassToMannerWeight Semantics.Lexical.LevinClass.mannerOfSpeaking ≠ levinClassToMannerWeight Semantics.Lexical.LevinClass.say ∧ Semantics.Lexical.LevinClass.mannerOfSpeaking.meaningComponents.changeOfState = Semantics.Lexical.LevinClass.say.meaningComponents.changeOfState ∧ Semantics.Lexical.LevinClass.mannerOfSpeaking.meaningComponents.contact = Semantics.Lexical.LevinClass.say.meaningComponents.contact ∧ Semantics.Lexical.LevinClass.mannerOfSpeaking.meaningComponents.motion = Semantics.Lexical.LevinClass.say.meaningComponents.motion ∧ Semantics.Lexical.LevinClass.mannerOfSpeaking.meaningComponents.causation = Semantics.Lexical.LevinClass.say.meaningComponents.causation

The Levin distinction between §37.3 and §37.7 is exclusively about manner. All other meaning components are identical (both are communication verbs with no change-of-state, contact, motion, causation, or instrument specification). Manner specification is the ONLY lexical feature that distinguishes them.

§3. Cross-Theory Predictions

Different island theories make different predictions about which manipulations should affect which island types. The backgroundedness account uniquely predicts that discourse manipulations (prosodic focus, manner adverb addition) affect MoS islands but not structural islands.

structure LuPanDegen2025.ManipulationPrediction : Type

A manipulation and the theories' predictions about its effect.

• manipulation : String
• affectsStructuralIslands : Bool
• affectsMoSIslands : Bool

def LuPanDegen2025.instReprManipulationPrediction.repr : ManipulationPrediction → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance LuPanDegen2025.instReprManipulationPrediction : Repr ManipulationPrediction

Equations

• LuPanDegen2025.instReprManipulationPrediction = { reprPrec := LuPanDegen2025.instReprManipulationPrediction.repr }

def LuPanDegen2025.manipulationPredictions : List ManipulationPrediction

Predictions of the backgroundedness account vs. structural accounts.

Equations

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

theorem LuPanDegen2025.discourse_structural_dissociation : (manipulationPredictions.all fun (p : ManipulationPrediction) => p.affectsStructuralIslands != p.affectsMoSIslands) = true

Discourse and structural island types respond to DIFFERENT manipulations. This is the core empirical prediction that distinguishes the two account types.

§4. D-Linking Prediction

The backgroundedness account predicts that D-linking (which-N vs bare wh) should NOT ameliorate MoS islands, because D-linking changes filler complexity (processing-relevant) but does not change the QUD or information structure.

This contrasts with structural weak islands (wh-islands), where D-linking DOES ameliorate. The dissociation is a testable prediction that distinguishes discourse-sourced from syntax/processing-sourced islands.

theorem LuPanDegen2025.dlinking_does_not_change_backgroundedness (v : VerbDecomp) (h : v.hasMannerWeight) : complementStatus (defaultDimension v) = Features.BinaryGivenness.given

D-linking does not change QUD: D-linking modifies the filler's referential properties but does not affect which dimension of the communication event is foregrounded. The manner QUD remains active regardless of filler complexity.

theorem LuPanDegen2025.differential_amelioration : mosIslandSources = [IslandSource.discourse] ∧ traditionalIslandSource = IslandSource.syntactic ∧ mosIslandSources ≠ [traditionalIslandSource]

Differential amelioration prediction: D-linking ameliorates structural weak islands but NOT MoS islands, while prosodic focus ameliorates MoS islands but NOT structural islands. This double dissociation is the core prediction separating discourse from syntax/processing accounts.

§5. Per-Verb Backgroundedness–Acceptability Correlation

[LPD25] Experiment 2b (Figure 13) shows a negative correlation between per-verb backgroundedness proportion and extraction acceptability across the 13 verbs (12 MoS + say; β = −0.44, p = 0.014; MoS-only: β = −0.38, p = 0.076, marginally significant).

The formal model predicts this: verbs whose manner component is more salient activate the manner QUD more strongly, producing stronger default backgroundedness and therefore worse extraction.

theorem LuPanDegen2025.per_verb_correlation_predicted : complementStatus (defaultDimension whisperDecomp) = Features.BinaryGivenness.given ∧ complementStatus (defaultDimension shoutDecomp) = Features.BinaryGivenness.given

Per-verb backgroundedness predicts acceptability: verbs that background their complements more strongly also show more degraded extraction. The model derives this from manner salience → QUD strength → backgroundedness. The conceptually-right substrate for "backgroundedness" is Discourse.AtIssuenessDegree, not BinaryGivenness (which orders by salience, given > new); future work could rephrase complementStatus over AtIssuenessDegree directly.

§6. Fragment Verb → Island Prediction Pipeline

Each MoS verb in Fragments/English/Predicates/Verbal.lean has levinClass := some .mannerOfSpeaking, and each bridge verb has a non-MoS Levin class. Per-verb verification theorems connect Fragment entries to island predictions: changing a Fragment entry's levinClass field breaks exactly one theorem, making the dependency explicit and auditable.

The derivation chain per verb:

Fragment entry → .levinClass = some .mannerOfSpeaking
    → levinClassToMannerWeight = true
    → hasMannerWeight = true
    → defaultDimension = .manner
    → complementStatus = .given
    → extraction degraded

def LuPanDegen2025.fragmentPredictsIsland (v : English.Predicates.Verbal.VerbEntry) : Bool

Does a Fragment verb entry predict an island effect? Derived from the verb's Levin class via levinClassToMannerWeight.

Equations

• LuPanDegen2025.fragmentPredictsIsland v = match v.levinClass with | some lc => LuPanDegen2025.levinClassToMannerWeight lc | none => false

MoS verbs: all predict islands

These 15 verbs have levinClass := some .mannerOfSpeaking in the Fragment. The per-verb theorems cover both the 12 experimental stimuli from [LPD25] (whisper, murmur, shout, scream, mumble, mutter, shriek, yell, groan — 9 of 12 overlap with Fragment inventory) and 6 additional MoS verbs in the Fragment (cry, grumble, hiss, sigh, whimper, snap).

Three experimental verbs (stammer, whine, moan) are not yet in the Fragment.

theorem LuPanDegen2025.mos_verbs_predict_islands : fragmentPredictsIsland English.Predicates.Verbal.whisper = true ∧ fragmentPredictsIsland English.Predicates.Verbal.murmur = true ∧ fragmentPredictsIsland English.Predicates.Verbal.shout = true ∧ fragmentPredictsIsland English.Predicates.Verbal.cry = true ∧ fragmentPredictsIsland English.Predicates.Verbal.scream = true ∧ fragmentPredictsIsland English.Predicates.Verbal.mumble = true ∧ fragmentPredictsIsland English.Predicates.Verbal.mutter = true ∧ fragmentPredictsIsland English.Predicates.Verbal.shriek = true ∧ fragmentPredictsIsland English.Predicates.Verbal.yell = true ∧ fragmentPredictsIsland English.Predicates.Verbal.groan = true ∧ fragmentPredictsIsland English.Predicates.Verbal.grumble = true ∧ fragmentPredictsIsland English.Predicates.Verbal.hiss = true ∧ fragmentPredictsIsland English.Predicates.Verbal.sigh = true ∧ fragmentPredictsIsland English.Predicates.Verbal.whimper = true ∧ fragmentPredictsIsland English.Predicates.Verbal.snap = true

Bridge verbs: no island prediction

say and tell are bridge verbs (Levin §37.7 and §37.2 respectively). They lack manner specification and therefore do not background their complements by default.

theorem LuPanDegen2025.bridge_verbs_no_island : fragmentPredictsIsland English.Predicates.Verbal.say = false ∧ fragmentPredictsIsland English.Predicates.Verbal.tell = false

Gradient predictions for Fragment verbs

Using the gradient at-issueness model above, Fragment MoS verbs have strictly lower complement at-issueness than bridge verbs. This connects Fragment entries → Levin class → manner weight source → gradient at-issueness in a single derivation chain.

theorem LuPanDegen2025.fragment_gradient_contrast : ↑(complementAtIssueness whisperDecomp.mannerWeightSource) < ↑(complementAtIssueness sayDecomp.mannerWeightSource)

Fragment MoS verbs map to lexical manner weight source, yielding the lowest complement at-issueness (maximally backgrounded). Bridge verbs map to none, yielding the highest (fully at-issue).

§7. Experimental Data → Formal Model Connection

The experimental data in §0 records per-experiment acceptability and backgroundedness values. Here we connect these empirical observations to the formal model's predictions, closing the loop between raw data and theoretical derivation.

The key connection: the formal model predicts that backgroundedness causes extraction degradation (complementStatus .given → .rank = 0). The experimental data confirms this directionally: higher backgroundedness proportions consistently co-occur with lower acceptability ratings.

theorem LuPanDegen2025.experimental_matches_model : (exp2b_bg_mos > exp2b_bg_say ∧ exp2b_acc_mos < exp2b_acc_say) ∧ exp1_backgrounded_verbFocus > exp1_backgrounded_embeddedFocus ∧ exp1_acceptability_verbFocus < exp1_acceptability_embeddedFocus

Experimental data matches formal model direction: the formal model predicts that backgrounded complements have degraded extraction. Experiments 1, 2b, and 3b all show the predicted anti-correlation: higher backgroundedness → lower acceptability.

theorem LuPanDegen2025.adverb_replicates_model : complementStatus (defaultDimension saySoftlyDecomp) = Features.BinaryGivenness.given ∧ exp3a_acc_say > exp3a_acc_sayAdverb

Say+adverb replicates formal model prediction: adding manner weight compositionally (say + adverb) degrades extraction without changing syntax. This is exactly what the formal model predicts: manner weight → backgroundedness → island, regardless of whether the weight is lexical or compositional.

§8. Cross-Theory Comparison Across Manipulations

This section integrates [LPD25]'s findings with [HS10]'s processing manipulations and [Sag10]'s grammar-based island typology, comparing how three account types (competence, processing, discourse) score against the empirical data.

The key empirical claim of [LPD25]: discourse and processing accounts cover disjoint sets of manipulations. Together they explain the full range; neither suffices alone.

structure LuPanDegen2025.IslandManipulation : Type

A nonstructural manipulation that changes island acceptability without altering the island configuration. Each account makes a prediction about whether the manipulation affects acceptability.

• description : String
• competencePredictsDifference : Bool

  Does any competence theory predict an acceptability difference?

• processingPredictsDifference : Bool

  Does the processing account predict a difference?

• discoursePredictsDifference : Bool

  Does the discourse/backgroundedness account predict a difference?

• differenceObserved : Bool

  Is a difference actually observed?

@[implicit_reducible]

instance LuPanDegen2025.instReprIslandManipulation : Repr IslandManipulation

Equations

• LuPanDegen2025.instReprIslandManipulation = { reprPrec := LuPanDegen2025.instReprIslandManipulation.repr }

def LuPanDegen2025.instReprIslandManipulation.repr : IslandManipulation → ℕ → Std.Format

Equations

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

[HS10] manipulations

def LuPanDegen2025.fillerComplexityCNPC : IslandManipulation

Filler complexity in CNPC (which-N vs bare wh — same island structure).

Equations

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

def LuPanDegen2025.fillerComplexityWhIsland : IslandManipulation

Filler complexity in wh-islands (which-N vs bare wh — same island structure).

Equations

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

def LuPanDegen2025.npTypeCNPC : IslandManipulation

NP type in CNPC (definite vs indefinite — same CNPC configuration).

Equations

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

def LuPanDegen2025.fillerComplexityAdjunct : IslandManipulation

Filler complexity in adjunct islands (complex vs simple temporal adjunct).

Equations

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

[LPD25] MoS manipulations

def LuPanDegen2025.prosodicFocusMoS : IslandManipulation

Prosodic focus on embedded object in MoS islands. Focus changes information structure without changing syntax or processing load.

Equations

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

def LuPanDegen2025.sayAdverbIsland : IslandManipulation

Say + manner adverb creates an island. Adding an adverb doesn't change CP structure but adds manner weight.

Equations

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

def LuPanDegen2025.frequencyMoS : IslandManipulation

Verb-frame frequency in MoS islands: not significant in any experiment.

Equations

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

def LuPanDegen2025.allManipulations : List IslandManipulation

Equations

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

def LuPanDegen2025.processingCorrect (m : IslandManipulation) : Bool

Processing correctly predicts the observed (non-)difference.

Equations

• LuPanDegen2025.processingCorrect m = (m.differenceObserved == m.processingPredictsDifference)

def LuPanDegen2025.competenceCorrect (m : IslandManipulation) : Bool

Competence correctly predicts the observed (non-)difference.

Equations

• LuPanDegen2025.competenceCorrect m = (m.differenceObserved == m.competencePredictsDifference)

def LuPanDegen2025.discourseCorrect (m : IslandManipulation) : Bool

Discourse correctly predicts the observed (non-)difference.

Equations

• LuPanDegen2025.discourseCorrect m = (m.differenceObserved == m.discoursePredictsDifference)

def LuPanDegen2025.processingScore : ℕ

Equations

• LuPanDegen2025.processingScore = (List.filter LuPanDegen2025.processingCorrect LuPanDegen2025.allManipulations).length

def LuPanDegen2025.competenceScore : ℕ

Equations

• LuPanDegen2025.competenceScore = (List.filter LuPanDegen2025.competenceCorrect LuPanDegen2025.allManipulations).length

def LuPanDegen2025.discourseScore : ℕ

Equations

• LuPanDegen2025.discourseScore = (List.filter LuPanDegen2025.discourseCorrect LuPanDegen2025.allManipulations).length

theorem LuPanDegen2025.processing_scores_4_of_7 : processingScore = 4

Processing scores 4/7: correct on all four H&S manipulations, incorrect on the three MoS manipulations (predicts effect or null incorrectly).

theorem LuPanDegen2025.competence_scores_1_of_7 : competenceScore = 1

Competence scores 1/7 — only the frequency null result, where it correctly predicts no effect for the wrong reason.

theorem LuPanDegen2025.discourse_scores_3_of_7 : discourseScore = 3

Discourse scores 3/7: correct on prosodic focus, say+adverb, and the frequency null. Misses the four H&S effects, which are processing, not discourse.

theorem LuPanDegen2025.complementary_accounts : (allManipulations.all fun (m : IslandManipulation) => processingCorrect m != discourseCorrect m) = true

Processing and discourse are perfectly complementary: for every manipulation, exactly one of the two accounts is correct (XOR). They have full coverage (together 7/7) with zero overlap.

§9. Connection to [Sag10]'s Construction-Based Islands

[Sag10]'s F-G typology classifies which constructions are grammar-based islands (those with [GAP ⟨⟩] on the mother). [HS10]'s findings explain within-island gradient effects. [LPD25]'s MoS islands are a third mechanism. Together the three accounts cover disjoint islands.

theorem LuPanDegen2025.sag_island_subset : Sag2010.islandConstructions.length < 5

[Sag10]'s two island constructions are a proper subset of all F-G types. The non-island types (interrogative, relative, the-clause) freely permit extraction.

theorem LuPanDegen2025.complementary_coverage : Sag2010.FGClauseType.topicalized.IsIsland ∧ Sag2010.FGClauseType.whExclamative.IsIsland ∧ mosIslandSources = [IslandSource.discourse]

[Sag10]'s grammar-based islands (topicalization, exclamatives) are disjoint from [HS10]'s processing-based islands (CNPC, wh-islands, adjuncts) and from [LPD25]'s discourse-based islands (MoS). The three accounts cover different cases under different mechanisms.

theorem LuPanDegen2025.mos_distinct_from_traditional_islands : mosIslandSources = [IslandSource.discourse] ∧ mosIslandSources ≠ [traditionalIslandSource]

MoS islands are discourse-sourced and so distinct from the syntactic baseline assumed for traditional islands.