Shen and Huang (2026): The Role of Phases and Specificity in Definite Islands

This file formalizes [SH26]'s two-constraint theory of the definite island effect, the degradation of a wh-dependency into a definite depiction nominal. The Phase Impenetrability Condition (4) freezes the wh-phrase in the complement of a definite determiner ((5), impenetrable) unless a verb of creation has incorporated the determiner and collapsed the phase, after [DD03] and [Bos15]; the Specificity Condition (13) forbids binding a variable inside a specific DP from outside, whether by a moved wh-phrase or by a question operator ([Fie87], [Hua82b], [Li92]). A fronted wh-phrase leaves a deleted copy in the DP, and the PIC is violated when the link between the two leaves the phase from its interior (Minimalist.Crosses); a wh-phrase in situ is bound there and has one copy, so no link and nothing for the PIC to constrain. Constraint stacking (§4.1) counts the constraints of an account that a configuration violates (violations); of the accounts built from the two constraints, only their combination predicts the observed pattern, a definite island in both English and Mandarin with a verb-of-creation effect for fronted wh-phrases alone (observed_iff). Binding escapes the PIC because it adds no ordering statement under cyclic linearization (§4.2, binding_linearizes). On the LF-movement analysis of wh-in-situ (§5.2), with covert movement subject to the PIC, an in-situ wh-phrase has a deleted copy above it whose link leaves the DP, and no account predicts the absence of a verb-of-creation effect in Mandarin (not_observed_covert).

Implementation notes

• The experiments' effect sizes stay out of the formalization: the theory predicts the presence and direction of the contrasts, not their magnitude, which the paper notes differs across the two languages.
• Incorporation is read off the verb: a verb of creation incorporates the determiner. The conditions on incorporation the paper leaves open, and the information-structure rival of §5.1, are not formalized. The LF-movement analysis enters only in the variant with covert movement subject to the PIC; the paper's further point against it, that English verbs of creation still show a smaller definite island, is a matter of effect sizes.
• The extracted wh-phrase moves out of the DP in one step, the escape hatch at its edge being denied (§2.1); the verb phrase stands in for the clause.

References

• [SH26]
• [DD03]
• [Bos15]
• [Fie87]
• [Hua82b]
• [Li92]
• [FP05]
• [Cho00]

structure ShenHuang2026.Config : Type

A cell of the factorial design (20), (21) fixes whether the wh-phrase is fronted, as in English, or stays in situ, as in Mandarin; the definiteness of the object DP the wh-element sits in, the demonstrative being specific; and whether the main verb is a verb of creation.

• fronted : Bool
• object : Reference.Definiteness
• creation : Bool

def ShenHuang2026.instDecidableEqConfig.decEq (x✝ x✝¹ : Config) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance ShenHuang2026.instDecidableEqConfig : DecidableEq Config

Equations

• ShenHuang2026.instDecidableEqConfig = ShenHuang2026.instDecidableEqConfig.decEq

def ShenHuang2026.instReprConfig.repr : Config → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ShenHuang2026.instReprConfig : Repr Config

Equations

• ShenHuang2026.instReprConfig = { reprPrec := ShenHuang2026.instReprConfig.repr }

The object DP (5)

def ShenHuang2026.wh : Minimalist.LexicalItem.Token

The wh-phrase, the complement of about.

Equations

• ShenHuang2026.wh = { item := Minimalist.LexicalItem.of Minimalist.Cat.D [] "what" true, id := 0 }

def ShenHuang2026.about : Minimalist.LexicalItem.Token

The preposition of the depiction nominal.

Equations

• ShenHuang2026.about = { item := Minimalist.LexicalItem.of Minimalist.Cat.P [Minimalist.Cat.D] "about", id := 1 }

def ShenHuang2026.book : Minimalist.LexicalItem.Token

The head noun, selecting the depiction PP.

Equations

• ShenHuang2026.book = { item := Minimalist.LexicalItem.of Minimalist.Cat.N [Minimalist.Cat.P] "book", id := 2 }

def ShenHuang2026.that : Minimalist.LexicalItem.Token

The demonstrative determiner of a definite object.

Equations

• ShenHuang2026.that = { item := Minimalist.LexicalItem.of Minimalist.Cat.D [Minimalist.Cat.N] "that", id := 3 }

def ShenHuang2026.a : Minimalist.LexicalItem.Token

The indefinite determiner.

Equations

• ShenHuang2026.a = { item := Minimalist.LexicalItem.of Minimalist.Cat.D [Minimalist.Cat.N] "a", id := 4 }

def ShenHuang2026.verb : Minimalist.LexicalItem.Token

The main verb.

Equations

• ShenHuang2026.verb = { item := Minimalist.LexicalItem.of Minimalist.Cat.V [Minimalist.Cat.D], id := 5 }

def ShenHuang2026.determiner : Reference.Definiteness → Minimalist.LexicalItem.Token

The determiner of the object is the demonstrative when it is definite.

Equations

• ShenHuang2026.determiner Reference.Definiteness.definite = ShenHuang2026.that
• ShenHuang2026.determiner Reference.Definiteness.indefinite = ShenHuang2026.a

def ShenHuang2026.dp (o : Reference.Definiteness) : Minimalist.PlanarSyntacticObject

The object DP of (25) has the wh-phrase in the complement of the determiner.

Equations

• ShenHuang2026.dp o = ↑(ShenHuang2026.determiner o) * (↑ShenHuang2026.book * (↑ShenHuang2026.about * ↑ShenHuang2026.wh))

def ShenHuang2026.vp (o : Reference.Definiteness) : Minimalist.PlanarSyntacticObject

The verb phrase of (25).

Equations

• ShenHuang2026.vp o = ↑ShenHuang2026.verb * ShenHuang2026.dp o

theorem ShenHuang2026.impenetrable (o : Reference.Definiteness) : (↑(vp o)).WithinComplement (determiner o) ↑wh

The wh-phrase lies in the domain of the determiner, so the PIC (4) freezes it in any phase the determiner heads (5).

def ShenHuang2026.vpEdge : Minimalist.PlanarSyntacticObject

The escape hatch the account denies (§2.1) is the verb phrase with the wh-phrase moved to Spec,DP.

Equations

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

theorem ShenHuang2026.edge_not_impenetrable : ↑wh ∈ (↑vpEdge).phaseEdge that

At the edge of the phase, the wh-phrase is in the phase but outside the reach of the PIC.

def ShenHuang2026.extracted (o : Reference.Definiteness) : Minimalist.PlanarSyntacticObject

The wh-phrase fronted out of the object DP, leaving a deleted copy in the complement of about.

Equations

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

def ShenHuang2026.covert (o : Reference.Definiteness) : Minimalist.PlanarSyntacticObject

The LF-movement analysis of an in-situ wh-phrase ([Hua82b], §5.2) puts a deleted copy above the pronounced one.

Equations

• ShenHuang2026.covert o = Minimalist.PlanarSyntacticObject.traceOf ShenHuang2026.wh * ShenHuang2026.vp o

def ShenHuang2026.Config.tree (c : Config) : Minimalist.PlanarSyntacticObject

The object of a cell is the wh-phrase extracted, or in situ, bound by an operator after [Li92].

Equations

• c.tree = if c.fronted = true then ShenHuang2026.extracted c.object else ShenHuang2026.vp c.object

def ShenHuang2026.Config.covertTree (c : Config) : Minimalist.PlanarSyntacticObject

The object of a cell on the LF-movement analysis of wh-in-situ.

Equations

• c.covertTree = if c.fronted = true then ShenHuang2026.extracted c.object else ShenHuang2026.covert c.object

The two constraints

def ShenHuang2026.Config.phaseHead (c : Config) : Option Minimalist.LexicalItem.Token

On the DP phasehood account (§2.1) the demonstrative heads a phase, which a verb of creation collapses by incorporating it.

Equations

• c.phaseHead = if c.object = Reference.Definiteness.definite ∧ c.creation = false then some ShenHuang2026.that else none

def ShenHuang2026.Config.specific (c : Config) : Option Minimalist.SyntacticObject

The demonstrative-marked DP is the specific one, in [Fie87]'s sense of familiar.

Equations

• c.specific = if c.object = Reference.Definiteness.definite then some ↑(ShenHuang2026.dp c.object) else none

def ShenHuang2026.Config.ViolatesPIC (c : Config) (t : Minimalist.PlanarSyntacticObject) : Prop

The PIC (4) is violated in t when a link of the wh-phrase's chain leaves the phase that the cell's determiner heads, from its interior.

Equations

• c.ViolatesPIC t = ∃ ℓ ∈ c.phaseHead, ∃ h ∈ Minimalist.occurrences t ℓ, Minimalist.Crosses t ShenHuang2026.wh h

@[instance_reducible]

instance ShenHuang2026.instDecidableViolatesPIC (c : Config) (t : Minimalist.PlanarSyntacticObject) : Decidable (c.ViolatesPIC t)

Equations

• ShenHuang2026.instDecidableViolatesPIC c t = ShenHuang2026.instDecidableViolatesPIC._aux_1 c t

inductive ShenHuang2026.Constraint : Type

The two constraints.

• pic : Constraint
• specificity : Constraint

@[instance_reducible]

instance ShenHuang2026.instDecidableEqConstraint : DecidableEq Constraint

Equations

• ShenHuang2026.instDecidableEqConstraint x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ShenHuang2026.instReprConstraint : Repr Constraint

Equations

• ShenHuang2026.instReprConstraint = { reprPrec := ShenHuang2026.instReprConstraint.repr }

def ShenHuang2026.instReprConstraint.repr : Constraint → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ShenHuang2026.instFintypeConstraint : Fintype Constraint

Equations

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

def ShenHuang2026.Constraint.Violated : Constraint → Config → Prop

The Phase Impenetrability Condition (4) is violated when a link of the wh-phrase's chain leaves a phase from its interior; the Specificity Condition (13) when a variable inside a specific DP is bound from outside, whatever the binder.

Equations

• ShenHuang2026.Constraint.pic.Violated x✝ = x✝.ViolatesPIC x✝.tree
• ShenHuang2026.Constraint.specificity.Violated x✝ = ∃ d ∈ x✝.specific, d.Contains ↑ShenHuang2026.wh

@[instance_reducible]

instance ShenHuang2026.instDecidablePredConfigViolated (k : Constraint) : DecidablePred k.Violated

Equations

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

theorem ShenHuang2026.violatesPIC_iff_not_accessible (c : Config) : c.ViolatesPIC c.tree ↔ ¬(↑c.tree).Accessible c.phaseHead.toList Minimalist.Impenetrability.phase (↑wh) (Minimalist.SyntacticObject.traceOf wh)

The PIC on the links of the chain agrees with the PIC on terms: a link leaves the phase from its interior exactly when the deleted copy, within the complement of the cell's phase head, is inaccessible to the pronounced one under [Cho00]'s condition.

theorem ShenHuang2026.pic_violated_iff (c : Config) : Constraint.pic.Violated c ↔ c.fronted = true ∧ c.object = Reference.Definiteness.definite ∧ c.creation = false

Fronting out of a definite object under a verb that is not a verb of creation, and nothing else, violates the PIC.

theorem ShenHuang2026.violatesPIC_covertTree_iff (c : Config) : c.ViolatesPIC c.covertTree ↔ c.object = Reference.Definiteness.definite ∧ c.creation = false

On the LF-movement analysis with covert movement subject to the PIC, an in-situ wh-phrase crosses the phase wherever a fronted one does, so the analysis predicts a definite island that a verb of creation removes in Mandarin too (§3, §5.2), the verb-of-creation effect the Mandarin experiment does not find (Table 2).

theorem ShenHuang2026.specificity_violated_iff (c : Config) : Constraint.specificity.Violated c ↔ c.object = Reference.Definiteness.definite

A definite object, and nothing else, violates the Specificity Condition.

Constraint stacking (§4.1)

def ShenHuang2026.violations (account : Finset Constraint) (c : Config) : ℕ

The number of constraints of an account that a configuration violates, the more the less acceptable.

Equations

• ShenHuang2026.violations account c = {x ∈ account | x.Violated c}.card

def ShenHuang2026.phasehood : Finset Constraint

The DP phasehood account.

Equations

• ShenHuang2026.phasehood = {ShenHuang2026.Constraint.pic}

def ShenHuang2026.specificity : Finset Constraint

The Specificity Condition account.

Equations

• ShenHuang2026.specificity = {ShenHuang2026.Constraint.specificity}

def ShenHuang2026.combined : Finset Constraint

The paper's proposal combines both constraints.

Equations

• ShenHuang2026.combined = {ShenHuang2026.Constraint.pic, ShenHuang2026.Constraint.specificity}

theorem ShenHuang2026.violations_indefinite (account : Finset Constraint) (fronted v : Bool) : violations account { fronted := fronted, object := Reference.Definiteness.indefinite, creation := v } = 0

An indefinite object violates nothing under any account: it is neither a phase nor specific.

def ShenHuang2026.IslandEffect (account : Finset Constraint) (fronted v : Bool) : Prop

An account predicts a definite island effect for a fronted or an in-situ wh-phrase and a verb class when the definite object violates more of its constraints than the indefinite one.

Equations

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

def ShenHuang2026.VOCEffect (account : Finset Constraint) (fronted : Bool) : Prop

An account predicts a verb-of-creation effect for a fronted or an in-situ wh-phrase when a verb of creation lowers the count for a definite object; an indefinite one violates nothing either way.

Equations

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

@[instance_reducible]

instance ShenHuang2026.instDecidableIslandEffect (account : Finset Constraint) (fronted v : Bool) : Decidable (IslandEffect account fronted v)

Equations

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

@[instance_reducible]

instance ShenHuang2026.instDecidableVOCEffect (account : Finset Constraint) (fronted : Bool) : Decidable (VOCEffect account fronted)

Equations

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

def ShenHuang2026.Observed (account : Finset Constraint) : Prop

Experiments 1 and 2 found (Table 2) a definite island for fronted and in-situ wh-phrases under every verb class, and a verb-of-creation effect for the fronted ones alone.

Equations

• ShenHuang2026.Observed account = ((∀ (fronted v : Bool), ShenHuang2026.IslandEffect account fronted v) ∧ ShenHuang2026.VOCEffect account true ∧ ¬ShenHuang2026.VOCEffect account false)

@[instance_reducible]

instance ShenHuang2026.instDecidableObserved (account : Finset Constraint) : Decidable (Observed account)

Equations

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

theorem ShenHuang2026.phasehood_predictions : IslandEffect phasehood true false ∧ ¬IslandEffect phasehood true true ∧ VOCEffect phasehood true ∧ ∀ (v : Bool), ¬IslandEffect phasehood false v

DP phasehood alone (Table 1) predicts an island for a fronted wh-phrase only under a verb that is not a verb of creation, hence a verb-of-creation effect, and no island in situ.

theorem ShenHuang2026.specificity_predictions : (∀ (fronted v : Bool), IslandEffect specificity fronted v) ∧ ∀ (fronted : Bool), ¬VOCEffect specificity fronted

The Specificity Condition alone (Table 1) predicts an island for fronted and in-situ wh-phrases under every verb class, and no verb-of-creation effect.

theorem ShenHuang2026.observed_iff (account : Finset Constraint) : Observed account ↔ account = combined

Of the accounts built from the two constraints, exactly the combination predicts the observed pattern (Table 2): one constraint is not empirically adequate.

The cited judgments

def ShenHuang2026.Config.ofDatum (ex : Datum) : Option Config

The configuration an example's features record.

Equations

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

theorem ShenHuang2026.stacking_daviesDubinsky (ex₁ : Datum) : ex₁ ∈ DaviesDubinsky2003.Examples.all → ∀ ex₂ ∈ DaviesDubinsky2003.Examples.all, ∀ c₁ ∈ Config.ofDatum ex₁, ∀ c₂ ∈ Config.ofDatum ex₂, violations combined c₁ < violations combined c₂ → ex₂.judgment.rank ≤ ex₁.judgment.rank

In the verb-of-creation contrasts of [DD03], (52)–(54), which the paper's Experiment 1 revisits, a non-creation verb with a definite object violates one constraint of the combined account more than a creation verb, and the row is judged no better.

theorem ShenHuang2026.stacking (ex₁ : Datum) : ex₁ ∈ Examples.all → ∀ ex₂ ∈ Examples.all, ex₁.language = ex₂.language → ∀ c₁ ∈ Config.ofDatum ex₁, ∀ c₂ ∈ Config.ofDatum ex₂, violations combined c₁ < violations combined c₂ → ex₂.judgment.rank ≤ ex₁.judgment.rank

Constraints stack on the paper's cited judgments, since within a language an example violating strictly more constraints of the combined account is judged no better.

Binding and the PIC under cyclic linearization (§4.2)

inductive ShenHuang2026.Terminal : Type

A terminal is a word of What do you think Mary would eat? (27).

• what : Terminal
• do : Terminal
• you : Terminal
• think : Terminal
• mary : Terminal
• would : Terminal
• eat : Terminal

@[instance_reducible]

instance ShenHuang2026.instDecidableEqTerminal : DecidableEq Terminal

Equations

• ShenHuang2026.instDecidableEqTerminal x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ShenHuang2026.instReprTerminal.repr : Terminal → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ShenHuang2026.instReprTerminal : Repr Terminal

Equations

• ShenHuang2026.instReprTerminal = { reprPrec := ShenHuang2026.instReprTerminal.repr }

def ShenHuang2026.Terminal.token : Terminal → Minimalist.LexicalItem.Token

Each terminal spells out its own lexical item.

Equations

• ShenHuang2026.Terminal.what.token = { item := Minimalist.LexicalItem.of Minimalist.Cat.D [], id := 11 }
• ShenHuang2026.Terminal.do.token = { item := Minimalist.LexicalItem.of Minimalist.Cat.T [], id := 12 }
• ShenHuang2026.Terminal.you.token = { item := Minimalist.LexicalItem.of Minimalist.Cat.D [], id := 13 }
• ShenHuang2026.Terminal.think.token = { item := Minimalist.LexicalItem.of Minimalist.Cat.V [], id := 14 }
• ShenHuang2026.Terminal.mary.token = { item := Minimalist.LexicalItem.of Minimalist.Cat.D [], id := 15 }
• ShenHuang2026.Terminal.would.token = { item := Minimalist.LexicalItem.of Minimalist.Cat.T [], id := 16 }
• ShenHuang2026.Terminal.eat.token = { item := Minimalist.LexicalItem.of Minimalist.Cat.V [], id := 17 }

def ShenHuang2026.Terminal.ofToken? (tok : Minimalist.LexicalItem.Token) : Option Terminal

A lexical item spells out at most one terminal.

Equations

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

def ShenHuang2026.embeddedC : Minimalist.LexicalItem.Token

The embedded complementizer is silent.

Equations

• ShenHuang2026.embeddedC = { item := Minimalist.LexicalItem.of Minimalist.Cat.C [], id := 18 }

def ShenHuang2026.embeddedSteps : List Minimalist.Step

In the embedded clause eat merges with what, then would, Mary and the complementizer.

Equations

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

def ShenHuang2026.matrixSteps : List Minimalist.Step

In the matrix clause think, you and do merge over the embedded clause.

Equations

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

def ShenHuang2026.moveWhat (b : Bool) : List Minimalist.Step

What moves to the edge of the clause built so far, or stays.

Equations

• ShenHuang2026.moveWhat b = if b = true then [Minimalist.Step.im ↑ShenHuang2026.Terminal.what.token] else []

def ShenHuang2026.derivation (edge front : Bool) : Minimalist.Derivation

In a derivation of (27) what stops at the edge of the embedded clause or not, and then moves to the edge of the matrix clause or stays in situ.

Equations

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

def ShenHuang2026.embeddedStage (edge : Bool) : ℕ

The embedded clause is built once what has stopped at its edge or not.

Equations

• ShenHuang2026.embeddedStage edge = (ShenHuang2026.embeddedSteps ++ ShenHuang2026.moveWhat edge).length

def ShenHuang2026.schedule (edge front : Bool) : List (ℕ × ℕ)

Each clause is spelled out when it is built.

Equations

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

theorem ShenHuang2026.embedded_spellout (edge front : Bool) : List.filterMap Terminal.ofToken? ((derivation edge front).spellout (embeddedStage edge) (embeddedStage edge)) = if edge = true then [Terminal.what, Terminal.mary, Terminal.would, Terminal.eat] else [Terminal.mary, Terminal.would, Terminal.eat, Terminal.what]

The embedded clause is spelled out with what first when it stops at the edge, and last when it stays in situ (27).

theorem ShenHuang2026.edge_stop_linearizes : (derivation true true).Linearizes (schedule true true)

When what stops at the edge of the embedded clause (27a), the order fixed there is preserved at the matrix Spell-out and the derivation linearizes.

theorem ShenHuang2026.phase_skip_not_linearizes : ¬(derivation false true).Linearizes (schedule false true)

When what stays in situ as the embedded clause is spelled out (27b), it follows Mary there and precedes her at the matrix Spell-out, an ordering contradiction; this is the cyclic-linearization content of the PIC on movement.

theorem ShenHuang2026.binding_linearizes : (derivation false false).Linearizes (schedule false false)

Binding leaves the word order alone: with what in situ at both Spell-outs no ordering statement is added and the derivation linearizes, so a dependency established by binding never meets the contradiction that enforces the PIC on movement.

Verbs of creation in the Fragment

def ShenHuang2026.IsVerbOfCreation (v : English.Verbs.Verb) : Prop

The paper names as verbs of creation, after [DD03]'s verbs of creation selecting a result nominal (write for a book, tell for a joke, paint for a portrait), compose (3), tell a joke (20b), direct (23), shoot, make and compose a video or song (footnote 12), and write (25b). The notion is per verb, not a Levin class: tell and shoot belong to no class of creation in [Lev93].

Equations

• ShenHuang2026.IsVerbOfCreation v = (v.form ∈ ["compose", "direct", "make", "shoot", "tell", "write"])

@[instance_reducible]

instance ShenHuang2026.instDecidablePredVerbIsVerbOfCreation : DecidablePred IsVerbOfCreation

Equations

• ShenHuang2026.instDecidablePredVerbIsVerbOfCreation v = { decide := decide (List.elem v.form ["compose", "direct", "make", "shoot", "tell", "write"] = true), reflects_decide := ⋯ }

def ShenHuang2026.Config.ofVerb (fronted : Bool) (o : Reference.Definiteness) (v : English.Verbs.Verb) : Config

The configuration of an item whose main verb is a Fragment entry.

Equations

• ShenHuang2026.Config.ofVerb fronted o v = { fronted := fronted, object := o, creation := decide (ShenHuang2026.IsVerbOfCreation v) }

theorem ShenHuang2026.read_write : violations combined (Config.ofVerb true Reference.Definiteness.definite English.Verbs.read) = 2 ∧ violations combined (Config.ofVerb true Reference.Definiteness.definite English.Verbs.write) = 1

In (25) read that book about violates both constraints and write that book about the Specificity Condition alone, the residual definite island under a verb of creation.