Verbal Templates Can Influence L-Selection in Semitic

Formalization of [Hew26] (Linguistic Inquiry 57(1), 197–215): l-selection — which preposition heads a verb's PP complement — varies by verbal template (binyan) in Tunisian Arabic, Syrian Arabic, and Hebrew. Neither the consonantal root nor the categorizing head varies across templates, so the data are problematic for root-based selection ([Har14b]) and categorizer-based selection ([Mer19a]) alike. Hewett's solution is joint selection via Activate (ex. (23), adapted from [Mer15]): a root's selectional feature is indexed by an ordered tuple of category features — for Semitic (V, Template) — and each c-commanding head strips one index; the feature determines the l-selected P only once fully activated.

Main declarations

• SemiticTemplate, lSelect: the binyan inventory and l-selection as a joint function of root and template.
• lSelData, lSelect_consistent: the paper's attested data (exx. (11)–(18)) and the proof that lSelect matches every datum.
• templateInvariant: the invariance prediction shared by root-only and categorizer-only accounts; refuted by krh_not_templateInvariant, dwr_not_templateInvariant, Hkm_not_templateInvariant.
• SelectionalFeature: an l-selectional feature indexed by an ActivationIndex, with the paper's worked derivations (exx. (24)–(25)).

Implementation notes

The Voice typing (SemiticTemplate.toVoiceHead), the bridges to [Kra96], [Woo15], and [Pyl08], and the verbal-decomposition rendering of mono-eventivity (fn. 11, [Nie20]) are this formalization's connections to the linglib Voice substrate, not claims of [Hew26], which deliberately leaves the template-head inventory open (fn. 8; p. 201: templates realize "a head or series of heads capable of inducing changes in adicity, presumably v/Voice"). Likewise the Mirror-Principle observation (templates_outside_mirror_scope): [Bak85] scopes the Mirror Principle to concatenative morphology, so templatic l-selection sits outside it — a linglib cross-reference Hewett does not draw.

Semitic verbal templates (binyanim)

inductive Hewett2026.SemiticTemplate : Type

Semitic verbal templates (binyanim) attested in the paper's l-selection data. Realized as nonconcatenative vocalic patterns on consonantal roots (for the phonological CV-skeleton view see the template infrastructure in Studies/Faust2026.lean); syntactically they realize functional heads above the root.

• XaYaZ : SemiticTemplate
• XaYYaZ : SemiticTemplate
• nXaYaZ : SemiticTemplate
• tXaYYaZ : SemiticTemplate
• hiXYiZ : SemiticTemplate
• huXYaZ : SemiticTemplate
• XiYeZ : SemiticTemplate
• XuYaZ : SemiticTemplate

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

def Hewett2026.SemiticTemplate.toVoiceHead : SemiticTemplate → Minimalist.VoiceHead

Map each template to a canonical Voice head. Formalizer's bridge into the linglib Voice substrate: [Hew26] assumes only that templates realize a head or series of heads capable of inducing changes in adicity, presumably v/Voice (p. 201), and deliberately leaves the inventory open (fn. 8); the mapping below follows the templates' traditional active, causative, and medio-passive glosses.

Equations

• Hewett2026.SemiticTemplate.XaYaZ.toVoiceHead = Minimalist.voiceAgent
• Hewett2026.SemiticTemplate.XaYYaZ.toVoiceHead = Minimalist.voiceCauser
• Hewett2026.SemiticTemplate.hiXYiZ.toVoiceHead = Minimalist.voiceCauser
• Hewett2026.SemiticTemplate.XiYeZ.toVoiceHead = Minimalist.voiceCauser
• Hewett2026.SemiticTemplate.nXaYaZ.toVoiceHead = Minimalist.voicePassive
• Hewett2026.SemiticTemplate.huXYaZ.toVoiceHead = Minimalist.voicePassive
• Hewett2026.SemiticTemplate.XuYaZ.toVoiceHead = Minimalist.voicePassive
• Hewett2026.SemiticTemplate.tXaYYaZ.toVoiceHead = Minimalist.voiceAnticausative

def Hewett2026.SemiticTemplate.toVoiceFlavor (t : SemiticTemplate) : Minimalist.VoiceFlavor

The Voice flavor a template realizes, derived from toVoiceHead.

Equations

• t.toVoiceFlavor = t.toVoiceHead.flavor

theorem Hewett2026.templates_outside_mirror_scope : ¬Morphology.MirrorPrinciple.MorphDomain.nonconcatenative.InScope

Templates are nonconcatenative, hence outside the Mirror Principle's scope as formalized by [Bak85]'s MorphDomain.InScope — a linglib cross-reference; [Hew26] does not discuss the Mirror Principle.

Roots and prepositions

inductive Hewett2026.RootLabel : Type

Consonantal roots with attested l-selection data, transliterated to ASCII-safe identifiers.

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

@[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 : Repr RootLabel

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✝

inductive Hewett2026.SemiticPrep : Type

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

• fi : SemiticPrep
• bi : SemiticPrep
• Eala : SemiticPrep
• min : SemiticPrep
• Ealej : SemiticPrep
• be : SemiticPrep
• al : SemiticPrep

@[implicit_reducible]

instance Hewett2026.instDecidableEqSemiticPrep : DecidableEq SemiticPrep

Equations

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

def Hewett2026.instReprSemiticPrep.repr : SemiticPrep → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Hewett2026.instReprSemiticPrep : Repr SemiticPrep

Equations

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

inductive Hewett2026.SemiticLang : Type

Languages providing l-selection data in the paper.

• tunisianArabic : SemiticLang
• syrianArabic : SemiticLang
• hebrew : SemiticLang

@[implicit_reducible]

instance Hewett2026.instDecidableEqSemiticLang : DecidableEq SemiticLang

Equations

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

@[implicit_reducible]

instance Hewett2026.instReprSemiticLang : Repr SemiticLang

Equations

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

def Hewett2026.instReprSemiticLang.repr : SemiticLang → ℕ → Std.Format

Equations

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

L-selection data

structure Hewett2026.LSelDatum : Type

An l-selection datum: a root in a template selects a preposition, or none (bare transitive use or passive P-suppression).

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

@[implicit_reducible]

instance Hewett2026.instReprLSelDatum : Repr LSelDatum

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.

def Hewett2026.xwf_XaYaZ : LSelDatum

Template-independent l-selection (ex. (11)): xwf 'fear' selects min 'from' in both XaYaZ (xa:f min l-ʔasad 'He was afraid of the lion') and XaYYaZ (xawwəf-u min l-ʔasad 'He made him afraid of the lion').

Equations

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

def Hewett2026.xwf_XaYYaZ : LSelDatum

See xwf_XaYaZ.

Equations

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

def Hewett2026.krh_XaYaZ : LSelDatum

Template-dependent l-selection (ex. (13a)): krh 'hate' is bare transitive in XaYaZ (kraht (*fi) Sami 'I hate Sami') but requires fi in XaYYaZ (karraht-ha *(fi) Sami 'I made her hate Sami').

Equations

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

def Hewett2026.krh_XaYYaZ : LSelDatum

See krh_XaYaZ.

Equations

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

def Hewett2026.dwr_XaYaZ : LSelDatum

Template-dependent l-selection (ex. (13b)): dwr 'encircle' selects bi: in XaYaZ (l-hnaʃ da:r bi:-k 'The snake encircled you') but ʕla in XaYYaZ (dawwart l-hnaʃ ʕli:-k 'I made the snake encircle you').

Equations

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

def Hewett2026.dwr_XaYYaZ : LSelDatum

See dwr_XaYaZ.

Equations

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

def Hewett2026.Hkm_XaYaZ : LSelDatum

Direction-reversing case (ex. (14), Syrian Arabic): ħkm selects ʕalej in XaYaZ (hakam ʕalej-o b-s-sidʒn 'He sentenced him to jail') but rejects any PP in XaYYaZ (hakkam (l-muba:re:t) 'He refereed (the match)').

Equations

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

def Hewett2026.Hkm_XaYYaZ : LSelDatum

See Hkm_XaYaZ.

Equations

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

def Hewett2026.tpl_XiYeZ : LSelDatum

Hebrew P-suppression (ex. (17)): tpl 'treat' selects be in XiYeZ (tipel be-) and suppresses it in the passive XuYaZ (tupal).

Equations

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

def Hewett2026.tpl_XuYaZ : LSelDatum

See tpl_XiYeZ.

Equations

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

def Hewett2026.shps_hiXYiZ : LSelDatum

Hebrew P-suppression (ex. (18)): ʃpʕ 'influence' selects al in hiXYiZ (hišpia al) and suppresses it in the passive huXYaZ (hušpa).

Equations

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

def Hewett2026.shps_huXYaZ : LSelDatum

See shps_hiXYiZ.

Equations

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

def Hewett2026.lSelData : List LSelDatum

The pooled l-selection data (exx. (11), (13), (14), (17), (18)).

Equations

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

Joint selection

def Hewett2026.lSelect : RootLabel → SemiticTemplate → Option SemiticPrep

L-selection as a joint function of root and template — the paper's core claim. none marks bare transitive use or passive P-suppression; unattested root–template pairs also map to none. xwf is generalized to all templates per the paper's claim that its l-selection is stable across templatic realizations of the root (p. 202).

Equations

• Hewett2026.lSelect Hewett2026.RootLabel.xwf x✝ = some Hewett2026.SemiticPrep.min
• Hewett2026.lSelect Hewett2026.RootLabel.krh Hewett2026.SemiticTemplate.XaYaZ = none
• Hewett2026.lSelect Hewett2026.RootLabel.krh Hewett2026.SemiticTemplate.XaYYaZ = some Hewett2026.SemiticPrep.fi
• Hewett2026.lSelect Hewett2026.RootLabel.dwr Hewett2026.SemiticTemplate.XaYaZ = some Hewett2026.SemiticPrep.bi
• Hewett2026.lSelect Hewett2026.RootLabel.dwr Hewett2026.SemiticTemplate.XaYYaZ = some Hewett2026.SemiticPrep.Eala
• Hewett2026.lSelect Hewett2026.RootLabel.Hkm Hewett2026.SemiticTemplate.XaYaZ = some Hewett2026.SemiticPrep.Ealej
• Hewett2026.lSelect Hewett2026.RootLabel.Hkm Hewett2026.SemiticTemplate.XaYYaZ = none
• Hewett2026.lSelect Hewett2026.RootLabel.tpl Hewett2026.SemiticTemplate.XiYeZ = some Hewett2026.SemiticPrep.be
• Hewett2026.lSelect Hewett2026.RootLabel.tpl Hewett2026.SemiticTemplate.XuYaZ = none
• Hewett2026.lSelect Hewett2026.RootLabel.shps Hewett2026.SemiticTemplate.hiXYiZ = some Hewett2026.SemiticPrep.al
• Hewett2026.lSelect Hewett2026.RootLabel.shps Hewett2026.SemiticTemplate.huXYaZ = none
• Hewett2026.lSelect x✝¹ x✝ = none

theorem Hewett2026.lSelect_consistent (d : LSelDatum) : d ∈ lSelData → lSelect d.root d.template = d.prep

lSelect agrees with every attested datum.

Template-(in)dependence

templateInvariant is the prediction shared by root-only ([Har14b]) and categorizer-only ([Mer19a]) selection: since neither root nor categorizer varies across templates, l-selection should not either. The attested counterexamples refute it; xwf shows the invariant case also exists.

Template-dependence cannot be reduced to homophonous roots (krh₁ in XaYaZ, krh₂ in XaYYaZ): that would leave their mutually exclusive distribution unexplained, parallel to the nonoverlapping distribution of suppletive go ~ went (p. 208). RootLabel accordingly carries a single krh constructor.

def Hewett2026.templateInvariant (r : RootLabel) : Prop

L-selection for root r is constant across templates — the prediction both root-only and categorizer-only accounts make.

Equations

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

theorem Hewett2026.xwf_templateInvariant : templateInvariant RootLabel.xwf

xwf 'fear' is template-independent: min in every template (ex. (11)).

theorem Hewett2026.krh_not_templateInvariant : ¬templateInvariant RootLabel.krh

krh 'hate' refutes template-invariance: bare transitive in XaYaZ but fi in XaYYaZ (ex. (13a)) — the counterexample to [Har14b]'s root-level l-selection.

theorem Hewett2026.dwr_not_templateInvariant : ¬templateInvariant RootLabel.dwr

dwr 'encircle' refutes template-invariance with two distinct prepositions: bi: in XaYaZ vs ʕla in XaYYaZ (ex. (13b)) — an independent counterexample to [Mer19a]'s categorizer-level l-selection.

theorem Hewett2026.Hkm_not_templateInvariant : ¬templateInvariant RootLabel.Hkm

ħkm refutes template-invariance in the reverse direction: PP in XaYaZ, none in XaYYaZ (ex. (14)).

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 ([Har14b]; see complement_selection_at_root_level in Categorizer.lean) but l-selection is not: the two kinds of selection factor differently in the grammar.

Verbalized roots

structure Hewett2026.VerbalizedRoot : Type

A root that has been categorized as a verb and placed in a template — the structure that jointly determines l-selection. Bridges CategorizedRoot (categorizer side) and the template's Voice contribution.

• categorized : Morphology.DM.CategorizedRoot

  The root with its categorizer.

• template : SemiticTemplate

  The Semitic template (functional head bundle).

• rootLabel : RootLabel

  The root label for l-selection lookup.

def Hewett2026.instReprVerbalizedRoot.repr : VerbalizedRoot → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Hewett2026.instReprVerbalizedRoot : Repr VerbalizedRoot

Equations

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

def Hewett2026.VerbalizedRoot.lSelectedP (vr : VerbalizedRoot) : Option SemiticPrep

The l-selected preposition, derived from root and template.

Equations

• vr.lSelectedP = Hewett2026.lSelect vr.rootLabel vr.template

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

The Voice flavor, determined by the template rather than the root.

Equations

• vr.voiceFlavor = vr.template.toVoiceFlavor

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), unlike l-selection: c-selection and l-selection factor differently in the grammar.

Template-to-Voice correspondence

Formalizer's bridge (see the module docstring): the template determines the Voice head merged above the verbalized root, and that functional structure — above the selectional domain — is what varies across templates while root and categorizer stay fixed.

theorem Hewett2026.active_template_assigns_theta : SemiticTemplate.XaYaZ.toVoiceHead.AssignsTheta

The basic active template maps to θ-assigning (agentive) Voice.

theorem Hewett2026.causer_template_assigns_theta : SemiticTemplate.XaYYaZ.toVoiceHead.AssignsTheta

Causative templates map to θ-assigning (causer) Voice.

theorem Hewett2026.passive_template_no_theta : ¬SemiticTemplate.huXYaZ.toVoiceHead.AssignsTheta

Passive templates map to non-θ-assigning Voice — the structural basis for Hebrew P-suppression under passivization (exx. (17b), (18b)).

theorem Hewett2026.voice_distinguishes_templates : SemiticTemplate.XaYaZ.toVoiceFlavor ≠ SemiticTemplate.XaYYaZ.toVoiceFlavor

XaYaZ and XaYYaZ differ in Voice contribution (agentive vs causer): the functional structure above the selectional domain varies even when root and categorizer do not.

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

[Kra96]'s severing instantiated for Semitic: root-level arity is template-invariant while the Voice contribution varies by template.

Cross-linguistic Voice coverage

Formalizer's bridge, not content of [Hew26] (which cites [Woo15] only in passing, as a language where Voice is overt): Semitic templates and Icelandic -st relate to Voice differently. Each Semitic template realizes a single Voice flavor (including the θ-assigning ones); -st is a clitic that merely co-occurs with a Voice flavor without realizing it ([Woo15]). Read as coverage sets over VoiceFlavor, the Semitic image and the set of flavors -st appears with overlap on the non-thematic and agentive flavors (the latter because -st appears in agentive figure reflexives) but diverge elsewhere. The Icelandic set is derived from [Woo15]'s Construction.voiceFlavor, so the theorem relates the two studies' actual mappings.

def Hewett2026.semiticVoiceFlavors : List Minimalist.VoiceFlavor

The Voice flavors Semitic templates realize: the image of toVoiceFlavor.

Equations

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

theorem Hewett2026.template_flavors_in_coverage (t : SemiticTemplate) : t.toVoiceFlavor ∈ semiticVoiceFlavors

Every template's flavor is in the Semitic coverage set.

def Hewett2026.icelandicStFlavors : List Minimalist.VoiceFlavor

The host-clause Voice flavors Icelandic -st co-occurs with, derived from [Woo15]'s Construction.voiceFlavor.

Equations

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

theorem Hewett2026.stType_flavors_in_coverage (st : Wood2015.Construction) : st.voiceFlavor ∈ icelandicStFlavors

Every -st configuration's flavor is in the Icelandic coverage set (inherent and reciprocal reuse flavors of the four representatives).

theorem Hewett2026.voice_coverage_complementary : Minimalist.VoiceFlavor.nonThematic ∈ semiticVoiceFlavors ∧ Minimalist.VoiceFlavor.nonThematic ∈ icelandicStFlavors ∧ Minimalist.VoiceFlavor.agentive ∈ semiticVoiceFlavors ∧ Minimalist.VoiceFlavor.agentive ∈ icelandicStFlavors ∧ Minimalist.VoiceFlavor.causer ∉ icelandicStFlavors ∧ Minimalist.VoiceFlavor.passive ∉ icelandicStFlavors ∧ Minimalist.VoiceFlavor.expletive ∈ icelandicStFlavors ∧ Minimalist.VoiceFlavor.expletive ∉ semiticVoiceFlavors

The two coverage sets overlap on .nonThematic (Semitic medio-passive, Icelandic anticausative -st) and .agentive (Semitic active templates, Icelandic figure reflexives — -st co-occurs with agentive Voice); Semitic alone realizes the causer and passive flavors, Icelandic -st alone appears with the expletive Voice of the generic middle.

theorem Hewett2026.causative_alternation_parallel : SemiticTemplate.XaYaZ.toVoiceHead.AssignsTheta ∧ ¬SemiticTemplate.tXaYYaZ.toVoiceHead.AssignsTheta

The Semitic XaYaZ ~ tXaYYaZ alternation instantiates [Kra96]'s causative alternation: toVoiceHead maps the two templates to the canonical heads, so the Semitic statement is Kratzer1996.causative_pair_voice_contrast.

Template → Voice → applicative licensing

Formalizer's bridge to [Pyl08] (not cited by [Hew26]): high applicatives require Voice with event semantics, low applicatives are unconditional. Pulled back along toVoiceHead, the Voice-predicate chain assignsTheta ⊂ hasSemantics = licenses high Appl ⊂ licenses low Appl = ⊤ yields: +θ templates ⊊ high-Appl-licensing templates ⊊ all templates. The general inclusions live in the substrate (VoiceHead.AssignsTheta.hasSemantics, high_licensed_of_assignsTheta, low_licensed_with_any); this section instantiates them for the Semitic template space, paralleling the Icelandic asymmetry in Wood2015.dative_voice_asymmetry.

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

Does this template license a given applicative type? Composes the substrate's ApplHead.Licensed with toVoiceHead.

Equations

• t.licensesAppl appl = appl.Licensed t.toVoiceHead

@[implicit_reducible]

instance Hewett2026.instDecidableLicensesAppl (t : SemiticTemplate) (appl : Minimalist.ApplHead) : Decidable (t.licensesAppl appl)

Equations

• Hewett2026.instDecidableLicensesAppl t appl = Hewett2026.instDecidableLicensesAppl._aux_1 t appl

theorem Hewett2026.high_appl_iff_hasSemantics (t : SemiticTemplate) : t.licensesAppl Minimalist.applHigh ↔ t.toVoiceHead.HasSemantics

High-Appl licensing factors through HasSemantics.

theorem Hewett2026.high_appl_blocked_implies_no_theta (t : SemiticTemplate) (h : ¬t.licensesAppl Minimalist.applHigh) : ¬t.toVoiceHead.AssignsTheta

A template that blocks high applicatives assigns no θ — via the substrate implication, not template enumeration.

theorem Hewett2026.theta_licenses_all_appl (t : SemiticTemplate) (appl : Minimalist.ApplHead) (hθ : t.toVoiceHead.AssignsTheta) : t.licensesAppl appl

A θ-assigning template licenses every applicative type.

theorem Hewett2026.voice_predicate_chain : (∀ (t : SemiticTemplate), t.toVoiceHead.AssignsTheta → t.licensesAppl Minimalist.applHigh) ∧ (∃ (t : SemiticTemplate), t.licensesAppl Minimalist.applHigh ∧ ¬t.toVoiceHead.AssignsTheta) ∧ (∀ (t : SemiticTemplate), t.licensesAppl Minimalist.applHigh → t.licensesAppl Minimalist.applLowRecipient) ∧ ∃ (t : SemiticTemplate), ¬t.licensesAppl Minimalist.applHigh

The Voice-predicate chain pulled back to the Semitic template space; both inclusions are strict: nXaYaZ licenses high Appl without assigning θ, and tXaYYaZ blocks high Appl.

Feature activation

[Hew26] ex. (23) (adapted from [Mer15]): Activate(X,Y;F) — X bears a category feature c; Y bears an inactive feature F^C with C = (c₁,...,cₙ) an ordered tuple. If c = c₁, Activate strips c₁; when the tuple is exhausted, F is fully active. For Semitic l-selection the tuple is (V, Template): the categorizing head strips the first index, the template-defining head the second. The tuple machinery is ActivationIndex from Checking.lean.

inductive Hewett2026.ActivationKey : Type

Activation keys for Semitic l-selection: the activation tuple mixes syntactic categories (stripped by the categorizing head) and template identities (stripped by the template-defining head).

• cat : Minimalist.Cat → ActivationKey

  A syntactic category key.

• template : SemiticTemplate → ActivationKey

  A template key.

@[implicit_reducible]

instance Hewett2026.instDecidableEqActivationKey : DecidableEq ActivationKey

Equations

• Hewett2026.instDecidableEqActivationKey = Hewett2026.instDecidableEqActivationKey.decEq

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 ⋯

def Hewett2026.instReprActivationKey.repr : ActivationKey → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Hewett2026.instReprActivationKey : Repr ActivationKey

Equations

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

@[implicit_reducible]

instance Hewett2026.instBEqActivationKey : BEq ActivationKey

BEq via decide so that activation reduces definitionally on concrete keys (ActivationIndex requires [BEq α]).

Equations

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

instance Hewett2026.instLawfulBEqActivationKey : LawfulBEq ActivationKey

structure Hewett2026.SelectionalFeature : Type

A selectional feature indexed by an ordered activation tuple ([Hew26] ex. (23)): selectedP becomes visible to selection only once activation is exhausted.

• selectedP : SemiticPrep

  The preposition selected when fully activated.

• activation : Minimalist.ActivationIndex ActivationKey

  Ordered activation tuple; empty = fully active.

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

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

The feature's lifecycle status, via ActivationIndex.toStatus.

Equations

• sf.status = sf.activation.toStatus

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

Attempt to activate with the given key (matching left-to-right stripping, via ActivationIndex.activate).

Equations

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

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] } }

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: ex. (23) strips only when the key matches the leftmost index.

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.

Worked derivation (exx. (24)–(25))

def Hewett2026.dwr_sel_XaYaZ : SelectionalFeature

The root dwr carries one selectional feature per template pairing ([Hew26] exx. (24)–(25)): [SEL: bi^(V, XaYaZ)] selects bi: when activated by V and XaYaZ.

Equations

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

def Hewett2026.dwr_sel_XaYYaZ : SelectionalFeature

[SEL: ʕla^(V, XaYYaZ)] selects ʕla when activated by V and XaYYaZ.

Equations

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

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

Ex. (24), dar b- 'encircled': V strips .cat .v from both features; XaYaZ then strips the template key from the bi: feature only (template mismatch leaves the ʕla feature inactive), and the active feature matches lSelect.

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

Ex. (25), dawwər ʕla 'made encircle': same root, different template — XaYYaZ activates the ʕla feature and leaves the bi: feature inactive.

Mono-eventive causatives

Fn. 11 (p. 204): XaYYaZ causatives reject conflicting temporal adverbials, which [Hew26] takes to show they are mono-eventive, assuming with [Nie20] that morphological causatives are crosslinguistically mono-eventive. The decompositions below render this in the local VerbHead substrate — the formalizer's encoding, not the paper's ([Nie20]'s own analysis is Voice-over-Voice, not a subevent inventory).

def Hewett2026.monoEventiveCausative : List Minimalist.VerbHead

Mono-eventive causative decomposition: θ-assigning Voice over a root structure lacking the becoming subevent vGO.

Equations

• Hewett2026.monoEventiveCausative = Minimalist.buildDecomposition Minimalist.voiceCauser [Minimalist.VerbHead.vCAUSE, Minimalist.VerbHead.vBE]

def Hewett2026.biEventiveCausative : List Minimalist.VerbHead

Bi-eventive causative decomposition (analytic causatives): θ-assigning Voice over the full change-of-state root structure.

Equations

• Hewett2026.biEventiveCausative = Minimalist.buildDecomposition Minimalist.voiceCauser [Minimalist.VerbHead.vCAUSE, Minimalist.VerbHead.vGO, Minimalist.VerbHead.vBE]

theorem Hewett2026.mono_eventive_has_cause_no_go : Minimalist.VerbHead.vCAUSE ∈ monoEventiveCausative ∧ Minimalist.VerbHead.vGO ∉ monoEventiveCausative

Mono-eventive causatives have CAUSE but lack GO.

theorem Hewett2026.mono_eventive_not_standard_causative : Minimalist.isCausative monoEventiveCausative = false

Mono-eventive causatives are not standard causatives (which require the vGO becoming subevent).

theorem Hewett2026.bi_eventive_is_causative : Minimalist.isCausative biEventiveCausative = true

Bi-eventive causatives are standard causatives.

Summary

theorem Hewett2026.joint_selection : (∃ (r : RootLabel), ¬templateInvariant r) ∧ ∃ (r : RootLabel), templateInvariant r

Main result: l-selection is a function of root and template jointly — template-dependent and template-independent roots both exist, so neither root alone ([Har14b]) nor categorizer alone ([Mer19a]) determines it.