Pietraszko (2026): In Defense of the Clause-Internal Phase

This file formalizes the argument of [Pie26] that VoiceP in Zimbabwean Ndebele is a phase, from its opacity to A-movement and φ-agreement rather than from footprints of successive-cyclic movement. A subject may move to Spec,TP and control agreement on T (5), or stay in situ under default agreement (6); of the three sources of a missing probe–goal relation (8), the account is locality: T always bears EPP and φ, VoiceP is a phase under the strong Phase Impenetrability Condition of [Cho00], and Voice bears EPP optionally (9), (10). A subject that reaches Spec,VoiceP is visible to every head above and, operations being obligatory when possible with an unchecked EPP tolerated as in [Pre14], moves on to Spec,TP; a subject left in the phase's complement is invisible to them all. Hence movement and agreement go together (11)–(14) (simple_clause); auxiliary constructions agree on every head or on none and admit no intermediate landing site (16)–(21) (auxV_uniform, auxV_no_partial); a reduced clause whose highest head is Asp lets Asp attract the subject on its own (34)–(42) (reduced_clause); a subject that leaves its VoiceP has agreed with T on the way (25)–(28) (agrees_of_lt_landing); and hyperraising yields the four subject positions of (77) from the EPP of the phase heads alone, the VP-internal one included (69), (76) (hyperraising_sites). The general form is phase-delimited movement (79): movement within a phase is obligatory (phase_internal_obligatory), and a phase head without EPP freezes the subject below it (cross_phasal_frozen). The account with an optional [EPP, φ] on T of [CM15a] admits the unattested partial patterns (30), (31) and default agreement on a T the subject has crossed (25) (optional_T_overgenerates), where the phasal account excludes them.

Implementation notes

A clause is the list of heads above the subject's base position, bottom-up, each with its category and whether it bears EPP, a φ-probe, and heads a phase; one bottom-up pass computes the subject's landing site and the heads it is accessible to: an EPP head attracts an accessible subject to its specifier and a phase head without EPP freezes it in its complement (stateAt, landing, Accessible). The rival account is the same derivation with Voice non-phasal and [EPP, φ] optional on T and Asp. The expletive-pro account of [Hal15] (§3.2), the antifocus account of [Zel15] (§4), the modification of [Hen06], object dislocation (55) and the information-structural properties of the two orders are prose. The trees the derivation builds (treeAt) tie the spine to the substrate's phases: on them the spine's accessibility is [Cho00]'s condition (simple_accessible_iff, auxV_accessible_iff, reduced_accessible_iff), and [Cho01]'s would let T reach a subject left in VoiceP (nextPhase_overgenerates).

References

• [Pie26]
• [Cho00]
• [Cho01]
• [Pre14]
• [CM15a]
• [Hal15]
• [Zel15]
• [Hen06]

Clauses and the derivation (§2.2)

structure Pietraszko2026.Head : Type

A head of the clausal spine, as subject movement sees it, has a category and records whether it bears EPP, a φ-probe, and heads a phase.

• cat : Minimalist.Cat
• epp : Bool
• phi : Bool
• phase : Bool

def Pietraszko2026.instDecidableEqHead.decEq (x✝ x✝¹ : Head) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Pietraszko2026.instDecidableEqHead : DecidableEq Head

Equations

• Pietraszko2026.instDecidableEqHead = Pietraszko2026.instDecidableEqHead.decEq

@[instance_reducible]

instance Pietraszko2026.instReprHead : Repr Head

Equations

• Pietraszko2026.instReprHead = { reprPrec := Pietraszko2026.instReprHead.repr }

def Pietraszko2026.instReprHead.repr : Head → ℕ → Std.Format

Equations

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

@[reducible, inline]

abbrev Pietraszko2026.Spine : Type

A clause is the list of heads above the subject's base position, bottom-up.

Equations

• Pietraszko2026.Spine = List Pietraszko2026.Head

structure Pietraszko2026.State : Type

The derivational state of the subject records its height, 0 in situ and i + 1 in the specifier of the head at index i, and whether it is frozen in a phase's complement.

• height : ℕ
• frozen : Bool

@[instance_reducible]

instance Pietraszko2026.instDecidableEqState : DecidableEq State

Equations

• Pietraszko2026.instDecidableEqState = Pietraszko2026.instDecidableEqState.decEq

def Pietraszko2026.instDecidableEqState.decEq (x✝ x✝¹ : State) : Decidable (x✝ = x✝¹)

Equations

• Pietraszko2026.instDecidableEqState.decEq { height := a, frozen := a_1 } { height := b, frozen := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Pietraszko2026.instReprState : Repr State

Equations

• Pietraszko2026.instReprState = { reprPrec := Pietraszko2026.instReprState.repr }

def Pietraszko2026.instReprState.repr : State → ℕ → Std.Format

Equations

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

def Pietraszko2026.step (i : ℕ) (h : Head) (s : State) : State

When the head at index i is merged, an EPP head attracts an accessible subject to its specifier, a phase head without EPP freezes an accessible subject in its complement, and otherwise the subject stays where it is.

Equations

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

def Pietraszko2026.stateAt (sp : Spine) : ℕ → State

The state after merging the first n heads.

Equations

• Pietraszko2026.stateAt sp 0 = { height := 0, frozen := false }
• Pietraszko2026.stateAt sp n.succ = match sp[n]? with | some h => Pietraszko2026.step n h (Pietraszko2026.stateAt sp n) | none => Pietraszko2026.stateAt sp n

def Pietraszko2026.landing (sp : Spine) : ℕ

The subject's landing site is its height once the clause is built.

Equations

• Pietraszko2026.landing sp = (Pietraszko2026.stateAt sp (List.length sp)).height

def Pietraszko2026.Accessible (sp : Spine) (i : ℕ) : Prop

The subject is accessible to the head at index i when it is not frozen as that head is merged.

Equations

• Pietraszko2026.Accessible sp i = ((Pietraszko2026.stateAt sp i).frozen = false)

@[instance_reducible]

instance Pietraszko2026.instDecidableAccessible (sp : Spine) (i : ℕ) : Decidable (Accessible sp i)

Equations

• Pietraszko2026.instDecidableAccessible sp i = Pietraszko2026.instDecidableAccessible._aux_1 sp i

def Pietraszko2026.Agrees (sp : Spine) (i : ℕ) : Prop

The head at index i agrees with the subject when it bears a φ-probe and the subject is accessible to it.

Equations

• Pietraszko2026.Agrees sp i = match sp[i]? with | some h => h.phi = true ∧ Pietraszko2026.Accessible sp i | none => False

@[instance_reducible]

instance Pietraszko2026.instDecidableAgrees (sp : Spine) (i : ℕ) : Decidable (Agrees sp i)

Equations

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

The heads of Ndebele

def Pietraszko2026.T : Head

T, with EPP and φ.

Equations

• Pietraszko2026.T = { cat := Minimalist.Cat.T, epp := true, phi := true, phase := false }

def Pietraszko2026.Asp : Head

Asp, with EPP and φ (§2.4, §3.1.3).

Equations

• Pietraszko2026.Asp = { cat := Minimalist.Cat.Asp, epp := true, phi := true, phase := false }

def Pietraszko2026.Voice (e : Bool) : Head

Voice, a phase head, with EPP e (§2.2).

Equations

• Pietraszko2026.Voice e = { cat := Minimalist.Cat.Voice, epp := e, phi := false, phase := true }

def Pietraszko2026.C (e : Bool) : Head

C, a phase head, with EPP e (§4).

Equations

• Pietraszko2026.C e = { cat := Minimalist.Cat.C, epp := e, phi := false, phase := true }

def Pietraszko2026.raisingV : Head

The matrix V of a raising verb, with EPP (§4).

Equations

• Pietraszko2026.raisingV = { cat := Minimalist.Cat.V, epp := true, phi := false, phase := false }

def Pietraszko2026.simple (e : Bool) : Spine

A simple clause (9), (10).

Equations

• Pietraszko2026.simple e = [Pietraszko2026.Voice e, Pietraszko2026.T]

def Pietraszko2026.auxV (e : Bool) : Spine

An auxiliary construction (17), (19): Asp and T above Voice.

Equations

• Pietraszko2026.auxV e = [Pietraszko2026.Voice e, Pietraszko2026.Asp, Pietraszko2026.T]

def Pietraszko2026.reduced (e : Bool) : Spine

A reduced clause (40): Asp is the highest head.

Equations

• Pietraszko2026.reduced e = [Pietraszko2026.Voice e, Pietraszko2026.Asp]

def Pietraszko2026.hyperraising (e₁ e₂ e₃ : Bool) : Spine

Hyperraising (77): the embedded Voice and T, C, the matrix raising verb, and the matrix Voice and T.

Equations

• Pietraszko2026.hyperraising e₁ e₂ e₃ = [Pietraszko2026.Voice e₃, Pietraszko2026.T, Pietraszko2026.C e₂, Pietraszko2026.raisingV, Pietraszko2026.Voice e₁, Pietraszko2026.T]

Predictions (§2.3, §2.4, §3.1.3, §4)

theorem Pietraszko2026.simple_clause (e : Bool) : (landing (simple e) = 2 ↔ e = true) ∧ (Agrees (simple e) 1 ↔ e = true) ∧ (landing (simple e) = 0 ↔ ¬e = true)

Prediction 1 (11)–(14): the subject moves to Spec,TP exactly when T agrees with it, both exactly when Voice bears EPP.

theorem Pietraszko2026.auxV_uniform (e : Bool) : Agrees (auxV e) 1 ∧ Agrees (auxV e) 2 ∨ ¬Agrees (auxV e) 1 ∧ ¬Agrees (auxV e) 2

Prediction 2 (16)–(20): in an auxiliary construction every head above Voice agrees with the subject or none does.

theorem Pietraszko2026.auxV_no_partial (e : Bool) : landing (auxV e) = 0 ∨ landing (auxV e) = 3

(21): the subject is in situ or in Spec,TP, never in an intermediate specifier.

theorem Pietraszko2026.reduced_clause (e : Bool) : (landing (reduced e) = 2 ↔ e = true) ∧ (Agrees (reduced e) 1 ↔ e = true)

Reduced clauses (41), (42): with Asp the highest head, the subject lands in Spec,AspP exactly when Voice bears EPP, and Asp agrees with it exactly then.

theorem Pietraszko2026.hyperraising_sites (e₁ e₂ e₃ : Bool) : landing (hyperraising e₁ e₂ e₃) = if ¬e₃ = true then 0 else if ¬e₂ = true then 2 else if ¬e₁ = true then 4 else 6

Hyperraising (77): the subject stays in situ when the embedded Voice lacks EPP, stops in the embedded Spec,TP when C lacks EPP, in the matrix VP when the matrix Voice lacks EPP (69), (76), and reaches the matrix Spec,TP otherwise.

Phase-delimited movement (79)

theorem Pietraszko2026.stateAt_succ_of_getElem? {sp : Spine} {n : ℕ} {h : Head} (hn : sp[n]? = some h) : stateAt sp (n + 1) = step n h (stateAt sp n)

theorem Pietraszko2026.frozen_stateAt_succ {sp : Spine} {n : ℕ} (hf : (stateAt sp n).frozen = true) : stateAt sp (n + 1) = stateAt sp n

A frozen subject stays frozen at the same height.

theorem Pietraszko2026.frozen_stateAt_of_le {sp : Spine} {m n : ℕ} (hmn : m ≤ n) (hf : (stateAt sp m).frozen = true) : stateAt sp n = stateAt sp m

theorem Pietraszko2026.height_step_le {i : ℕ} {h : Head} {s : State} (hs : s.height ≤ i) : (step i h s).height ≤ i + 1

theorem Pietraszko2026.height_le_height_step {i : ℕ} {h : Head} {s : State} (hs : s.height ≤ i) : s.height ≤ (step i h s).height

theorem Pietraszko2026.height_stateAt_le (sp : Spine) (n : ℕ) : (stateAt sp n).height ≤ n

The subject never sits above the heads merged so far.

theorem Pietraszko2026.height_stateAt_mono (sp : Spine) {m n : ℕ} (hmn : m ≤ n) : (stateAt sp m).height ≤ (stateAt sp n).height

The subject never moves down.

theorem Pietraszko2026.phase_internal_obligatory {sp : Spine} {i : ℕ} {h : Head} (hi : sp[i]? = some h) (he : h.epp = true) (ha : Accessible sp i) : i + 1 ≤ landing sp

Phase-internal movement is obligatory (79i): a head bearing EPP attracts the subject whenever it is accessible, so the subject lands at least in its specifier.

theorem Pietraszko2026.cross_phasal_frozen {sp : Spine} {i : ℕ} {h : Head} (hi : sp[i]? = some h) (hp : h.phase = true) (he : h.epp = false) (ha : Accessible sp i) : landing sp ≤ i ∧ ∀ (j : ℕ), i < j → ¬Accessible sp j

Cross-phasal movement needs EPP on the phase head (79ii): a phase head without EPP freezes an accessible subject in its complement, so the subject lands below it and no higher head can reach it.

theorem Pietraszko2026.agrees_of_lt_landing {sp : Spine} {i : ℕ} {h : Head} (hi : sp[i]? = some h) (hphi : h.phi = true) (hlt : i < landing sp) : Agrees sp i

Movement past a φ-bearing head requires agreement with it (25)–(28): a subject that lands above a head was accessible to it.

The optional [EPP, φ] on T (§3.1)

def Pietraszko2026.optionalT (a t : Bool) : Spine

The account of [CM15a]: Voice is not a phase and each inflectional head bears [EPP, φ] optionally, Asp with a and T with t.

Equations

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

def Pietraszko2026.optionalTRaising (t : Bool) : Spine

On that account an embedded T may lack [EPP, φ] below C and a raising verb, the configuration of raising to object.

Equations

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

theorem Pietraszko2026.optional_T_overgenerates : (landing (optionalT true false) = 2 ∧ Agrees (optionalT true false) 1 ∧ ¬Agrees (optionalT true false) 2) ∧ (landing (optionalT false true) = 3 ∧ ¬Agrees (optionalT false true) 1 ∧ Agrees (optionalT false true) 2) ∧ landing (optionalTRaising false) = 4 ∧ ¬Agrees (optionalTRaising false) 1

The optional-probe account overgenerates: Asp alone may attract and agree with the subject (30), T alone may (31), and the subject may raise to object across a non-agreeing T (25), the patterns the phasal account excludes.

The trees the derivation builds

def Pietraszko2026.obj : Minimalist.LexicalItem.Token

The object.

Equations

• Pietraszko2026.obj = { item := Minimalist.LexicalItem.of Minimalist.Cat.D [] "obj", id := 0 }

def Pietraszko2026.subj : Minimalist.LexicalItem.Token

The subject.

Equations

• Pietraszko2026.subj = { item := Minimalist.LexicalItem.of Minimalist.Cat.D [] "subj", id := 1 }

def Pietraszko2026.V : Minimalist.LexicalItem.Token

The verb.

Equations

• Pietraszko2026.V = { item := Minimalist.LexicalItem.of Minimalist.Cat.V [Minimalist.Cat.D] "V", id := 2 }

def Pietraszko2026.v : Minimalist.LexicalItem.Token

The head that introduces the subject, below Voice (fn. 3).

Equations

• Pietraszko2026.v = { item := Minimalist.LexicalItem.of Minimalist.Cat.v [Minimalist.Cat.V, Minimalist.Cat.D] "v", id := 3 }

def Pietraszko2026.tokOf (sp : Spine) (i : ℕ) (hd : Head) : Minimalist.LexicalItem.Token

The head at index i of a spine, selecting the category of the head below it.

Equations

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

def Pietraszko2026.phaseHeads (sp : Spine) : List Minimalist.LexicalItem.Token

The phase heads of a spine.

Equations

• Pietraszko2026.phaseHeads sp = List.map (fun (x : Pietraszko2026.Head × ℕ) => Pietraszko2026.tokOf sp x.2 x.1) (List.filter (fun (x : Pietraszko2026.Head × ℕ) => x.1.phase) (List.zipIdx sp))

def Pietraszko2026.copyAt (k j : ℕ) : Minimalist.PlanarSyntacticObject

The copy of the subject at height j, when it is pronounced at height k.

Equations

• Pietraszko2026.copyAt k j = if j = k then ↑Pietraszko2026.subj else Minimalist.PlanarSyntacticObject.traceOf Pietraszko2026.subj

def Pietraszko2026.treeAt (sp : Spine) (n : ℕ) : Minimalist.PlanarSyntacticObject

Once the first n heads are merged, the tree has the subject pronounced at its height then, with deleted copies at its base and in every specifier it passed through.

Equations

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

def Pietraszko2026.TreeAccessible (s : Minimalist.Impenetrability) (sp : Spine) (i : ℕ) : Prop

The subject is accessible under the condition s to the head at index i, merged on the tree built so far.

Equations

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

@[instance_reducible]

instance Pietraszko2026.instDecidableTreeAccessible (s : Minimalist.Impenetrability) (sp : Spine) (i : ℕ) : Decidable (TreeAccessible s sp i)

Equations

• Pietraszko2026.instDecidableTreeAccessible s sp i = Pietraszko2026.instDecidableTreeAccessible._aux_1 s sp i

theorem Pietraszko2026.simple_accessible_iff (e : Bool) (i : ℕ) : i < 2 → (Accessible (simple e) i ↔ TreeAccessible Minimalist.Impenetrability.phase (simple e) i)

In simple clauses (9)–(14) the subject is accessible to a head exactly when it is under [Cho00]'s condition on the tree the derivation has built.

theorem Pietraszko2026.auxV_accessible_iff (e : Bool) (i : ℕ) : i < 3 → (Accessible (auxV e) i ↔ TreeAccessible Minimalist.Impenetrability.phase (auxV e) i)

The same in auxiliary constructions (16)–(21).

theorem Pietraszko2026.reduced_accessible_iff (e : Bool) (i : ℕ) : i < 2 → (Accessible (reduced e) i ↔ TreeAccessible Minimalist.Impenetrability.phase (reduced e) i)

The same in reduced clauses (34)–(42).

theorem Pietraszko2026.nextPhase_overgenerates : ¬TreeAccessible Minimalist.Impenetrability.phase (simple false) 1 ∧ TreeAccessible Minimalist.Impenetrability.nextPhase (simple false) 1

Under [Cho01]'s condition T would reach a subject left in the complement of Voice and agree with it, against the default agreement of (6) and (11).