[Hal19]: Raising, unphased

Halpert derives cross-linguistic variation in raising-to-subject without the Phase Impenetrability Condition. Two clause-and-language properties do the work:

1. whether a clausal complement is a φ-goal matrix T interacts with;
2. whether that clause can satisfy the EPP (move to Spec,TP);

plus whether T has an EPP at all. The engine is the canonical Probe (Probe/Basic.lean): Deal's ([Dea15]) interaction is Probe.vis (the search halts on a φ-bearing clause — an A-over-A intervener) and satisfaction is Probe.act (the goal can occupy Spec,TP). When the closest clause interacts but cannot satisfy the EPP it absorbs the probe (Probe.agree_eq_none_of_inactive); T then probes a second time ([RR05]), reaching the embedded subject — hyper-raising — when it genuinely Agreed with the clause, and stalling (defective intervention) when it did not.

This relativizes phasehood to φ-probes rather than positing a fixed PIC (phaseImpenetrable, Syntax/Minimalist/Phase.lean): finite CPs and nonfinite TPs of the same size get opposite raising outcomes across languages, so the split cannot be size/phase-driven (finite_cp_outcome_not_size_driven, nonfinite_tp_outcome_not_size_driven).

Main declarations

• Clause — a complement by its three probe-relevant properties.
• eppProbe / raisingOutcome — the matrix-T EPP probe and the derivation it drives, run through Probe.agree.
• english_profile, zulu_profile, uyghur_profile, makhuwa_no_raising — the attested profiles, derived from the engine.

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.

@[implicit_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.

@[implicit_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

@[implicit_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 ⋯

@[implicit_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: [Dea15]'s interaction is Probe.vis (the search halts on an intervening clause), satisfaction is Probe.act (the goal can occupy Spec,TP). The embedded subject is a movable φ-goal — visible and EPP-satisfying.

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).

@[implicit_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.

@[implicit_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_inactive), 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.