Documentation

Linglib.Theories.Semantics.Focus.BackgroundedIslands

Backgrounded Constituents Are Islands #

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

Formalization of the discourse-backgroundedness account of manner-of-speaking (MoS) island effects, following @cite{lu-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:

Manner QUD → content is invisible to the partition → content is backgrounded
Content QUD → manner is invisible → content is foregrounded
Verb with manner weight → manner QUD is default → island effect
Prosodic focus on embedded object → overrides to content QUD → amelioration
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 (Focus/Interpretation.lean) = same as QUD cell membership

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

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

Instances For

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 ⋯

Instances For

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.

Instances For

instance Semantics.Focus.BackgroundedIslands.instReprMannerComponent :

Repr MannerComponent

Equations

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

instance Semantics.Focus.BackgroundedIslands.instBEqMannerComponent :

BEq MannerComponent

Equations

Semantics.Focus.BackgroundedIslands.instBEqMannerComponent = { beq := Semantics.Focus.BackgroundedIslands.instBEqMannerComponent.beq }

def Semantics.Focus.BackgroundedIslands.instBEqMannerComponent.beq :

MannerComponent → MannerComponent → Bool

Equations

Semantics.Focus.BackgroundedIslands.instBEqMannerComponent.beq { name := a } { name := b } = (a == b)
Semantics.Focus.BackgroundedIslands.instBEqMannerComponent.beq x✝¹ x✝ = false

Instances For

structure Semantics.Focus.BackgroundedIslands.VerbDecomp :

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)

Instances For

def Semantics.Focus.BackgroundedIslands.instReprVerbDecomp.repr :

VerbDecomp → ℕ → Std.Format

Equations

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

Instances For

instance Semantics.Focus.BackgroundedIslands.instReprVerbDecomp :

Repr VerbDecomp

Equations

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

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

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.isSome || v.mannerAdverb.isSome)

Instances For

def Semantics.Focus.BackgroundedIslands.whisperDecomp :

Equations

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

Instances For

def Semantics.Focus.BackgroundedIslands.shoutDecomp :

Equations

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

Instances For

def Semantics.Focus.BackgroundedIslands.sayDecomp :

Equations

Semantics.Focus.BackgroundedIslands.sayDecomp = { }

Instances For

def Semantics.Focus.BackgroundedIslands.saySoftlyDecomp :

Equations

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

Instances For

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

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?"

Instances For

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.

Instances For

instance Semantics.Focus.BackgroundedIslands.instReprCommDimension :

Repr CommDimension

Equations

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

instance Semantics.Focus.BackgroundedIslands.instBEqCommDimension :

BEq CommDimension

Equations

Semantics.Focus.BackgroundedIslands.instBEqCommDimension = { beq := Semantics.Focus.BackgroundedIslands.instBEqCommDimension.beq }

def Semantics.Focus.BackgroundedIslands.instBEqCommDimension.beq :

CommDimension → CommDimension → Bool

Equations

Semantics.Focus.BackgroundedIslands.instBEqCommDimension.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

structure Semantics.Focus.BackgroundedIslands.CommEvent (Manner Content : 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

Instances For

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"

Instances For

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"

Instances For

§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] [DecidableEq Content] (e1 e2 : CommEvent Manner Content) (h : e1.manner = e2.manner) :

mannerQUD.sameAnswer e1 e2 = true

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 Manner] [DecidableEq Content] (e1 e2 : CommEvent Manner Content) (h : e1.content = e2.content) :

contentQUD.sameAnswer e1 e2 = true

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] [DecidableEq Content] (e : CommEvent Manner Content) (c' : Content) :

mannerQUD.sameAnswer e { manner := e.manner, content := c' } = true

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] [DecidableEq Content] [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] [DecidableEq Content] (e1 e2 : CommEvent Manner Content) (h : mannerQUD.sameAnswer e1 e2 = true) :

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 Manner] [DecidableEq Content] (e1 e2 : CommEvent Manner Content) (h : contentQUD.sameAnswer e1 e2 = true) :

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.sameAnswer e1 e2 = true ∧ ¬contentQUD.sameAnswer e1 e2 = true

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

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.

Instances For

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

Core.InformationStructure.DiscourseStatus

Discourse status of the complement content under a given QUD.

Under manner QUD: content is backgrounded (K&S DiscourseStatus.given). Under content QUD: content is foregrounded (K&S DiscourseStatus.new).

Equations

Instances For

def Semantics.Focus.BackgroundedIslands.verbStatus (dim : CommDimension) :

Core.InformationStructure.DiscourseStatus

Discourse status of the matrix verb under a given QUD.

Equations

Instances For

§5. The MoS Island Effect: Main Derivation #

We derive the island effect from the chain: manner weight → manner QUD → content backgrounded → extraction degraded

Each step is proved, and the full chain is stated as a single theorem.

def Semantics.Focus.BackgroundedIslands.extractionRank (status : Core.InformationStructure.DiscourseStatus) :

The Backgroundedness Constraint on Extraction:

Backgrounded constituents resist syntactic extraction. The more backgrounded a constituent, the less acceptable extraction from it.

This is the bridge between information structure and island effects. The constraint is purely ordinal: given < new < focused.

Equations

Instances For

theorem Semantics.Focus.BackgroundedIslands.mos_island_effect (v : VerbDecomp) (h : v.hasMannerWeight = true) :

complementStatus (defaultDimension v) = Core.InformationStructure.DiscourseStatus.given

MoS Island Effect (Main Theorem): MoS verbs default-background their complements, degrading extraction.

Derivation chain:

MoS verb has manner weight (lexical decomposition)
Manner weight → default dimension is manner
Manner dimension → complement status is.given (backgrounded)
Backgrounded → extraction degraded (.given <.new)

theorem Semantics.Focus.BackgroundedIslands.bridge_verb_transparent (v : VerbDecomp) (h : v.hasMannerWeight = false) :

complementStatus (defaultDimension v) = Core.InformationStructure.DiscourseStatus.new

Bridge Verb Transparency: Bridge verbs do NOT produce island effects, because they lack manner weight → default to content QUD → complement foregrounded.

theorem Semantics.Focus.BackgroundedIslands.backgrounded_lt_new :

extractionRank Core.InformationStructure.DiscourseStatus.given < extractionRank Core.InformationStructure.DiscourseStatus.new

Backgrounded extraction is strictly worse than neutral.

theorem Semantics.Focus.BackgroundedIslands.new_lt_focused :

extractionRank Core.InformationStructure.DiscourseStatus.new < extractionRank Core.InformationStructure.DiscourseStatus.focused

Neutral extraction is strictly worse than focused.

theorem Semantics.Focus.BackgroundedIslands.extraction_ordering :

extractionRank Core.InformationStructure.DiscourseStatus.given < extractionRank Core.InformationStructure.DiscourseStatus.new ∧ extractionRank Core.InformationStructure.DiscourseStatus.new < extractionRank Core.InformationStructure.DiscourseStatus.focused

The full ordering: given < new < focused.

theorem Semantics.Focus.BackgroundedIslands.full_derivation (v : VerbDecomp) :

(v.hasMannerWeight = true → complementStatus (defaultDimension v) = Core.InformationStructure.DiscourseStatus.given) ∧ (v.hasMannerWeight = false → complementStatus (defaultDimension v) = Core.InformationStructure.DiscourseStatus.new)

Full Derivation: the complete causal chain from verb decomposition to extraction prediction, for both MoS and bridge verbs, in a single theorem.

For any communication verb:

If it has manner weight → complement is backgrounded (given)
If it lacks manner weight → complement is neutral (new)

Combined with extraction_ordering, this yields the acceptability contrast.

§6. Prosodic Amelioration (Experiments 1 & 3b) #

Prosodic focus ([FoC]) on the embedded object overrides the default backgroundedness, forcing the content QUD and ameliorating the island.

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

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.

Instances For

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

Under prosodic focus, complement is not backgrounded.

theorem Semantics.Focus.BackgroundedIslands.unfocused_mos_complement_backgrounded (v : VerbDecomp) (h : v.hasMannerWeight = true) :

complementStatus (activeDimension v false) = Core.InformationStructure.DiscourseStatus.given

Without prosodic focus, MoS verb complements ARE backgrounded.

theorem Semantics.Focus.BackgroundedIslands.amelioration_improves_extraction :

extractionRank (complementStatus CommDimension.content) > extractionRank (complementStatus CommDimension.manner)

Amelioration improves extraction: Extraction from prosodically focused complement is better than extraction from default-backgrounded complement.

theorem Semantics.Focus.BackgroundedIslands.mos_focus_sensitivity (v : VerbDecomp) (h : v.hasMannerWeight = true) :

extractionRank (complementStatus (activeDimension v true)) > extractionRank (complementStatus (activeDimension v false))

Focus sensitivity for MoS verbs: Prosodic focus changes the extraction prediction for MoS verbs from degraded (backgrounded) to acceptable (new).

§7. 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 = false

say has no manner weight.

theorem Semantics.Focus.BackgroundedIslands.say_softly_has_manner_weight :

saySoftlyDecomp.hasMannerWeight = true

say softly has manner weight (from the adverb).

theorem Semantics.Focus.BackgroundedIslands.whisper_has_manner_weight :

whisperDecomp.hasMannerWeight = true

whisper has manner weight (from lexical decomposition).

theorem Semantics.Focus.BackgroundedIslands.shout_has_manner_weight :

shoutDecomp.hasMannerWeight = true

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 :

extractionRank (complementStatus (defaultDimension sayDecomp)) > extractionRank (complementStatus (defaultDimension saySoftlyDecomp))

say extraction is better than say softly extraction.

theorem Semantics.Focus.BackgroundedIslands.say_adverb_focus_sensitive :

extractionRank (complementStatus (activeDimension saySoftlyDecomp true)) > extractionRank (complementStatus (activeDimension saySoftlyDecomp false))

The say+adverb island is also focus-sensitive (like the MoS island).

§8. 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 :

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.

Instances For

instance Semantics.Focus.BackgroundedIslands.instDecidableEqMoSAccount :

DecidableEq MoSAccount

Equations

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

def Semantics.Focus.BackgroundedIslands.instReprMoSAccount.repr :

MoSAccount → ℕ → Std.Format

Equations

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

Instances For

instance Semantics.Focus.BackgroundedIslands.instReprMoSAccount :

Repr MoSAccount

Equations

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

def Semantics.Focus.BackgroundedIslands.instBEqMoSAccount.beq :

MoSAccount → MoSAccount → Bool

Equations

Semantics.Focus.BackgroundedIslands.instBEqMoSAccount.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Semantics.Focus.BackgroundedIslands.instBEqMoSAccount :

Equations

Semantics.Focus.BackgroundedIslands.instBEqMoSAccount = { beq := Semantics.Focus.BackgroundedIslands.instBEqMoSAccount.beq }

structure Semantics.Focus.BackgroundedIslands.Prediction :

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)

Instances For

instance Semantics.Focus.BackgroundedIslands.instDecidableEqPrediction :

DecidableEq Prediction

Equations

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

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.

Instances For

def Semantics.Focus.BackgroundedIslands.instReprPrediction.repr :

Prediction → ℕ → Std.Format

Equations

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

Instances For

instance Semantics.Focus.BackgroundedIslands.instReprPrediction :

Repr Prediction

Equations

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

instance Semantics.Focus.BackgroundedIslands.instBEqPrediction :

Equations

Semantics.Focus.BackgroundedIslands.instBEqPrediction = { beq := Semantics.Focus.BackgroundedIslands.instBEqPrediction.beq }

def Semantics.Focus.BackgroundedIslands.instBEqPrediction.beq :

Prediction → Prediction → Bool

Equations

One or more equations did not get rendered due to their size.
Semantics.Focus.BackgroundedIslands.instBEqPrediction.beq x✝¹ x✝ = false

Instances For

def Semantics.Focus.BackgroundedIslands.accountPredictions :

MoSAccount → Prediction

Predictions of each account.

Equations

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

Instances For

def Semantics.Focus.BackgroundedIslands.empiricalResults :

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

Equations

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

Instances For

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.

Instances For

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.

§9. 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] [DecidableEq Content] (e1 e2 : CommEvent Manner Content) :

mannerQUD.sameAnswer e1 e2 = true ↔ 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 Manner] [DecidableEq Content] (e1 e2 : CommEvent Manner Content) :

contentQUD.sameAnswer e1 e2 = true ↔ e1.content = e2.content

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

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 = Core.InformationStructure.DiscourseStatus.given

Backgroundedness = DiscourseStatus.given: The paper's notion of "backgrounded" maps directly to Kratzer & Selkirk's [G]-marked status in the existing @cite{kratzer-selkirk-2020} formalization.

This grounds the paper's informal notion of backgroundedness in the formal two-feature system already in the codebase.

theorem Semantics.Focus.BackgroundedIslands.foregrounding_is_focused :

verbStatus CommDimension.manner = Core.InformationStructure.DiscourseStatus.focused

Foregrounding = DiscourseStatus.focused: The paper's notion of "foregrounded" maps to Kratzer & Selkirk's [FoC]-marked status.