Smuggling

A constituent YP containing XP moves past W, which blocked XP: after the move YP c-commands W and W no longer c-commands XP, so a probe above W that W would have intervened for now reaches XP. On a derivation this is the step predicate Derivation.IsSmugglingStep, read off the replayed stages through Derivation.CCommandsAt: the mover of the step contains xp, w c-commands xp before the step, and after it the mover c-commands w and w no longer c-commands xp. The blocking is rendered as w's c-command of xp; the probe it matters for is the consumer's to supply, as the passive study does when Infl finds the object closest once PartP has carried it past the external argument in Spec-vP. Which heads let a constituent out of their complement is a question each account answers for itself, and none is fixed here. What a step smuggles is frozen, so a derivation that goes on to move it violates Freezing, which smuggling accounts must therefore lift for the smuggling movement.

Main results

• Minimalist.Derivation.IsSmugglingStep.not_obeysFreezing_append_im: moving the smuggled phrase on violates Freezing.

References

• [Col05]
• [Mul98]

def Minimalist.Derivation.IsSmugglingStep (d : Derivation) (i : ℕ) (xp w : SyntacticObject) : Prop

Step i of d smuggles xp past w when its mover contains xp, which w c-commands before the step, and after it the mover c-commands w and w no longer c-commands xp.

Equations

• d.IsSmugglingStep i xp w = ∃ m ∈ d.mover? i, m.Contains xp ∧ d.CCommandsAt i w xp ∧ d.CCommandsAt (i + 1) m w ∧ ¬d.CCommandsAt (i + 1) w xp

@[instance_reducible]

instance Minimalist.Derivation.instDecidableIsSmugglingStep (d : Derivation) (i : ℕ) (xp w : SyntacticObject) : Decidable (d.IsSmugglingStep i xp w)

Equations

• d.instDecidableIsSmugglingStep i xp w = id inferInstance

theorem Minimalist.Derivation.IsSmugglingStep.append {d : Derivation} {steps : List Step} {i : ℕ} {xp w : SyntacticObject} (h : d.IsSmugglingStep i xp w) : (d.append steps).IsSmugglingStep i xp w

A smuggling step of a derivation is one of every extension.

theorem Minimalist.Derivation.IsSmugglingStep.frozen {d : Derivation} {i : ℕ} {xp w : SyntacticObject} (h : d.IsSmugglingStep i xp w) : d.Frozen xp

What a step smuggles is frozen, since the smuggler contains it.

theorem Minimalist.Derivation.IsSmugglingStep.not_obeysFreezing_append_im {d : Derivation} {i : ℕ} {xp w : SyntacticObject} (h : d.IsSmugglingStep i xp w) (side : Edge) : ¬(d.append [Step.im xp side]).ObeysFreezing

Moving the smuggled phrase on violates Freezing.