Documentation

Linglib.Phenomena.ArgumentStructure.Studies.Hewett2026

Verbal Templates Can Influence L-Selection in Semitic #

@cite{hewett-2026}

Linguistic Inquiry 57(1): 197--215.

L-selection — which specific preposition heads a PP complement — can vary by verbal template (binyan) in Tunisian Arabic, Syrian Arabic, and Hebrew. This falsifies both @cite{harley-2014} (roots select) and @cite{merchant-2019} (categorizing heads select), because neither root nor categorizer varies across templates.

Core Contribution #

Joint Selection via Activate (Def 23, adapted from @cite{merchant-2019}): roots carry inactive selectional features indexed by an ordered tuple of category features. Each head that c-commands the root strips one category from the tuple. When the tuple is exhausted, the feature is fully active and determines the l-selected P. For Semitic, the tuple is (V, Template): the categorizing head V strips the first index, the template-defining head strips the second.

Scope #

Templates are realized by nonconcatenative morphology (vocalic melodies applied to consonantal roots). The Mirror Principle (@cite{baker-1985}) explicitly scopes out nonconcatenative morphology (see Morphology.MirrorPrinciple.MorphDomain.InScope). Template-dependent l-selection is therefore a phenomenon that falls outside the domain where morphological and syntactic orderings are required to mirror each other.

inductive Hewett2026.SemiticTemplate :

Semitic verbal templates (binyanim).

Each template is realized as a nonconcatenative vocalic pattern applied to a consonantal root. Syntactically, templates correspond to bundles of functional heads (v, Voice) — they are not roots, and they are not categorizers.

@cite{hewett-2026} assumes templates realize a head or series of heads capable of inducing changes in adicity, presumably v/Voice (p. 201).

Instances For

@[implicit_reducible]

instance Hewett2026.instDecidableEqSemiticTemplate :

DecidableEq SemiticTemplate

Equations

Hewett2026.instDecidableEqSemiticTemplate x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Hewett2026.instReprSemiticTemplate :

Repr SemiticTemplate

Equations

Hewett2026.instReprSemiticTemplate = { reprPrec := Hewett2026.instReprSemiticTemplate.repr }

def Hewett2026.instReprSemiticTemplate.repr :

SemiticTemplate → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Hewett2026.instBEqSemiticTemplate :

BEq SemiticTemplate

BEq via DecidableEq so that decide (a = b) reduces definitionally on concrete values — required for rfl proofs in the activation mechanism.

Equations

Hewett2026.instBEqSemiticTemplate = { beq := fun (a b : Hewett2026.SemiticTemplate) => decide (a = b) }

instance Hewett2026.instLawfulBEqSemiticTemplate :

LawfulBEq SemiticTemplate

def Hewett2026.SemiticTemplate.toVoiceFlavor :

SemiticTemplate → Minimalist.VoiceFlavor

Map templates to Voice flavors.

Active templates (XaYaZ, XaYYaZ, XiYeZ, hiXYiZ) select agentive or causer Voice. Passive/medio-passive templates (nXaYaZ, tXaYYaZ, huXYaZ, XuYaZ) correspond to passive or non-thematic Voice.

XaYYaZ introduces a causer (intensive/causative), distinguished from XaYaZ (basic agentive). This is the key structural difference that drives l-selection variation: the template determines which Voice head merges, and the Voice head is above the selectional domain.

Equations

Instances For

def Hewett2026.SemiticTemplate.introducesCauser :

SemiticTemplate → Bool

Does this template introduce a causer argument?

Equations

Hewett2026.SemiticTemplate.XaYYaZ.introducesCauser = true
Hewett2026.SemiticTemplate.hiXYiZ.introducesCauser = true
Hewett2026.SemiticTemplate.XiYeZ.introducesCauser = true
x✝.introducesCauser = false

Instances For

def Hewett2026.SemiticTemplate.isPassiveLike :

SemiticTemplate → Bool

Is this template passive or medio-passive?

Equations

Hewett2026.SemiticTemplate.nXaYaZ.isPassiveLike = true
Hewett2026.SemiticTemplate.tXaYYaZ.isPassiveLike = true
Hewett2026.SemiticTemplate.huXYaZ.isPassiveLike = true
Hewett2026.SemiticTemplate.XuYaZ.isPassiveLike = true
x✝.isPassiveLike = false

Instances For

theorem Hewett2026.templates_outside_mirror_scope :

¬Morphology.MirrorPrinciple.MorphDomain.nonconcatenative.InScope

Templates are nonconcatenative morphology — outside the scope of the Mirror Principle (@cite{baker-1985} S5).

inductive Hewett2026.RootLabel :

Consonantal roots from the paper's examples. Only roots with attested l-selection data are included. Transliterated to ASCII-safe identifiers.

xwf : RootLabel
krh : RootLabel
dwr : RootLabel
Hkm : RootLabel
tpl : RootLabel
shps : RootLabel

Instances For

@[implicit_reducible]

instance Hewett2026.instDecidableEqRootLabel :

DecidableEq RootLabel

Equations

Hewett2026.instDecidableEqRootLabel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Hewett2026.instReprRootLabel :

Equations

Hewett2026.instReprRootLabel = { reprPrec := Hewett2026.instReprRootLabel.repr }

def Hewett2026.instReprRootLabel.repr :

RootLabel → ℕ → Std.Format

Equations

Hewett2026.instReprRootLabel.repr Hewett2026.RootLabel.xwf prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hewett2026.RootLabel.xwf")).group prec✝
Hewett2026.instReprRootLabel.repr Hewett2026.RootLabel.krh prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hewett2026.RootLabel.krh")).group prec✝
Hewett2026.instReprRootLabel.repr Hewett2026.RootLabel.dwr prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hewett2026.RootLabel.dwr")).group prec✝
Hewett2026.instReprRootLabel.repr Hewett2026.RootLabel.Hkm prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hewett2026.RootLabel.Hkm")).group prec✝
Hewett2026.instReprRootLabel.repr Hewett2026.RootLabel.tpl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hewett2026.RootLabel.tpl")).group prec✝
Hewett2026.instReprRootLabel.repr Hewett2026.RootLabel.shps prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hewett2026.RootLabel.shps")).group prec✝

Instances For

def Hewett2026.instBEqRootLabel.beq :

RootLabel → RootLabel → Bool

Equations

Hewett2026.instBEqRootLabel.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

@[implicit_reducible]

instance Hewett2026.instBEqRootLabel :

Equations

Hewett2026.instBEqRootLabel = { beq := Hewett2026.instBEqRootLabel.beq }

inductive Hewett2026.SemiticPrep :

Prepositions attested in the paper's l-selection data.

Instances For

@[implicit_reducible]

instance Hewett2026.instDecidableEqSemiticPrep :

DecidableEq SemiticPrep

Equations

Hewett2026.instDecidableEqSemiticPrep x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Hewett2026.instReprSemiticPrep :

Repr SemiticPrep

Equations

Hewett2026.instReprSemiticPrep = { reprPrec := Hewett2026.instReprSemiticPrep.repr }

def Hewett2026.instReprSemiticPrep.repr :

SemiticPrep → ℕ → Std.Format

Equations

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

Instances For

def Hewett2026.instBEqSemiticPrep.beq :

SemiticPrep → SemiticPrep → Bool

Equations

Hewett2026.instBEqSemiticPrep.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

@[implicit_reducible]

instance Hewett2026.instBEqSemiticPrep :

BEq SemiticPrep

Equations

Hewett2026.instBEqSemiticPrep = { beq := Hewett2026.instBEqSemiticPrep.beq }

inductive Hewett2026.SemiticLang :

Languages providing l-selection data in the paper.

tunisianArabic : SemiticLang
syrianArabic : SemiticLang
hebrew : SemiticLang

Instances For

@[implicit_reducible]

instance Hewett2026.instDecidableEqSemiticLang :

DecidableEq SemiticLang

Equations

Hewett2026.instDecidableEqSemiticLang x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Hewett2026.instReprSemiticLang.repr :

SemiticLang → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Hewett2026.instReprSemiticLang :

Repr SemiticLang

Equations

Hewett2026.instReprSemiticLang = { reprPrec := Hewett2026.instReprSemiticLang.repr }

@[implicit_reducible]

instance Hewett2026.instBEqSemiticLang :

BEq SemiticLang

Equations

Hewett2026.instBEqSemiticLang = { beq := Hewett2026.instBEqSemiticLang.beq }

def Hewett2026.instBEqSemiticLang.beq :

SemiticLang → SemiticLang → Bool

Equations

Hewett2026.instBEqSemiticLang.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

structure Hewett2026.LSelDatum :

An l-selection datum: a root in a specific template selects a specific preposition (or none, for transitive/unergative uses or passive P-suppression).

root : RootLabel
template : SemiticTemplate
prep : Option SemiticPrep
lang : SemiticLang

Instances For

@[implicit_reducible]

instance Hewett2026.instReprLSelDatum :

Equations

Hewett2026.instReprLSelDatum = { reprPrec := Hewett2026.instReprLSelDatum.repr }

def Hewett2026.instReprLSelDatum.repr :

LSelDatum → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Hewett2026.instBEqLSelDatum :

Equations

Hewett2026.instBEqLSelDatum = { beq := Hewett2026.instBEqLSelDatum.beq }

def Hewett2026.instBEqLSelDatum.beq :

LSelDatum → LSelDatum → Bool

Equations

One or more equations did not get rendered due to their size.
Hewett2026.instBEqLSelDatum.beq x✝¹ x✝ = false

Instances For

def Hewett2026.xwf_XaYaZ :

Template-independent l-selection: xwf selects min 'from' regardless of template. XaYaZ: xa:f min l-?asad 'He was afraid of the lion.' XaYYaZ: xawwaf-u min l-?asad 'He made him afraid of the lion.' @cite{hewett-2026} ex. (11).

Equations

Hewett2026.xwf_XaYaZ = { root := Hewett2026.RootLabel.xwf, template := Hewett2026.SemiticTemplate.XaYaZ, prep := some Hewett2026.SemiticPrep.min, lang := Hewett2026.SemiticLang.tunisianArabic }

Instances For

def Hewett2026.xwf_XaYYaZ :

Equations

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

Instances For

def Hewett2026.krh_XaYaZ :

Template-dependent l-selection: krh 'hate'. XaYaZ: kraht (*fi) Sami 'I hate (*in) Sami.' — no PP, transitive. XaYYaZ: karraht-ha *(fi) Sami 'I made her hate *(in) Sami.' — requires fi. @cite{hewett-2026} ex. (13a).

Equations

Hewett2026.krh_XaYaZ = { root := Hewett2026.RootLabel.krh, template := Hewett2026.SemiticTemplate.XaYaZ, prep := none, lang := Hewett2026.SemiticLang.tunisianArabic }

Instances For

def Hewett2026.krh_XaYYaZ :

Equations

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

Instances For

def Hewett2026.dwr_XaYaZ :

Template-dependent l-selection: dwr 'encircle'. XaYaZ: l-hnash da:r bi: k 'The snake encircled you.' — selects bi:. XaYYaZ: dawwart l-hnash fli: k 'I made the snake encircle you.' — selects fli: (= Eala). @cite{hewett-2026} ex. (13b).

Equations

Hewett2026.dwr_XaYaZ = { root := Hewett2026.RootLabel.dwr, template := Hewett2026.SemiticTemplate.XaYaZ, prep := some Hewett2026.SemiticPrep.bi, lang := Hewett2026.SemiticLang.tunisianArabic }

Instances For

def Hewett2026.dwr_XaYYaZ :

Equations

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

Instances For

def Hewett2026.Hkm_XaYaZ :

Template-dependent l-selection: Hkm 'sentence/referee' (Syrian Arabic). XaYaZ: hakam Ealej-o b-s-sidjn 'He sentenced him to jail.' — selects Ealej. XaYYaZ: Hakkam (l-muba:re:t) 'He refereed (the match).' — no PP (rejects Eala and b-). @cite{hewett-2026} ex. (14).

Equations

Hewett2026.Hkm_XaYaZ = { root := Hewett2026.RootLabel.Hkm, template := Hewett2026.SemiticTemplate.XaYaZ, prep := some Hewett2026.SemiticPrep.Ealej, lang := Hewett2026.SemiticLang.syrianArabic }

Instances For

def Hewett2026.Hkm_XaYYaZ :

Equations

Hewett2026.Hkm_XaYYaZ = { root := Hewett2026.RootLabel.Hkm, template := Hewett2026.SemiticTemplate.XaYYaZ, prep := none, lang := Hewett2026.SemiticLang.syrianArabic }

Instances For

def Hewett2026.tpl_XiYeZ :

Template-dependent l-selection: tpl 'treat' (Hebrew). XiYeZ: tipel be- NP 'treated in NP'. — selects be. XuYaZ: NP tupal (al jedej NP) 'NP was treated (by NP).' — P suppressed by passive. @cite{hewett-2026} ex. (17).

Equations

Hewett2026.tpl_XiYeZ = { root := Hewett2026.RootLabel.tpl, template := Hewett2026.SemiticTemplate.XiYeZ, prep := some Hewett2026.SemiticPrep.be, lang := Hewett2026.SemiticLang.hebrew }

Instances For

def Hewett2026.tpl_XuYaZ :

Equations

Hewett2026.tpl_XuYaZ = { root := Hewett2026.RootLabel.tpl, template := Hewett2026.SemiticTemplate.XuYaZ, prep := none, lang := Hewett2026.SemiticLang.hebrew }

Instances For

def Hewett2026.shps_hiXYiZ :

Template-dependent l-selection: shps 'influence' (Hebrew). hiXYiZ: hishpia al NP 'influenced over NP'. — selects al. huXYaZ: NP hushpa (al jedej NP) 'NP was influenced (by NP).' — P suppressed by passive. @cite{hewett-2026} ex. (18).

Equations

Hewett2026.shps_hiXYiZ = { root := Hewett2026.RootLabel.shps, template := Hewett2026.SemiticTemplate.hiXYiZ, prep := some Hewett2026.SemiticPrep.al, lang := Hewett2026.SemiticLang.hebrew }

Instances For

def Hewett2026.shps_huXYaZ :

Equations

Hewett2026.shps_huXYaZ = { root := Hewett2026.RootLabel.shps, template := Hewett2026.SemiticTemplate.huXYaZ, prep := none, lang := Hewett2026.SemiticLang.hebrew }

Instances For

def Hewett2026.lSelect :

RootLabel → SemiticTemplate → Option SemiticPrep

L-selection as a function of root AND template — the paper's core insight. L-selection is NOT a function of root alone.

Returns none when the root+template combination does not select a PP complement (transitive/unergative use or passive suppression).

xwf uses a wildcard: the paper attests min in both XaYaZ and XaYYaZ, and the claim is that xwf is template-independent — we generalize to all templates.

Equations

Instances For

theorem Hewett2026.xwf_data_consistent :

lSelect xwf_XaYaZ.root xwf_XaYaZ.template = xwf_XaYaZ.prep ∧ lSelect xwf_XaYYaZ.root xwf_XaYYaZ.template = xwf_XaYYaZ.prep

Verify data consistency: lSelect matches each LSelDatum.

theorem Hewett2026.krh_data_consistent :

lSelect krh_XaYaZ.root krh_XaYaZ.template = krh_XaYaZ.prep ∧ lSelect krh_XaYYaZ.root krh_XaYYaZ.template = krh_XaYYaZ.prep

theorem Hewett2026.dwr_data_consistent :

lSelect dwr_XaYaZ.root dwr_XaYaZ.template = dwr_XaYaZ.prep ∧ lSelect dwr_XaYYaZ.root dwr_XaYYaZ.template = dwr_XaYYaZ.prep

theorem Hewett2026.Hkm_data_consistent :

lSelect Hkm_XaYaZ.root Hkm_XaYaZ.template = Hkm_XaYaZ.prep ∧ lSelect Hkm_XaYYaZ.root Hkm_XaYYaZ.template = Hkm_XaYYaZ.prep

theorem Hewett2026.tpl_data_consistent :

lSelect tpl_XiYeZ.root tpl_XiYeZ.template = tpl_XiYeZ.prep ∧ lSelect tpl_XuYaZ.root tpl_XuYaZ.template = tpl_XuYaZ.prep

theorem Hewett2026.shps_data_consistent :

lSelect shps_hiXYiZ.root shps_hiXYiZ.template = shps_hiXYiZ.prep ∧ lSelect shps_huXYaZ.root shps_huXYaZ.template = shps_huXYaZ.prep

def Hewett2026.isTemplateDependentWitness (r : RootLabel) :

Option (SemiticTemplate × SemiticTemplate)

A root is template-dependent for l-selection iff there exist two attested template pairings for which lSelect returns different prepositions. Derived from lSelect, not stipulated.

Equations

Instances For

def Hewett2026.isTemplateDependent (r : RootLabel) :

Bool

Derived classification: a root is template-dependent iff a witnessing pair exists AND its two values actually differ.

Equations

Hewett2026.isTemplateDependent r = match Hewett2026.isTemplateDependentWitness r with | some (t1, t2) => Hewett2026.lSelect r t1 != Hewett2026.lSelect r t2 | none => false

Instances For

theorem Hewett2026.xwf_template_independent :

lSelect RootLabel.xwf SemiticTemplate.XaYaZ = lSelect RootLabel.xwf SemiticTemplate.XaYYaZ

xwf is template-independent: same P regardless of template.

theorem Hewett2026.krh_template_dependent :

isTemplateDependent RootLabel.krh = true

krh is template-dependent: different P across templates.

theorem Hewett2026.dwr_template_dependent :

isTemplateDependent RootLabel.dwr = true

dwr is template-dependent: different P across templates.

theorem Hewett2026.Hkm_template_dependent :

isTemplateDependent RootLabel.Hkm = true

Hkm is template-dependent: the direction reverses (XaYaZ takes PP, XaYYaZ doesn't).

theorem Hewett2026.xwf_not_template_dependent :

isTemplateDependent RootLabel.xwf = false

xwf is NOT template-dependent.

def Hewett2026.templateInvariant (r : RootLabel) :

Template-invariance prediction: l-selection for a given root is constant across all templates.

Both @cite{harley-2014} (roots select) and @cite{merchant-2019} (categorizing heads select) predict this, for different reasons:

Harley: the root takes its complement directly, so only the root determines the l-selected P.
Merchant: the categorizing head (V) selects, but since all templates verbalize the root with the same categorizer V, the l-selected P should be template-invariant.

Since neither root nor categorizer varies across templates, both theories make the same prediction for verbs. The paper shows this prediction is false.

Equations

Hewett2026.templateInvariant r = ∀ (t1 t2 : Hewett2026.SemiticTemplate), Hewett2026.lSelect r t1 = Hewett2026.lSelect r t2

Instances For

theorem Hewett2026.harley_falsified :

¬templateInvariant RootLabel.krh

@cite{harley-2014} is falsified: krh is a counterexample. XaYaZ krh is transitive (no PP), XaYYaZ krh requires fi.

theorem Hewett2026.merchant_falsified :

¬templateInvariant RootLabel.dwr

@cite{merchant-2019} is falsified by independent data: dwr. XaYaZ dwr selects bi:, XaYYaZ dwr selects Eala.

theorem Hewett2026.xwf_satisfies_invariance :

templateInvariant RootLabel.xwf

Template-independent roots DO satisfy the invariance prediction. Joint Selection is a refinement, not a wholesale rejection: it reduces to root-level selection when the template dimension is vacuous (the selectional feature's template index is the same across all templates).

theorem Hewett2026.homophony_argument_krh :

lSelect RootLabel.krh SemiticTemplate.XaYaZ ≠ lSelect RootLabel.krh SemiticTemplate.XaYYaZ ∧ ∀ (r : RootLabel), r = RootLabel.krh → lSelect r SemiticTemplate.XaYaZ = none ∧ lSelect r SemiticTemplate.XaYYaZ = some SemiticPrep.fi

The homophony argument (p. 208): template-dependent l-selection cannot be explained by positing distinct homophonous roots (krh₁ for XaYaZ, krh₂ for XaYYaZ), because this would fail to explain mutual exclusivity — krh₁ only appears in XaYaZ and krh₂ only in XaYYaZ, parallel to the suppletive distribution of go~went.

If roots were truly distinct, we'd expect each to freely appear in any template. The mutual exclusivity shows a single root with template-sensitive selectional properties.

theorem Hewett2026.cSelection_vs_lSelection :

(∀ (r : RootClassification) (c1 c2 : Morphology.DM.Categorizer), { root := r, categorizer := c1 }.root.arity = { root := r, categorizer := c2 }.root.arity) ∧ ∃ (r : RootLabel), ¬templateInvariant r

C-selection (arity) IS root-level per @cite{harley-2014} S3. This connects to complement_selection_at_root_level in Categorizer.lean. L-selection is the dimension that escapes root determination, not c-selection.

structure Hewett2026.VerbalizedRoot :

A verbalized root: a root that has been categorized as a verb AND placed in a specific template. This is the structure that jointly determines l-selection.

VerbalizedRoot bridges two types that never previously appeared together: CategorizedRoot (from Categorizer.lean) and VoiceHead (from Voice.lean). The template connects them — it determines which Voice flavor the root appears with AND which P is l-selected.

categorized : Morphology.DM.CategorizedRoot
The root with its categorizer.
template : SemiticTemplate
The Semitic template (functional head bundle).
rootLabel : RootLabel
The paper-specific root label (for l-selection lookup).
lSelectedP : Option SemiticPrep
The l-selected preposition, derived from root + template.

Instances For

@[implicit_reducible]

instance Hewett2026.instReprVerbalizedRoot :

Repr VerbalizedRoot

Equations

Hewett2026.instReprVerbalizedRoot = { reprPrec := Hewett2026.instReprVerbalizedRoot.repr }

def Hewett2026.instReprVerbalizedRoot.repr :

VerbalizedRoot → ℕ → Std.Format

Equations

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

Instances For

def Hewett2026.VerbalizedRoot.voiceFlavor (vr : VerbalizedRoot) :

Minimalist.VoiceFlavor

The Voice flavor is determined by the template, not the root.

Equations

vr.voiceFlavor = vr.template.toVoiceFlavor

Instances For

theorem Hewett2026.arity_template_invariant (cr : Morphology.DM.CategorizedRoot) (rl : RootLabel) (t1 t2 : SemiticTemplate) :

{ categorized := cr, template := t1, rootLabel := rl }.categorized.root.arity = { categorized := cr, template := t2, rootLabel := rl }.categorized.root.arity

Arity is template-invariant (root-level) but l-selection is not. This is the core architectural claim: c-selection and l-selection factor differently in the grammar.

theorem Hewett2026.causer_template_assigns_theta :

have voice := { flavor := SemiticTemplate.XaYYaZ.toVoiceFlavor, hasD := true }; voice.AssignsTheta

Causer templates map to theta-assigning Voice. XaYYaZ introduces a causer → theta-assigning → vDO in decomposition. This is why the template can influence l-selection: it determines the functional structure above VP.

theorem Hewett2026.active_template_assigns_theta :

have voice := { flavor := SemiticTemplate.XaYaZ.toVoiceFlavor, hasD := true }; voice.AssignsTheta

Basic active template maps to agentive Voice, also theta-assigning.

theorem Hewett2026.passive_template_no_theta :

have voice := { flavor := SemiticTemplate.huXYaZ.toVoiceFlavor, hasD := true }; ¬voice.AssignsTheta

Passive templates do NOT assign theta — the external argument is demoted or absent. This is the structural basis for Hebrew P-suppression: the passivizing template head merged above the verbalized root suppresses the l-selected P.

theorem Hewett2026.voice_distinguishes_templates :

SemiticTemplate.XaYaZ.toVoiceFlavor ≠ SemiticTemplate.XaYYaZ.toVoiceFlavor

XaYaZ and XaYYaZ differ in their Voice contribution: XaYaZ maps to agentive, XaYYaZ maps to causer. This Voice difference is what drives the l-selection variation — it's the functional structure ABOVE the selectional domain that varies.

Connection to @cite{kratzer-1996} and @cite{wood-2015} #

@cite{kratzer-1996} argues that Voice is a separate head from V, introducing the external argument. @cite{wood-2015} shows Icelandic -st morphology spells out Voice across six distinct configurations (anticausative, middle, reflexive, experiencer, inherent, reciprocal), parameterized by ±θ (theta-assignment) and ±D (specifier requirement).

Semitic templates instantiate the SAME Voice architecture: toVoiceFlavor maps each template to a VoiceFlavor, and the resulting VoiceHead determines theta-assignment via assignsTheta. The cross-linguistic parallel: Semitic templates and Icelandic -st are both morphology that realizes Voice heads, determining argument structure above the root.

The key difference: Semitic templates are EACH associated with a SINGLE Voice flavor (XaYaZ → agentive, XaYYaZ → causer, etc.), while Icelandic -st spells out ALL non-agentive Voice types as an elsewhere exponent. The two languages carve up the VoiceFlavor space complementarily.

def Hewett2026.SemiticTemplate.isTheta :

SemiticTemplate → Bool

Exhaustive theta classification: every template maps to either theta-assigning (+θ) or non-theta-assigning (-θ) Voice. Active templates (XaYaZ, XaYYaZ, hiXYiZ, XiYeZ) are +θ; passive/medio-passive templates (nXaYaZ, tXaYYaZ, huXYaZ, XuYaZ) are -θ. This is an exhaustive partition with no exceptions.

Equations

Hewett2026.SemiticTemplate.XaYaZ.isTheta = true
Hewett2026.SemiticTemplate.XaYYaZ.isTheta = true
Hewett2026.SemiticTemplate.hiXYiZ.isTheta = true
Hewett2026.SemiticTemplate.XiYeZ.isTheta = true
Hewett2026.SemiticTemplate.nXaYaZ.isTheta = false
Hewett2026.SemiticTemplate.tXaYYaZ.isTheta = false
Hewett2026.SemiticTemplate.huXYaZ.isTheta = false
Hewett2026.SemiticTemplate.XuYaZ.isTheta = false

Instances For

theorem Hewett2026.isTheta_matches_assignsTheta (t : SemiticTemplate) :

have voice := { flavor := t.toVoiceFlavor, hasD := true }; voice.AssignsTheta ↔ t.isTheta = true

isTheta agrees with VoiceHead.AssignsTheta for all templates.

theorem Hewett2026.severing_instantiated (cr : Morphology.DM.CategorizedRoot) (rl : RootLabel) :

{ categorized := cr, template := SemiticTemplate.XaYaZ, rootLabel := rl }.categorized.root.arity = { categorized := cr, template := SemiticTemplate.XaYYaZ, rootLabel := rl }.categorized.root.arity ∧ SemiticTemplate.XaYaZ.toVoiceFlavor ≠ SemiticTemplate.XaYYaZ.toVoiceFlavor

@cite{kratzer-1996}'s severing instantiated for Semitic: VerbalizedRoot factors argument structure into V (CategorizedRoot) and Voice (template.toVoiceFlavor). The categorizer determines arity (c-selection); Voice determines whether an external argument is introduced. L-selection depends on both — it is determined by the root AND the Voice-determining template jointly.

def Hewett2026.semiticVoiceFlavors :

List Minimalist.VoiceFlavor

Semitic Voice coverage: the four VoiceFlavor values that Semitic templates produce. These are exactly the flavors relevant to TRANSITIVE and PASSIVE argument structure.

Equations

Hewett2026.semiticVoiceFlavors = [Minimalist.VoiceFlavor.agentive, Minimalist.VoiceFlavor.causer, Minimalist.VoiceFlavor.passive, Minimalist.VoiceFlavor.nonThematic]

Instances For

theorem Hewett2026.template_flavors_in_coverage (t : SemiticTemplate) :

semiticVoiceFlavors.contains t.toVoiceFlavor = true

All template voice flavors are in the Semitic coverage set.

def Hewett2026.icelandicStFlavors :

List Minimalist.VoiceFlavor

Icelandic -st Voice coverage: the non-agentive flavors from @cite{wood-2015}. These are exactly the flavors relevant to DETRANSITIVIZED and DERIVED argument structure.

Equations

Hewett2026.icelandicStFlavors = [Minimalist.VoiceFlavor.nonThematic, Minimalist.VoiceFlavor.expletive, Minimalist.VoiceFlavor.reflexive, Minimalist.VoiceFlavor.experiencer]

Instances For

theorem Hewett2026.voice_coverage_complementary :

semiticVoiceFlavors.contains Minimalist.VoiceFlavor.nonThematic = true ∧ icelandicStFlavors.contains Minimalist.VoiceFlavor.nonThematic = true ∧ icelandicStFlavors.contains Minimalist.VoiceFlavor.agentive = false ∧ icelandicStFlavors.contains Minimalist.VoiceFlavor.causer = false ∧ icelandicStFlavors.contains Minimalist.VoiceFlavor.passive = false ∧ semiticVoiceFlavors.contains Minimalist.VoiceFlavor.expletive = false ∧ semiticVoiceFlavors.contains Minimalist.VoiceFlavor.reflexive = false ∧ semiticVoiceFlavors.contains Minimalist.VoiceFlavor.experiencer = false

The Semitic and Icelandic coverage sets are complementary: they share only .nonThematic (anticausative, which in Semitic is the medio-passive template nXaYaZ/tXaYYaZ and in Icelandic is -st).

theorem Hewett2026.templates_map_to_canonical_voices :

Minimalist.voiceAgent.flavor = SemiticTemplate.XaYaZ.toVoiceFlavor ∧ Minimalist.voiceCauser.flavor = SemiticTemplate.XaYYaZ.toVoiceFlavor ∧ Minimalist.voicePassive.flavor = SemiticTemplate.nXaYaZ.toVoiceFlavor ∧ Minimalist.voiceAnticausative.flavor = SemiticTemplate.tXaYYaZ.toVoiceFlavor

The canonical Voice heads from Voice.lean that correspond to each template family. Active templates map to voiceAgent/voiceCauser; passive templates map to voicePassive/voiceAnticausative. This is the same typology @cite{kratzer-1996} uses for the causative alternation and @cite{wood-2015} extends for Icelandic -st.

theorem Hewett2026.causative_alternation_parallel :

Minimalist.voiceAgent.AssignsTheta ∧ ¬Minimalist.voiceAnticausative.AssignsTheta ∧ SemiticTemplate.XaYaZ.isTheta = true ∧ SemiticTemplate.nXaYaZ.isTheta = false

@cite{kratzer-1996}'s causative alternation parallels the Semitic template alternation: both are Voice alternations over a shared VP. Kratzer: "John broke the vase" (Voice_AG) ↔ "The vase broke" (Voice_∅). Semitic: dar b- (XaYaZ/agentive) ↔ ndar (nXaYaZ/passive). In both, the causal relation is shared; only Voice varies.

The Template → Voice → Applicative chain #

@cite{pylkkanen-2008} establishes that high applicatives require Voice with event semantics, while low applicatives are independent of Voice. @cite{hewett-2026}'s template system instantiates this: each template determines a VoiceFlavor (via toVoiceFlavor), and that flavor determines whether Voice has event semantics (via hasSemantics).

The mathematical content is a chain of strict inclusions on Voice predicates:

assignsTheta ⊂ hasSemantics = licensesAppl(high) ⊂ licensesAppl(low) = ⊤

The first inclusion is a general property of the Voice architecture (theta_implies_hasSemantics), not specific to Semitic: every θ-role assigning Voice head contributes event semantics, but the converse fails (passive and impersonal Voice have semantics without θ). The second inclusion is trivial — low applicatives are unconditional.

For the Semitic template space, the pullback of this chain yields: +θ templates ⊂ high-Appl-licensing templates ⊂ all templates. The blocking set {tXaYYaZ} is a singleton because the Semitic inventory includes exactly one semantics-free flavor (.nonThematic).

This instantiates for Semitic the same high/low asymmetry that @cite{wood-2015} documents for Icelandic (dative_voice_asymmetry in Wood2015.lean): middles block ethical datives but license possessive datives.

theorem Hewett2026.theta_implies_hasSemantics (v : Minimalist.VoiceHead) :

v.AssignsTheta → v.HasSemantics

θ-assignment entails event semantics: every Voice head that introduces an external argument also contributes semantic content. The converse fails (hasSemantics_not_implies_theta).

theorem Hewett2026.hasSemantics_not_implies_theta :

Minimalist.voicePassive.HasSemantics ∧ ¬Minimalist.voicePassive.AssignsTheta ∧ ¬Minimalist.voiceMiddle.HasSemantics ∧ ¬Minimalist.voiceMiddle.AssignsTheta

The converse fails: passive Voice has semantics (it contributes a by-phrase) but does not assign θ (the external argument is demoted). Impersonal Voice is another counterexample (existential closure without a projected specifier).

theorem Hewett2026.no_semantics_implies_no_theta (v : Minimalist.VoiceHead) :

¬v.HasSemantics → ¬v.AssignsTheta

Contrapositive: no event semantics entails no θ-assignment. Derived from theta_implies_hasSemantics by mt.

theorem Hewett2026.low_appl_unconditional (v : Minimalist.VoiceHead) :

Minimalist.applLowRecipient.licensedWith v = true ∧ Minimalist.applLowSource.licensedWith v = true

Low applicatives are unconditionally licensed regardless of Voice. The if on requiresEventSemantics takes the else branch for both low types, yielding true for any Voice head.

def Hewett2026.SemiticTemplate.toVoiceHead (t : SemiticTemplate) :

Minimalist.VoiceHead

Construct a canonical VoiceHead from a template. hasD is set to match the template's θ properties; phasehood follows the flavor default (which agrees with t.isTheta for all currently-defined templates). Only flavor matters for applicative licensing (via hasSemantics).

Equations

t.toVoiceHead = { flavor := t.toVoiceFlavor, hasD := t.isTheta }

Instances For

def Hewett2026.SemiticTemplate.licensesAppl (t : SemiticTemplate) (appl : Minimalist.ApplHead) :

Bool

Does this template license a given applicative type? Composes licensedWith ∘ toVoiceHead.

Equations

t.licensesAppl appl = appl.licensedWith t.toVoiceHead

Instances For

theorem Hewett2026.high_appl_iff_hasSemantics (t : SemiticTemplate) :

t.licensesAppl Minimalist.applHigh = true ↔ t.toVoiceHead.HasSemantics

Licensing factors through HasSemantics for high Appl.

theorem Hewett2026.high_appl_blocked_implies_no_theta (t : SemiticTemplate) :

t.licensesAppl Minimalist.applHigh = false → ¬t.toVoiceHead.AssignsTheta

If a template blocks high applicatives, it also fails to assign θ. Proved via the general implication θ → hasSemantics, not by enumerating templates.

theorem Hewett2026.theta_licenses_all_appl (t : SemiticTemplate) (appl : Minimalist.ApplHead) :

t.toVoiceHead.AssignsTheta → t.licensesAppl appl = true

If a template assigns θ, it licenses ALL applicative types. Chain: θ → hasSemantics → high licensed; low always licensed. Proved via the general implication, quantified over ApplHead.

theorem Hewett2026.voice_predicate_chain :

(∀ (t : SemiticTemplate), t.toVoiceHead.AssignsTheta → t.licensesAppl Minimalist.applHigh = true) ∧ (∃ (t : SemiticTemplate), t.licensesAppl Minimalist.applHigh = true ∧ ¬t.toVoiceHead.AssignsTheta) ∧ (∀ (t : SemiticTemplate), t.licensesAppl Minimalist.applHigh = true → t.licensesAppl Minimalist.applLowRecipient = true) ∧ ∃ (t : SemiticTemplate), t.licensesAppl Minimalist.applHigh = false

The full implication chain on Voice predicates, instantiated for the Semitic template space. Both inclusions are STRICT:

+θ templates ⊂ high-Appl-licensing templates: nXaYaZ (passive) licenses high Appl but assigns no θ.
High-Appl-licensing templates ⊂ all templates: tXaYYaZ blocks high Appl.

The first inclusion is proved via the general theta_implies_hasSemantics, not by enumerating templates.

inductive Hewett2026.ActivationKey :

Activation keys for Semitic l-selection. The activation tuple (c₁, …, cₙ) in @cite{hewett-2026} Def 23 mixes two sorts of key: syntactic categories (Cat from the Minimalist architecture) and template identities. This sum type makes the key space explicit.

cat : Minimalist.Cat → ActivationKey
A syntactic category key (stripped by a categorizing head).
template : SemiticTemplate → ActivationKey
A template key (stripped by the template-defining head).

Instances For

def Hewett2026.instDecidableEqActivationKey.decEq (x✝ x✝¹ : ActivationKey) :

Decidable (x✝ = x✝¹)

Equations

Hewett2026.instDecidableEqActivationKey.decEq (Hewett2026.ActivationKey.cat a) (Hewett2026.ActivationKey.cat b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
Hewett2026.instDecidableEqActivationKey.decEq (Hewett2026.ActivationKey.cat a) (Hewett2026.ActivationKey.template a_1) = isFalse ⋯
Hewett2026.instDecidableEqActivationKey.decEq (Hewett2026.ActivationKey.template a) (Hewett2026.ActivationKey.cat a_1) = isFalse ⋯
Hewett2026.instDecidableEqActivationKey.decEq (Hewett2026.ActivationKey.template a) (Hewett2026.ActivationKey.template b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

Instances For

@[implicit_reducible]

instance Hewett2026.instDecidableEqActivationKey :

DecidableEq ActivationKey

Equations

Hewett2026.instDecidableEqActivationKey = Hewett2026.instDecidableEqActivationKey.decEq

@[implicit_reducible]

instance Hewett2026.instReprActivationKey :

Repr ActivationKey

Equations

Hewett2026.instReprActivationKey = { reprPrec := Hewett2026.instReprActivationKey.repr }

def Hewett2026.instReprActivationKey.repr :

ActivationKey → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Hewett2026.instBEqActivationKey :

BEq ActivationKey

BEq via DecidableEq ensures LawfulBEq follows trivially.

Equations

Hewett2026.instBEqActivationKey = { beq := fun (a b : Hewett2026.ActivationKey) => decide (a = b) }

instance Hewett2026.instLawfulBEqActivationKey :

LawfulBEq ActivationKey

structure Hewett2026.SelectionalFeature :

A selectional feature indexed by an ordered activation tuple.

@cite{hewett-2026} Def 23 (adapted from @cite{merchant-2019}): Activate(X,Y;F) — X activates F on Y. X bears a category feature c, Y bears an inactive feature F^C where C = (c₁,...,cₙ). If c = c₁, Activate strips c₁ from C, leaving F^(c₂,...,cₙ). If n = 1 and c = c₁, F^C becomes F (fully active).

The activation field uses the general ActivationIndex from Checking.lean — the same ordered n-tuple stripping mechanism. For Semitic l-selection, the tuple is [.cat .v, .template T]: the categorizing head V strips the first index, the template-defining head strips the second.

selectedP : SemiticPrep
The preposition this feature selects when fully activated.
activation : Minimalist.ActivationIndex ActivationKey
Ordered activation tuple. Empty = fully active.

Instances For

@[implicit_reducible]

instance Hewett2026.instReprSelectionalFeature :

Repr SelectionalFeature

Equations

Hewett2026.instReprSelectionalFeature = { reprPrec := Hewett2026.instReprSelectionalFeature.repr }

def Hewett2026.instReprSelectionalFeature.repr :

SelectionalFeature → ℕ → Std.Format

Equations

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

Instances For

def Hewett2026.SelectionalFeature.status (sf : SelectionalFeature) :

Minimalist.FeatureStatus

The overall status of a selectional feature, derived from its activation tuple. Maps to the FeatureStatus lifecycle in Checking.lean via ActivationIndex.toStatus.

Equations

sf.status = sf.activation.toStatus

Instances For

def Hewett2026.SelectionalFeature.activate (sf : SelectionalFeature) (key : ActivationKey) :

SelectionalFeature

Attempt to activate this feature with the given key. Delegates to ActivationIndex.activate (matching left-to-right stripping).

Equations

sf.activate key = { selectedP := sf.selectedP, activation := sf.activation.activate key }

Instances For

def Hewett2026.SelectionalFeature.dormant (p : SemiticPrep) (t : SemiticTemplate) :

SelectionalFeature

A dormant feature indexed by (V, T): needs V then T to activate.

Equations

Hewett2026.SelectionalFeature.dormant p t = { selectedP := p, activation := { remaining := [Hewett2026.ActivationKey.cat Minimalist.Cat.v, Hewett2026.ActivationKey.template t] } }

Instances For

theorem Hewett2026.dormant_is_inactive (p : SemiticPrep) (t : SemiticTemplate) :

(SelectionalFeature.dormant p t).status = Minimalist.FeatureStatus.inactive

A dormant feature is inactive.

theorem Hewett2026.cat_alone_inactive (p : SemiticPrep) (t : SemiticTemplate) :

((SelectionalFeature.dormant p t).activate (ActivationKey.cat Minimalist.Cat.v)).status = Minimalist.FeatureStatus.inactive

Activating V alone strips one key but leaves the template key.

theorem Hewett2026.wrong_order_noop (p : SemiticPrep) (t : SemiticTemplate) :

((SelectionalFeature.dormant p t).activate (ActivationKey.template t)).status = Minimalist.FeatureStatus.inactive

Activating with a non-matching key (template before V) is a no-op.

theorem Hewett2026.both_activations_active (p : SemiticPrep) (t : SemiticTemplate) :

(((SelectionalFeature.dormant p t).activate (ActivationKey.cat Minimalist.Cat.v)).activate (ActivationKey.template t)).status = Minimalist.FeatureStatus.active

Both activations in the correct order yield an active feature.

theorem Hewett2026.activation_matches_lifecycle (p : SemiticPrep) (t : SemiticTemplate) :

have dormant := SelectionalFeature.dormant p t; have activated := (dormant.activate (ActivationKey.cat Minimalist.Cat.v)).activate (ActivationKey.template t); dormant.status = Minimalist.FeatureStatus.inactive ∧ activated.status = Minimalist.FeatureStatus.active

Connect to Checking.lean's lifecycle: a dormant selectional feature uses the .inactive status, and after both activations it transitions to .active, ready for the standard checking lifecycle.

theorem Hewett2026.activated_feature_enters_lifecycle :

have tf := { val := Minimalist.FeatureVal.phi (Minimalist.PhiFeature.person Features.Prominence.PersonLevel.first), host := Minimalist.Cat.v, interp := Minimalist.Interpretability.uninterpretable, status := Minimalist.FeatureStatus.inactive }; ∃ (tf1 : Minimalist.TrackedFeature), tf.activate = some tf1 ∧ ∃ (tf2 : Minimalist.TrackedFeature), tf1.check = some tf2 ∧ ∃ (tf3 : Minimalist.TrackedFeature), tf2.erase = some tf3 ∧ tf3.status = Minimalist.FeatureStatus.erased

The Checking.lean lifecycle continues after activation: an activated selectional feature can be checked and erased.

def Hewett2026.dwr_sel_XaYaZ :

SelectionalFeature

The root dwr carries two selectional features, each indexed by [.cat .v, .template T] for its specific template. [SEL: bi^{V, XaYaZ}] selects bi: when activated by V + XaYaZ. [SEL: Eala^{V, XaYYaZ}] selects Eala when activated by V + XaYYaZ. @cite{hewett-2026} ex. (24)--(25).

Equations

Hewett2026.dwr_sel_XaYaZ = Hewett2026.SelectionalFeature.dormant Hewett2026.SemiticPrep.bi Hewett2026.SemiticTemplate.XaYaZ

Instances For

def Hewett2026.dwr_sel_XaYYaZ :

SelectionalFeature

Equations

Hewett2026.dwr_sel_XaYYaZ = Hewett2026.SelectionalFeature.dormant Hewett2026.SemiticPrep.Eala Hewett2026.SemiticTemplate.XaYYaZ

Instances For

theorem Hewett2026.dwr_XaYaZ_derivation :

have bi_afterV := dwr_sel_XaYaZ.activate (ActivationKey.cat Minimalist.Cat.v); have bi_afterT := bi_afterV.activate (ActivationKey.template SemiticTemplate.XaYaZ); have eala_afterV := dwr_sel_XaYYaZ.activate (ActivationKey.cat Minimalist.Cat.v); have eala_afterT := eala_afterV.activate (ActivationKey.template SemiticTemplate.XaYaZ); bi_afterT.status = Minimalist.FeatureStatus.active ∧ bi_afterT.selectedP = SemiticPrep.bi ∧ eala_afterT.status = Minimalist.FeatureStatus.inactive ∧ some bi_afterT.selectedP = lSelect RootLabel.dwr SemiticTemplate.XaYaZ

Derivation of ex. (24): dar b- 'encircled'. Step 1: V merges → strips .cat .v from both features. Step 2: XaYaZ merges → strips .template .XaYaZ from the bi: feature (match!), but NOT from the Eala feature (.template .XaYYaZ ≠ .template .XaYaZ — no match, no strip). Result: bi: feature is fully active; Eala feature stays inactive.

theorem Hewett2026.dwr_XaYYaZ_derivation :

have eala_afterV := dwr_sel_XaYYaZ.activate (ActivationKey.cat Minimalist.Cat.v); have eala_afterT := eala_afterV.activate (ActivationKey.template SemiticTemplate.XaYYaZ); have bi_afterV := dwr_sel_XaYaZ.activate (ActivationKey.cat Minimalist.Cat.v); have bi_afterT := bi_afterV.activate (ActivationKey.template SemiticTemplate.XaYYaZ); eala_afterT.status = Minimalist.FeatureStatus.active ∧ eala_afterT.selectedP = SemiticPrep.Eala ∧ bi_afterT.status = Minimalist.FeatureStatus.inactive ∧ some eala_afterT.selectedP = lSelect RootLabel.dwr SemiticTemplate.XaYYaZ

Derivation of ex. (25): dawwar Eala 'made encircle'. Same root, different template → different feature activated. Now XaYYaZ strips .template .XaYYaZ from the Eala feature (match!), but NOT from the bi: feature (.template .XaYaZ ≠ .template .XaYYaZ).

def Hewett2026.monoEventiveCausative :

List Minimalist.VerbHead

XaYYaZ causatives are mono-eventive: they don't license conflicting temporal adverbials (Nie 2020). If XaYYaZ were bi-eventive (containing a syntactically represented causing event), we'd expect multiple temporal adverbials to modify distinct subevents. The prediction is not borne out (p. 204, fn 11).

Formally: XaYYaZ's decomposition lacks vGO — it is [vDO, vCAUSE, vBE], a direct causation structure without a separate becoming subevent. This contrasts with analytic causatives that have the full [vDO, vCAUSE, vGO, vBE] decomposition.

Equations

Hewett2026.monoEventiveCausative = [Minimalist.VerbHead.vDO, Minimalist.VerbHead.vCAUSE, Minimalist.VerbHead.vBE]

Instances For

theorem Hewett2026.mono_eventive_has_cause_no_go :

monoEventiveCausative.contains Minimalist.VerbHead.vCAUSE = true ∧ monoEventiveCausative.contains Minimalist.VerbHead.vGO = false

Mono-eventive causatives have CAUSE but lack GO.

theorem Hewett2026.mono_eventive_not_standard_causative :

Minimalist.isCausative monoEventiveCausative = false

Mono-eventive causatives are NOT classified as standard causatives (which require vGO for the becoming subevent).

def Hewett2026.biEventiveCausative :

List Minimalist.VerbHead

The full bi-eventive causative decomposition from Voice.lean.

Equations

Hewett2026.biEventiveCausative = [Minimalist.VerbHead.vDO, Minimalist.VerbHead.vCAUSE, Minimalist.VerbHead.vGO, Minimalist.VerbHead.vBE]

Instances For

theorem Hewett2026.bi_eventive_is_causative :

Minimalist.isCausative biEventiveCausative = true

Bi-eventive causatives ARE standard causatives.

theorem Hewett2026.joint_selection :

(∃ (r : RootLabel), isTemplateDependent r = true) ∧ ∃ (r : RootLabel), isTemplateDependent r = false

Main result: l-selection is a function of root AND template jointly. Neither root alone (@cite{harley-2014}) nor categorizer alone (@cite{merchant-2019}) determines l-selection.

theorem Hewett2026.selection_factors :

(∀ (r : RootClassification) (c1 c2 : Morphology.DM.Categorizer), { root := r, categorizer := c1 }.root.arity = { root := r, categorizer := c2 }.root.arity) ∧ ∃ (r : RootLabel), ¬templateInvariant r

Harley's root-level account of ARITY (c-selection) is correct. His root-level account of L-SELECTION is not. The two types of selection factor differently in the grammar.

theorem Hewett2026.activation_matches_lSelect_dwr :

have bi := (dwr_sel_XaYaZ.activate (ActivationKey.cat Minimalist.Cat.v)).activate (ActivationKey.template SemiticTemplate.XaYaZ); have eala := (dwr_sel_XaYYaZ.activate (ActivationKey.cat Minimalist.Cat.v)).activate (ActivationKey.template SemiticTemplate.XaYYaZ); bi.selectedP = SemiticPrep.bi ∧ some SemiticPrep.bi = lSelect RootLabel.dwr SemiticTemplate.XaYaZ ∧ eala.selectedP = SemiticPrep.Eala ∧ some SemiticPrep.Eala = lSelect RootLabel.dwr SemiticTemplate.XaYYaZ

The activation mechanism produces the correct l-selected P for every root with data in both templates. Matching activation ensures only the correct feature activates in each template environment.