Phases

The phases of [MCB25] §1.14, after [Cho13], 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 [Cho00]'s condition to everything outside the phase, under [Cho01]'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: [Cho00]'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 SyntacticObject/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.

References

• [MCB25]
• [Cho13]
• [Cho00]
• [Cho01]

inductive Minimalist.Impenetrability : Type

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

• phase : Impenetrability

  Once the phase is built, to everything outside it ([Cho00]).

• nextPhase : Impenetrability

  Once the next phase head up is merged, to everything outside its interior ([Cho01]).

@[instance_reducible]

instance Minimalist.instDecidableEqImpenetrability : DecidableEq Impenetrability

Equations

• Minimalist.instDecidableEqImpenetrability x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Minimalist.instReprImpenetrability : Repr Impenetrability

Equations

• Minimalist.instReprImpenetrability = { reprPrec := Minimalist.instReprImpenetrability.repr }

def Minimalist.instReprImpenetrability.repr : Impenetrability → ℕ → Std.Format

Equations

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

def Minimalist.SyntacticObject.IsPhaseHead (T : SyntacticObject) (ℓ : LexicalItem.Token) : Prop

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

Equations

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

@[instance_reducible]

instance Minimalist.SyntacticObject.instDecidableIsPhaseHead (T : SyntacticObject) (ℓ : LexicalItem.Token) : Decidable (T.IsPhaseHead ℓ)

Equations

• T.instDecidableIsPhaseHead ℓ = Multiset.decidableExistsMultiset

def Minimalist.SyntacticObject.IsComplementOf (T : SyntacticObject) (ℓ : LexicalItem.Token) (z : SyntacticObject) : Prop

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

Equations

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

@[instance_reducible]

instance Minimalist.SyntacticObject.instDecidableIsComplementOf (T : SyntacticObject) (ℓ : LexicalItem.Token) (z : SyntacticObject) : Decidable (T.IsComplementOf ℓ z)

Equations

• T.instDecidableIsComplementOf ℓ z = Multiset.decidableExistsMultiset

def Minimalist.SyntacticObject.WithinProjection (T : SyntacticObject) (ℓ : LexicalItem.Token) (x : SyntacticObject) : Prop

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

Equations

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

@[instance_reducible]

instance Minimalist.SyntacticObject.instDecidableWithinProjection (T : SyntacticObject) (ℓ : LexicalItem.Token) (x : SyntacticObject) : Decidable (T.WithinProjection ℓ x)

Equations

• T.instDecidableWithinProjection ℓ x = Multiset.decidableExistsMultiset

def Minimalist.SyntacticObject.WithinComplement (T : SyntacticObject) (ℓ : LexicalItem.Token) (x : SyntacticObject) : Prop

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

Equations

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

@[instance_reducible]

instance Minimalist.SyntacticObject.instDecidableWithinComplement (T : SyntacticObject) (ℓ : LexicalItem.Token) (x : SyntacticObject) : Decidable (T.WithinComplement ℓ x)

Equations

• T.instDecidableWithinComplement ℓ x = Multiset.decidableExistsMultiset

def Minimalist.SyntacticObject.phase (T : SyntacticObject) (ℓ : LexicalItem.Token) : Multiset SyntacticObject

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

Equations

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

def Minimalist.SyntacticObject.phaseInterior (T : SyntacticObject) (ℓ : LexicalItem.Token) : Multiset SyntacticObject

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

Equations

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

def Minimalist.SyntacticObject.phaseEdge (T : SyntacticObject) (ℓ : LexicalItem.Token) : Multiset SyntacticObject

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

Equations

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

theorem Minimalist.SyntacticObject.IsComplementOf.mem_terms {T : SyntacticObject} {ℓ : LexicalItem.Token} {z : SyntacticObject} (h : T.IsComplementOf ℓ z) : z ∈ T.terms

theorem Minimalist.SyntacticObject.WithinProjection.mem_terms {T : SyntacticObject} {ℓ : LexicalItem.Token} {x : SyntacticObject} (h : T.WithinProjection ℓ x) : x ∈ T.terms

theorem Minimalist.SyntacticObject.WithinComplement.withinProjection {T : SyntacticObject} {ℓ : LexicalItem.Token} {x : SyntacticObject} (h : T.WithinComplement ℓ x) : T.WithinProjection ℓ x

What lies within the complement lies within the projection.

theorem Minimalist.SyntacticObject.WithinComplement.mem_terms {T : SyntacticObject} {ℓ : LexicalItem.Token} {x : SyntacticObject} (h : T.WithinComplement ℓ x) : x ∈ T.terms

theorem Minimalist.SyntacticObject.WithinProjection.trans {T : SyntacticObject} {ℓ : LexicalItem.Token} {x y : SyntacticObject} (hx : T.WithinProjection ℓ x) (hxy : x.ContainsOrEq y) : T.WithinProjection ℓ y

theorem Minimalist.SyntacticObject.WithinComplement.trans {T : SyntacticObject} {ℓ : LexicalItem.Token} {x y : SyntacticObject} (hx : T.WithinComplement ℓ x) (hxy : x.ContainsOrEq y) : T.WithinComplement ℓ y

Whatever a frozen term contains is frozen.

theorem Minimalist.SyntacticObject.WithinComplement.cCommands {T : SyntacticObject} {ℓ : LexicalItem.Token} {x : SyntacticObject} (h : T.WithinComplement ℓ x) : T.CCommands (↑ℓ) x

The head c-commands what lies within its complement.

@[simp]

theorem Minimalist.SyntacticObject.mem_phase {T : SyntacticObject} {ℓ : LexicalItem.Token} {x : SyntacticObject} : x ∈ T.phase ℓ ↔ T.WithinProjection ℓ x

@[simp]

theorem Minimalist.SyntacticObject.mem_phaseInterior {T : SyntacticObject} {ℓ : LexicalItem.Token} {x : SyntacticObject} : x ∈ T.phaseInterior ℓ ↔ T.WithinComplement ℓ x

@[simp]

theorem Minimalist.SyntacticObject.mem_phaseEdge {T : SyntacticObject} {ℓ : LexicalItem.Token} {x : SyntacticObject} : x ∈ T.phaseEdge ℓ ↔ T.WithinProjection ℓ x ∧ ¬T.WithinComplement ℓ x

theorem Minimalist.SyntacticObject.isPhaseHead_iff_exists_isComplementOf {T : SyntacticObject} {ℓ : LexicalItem.Token} : T.IsPhaseHead ℓ ↔ ∃ (z : SyntacticObject), T.IsComplementOf ℓ z

A head projects exactly when it has a complement, since an object merged with itself has no head.

theorem Minimalist.SyntacticObject.isPhaseHead_iff_phaseInterior_ne_zero {T : SyntacticObject} {ℓ : LexicalItem.Token} : T.IsPhaseHead ℓ ↔ T.phaseInterior ℓ ≠ 0

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

theorem Minimalist.SyntacticObject.phaseInterior_le_phase {T : SyntacticObject} {ℓ : LexicalItem.Token} : T.phaseInterior ℓ ≤ T.phase ℓ

theorem Minimalist.SyntacticObject.phaseInterior_add_phaseEdge {T : SyntacticObject} {ℓ : LexicalItem.Token} : T.phaseInterior ℓ + T.phaseEdge ℓ = T.phase ℓ

The interior and the edge partition the phase.

theorem Minimalist.SyntacticObject.phaseInterior_le_cCommandDomain {T : SyntacticObject} {ℓ : LexicalItem.Token} : T.phaseInterior ℓ ≤ T.cCommandDomain ↑ℓ

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

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

The Phase Impenetrability Condition

def Minimalist.SyntacticObject.Accessible (T : SyntacticObject) (heads : List LexicalItem.Token) : Impenetrability → SyntacticObject → SyntacticObject → Prop

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 [Cho01]'s condition only once a phase head above it is merged and the probe lies outside that head's interior.

Equations

• One or more equations did not get rendered due to their size.
• T.Accessible heads Minimalist.Impenetrability.phase x✝¹ x✝ = ∀ H ∈ heads, T.WithinComplement H x✝ → T.WithinProjection H x✝¹

@[instance_reducible]

instance Minimalist.SyntacticObject.instDecidableAccessible {T : SyntacticObject} (heads : List LexicalItem.Token) (s : Impenetrability) (probe goal : SyntacticObject) : Decidable (T.Accessible heads s probe goal)

Equations

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

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

[Cho00]'s condition is the stronger: what it leaves accessible, [Cho01]'s does too.