Locality on chains

Locality constrains the links of a chain. Chomsky's Phase Impenetrability Condition bars a link from the interior of a phase, the positions its head c-commands, to a position outside the head's maximal projection, so that the edge is the escape hatch (Crosses); an island is a domain no link may leave (Escapes). A token with one copy has no link, so binding in situ is subject to neither (not_crosses_of_length_le_one, not_escapes_of_length_le_one), and movement, covert movement included, is subject to both, as Sato and Ngui find. The interior of a phase on positions is the c-command domain of its head (RoseTree.cCommandDomain), and it carries the terms within the complement of the unordered phase (withinComplement_iff_exists_mem_cCommandDomain).

Main definitions

• Minimalist.Crosses, Minimalist.Escapes: a link leaving a phase from its interior, and a link leaving a domain.

Main statements

• Minimalist.withinComplement_iff_exists_mem_cCommandDomain: the positions a phase head occurring once c-commands carry the terms within its complement.

Implementation notes

• Positions, not terms, individuate copies, so the phase interior of the unordered object (SyntacticObject.phaseInterior) cannot tell the links of a successive-cyclic chain apart, and the locality of links is stated on positions.

References

• [Cho00]
• [SN17]
• [MCB25]

theorem Minimalist.withinComplement_iff_exists_mem_cCommandDomain {t : PlanarSyntacticObject} {ℓ : LexicalItem.Token} {a : (↑t).Positions} {x : SyntacticObject} (hu : ∀ (q : (↑t).Positions), t.termAt q = ↑ℓ ↔ q = a) (hph : (↑t).IsPhaseHead ℓ) : (↑t).WithinComplement ℓ x ↔ ∃ (q : (↑t).Positions), ↑q ∈ (↑t).cCommandDomain ↑a ∧ t.termAt q = x

The positions a phase head occurring only at a c-commands carry the terms within its complement.

def Minimalist.Crosses (t : PlanarSyntacticObject) (tok : LexicalItem.Token) (h : Core.Order.TreePath) : Prop

A link of the chain of tok leaves the phase headed at h when it runs from a position the head c-commands, the phase's interior, to a position outside the head's maximal projection; the Phase Impenetrability Condition forbids it, and a link to the edge does not leave.

Equations

• Minimalist.Crosses t tok h = ∃ x ∈ Minimalist.links t tok, x.2 ∈ (↑t).cCommandDomain h ∧ ¬Minimalist.projectionAt t h ≤ x.1

@[instance_reducible]

instance Minimalist.instDecidableCrosses (t : PlanarSyntacticObject) (tok : LexicalItem.Token) (h : Core.Order.TreePath) : Decidable (Crosses t tok h)

Equations

• Minimalist.instDecidableCrosses t tok h = Minimalist.instDecidableCrosses._aux_1 t tok h

def Minimalist.Escapes (t : PlanarSyntacticObject) (tok : LexicalItem.Token) (D : Core.Order.TreePath) : Prop

A link of the chain of tok leaves the domain at D when it runs from inside D to outside, as movement out of an island does.

Equations

• Minimalist.Escapes t tok D = ∃ x ∈ Minimalist.links t tok, D ≤ x.2 ∧ ¬D ≤ x.1

@[instance_reducible]

instance Minimalist.instDecidableEscapes (t : PlanarSyntacticObject) (tok : LexicalItem.Token) (D : Core.Order.TreePath) : Decidable (Escapes t tok D)

Equations

• Minimalist.instDecidableEscapes t tok D = Minimalist.instDecidableEscapes._aux_1 t tok D

theorem Minimalist.not_crosses_of_length_le_one (t : PlanarSyntacticObject) (tok : LexicalItem.Token) (h : (chain t tok).length ≤ 1) (hd : Core.Order.TreePath) : ¬Crosses t tok hd

theorem Minimalist.not_escapes_of_length_le_one (t : PlanarSyntacticObject) (tok : LexicalItem.Token) (h : (chain t tok).length ≤ 1) (D : Core.Order.TreePath) : ¬Escapes t tok D