Halpert 2012 — Argument Licensing and Agreement in Zulu [Hal12]

[Hal12] (MIT dissertation): the familiar structural licensers (T⁰, v⁰, P⁰) are not licensers in Zulu; instead a Licensing head L⁰ above vP licenses the highest element within vP, and the augment vowel on a nominal is itself an intrinsic case licenser. Augmentless nominals therefore need L⁰: they must be vP-internal, structurally highest there, and at most one occurs per simplex clause. The conjoint/disjoint alternation on the verb (present tense: conjoint ∅- vs. disjoint ya-) is the morphological spellout of L⁰ itself (her ch. 4): "the disjoint appears when L fails to find a goal", and "As long as probing is attempted, the derivation will still converge even if a probe fails to find a goal" — failure-tolerance, adopted by [Pre14] Ch. 6 as the second case study in tolerated failed agreement.

Formalized through Probe/Basic.lean: L⁰ is the indiscriminate instance of Probe.search (Probe.indiscriminate, so bare minimality delivers List.head?; augmented nominals intervene, her Chomsky-2000-style intervention), and the licensing condition is the off-diagonal Probe.AllLicensed with needs = augmentless. Contrast Kichean ([Pre14] Ch. 4): the diagonal case, π⁰ relativized to exactly the needy, hence omnivorous and position-insensitive.

Scope: simplex clauses only — the dissertation's second licensing route (V⁰ together with specifier-taking CAUS/APPL heads, licensing one additional augmentless nominal; her LP schemas in ch. 3) is not modeled. Nominal also under-populates L⁰'s search space: her L⁰ targets any vP-internal XP (locatives, adverbs), so a conjoint fed by a non-nominal is not representable here.

structure Halpert2012.Nominal : Type

A vP-internal nominal: noun class + augment status. Class numbers follow the standard Bantu numbering Halpert uses (1 muntu 'person', 5 qanda 'egg', ...).

• nounClass : ℕ
• augmented : Bool

@[implicit_reducible]

instance Halpert2012.instDecidableEqNominal : DecidableEq Nominal

Equations

• Halpert2012.instDecidableEqNominal = Halpert2012.instDecidableEqNominal.decEq

def Halpert2012.instDecidableEqNominal.decEq (x✝ x✝¹ : Nominal) : Decidable (x✝ = x✝¹)

Equations

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

def Halpert2012.instReprNominal.repr : Nominal → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Halpert2012.instReprNominal : Repr Nominal

Equations

• Halpert2012.instReprNominal = { reprPrec := Halpert2012.instReprNominal.repr }

def Halpert2012.needsL (n : Nominal) : Bool

Does a nominal need licensing by L⁰? Augmentless nominals do; the augment is an intrinsic case licenser, so augmented nominals don't (while still intervening for L⁰).

Equations

• Halpert2012.needsL n = !n.augmented

def Halpert2012.L : Minimalist.Probe Nominal

L⁰ itself: the indiscriminate probe — every element is visible, so bare minimality delivers the structurally highest one.

Equations

• Halpert2012.L = Minimalist.Probe.indiscriminate

def Halpert2012.lGoal (vp : List Nominal) : Option Nominal

L⁰'s goal in a vP.

Equations

• Halpert2012.lGoal vp = Halpert2012.L.search vp

theorem Halpert2012.lGoal_eq_head? (vp : List Nominal) : lGoal vp = vp.head?

Bare minimality, as a theorem: the indiscriminate search takes the head of the sequence.

def Halpert2012.LicensingOk (vp : List Nominal) : Prop

The licensing condition on a simplex vP: every augmentless nominal is licensed by L⁰'s single search.

Equations

• Halpert2012.LicensingOk vp = Halpert2012.L.AllLicensed Halpert2012.needsL vp

@[implicit_reducible]

instance Halpert2012.instDecidableLicensingOk (vp : List Nominal) : Decidable (LicensingOk vp)

Equations

• Halpert2012.instDecidableLicensingOk vp = Halpert2012.instDecidableLicensingOk._aux_1 vp

def Halpert2012.lOutcome (vp : List Nominal) : Minimalist.Probe.Outcome

L⁰'s probing outcome: valued iff the vP has any overt content.

Equations

• Halpert2012.lOutcome vp = Halpert2012.L.outcome vp

def Halpert2012.lSpellout (vp : List Nominal) : String

The conjoint/disjoint marker (present tense) as the spellout of L⁰: conjoint ∅- when L⁰ found a goal, disjoint ya- when it failed. A marked pattern — the overt member realizes FAILED valuation ([Pre14] Ch. 6 notes the parallel with English non-past -Ø vs. -z).

Equations

• Halpert2012.lSpellout vp = match Halpert2012.lOutcome vp with | Minimalist.Probe.Outcome.valued => "∅-" | Minimalist.Probe.Outcome.unvalued => "ya-"

The conjoint/disjoint distribution

theorem Halpert2012.disjoint_iff_empty (vp : List Nominal) : lSpellout vp = "ya-" ↔ vp = []

Disjoint iff vP is empty (after A-movement): the conjoint requires overt vP-internal material — L⁰'s indiscriminate search is sensitive even to non-arguments, which is the learner's evidence that L⁰ is unrelativized ([Pre14] Ch. 6 §6.1.3's locative-modifier point).

Licensing: highest-only and at-most-one

theorem Halpert2012.licensingOk_iff_highest (vp : List Nominal) : LicensingOk vp ↔ ∀ (n : Nominal), n ∈ vp → needsL n = true → vp.head? = some n

An augmentless nominal is licensed iff it is the structurally highest element of its vP — her ch. 3: L "licenses the highest element in vP". Instance of Probe.indiscriminate_allLicensed_iff.

theorem Halpert2012.at_most_one_augmentless {vp : List Nominal} (h : LicensingOk vp) (n : Nominal) : n ∈ vp → ∀ (m : Nominal), m ∈ vp → needsL n = true → needsL m = true → n = m

At most one augmentless nominal per simplex vP (her transitive and intransitive LP schemas): L⁰'s single Agree relation licenses at most one goal.

The negated-expletive VS(O) paradigm

theorem Halpert2012.augmentless_distribution : LicensingOk [{ nounClass := 1, augmented := false }] ∧ LicensingOk [{ nounClass := 1, augmented := false }, { nounClass := 5, augmented := true }] ∧ ¬LicensingOk [{ nounClass := 1, augmented := false }, { nounClass := 5, augmented := false }] ∧ ¬LicensingOk [{ nounClass := 1, augmented := true }, { nounClass := 5, augmented := false }]

The augmentless distribution in negated transitive-expletive clauses — augmentless nominals are NPIs in these contexts (her ch. 3 paradigm, (127); reproduced as [Pre14] (128)): an augmentless nominal is fine alone or above an augmented object; blocked in pairs (single Agree relation) and below an augmented subject (intervention). Tokens: muntu '1person', qanda '5egg'.

Tolerated failed agreement

theorem Halpert2012.failed_agree_spells_disjoint : lOutcome [] = Minimalist.Probe.Outcome.unvalued ∧ lSpellout [] = "ya-" ∧ lOutcome [{ nounClass := 5, augmented := true }] = Minimalist.Probe.Outcome.valued ∧ lSpellout [{ nounClass := 5, augmented := true }] = "∅-"

Failure-tolerance, in her own terms ("As long as probing is attempted, the derivation will still converge even if a probe fails to find a goal"; "When L fails to find a goal, the derivation records this failure in the morphological spell-out"): an empty vP leaves L⁰ unvalued, the derivation converges under the obligatory-operations model, and PF realizes the failure as the overt disjoint ya-. With any goal — even a licensing-indifferent augmented one — L⁰ is valued and the conjoint ∅- surfaces.