Halpert (2019): Raising, Unphased

This file formalizes [Hal19]'s derivation of cross-linguistic variation in raising-to-subject without the Phase Impenetrability Condition. Two properties of a clausal complement do the work, Clause: whether it is a φ-goal that matrix T interacts with, and whether it can satisfy the EPP by moving to Spec,TP, together with whether T has an EPP at all. The engine is Syntax/Minimalist/Probe/Basic.lean's Probe, whose search a φ-bearing clause halts, Probe.sat, and which Agrees with the goal it halts on when that goal can occupy Spec,TP, Probe.int, so the matrix-T EPP probe is eppProbe and the derivation it drives is raisingOutcome. When the closest clause interacts but cannot satisfy the EPP it absorbs the probe, and T probes a second time ([RR05]), reaching the embedded subject, hyper-raising, when it genuinely Agreed with the clause (section 4.3), and stalling in defective intervention when it did not, the English that-clause of section 5.3. The attested profiles follow from the engine: English, english_profile; Zulu, zulu_profile; Uyghur, uyghur_profile (section 4.5); and Makhuwa and Matengo, which lack the EPP, makhuwa_no_raising (section 5.1). Phasehood is thereby relativized to φ-probes rather than a fixed condition (Syntax/Minimalist/Phase.lean): finite CPs and nonfinite TPs of the same size get opposite raising outcomes across languages, finite_cp_outcome_not_size_driven and nonfinite_tp_outcome_not_size_driven.

Implementation notes

raisingOutcome is deterministic, so the optionality of Zulu hyper-raising out of a finite clause, where an expletive non-raising variant coexists with it, is abstracted over, as are the tend, happen, and keep selection matrix and the adjectival versus verbal small-clause split of English.

References

• [Hal19]
• [Dea15]
• [RR05]

structure Halpert2019.Clause : Type

A clausal complement, classified by the three probe-relevant properties Halpert's account turns on.

• interacts : Bool

  T's φ-probe halts on it: a φ-goal, or a defective nominal intervener (the English that-CP). Transparent clauses (English nonfinite TP, small clauses) are not interveners.

• canAgree : Bool

  T can Agree with it (copy φ) — a genuine φ-goal. The English that-CP interacts but has no φ to copy ([Mou09]).

• canSatisfyEPP : Bool

  It can satisfy the EPP by moving to Spec,TP (Zulu infinitival TP, Uyghur DP-nominalization), vs. clauses barred from Spec,TP (Zulu finite CP, Uyghur NP-nominalization).

def Halpert2019.instDecidableEqClause.decEq (x✝ x✝¹ : Clause) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Halpert2019.instDecidableEqClause : DecidableEq Clause

Equations

• Halpert2019.instDecidableEqClause = Halpert2019.instDecidableEqClause.decEq

def Halpert2019.instReprClause.repr : Clause → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Halpert2019.instReprClause : Repr Clause

Equations

• Halpert2019.instReprClause = { reprPrec := Halpert2019.instReprClause.repr }

inductive Halpert2019.Goal : Type

A goal the matrix-T EPP probe ranges over, in c-command order: the clausal complement (closest) then the embedded subject.

• clause (c : Clause) : Goal
• subject : Goal

@[instance_reducible]

instance Halpert2019.instDecidableEqGoal : DecidableEq Goal

Equations

• Halpert2019.instDecidableEqGoal = Halpert2019.instDecidableEqGoal.decEq

def Halpert2019.instDecidableEqGoal.decEq (x✝ x✝¹ : Goal) : Decidable (x✝ = x✝¹)

Equations

• Halpert2019.instDecidableEqGoal.decEq (Halpert2019.Goal.clause a) (Halpert2019.Goal.clause b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Halpert2019.instDecidableEqGoal.decEq (Halpert2019.Goal.clause c) Halpert2019.Goal.subject = isFalse ⋯
• Halpert2019.instDecidableEqGoal.decEq Halpert2019.Goal.subject (Halpert2019.Goal.clause c) = isFalse ⋯
• Halpert2019.instDecidableEqGoal.decEq Halpert2019.Goal.subject Halpert2019.Goal.subject = isTrue ⋯

@[instance_reducible]

instance Halpert2019.instReprGoal : Repr Goal

Equations

• Halpert2019.instReprGoal = { reprPrec := Halpert2019.instReprGoal.repr }

def Halpert2019.instReprGoal.repr : Goal → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Halpert2019.instReprGoal.repr Halpert2019.Goal.subject prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Halpert2019.Goal.subject")).group prec✝

def Halpert2019.eppProbe : Minimalist.Probe Goal

The matrix-T EPP probe, whose search an intervening φ-bearing clause halts and which Agrees with the goal it halts on when that goal can occupy Spec,TP. The embedded subject is a movable φ-goal, halting and EPP-satisfying. [Dea15]'s interaction is the halting here and satisfaction the Agree, the reverse of [Dea25a]'s algorithm, on which the second probing of section 4.3 is one Probe.run whose interacting clause does not satisfy the probe.

Equations

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

def Halpert2019.goals (c : Clause) : List Goal

The clause c-commands the embedded subject.

Equations

• Halpert2019.goals c = [Halpert2019.Goal.clause c, Halpert2019.Goal.subject]

inductive Halpert2019.RaisingOutcome : Type

The five raising outcomes Halpert's typology distinguishes.

• noRaising : RaisingOutcome

  No EPP: T Agrees with the clause in situ, nothing moves (Makhuwa, Matengo).

• subjectRaises : RaisingOutcome

  Ordinary raising: the embedded subject moves to matrix Spec,TP (English nonfinite TP).

• clauseRaises : RaisingOutcome

  The whole clause satisfies the EPP and moves (Zulu infinitival TP, Uyghur DP-nominalization).

• hyperRaises : RaisingOutcome

  A second Agree reaches the embedded subject (Zulu finite CP, Uyghur NP-nominalization).

• blocked : RaisingOutcome

  A defective intervener stalls the probe (English finite CP).

@[instance_reducible]

instance Halpert2019.instDecidableEqRaisingOutcome : DecidableEq RaisingOutcome

Equations

• Halpert2019.instDecidableEqRaisingOutcome x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Halpert2019.instReprRaisingOutcome.repr : RaisingOutcome → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Halpert2019.instReprRaisingOutcome : Repr RaisingOutcome

Equations

• Halpert2019.instReprRaisingOutcome = { reprPrec := Halpert2019.instReprRaisingOutcome.repr }

def Halpert2019.raisingOutcome (c : Clause) (hasEPP : Bool) : RaisingOutcome

The derivation, run through the canonical Probe engine. With no EPP nothing moves. With an EPP, matrix T runs eppProbe.agree over [clause, subject]: a transparent clause is skipped and the subject raises; a clause that satisfies the EPP is Agreed-with and raises whole; an interacting clause that cannot satisfy the EPP absorbs the probe (Probe.agree_eq_none_of_not_int), and the licensed second probe reaches the embedded subject (hyperRaises) iff T genuinely Agreed with the clause, else stalls (blocked).

Equations

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

The derivation, from the Probe engine

theorem Halpert2019.raisingOutcome_eq_noRaising (c : Clause) : raisingOutcome c false = RaisingOutcome.noRaising

No EPP ⇒ no raising, whatever the clause.

theorem Halpert2019.raisingOutcome_eq_subjectRaises {c : Clause} (h : c.interacts = false) : raisingOutcome c true = RaisingOutcome.subjectRaises

A transparent clause (not an intervener) lets T reach the embedded subject: ordinary raising.

theorem Halpert2019.raisingOutcome_eq_clauseRaises {c : Clause} (hi : c.interacts = true) (he : c.canSatisfyEPP = true) : raisingOutcome c true = RaisingOutcome.clauseRaises

A φ-goal that satisfies the EPP raises as a whole clause; the embedded subject does not move.

theorem Halpert2019.raisingOutcome_eq_hyperRaises {c : Clause} (hi : c.interacts = true) (ha : c.canAgree = true) (he : c.canSatisfyEPP = false) : raisingOutcome c true = RaisingOutcome.hyperRaises

A φ-goal that interacts but cannot satisfy the EPP absorbs the first Agree; the licensed second probe reaches the embedded subject.

theorem Halpert2019.raisingOutcome_eq_blocked {c : Clause} (hi : c.interacts = true) (ha : c.canAgree = false) (he : c.canSatisfyEPP = false) : raisingOutcome c true = RaisingOutcome.blocked

A defective intervener (interacts, but T cannot Agree with it) stalls the probe: no second Agree, no raising.

Cross-linguistic raising profiles

def Halpert2019.englishNonfiniteTP : Clause

English nonfinite TP: transparent, not an intervener.

Equations

• Halpert2019.englishNonfiniteTP = { interacts := false, canAgree := false, canSatisfyEPP := false }

def Halpert2019.englishFiniteCP : Clause

English finite that-CP: a defective intervener — visible, no φ to Agree, cannot move ([Mou09]).

Equations

• Halpert2019.englishFiniteCP = { interacts := true, canAgree := false, canSatisfyEPP := false }

def Halpert2019.zuluSmallClause : Clause

Zulu small clause: transparent.

Equations

• Halpert2019.zuluSmallClause = { interacts := false, canAgree := false, canSatisfyEPP := false }

def Halpert2019.zuluInfinitiveTP : Clause

Zulu infinitival TP: a φ-goal that satisfies the EPP.

Equations

• Halpert2019.zuluInfinitiveTP = { interacts := true, canAgree := true, canSatisfyEPP := true }

def Halpert2019.zuluFiniteCP : Clause

Zulu finite ukuthi-CP: a φ-goal that cannot satisfy the EPP.

Equations

• Halpert2019.zuluFiniteCP = { interacts := true, canAgree := true, canSatisfyEPP := false }

def Halpert2019.uyghurDP : Clause

Uyghur DP-nominalization (non-modal adjective): φ-goal, satisfies the EPP ([Asa11]).

Equations

• Halpert2019.uyghurDP = { interacts := true, canAgree := true, canSatisfyEPP := true }

def Halpert2019.uyghurNP : Clause

Uyghur NP-nominalization (modal adjective): φ-goal, cannot satisfy the EPP.

Equations

• Halpert2019.uyghurNP = { interacts := true, canAgree := true, canSatisfyEPP := false }

theorem Halpert2019.english_profile : raisingOutcome englishNonfiniteTP true = RaisingOutcome.subjectRaises ∧ raisingOutcome englishFiniteCP true = RaisingOutcome.blocked

English raising profile ([Hal19]): raising is required out of a nonfinite TP and blocked out of a finite CP. (Models the seem/be likely predicates; the tend/happen/keep selection matrix and the AP/NP-vs-VP small-clause split are not modelled.)

theorem Halpert2019.zulu_profile : raisingOutcome zuluFiniteCP true = RaisingOutcome.hyperRaises ∧ raisingOutcome zuluInfinitiveTP true = RaisingOutcome.clauseRaises ∧ raisingOutcome zuluSmallClause true = RaisingOutcome.subjectRaises

Zulu raising profile ([Hal19], building on [Ura94]'s hyper-raising): hyper-raising out of a finite CP, the whole clause raises out of a nonfinite TP (so the subject does not), and the subject raises out of a small clause. The finite-CP case is in fact optional — an expletive ku- non-raising variant coexists with hyper-raising, and the ku-/u- morphology spells out first- vs. second-Agree — an optionality this deterministic RaisingOutcome abstracts over.

theorem Halpert2019.uyghur_profile : raisingOutcome uyghurDP true = RaisingOutcome.clauseRaises ∧ raisingOutcome uyghurNP true = RaisingOutcome.hyperRaises

Uyghur raising profile ([Asa11], [Hal19]): a DP-nominalization raises whole; an NP-nominalization hyper-raises the embedded subject.

theorem Halpert2019.makhuwa_no_raising (c : Clause) : raisingOutcome c false = RaisingOutcome.noRaising

Makhuwa/Matengo: removing just the EPP from the Zulu setting kills raising entirely — even out of a finite-CP φ-goal.

Raising is unphased

theorem Halpert2019.finite_cp_outcome_not_size_driven : raisingOutcome zuluFiniteCP true ≠ raisingOutcome englishFiniteCP true

The thesis: a finite CP yields hyper-raising in Zulu but is blocked in English — same clause "size", opposite outcomes — because the split is φ-goal status (canAgree), not a size-driven phase boundary.

theorem Halpert2019.nonfinite_tp_outcome_not_size_driven : raisingOutcome zuluInfinitiveTP true ≠ raisingOutcome englishNonfiniteTP true

Likewise a nonfinite TP: the whole clause raises in Zulu but the subject raises in English — the split is EPP-satisfaction (canSatisfyEPP), not clause size.