Docs / Syntax / Minimalist / Locality / Phase

Phases

import Linglib.Syntax.Minimalist.Locality.Phase · namespace Minimalist

The phases of Marcolli et al. 2025 §1.14, after Chomsky 2013, with the raising head SyntacticObject.raisingHead as head function. A lexical item heads a phase when it projects, and its complement is the sister it projects over. The phase is what lies within the terms the head heads; its interior is what lies within the complement; and its edge is the rest of the phase, the head and what is merged above it, a phrase raised to the edge included. The Phase Impenetrability Condition seals the interior: under Chomsky 2000's condition to everything outside the phase, under Chomsky 2001's only once the next phase head up is merged, to what lies outside its interior.

Main definitions

SyntacticObject.IsPhaseHead, SyntacticObject.IsComplementOf: a lexical item projects, and the sister it projects over.
SyntacticObject.WithinProjection, SyntacticObject.WithinComplement: a term lies within the projection or the complement of a head.
SyntacticObject.phase, SyntacticObject.phaseInterior, SyntacticObject.phaseEdge: the phase of a head, its interior, and its edge.
Impenetrability, SyntacticObject.Accessible: the two conditions, and the goals each leaves accessible to a probe.

Main statements

SyntacticObject.isPhaseHead_iff_phaseInterior_ne_zero: a head projects exactly when its phase has a nonempty interior.
SyntacticObject.phaseInterior_add_phaseEdge: the interior and the edge partition the phase.
SyntacticObject.phaseInterior_eq_cCommandDomain: the interior of a head that projects wherever it occurs is its c-command domain.
SyntacticObject.Accessible.nextPhase_of_phase: Chomsky 2000's condition is the stronger.

Implementation notes

Terms are values, not occurrences, so all copies of a head share one phase, and the lower copies of a moved phrase are one term; positions tell copies apart in Copy/Chain.lean.
Every head that projects heads a phase, as in the book; the heads a study counts as phase heads (C alone, or also v, D, or Voice) are the list Accessible takes.
Under the raising head a phrase raised to the edge of a head lies in its phase; a phrase merged there in place lies in it only when the head selects it.

TODO

The terms made inaccessible by the interiors of lower phases, and the stricter variant that also freezes their heads.
The two statements of Chomsky 2001's condition differ on a phase in the edge of the next phase. Accessible .nextPhase seals the interior of H against a probe outside the complement of any phase head Z whose projection contains H, the edge of Z included, while Pic2 in Locality/Transfer.lean seals it only once a phase head whose complement contains the phase of H has merged.

References

Marcolli et al. 2025, Mathematical Structure of Syntactic Merge: An Algebraic Model for Generative Linguistics formalized
Chomsky 2013, Problems of Projection formalized
Chomsky 2000, Minimalist Inquiries: The Framework
Chomsky 2001, Derivation by Phase

Declarations

When the Phase Impenetrability Condition seals the interior of a phase head.

inductive Impenetrability L75–82

Type

phase : Impenetrability
Once the phase is built, to everything outside it (Chomsky 2000).
nextPhase : Impenetrability
Once the next phase head up is merged, to everything outside its interior (Chomsky 2001).

Derives DecidableEq, Repr.

Used by SyntacticObject.Accessible, SyntacticObject.instDecidableAccessible

Used in Pietraszko2026

ℓ heads a phase of T when it projects, heading a mother of its leaf.

def SyntacticObject.IsPhaseHead L90–91

(T : SyntacticObject) (ℓ : LexicalItem.Token) :

Prop

T.IsPhaseHead ℓ = ∃ m ∈ T.terms, m.raisingHead = some ℓ ∧ m.ImmediatelyContains ↑ℓ

Used by SyntacticObject.instDecidableIsPhaseHead, SyntacticObject.isPhaseHead_iff_exists_isComplementOf, SyntacticObject.isPhaseHead_iff_phaseInterior_ne_zero

Used in Syntax/Minimalist/Locality/Chain

L93

z is the complement of ℓ in T when ℓ projects over its sister z.

def SyntacticObject.IsComplementOf L95–98

(T : SyntacticObject) (ℓ : LexicalItem.Token) (z : SyntacticObject) :

Prop

T.IsComplementOf ℓ z = ∃ m ∈ T.terms, m.raisingHead = some ℓ ∧ m.ImmediatelyContains ↑ℓ ∧ m.ImmediatelyContains z ∧ z ≠ ↑ℓ

Used by SyntacticObject.instDecidableIsComplementOf, SyntacticObject.WithinComplement, SyntacticObject.IsComplementOf.mem_terms, SyntacticObject.isPhaseHead_iff_exists_isComplementOf

L100

x lies within the projection of ℓ in T when a term of T that ℓ heads contains it.

def SyntacticObject.WithinProjection L102–103

(T : SyntacticObject) (ℓ : LexicalItem.Token) (x : SyntacticObject) :

Prop

T.WithinProjection ℓ x = ∃ p ∈ T.terms, p.raisingHead = some ℓ ∧ p.ContainsOrEq x

Used by SyntacticObject.instDecidableWithinProjection, SyntacticObject.phase, SyntacticObject.WithinProjection.mem_terms, SyntacticObject.WithinComplement.withinProjection, SyntacticObject.WithinProjection.trans, SyntacticObject.mem_phase, SyntacticObject.mem_phaseEdge, SyntacticObject.Accessible

Used in Zeijlstra2012

L105

x lies within the complement of ℓ in T when a complement of ℓ contains it.

def SyntacticObject.WithinComplement L107–108

(T : SyntacticObject) (ℓ : LexicalItem.Token) (x : SyntacticObject) :

Prop

T.WithinComplement ℓ x = ∃ z ∈ T.terms, T.IsComplementOf ℓ z ∧ z.ContainsOrEq x

Built from

Used by SyntacticObject.instDecidableWithinComplement, SyntacticObject.phaseInterior, SyntacticObject.WithinComplement.withinProjection, SyntacticObject.WithinComplement.mem_terms, SyntacticObject.WithinComplement.trans, SyntacticObject.WithinComplement.cCommands, SyntacticObject.mem_phaseInterior, SyntacticObject.mem_phaseEdge, SyntacticObject.Accessible

Used in Syntax/Minimalist/Locality/Chain, Greco2020, ShenHuang2026, Zeijlstra2012

L110

The phase of ℓ in T is the multiset of terms within its projection.

def SyntacticObject.phase L112–113

(T : SyntacticObject) (ℓ : LexicalItem.Token) :

Multiset SyntacticObject

T.phase ℓ = Multiset.filter (T.WithinProjection ℓ) T.terms

Built from

Used by SyntacticObject.phaseEdge, SyntacticObject.mem_phase, SyntacticObject.phaseInterior_le_phase, SyntacticObject.phaseInterior_add_phaseEdge

Used in Zeijlstra2012

The interior of the phase of ℓ in T is the multiset of terms within its complement.

def SyntacticObject.phaseInterior L115–116

(T : SyntacticObject) (ℓ : LexicalItem.Token) :

Multiset SyntacticObject

T.phaseInterior ℓ = Multiset.filter (T.WithinComplement ℓ) T.terms

Built from

Used by SyntacticObject.phaseEdge, SyntacticObject.mem_phaseInterior, SyntacticObject.isPhaseHead_iff_phaseInterior_ne_zero, SyntacticObject.phaseInterior_le_phase, SyntacticObject.phaseInterior_add_phaseEdge, SyntacticObject.phaseInterior_le_cCommandDomain, SyntacticObject.phaseInterior_eq_cCommandDomain

Used in Zeijlstra2012

The edge of the phase of ℓ in T is the multiset of terms of the phase outside its interior.

def SyntacticObject.phaseEdge L118–120

(T : SyntacticObject) (ℓ : LexicalItem.Token) :

Multiset SyntacticObject

T.phaseEdge ℓ = Multiset.filter (fun (x : SyntacticObject) => x ∉ T.phaseInterior ℓ) (T.phase ℓ)

Built from ,

Used by SyntacticObject.mem_phaseEdge, SyntacticObject.phaseInterior_add_phaseEdge

Used in ShenHuang2026, Zeijlstra2012

A head projects exactly when its phase has a nonempty interior.

theorem SyntacticObject.isPhaseHead_iff_phaseInterior_ne_zero L175–182

{T : SyntacticObject} {ℓ : LexicalItem.Token} :

T.IsPhaseHead ℓ ↔ T.phaseInterior ℓ ≠ 0

Built from ,

L184–185

The interior and the edge partition the phase.

theorem SyntacticObject.phaseInterior_add_phaseEdge L187–193

{T : SyntacticObject} {ℓ : LexicalItem.Token} :

T.phaseInterior ℓ + T.phaseEdge ℓ = T.phase ℓ

Built from , ,

L195–196

The interior of a head that projects wherever it occurs is its c-command domain.

theorem SyntacticObject.phaseInterior_eq_cCommandDomain L198–203

{T : SyntacticObject} {ℓ : LexicalItem.Token} (h : ∀ m ∈ T.terms, m.ImmediatelyContains ↑ℓ → m.raisingHead = some ℓ) :

T.phaseInterior ℓ = T.cCommandDomain ↑ℓ

Built from

The Phase Impenetrability Condition

goal is accessible to probe in T under the condition s, the phase heads being heads: a goal within the complement of a phase head is reachable only from within its phase, under Chomsky 2001's condition only once a phase head above it is merged and the probe lies outside that head's interior.

def SyntacticObject.Accessible L208–216

(T : SyntacticObject) (heads : List LexicalItem.Token) :

Impenetrability → SyntacticObject → SyntacticObject → Prop

The definition is too large to print here; read it in the source.

Built from , ,

Used by SyntacticObject.instDecidableAccessible, SyntacticObject.Accessible.nextPhase_of_phase

Used in ShenHuang2026

L218–220

Chomsky 2000's condition is the stronger: what it leaves accessible, Chomsky 2001's does too.

theorem SyntacticObject.Accessible.nextPhase_of_phase L222–227

{T : SyntacticObject} {heads : List LexicalItem.Token} {probe goal : SyntacticObject} (h : T.Accessible heads Impenetrability.phase probe goal) :

T.Accessible heads Impenetrability.nextPhase probe goal

Built from