Docs / Syntax / Minimalist / Locality / Freezing

Freezing

import Linglib.Syntax.Minimalist.Locality.Freezing · namespace Minimalist.Derivation

A constituent that has moved is an island for later extraction, though it may itself move again. This is the Freezing condition, and it is what makes VP-raising analyses of VOS order testable, since whatever a raised VP still contains cannot be extracted and whatever left it before it raised can. Frozen d x says that x sits inside some mover of d, and ObeysFreezing d that no mover of d sits inside an earlier one, a pairwise condition on the list of movers in the shape of List.Nodup. Movers carry the traces of what evacuated them earlier, not the evacuees, so a remnant freezes nothing that left it. Its rival, the Unlabeled Immobility Condition, lets a moved constituent be extracted from and instead bars a constituent from moving when it is unlabeled in the object built so far, as a phrase whose specifier does not agree with it is.

Main definitions

Minimalist.Derivation.Frozen, Minimalist.Derivation.ObeysFreezing
Minimalist.Derivation.ObeysUIC: every mover is labeled when it moves.

Main results

Minimalist.Derivation.frozen_append_iff: extending a derivation freezes what its new movers contain and nothing else.
Minimalist.Derivation.obeysFreezing_append_im_iff: a further movement obeys Freezing exactly when its mover is not frozen.
Minimalist.Derivation.obeysUIC_append_im_iff: a further movement obeys the Unlabeled Immobility Condition exactly when its mover is labeled.

References

Müller 1998, Incomplete Category Fronting
Chung 2006, Properties of VOS Languages
Collins 2005, A Smuggling Approach to the Passive in English formalized
Cole & Hermon 2008, VP Raising in a VOS Language formalized
Bošković 2018, On movement out of moved elements, labels, and phases formalized

Declarations

x sits inside a constituent d has moved.

def Frozen L56–57

(d : Derivation) (x : SyntacticObject) :

Prop

d.Frozen x = ∃ m ∈ d.movedItems, m.Contains x

Used by instDecidableFrozen, frozen_append_iff, Frozen.append, frozen_leftward_iff, obeysFreezing_append_iff, obeysFreezing_append_im_iff, frozen_map_iff

Used in Syntax/Minimalist/Derivation/Smuggling, ColeHermon2008

L59–60

Extending a derivation freezes what its new movers contain and nothing else.

theorem frozen_append_iff L62–66

{d : Derivation} {steps : List Step} {x : SyntacticObject} :

(d.append steps).Frozen x ↔ d.Frozen x ∨ ∃ m ∈ List.filterMap Step.mover? steps, m.Contains x

Built from

L68–69

L71–72

A derivation obeys Freezing when no step moves a constituent that an earlier mover contains.

def ObeysFreezing L74–77

(d : Derivation) :

Prop

d.ObeysFreezing = List.Pairwise (fun (m m' : Minimalist.SyntacticObject) => ¬m.Contains m') d.movedItems

Used by instDecidableObeysFreezing, obeysFreezing_append_iff, obeysFreezing_append_im_iff, obeysFreezing_append_em_iff, obeysFreezing_map_iff

Used in Syntax/Minimalist/Derivation/Smuggling, Boskovic2018, ColeHermon2008, Collins2005, Privizentseva2026

L79–80

L82–87

A further movement obeys Freezing exactly when its mover is not frozen.

@[simp] theorem obeysFreezing_append_im_iff L89–92

{d : Derivation} {m : SyntacticObject} {side : Edge} :

(d.append [Step.im m side]).ObeysFreezing ↔ d.ObeysFreezing ∧ ¬d.Frozen m

Built from ,

L94–96

Relabelling

L104–105

L107–109

Unlabeled immobility

Bošković 2018's Unlabeled Immobility Condition: each mover of d is labeled, as L reads labels, in the object the derivation has built when it moves.

def ObeysUIC L117–120

(L : LinearizedSyntacticObject → SyntacticObject → Prop) (d : Derivation) :

Prop

ObeysUIC L d = ∀ i < d.length, ∀ m ∈ d.mover? i, ∃ p ∈ (d.take i).externalize?, L p m

Used by instDecidableObeysUICOfDecidablePredSyntacticObjectToken, ObeysUIC.mono, obeysUIC_append_singleton_iff, obeysUIC_append_im_iff, obeysUIC_append_em_iff

Used in Boskovic2018

L122–123

L127–129

L131–149

A further movement obeys the Unlabeled Immobility Condition exactly when its mover is labeled in the object built so far.

@[simp] theorem obeysUIC_append_im_iff L151–155

{d : Derivation} {L : LinearizedSyntacticObject → SyntacticObject → Prop} {m : SyntacticObject} {side : Edge} :

ObeysUIC L (d.append [Step.im m side]) ↔ ObeysUIC L d ∧ ∃ p ∈ d.externalize?, L p m

Built from

L157–159