Voice Head Flavors

[Cho01] [Coo19] [Cue03] [Har14b] [Kra96] [Leg03] [MSK25] [Sch08a] [Sil12] [Woo15]

Voice heads introduce (or fail to introduce) external arguments ([Kra96]).

Main definitions

• Flavor — the guise typology (after [Sch08a]), with projections onto neighboring substrates: alternation ([Cre25] coding-frame operation), thetaRole, defaultPhasal, recipFormation ([Sil12]).
• Head — a flavor plus featural and per-construction properties, with the predicate API IsPhasal/AssignsTheta/HasSemantics.
• buildDecomposition — the Voice–VerbHead bridge: Voice contributes vDO when it assigns θ; CAUSE belongs to the root ([Cue03], [Pyl08]).
• Params + Flavor.toParams — the ±D/±λx parametric decomposition ([AAS15]); ProjectionLocus — which projection an exponent spells out.

Implementation notes

[Woo15] uses a single v head whose interpretation introduces CAUSE; the multi-headed decomposition here follows [Cue03] and captures the same Voice–CAUSE independence. See Wood2015 for the Icelandic -st apparatus.

Flavors

inductive Minimalist.Voice.Flavor : Type

Typology of Voice head flavors (after [Sch08a]).

• agentive : Flavor

  Introduces an agent external argument ([Kra96] Voice_AG).

• causer : Flavor

  Introduces a causer ([Sch08a] Voice_CAUSE).

• nonThematic : Flavor

  Semantically vacuous, no θ-role, [D] for PF marking (Romance anticausative SE, Chuj -j; [MP26]).

• expletive : Flavor

  No specifier, no semantics (dispositional middles).

• impersonal : Flavor

  Demotes the agent to an implicit generic human (Finnish "passive").

• passive : Flavor

  Checks Case but does not assign θ ([Col05]: by heads VoiceP).

• antipassive : Flavor

  Introduces an agent with absolutive (not ergative) case; demotes the object to oblique ([Sco23]).

• reflexive : Flavor

  [+θ, +D]: agent binds the internal argument (Romance se; [MSK25]).

• reciprocal : Flavor

  [+θ, +D]: agent in the mutual relation with the internal argument — [Sil12]'s syntactic reciprocalization (Romance/Slavic reciprocal se).

• experiencer : Flavor

  [+θ, +D]: introduces an experiencer external argument (psych causatives).

@[instance_reducible]

instance Minimalist.Voice.instDecidableEqFlavor : DecidableEq Flavor

Equations

• Minimalist.Voice.instDecidableEqFlavor x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Minimalist.Voice.instReprFlavor.repr : Flavor → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Minimalist.Voice.instReprFlavor : Repr Flavor

Equations

• Minimalist.Voice.instReprFlavor = { reprPrec := Minimalist.Voice.instReprFlavor.repr }

Flavor projections

def Minimalist.Voice.Flavor.alternation : Flavor → Option Voice.ValencyAlternation

The [Cre25] valency alternation each flavor realizes; none when the coding frame is untouched or the effect is not a valency operation.

Equations

• Minimalist.Voice.Flavor.causer.alternation = some Voice.causativization
• Minimalist.Voice.Flavor.nonThematic.alternation = some Voice.decausativization
• Minimalist.Voice.Flavor.impersonal.alternation = some Voice.iPassivization
• Minimalist.Voice.Flavor.passive.alternation = some Voice.passivization
• Minimalist.Voice.Flavor.antipassive.alternation = some Voice.antipassivization
• Minimalist.Voice.Flavor.reflexive.alternation = some Voice.reflexivization
• Minimalist.Voice.Flavor.reciprocal.alternation = some Voice.reciprocalization
• Minimalist.Voice.Flavor.agentive.alternation = none
• Minimalist.Voice.Flavor.expletive.alternation = none
• Minimalist.Voice.Flavor.experiencer.alternation = none

def Minimalist.Voice.Flavor.thetaRole : Flavor → Option ThetaRole

The external θ-role a flavor assigns ([Kra96] severing). ThetaRole has no dedicated causer, so causer Voice maps to stimulus, its closest interface role.

Equations

• Minimalist.Voice.Flavor.agentive.thetaRole = some ThetaRole.agent
• Minimalist.Voice.Flavor.causer.thetaRole = some ThetaRole.stimulus
• Minimalist.Voice.Flavor.antipassive.thetaRole = some ThetaRole.agent
• Minimalist.Voice.Flavor.reflexive.thetaRole = some ThetaRole.agent
• Minimalist.Voice.Flavor.reciprocal.thetaRole = some ThetaRole.agent
• Minimalist.Voice.Flavor.experiencer.thetaRole = some ThetaRole.experiencer
• Minimalist.Voice.Flavor.nonThematic.thetaRole = none
• Minimalist.Voice.Flavor.expletive.thetaRole = none
• Minimalist.Voice.Flavor.impersonal.thetaRole = none
• Minimalist.Voice.Flavor.passive.thetaRole = none

def Minimalist.Voice.Flavor.defaultPhasal : Flavor → Bool

Default phasehood ([Col05]/[Cho01] baseline): θ-assigning, specifier-projecting Voice is phasal — tethered to the parameter grid by defaultPhasal_eq_baselinePhasal, with antipassive the machine-checked exception (antipassive_anomaly); per-construction divergences go via Head.phaseOverride.

Equations

• Minimalist.Voice.Flavor.agentive.defaultPhasal = true
• Minimalist.Voice.Flavor.causer.defaultPhasal = true
• Minimalist.Voice.Flavor.reflexive.defaultPhasal = true
• Minimalist.Voice.Flavor.reciprocal.defaultPhasal = true
• Minimalist.Voice.Flavor.experiencer.defaultPhasal = true
• Minimalist.Voice.Flavor.nonThematic.defaultPhasal = false
• Minimalist.Voice.Flavor.expletive.defaultPhasal = false
• Minimalist.Voice.Flavor.impersonal.defaultPhasal = false
• Minimalist.Voice.Flavor.passive.defaultPhasal = false
• Minimalist.Voice.Flavor.antipassive.defaultPhasal = false

def Minimalist.Voice.Flavor.recipFormation : Flavor → Option Reciprocal.Formation

The [Sil12] formation locus a flavor realizes: reciprocal Voice IS syntactic reciprocalization; no flavor realizes lexical formation.

Equations

• Minimalist.Voice.Flavor.reciprocal.recipFormation = some Reciprocal.Formation.syntactic
• x✝.recipFormation = none

theorem Minimalist.Voice.reciprocal_voice_no_discontinuous : Option.map Reciprocal.Formation.allowsDiscontinuous Flavor.reciprocal.recipFormation = some false

Voice-formed reciprocals license no discontinuous construction ([Sil12] §7: *Jean s'est embrassé avec Marie).

The Voice head

structure Minimalist.Voice.Head : Type

A Voice head: a flavor plus featural and per-construction properties.

• flavor : Flavor

  The flavor determining argument introduction and semantics.

• hasD : Bool

  [D] subcategorization feature: requires a specifier at PF.

• phaseOverride : Option Bool

  Per-construction override of flavor.defaultPhasal — the locus for per-paper divergence ([ES25b] Malayic passive, [CMPP14] Mam Agent Focus).

• checksCase : Bool

  Case-checking ([Col05] p. 96 feature dissociation: passive Voice/by checks Case). Default false.

• features : FeatureBundle

  Agree-relevant features (e.g., [uOblique] for Mam =(y)a'). Default empty.

def Minimalist.Voice.instDecidableEqHead.decEq (x✝ x✝¹ : Head) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Minimalist.Voice.instDecidableEqHead : DecidableEq Head

Equations

• Minimalist.Voice.instDecidableEqHead = Minimalist.Voice.instDecidableEqHead.decEq

@[instance_reducible]

instance Minimalist.Voice.instReprHead : Repr Head

Equations

• Minimalist.Voice.instReprHead = { reprPrec := Minimalist.Voice.instReprHead.repr }

def Minimalist.Voice.instReprHead.repr : Head → ℕ → Std.Format

Equations

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

Predicate API

Prop predicates with Decidable instances; the data fields hasD and checksCase are exposed in Prop form by HasD and ChecksCase.

def Minimalist.Voice.Head.IsPhasal (v : Head) : Prop

Phasal: the per-construction override if present, else the flavor default.

Equations

• v.IsPhasal = (v.phaseOverride.getD v.flavor.defaultPhasal = true)

@[instance_reducible]

instance Minimalist.Voice.instDecidableIsPhasal (v : Head) : Decidable v.IsPhasal

Equations

• Minimalist.Voice.instDecidableIsPhasal v = Minimalist.Voice.instDecidableIsPhasal._aux_1 v

def Minimalist.Voice.Head.AssignsTheta (v : Head) : Prop

Assigns a θ-role to its specifier (flavor.thetaRole.isSome). Narrower than Params.assignsTheta?, which also counts impersonal Voice's ∃-bound implicit agent.

Equations

• v.AssignsTheta = (v.flavor.thetaRole.isSome = true)

@[instance_reducible]

instance Minimalist.Voice.instDecidableAssignsTheta (v : Head) : Decidable v.AssignsTheta

Equations

• Minimalist.Voice.instDecidableAssignsTheta v = Minimalist.Voice.instDecidableAssignsTheta._aux_1 v

theorem Minimalist.Voice.Head.assignsTheta_iff (v : Head) : v.AssignsTheta ↔ v.flavor = Flavor.agentive ∨ v.flavor = Flavor.causer ∨ v.flavor = Flavor.antipassive ∨ v.flavor = Flavor.reflexive ∨ v.flavor = Flavor.reciprocal ∨ v.flavor = Flavor.experiencer

Characterization: exactly the agentive, causer, antipassive, reflexive, reciprocal, and experiencer flavors assign θ.

def Minimalist.Voice.Head.HasSemantics (v : Head) : Prop

Has semantic content — everything except nonThematic (purely PF) and expletive (vacuous middle).

Equations

• v.HasSemantics = (v.flavor ≠ Minimalist.Voice.Flavor.nonThematic ∧ v.flavor ≠ Minimalist.Voice.Flavor.expletive)

@[instance_reducible]

instance Minimalist.Voice.instDecidableHasSemantics (v : Head) : Decidable v.HasSemantics

Equations

• Minimalist.Voice.instDecidableHasSemantics v = id inferInstance

theorem Minimalist.Voice.Head.AssignsTheta.hasSemantics {v : Head} (h : v.AssignsTheta) : v.HasSemantics

θ-assignment entails semantic content. The converse fails — passive Voice has semantics without θ (passive_has_semantics, passive_no_theta).

def Minimalist.Voice.Head.HasD (v : Head) : Prop

Subcategorizes for a specifier (Prop form of hasD).

Equations

• v.HasD = (v.hasD = true)

@[instance_reducible]

instance Minimalist.Voice.instDecidableHasD (v : Head) : Decidable v.HasD

Equations

• Minimalist.Voice.instDecidableHasD v = Minimalist.Voice.instDecidableHasD._aux_1 v

def Minimalist.Voice.Head.ChecksCase (v : Head) : Prop

Checks Case (Prop form of checksCase).

Equations

• v.ChecksCase = (v.checksCase = true)

@[instance_reducible]

instance Minimalist.Voice.instDecidableChecksCase (v : Head) : Decidable v.ChecksCase

Equations

• Minimalist.Voice.instDecidableChecksCase v = Minimalist.Voice.instDecidableChecksCase._aux_1 v

Canonical heads

def Minimalist.Voice.agentive : Head

Agentive Voice (transitive/unergative): introduces an agent, phasal.

Equations

• Minimalist.Voice.agentive = { flavor := Minimalist.Voice.Flavor.agentive, hasD := true }

def Minimalist.Voice.causer : Head

Causer Voice: introduces a causer, phasal.

Equations

• Minimalist.Voice.causer = { flavor := Minimalist.Voice.Flavor.causer, hasD := true }

def Minimalist.Voice.anticausative : Head

Non-thematic Voice (anticausative): no θ-role, [D] for PF marking.

Equations

• Minimalist.Voice.anticausative = { flavor := Minimalist.Voice.Flavor.nonThematic, hasD := true }

def Minimalist.Voice.middle : Head

Expletive Voice (middle): no specifier, no semantics.

Equations

• Minimalist.Voice.middle = { flavor := Minimalist.Voice.Flavor.expletive, hasD := false }

def Minimalist.Voice.impersonal : Head

Impersonal Voice (Finnish "passive"): ∃-closes the agent; no θ-marked specifier.

Equations

• Minimalist.Voice.impersonal = { flavor := Minimalist.Voice.Flavor.impersonal, hasD := false }

def Minimalist.Voice.passive : Head

Passive Voice: by checks Case without assigning θ ([Col05]; v assigns the external θ-role in Spec,vP), and is non-phasal — which keeps PartP accessible for smuggling. Contested by [Leg03].

Equations

• Minimalist.Voice.passive = { flavor := Minimalist.Voice.Flavor.passive, hasD := true, checksCase := true }

def Minimalist.Voice.reflexive : Head

Reflexive Voice: agent coreferent with the internal argument (Romance se, [MSK25]). [Woo15]'s Icelandic -st is a SpecpP clitic, not an exponent of this head.

Equations

• Minimalist.Voice.reflexive = { flavor := Minimalist.Voice.Flavor.reflexive, hasD := true }

def Minimalist.Voice.reciprocal : Head

Reciprocal Voice: agent in the mutual relation with the internal argument — [Sil12]'s syntactic reciprocalization (Romance/Slavic reciprocal se), twin of reflexive. Lexicon-formed reciprocal verbs enter the syntax already symmetric and are not exponents of this head.

Equations

• Minimalist.Voice.reciprocal = { flavor := Minimalist.Voice.Flavor.reciprocal, hasD := true }

def Minimalist.Voice.experiencer : Head

Experiencer Voice: experiencer external argument in Spec,VoiceP. Distinct from [Woo15]'s Icelandic dative-subject experiencers, where Voice is non-thematic and the experiencer an applied dative.

Equations

• Minimalist.Voice.experiencer = { flavor := Minimalist.Voice.Flavor.experiencer, hasD := true }

Verification theorems

theorem Minimalist.Voice.agentive_assigns_theta : agentive.AssignsTheta

Agentive Voice assigns a θ-role.

theorem Minimalist.Voice.nonThematic_no_theta : ¬anticausative.AssignsTheta

Non-thematic Voice does NOT assign a θ-role ([MP26]).

theorem Minimalist.Voice.nonThematic_no_semantics : ¬anticausative.HasSemantics

Non-thematic Voice has no semantic contribution — the core claim of [MP26]: SE is a PF phenomenon.

theorem Minimalist.Voice.agentive_is_phase : agentive.IsPhasal

Agentive Voice is a phase head (v* = Voice_AG).

theorem Minimalist.Voice.anticausative_not_phase : ¬anticausative.IsPhasal

Non-thematic Voice is NOT a phase head.

theorem Minimalist.Voice.impersonal_no_theta : ¬impersonal.AssignsTheta

Impersonal Voice does NOT assign a θ-role (the agent is existentially closed, not projected to a specifier).

theorem Minimalist.Voice.impersonal_has_semantics : impersonal.HasSemantics

Impersonal Voice HAS semantics: existential closure over the agent, unlike vacuous non-thematic Voice.

theorem Minimalist.Voice.passive_no_theta : ¬passive.AssignsTheta

Passive Voice does NOT assign a θ-role (v does).

theorem Minimalist.Voice.passive_not_phase : ¬passive.IsPhasal

Passive Voice is NOT a phase head.

theorem Minimalist.Voice.passive_has_semantics : passive.HasSemantics

Passive Voice HAS semantic content (by mediates Case-checking).

theorem Minimalist.Voice.passive_checks_case : passive.ChecksCase

Passive Voice checks Case ([Col05], p. 96).

theorem Minimalist.Voice.reflexive_assigns_theta : reflexive.AssignsTheta

Reflexive Voice assigns a θ-role ([Woo15]).

theorem Minimalist.Voice.reciprocal_assigns_theta : reciprocal.AssignsTheta

Reciprocal Voice assigns a θ-role ([Sil12]: parasitic assignment gives the subject both roles).

theorem Minimalist.Voice.experiencer_assigns_theta : experiencer.AssignsTheta

Experiencer Voice assigns a θ-role ([Woo15]).

Voice–VerbHead bridge ([Kra96] in [Cue03] terms)

def Minimalist.Voice.buildDecomposition (voice : Head) (rootStructure : List VerbHead) : List VerbHead

The full verbal decomposition: Voice prepends vDO when it assigns θ; the root supplies the lower structure, including vCAUSE for change-of-state roots ([Woo15], [Pyl08]).

Equations

• Minimalist.Voice.buildDecomposition voice rootStructure = if voice.AssignsTheta then Minimalist.VerbHead.vDO :: rootStructure else rootStructure

theorem Minimalist.Voice.theta_voice_prepends_vDO (v : Head) (root : List VerbHead) (h : v.AssignsTheta) : buildDecomposition v root = VerbHead.vDO :: root

θ-assigning Voice prepends vDO to the root structure.

theorem Minimalist.Voice.no_theta_passthrough (v : Head) (root : List VerbHead) (h : ¬v.AssignsTheta) : buildDecomposition v root = root

Non-θ Voice leaves the root structure unchanged.

theorem Minimalist.Voice.agent_plus_change_is_causative : isCausative (buildDecomposition agentive [VerbHead.vCAUSE, VerbHead.vGO, VerbHead.vBE]) = true

Causative pattern: agentive Voice + [vCAUSE, vGO, vBE] is causative.

theorem Minimalist.Voice.nonthematic_plus_change_is_inchoative : isInchoative (buildDecomposition anticausative [VerbHead.vCAUSE, VerbHead.vGO, VerbHead.vBE]) = true

Inchoative pattern: non-thematic Voice + [vCAUSE, vGO, vBE] stays inchoative.

theorem Minimalist.Voice.agent_plus_nothing_is_activity : isActivity (buildDecomposition agentive []) = true

Activity pattern: agentive Voice + [] yields an activity.

theorem Minimalist.Voice.nonthematic_plus_state_is_state : isState (buildDecomposition anticausative [VerbHead.vBE]) = true

State pattern: non-thematic Voice + [vBE] yields a state.

theorem Minimalist.Voice.causative_alternation : isCausative (buildDecomposition agentive [VerbHead.vCAUSE, VerbHead.vGO, VerbHead.vBE]) = true ∧ isInchoative (buildDecomposition anticausative [VerbHead.vCAUSE, VerbHead.vGO, VerbHead.vBE]) = true

The causative alternation: [vCAUSE, vGO, vBE] is causative under agentive Voice, inchoative under non-thematic Voice — only vDO differs.

theorem Minimalist.Voice.voice_determines_causativity (v : Head) : isCausative (buildDecomposition v [VerbHead.vCAUSE, VerbHead.vGO, VerbHead.vBE]) = true ↔ v.AssignsTheta

Voice determines causativity: over the root structure [vCAUSE, vGO, vBE], the result is causative iff Voice assigns θ.

theorem Minimalist.Voice.cause_independent_of_voice : hasCause (buildDecomposition agentive [VerbHead.vCAUSE, VerbHead.vGO, VerbHead.vBE]) = true ∧ hasCause (buildDecomposition anticausative [VerbHead.vCAUSE, VerbHead.vGO, VerbHead.vBE]) = true

CAUSE is present in both causative and anticausative decompositions — the independence claim: CAUSE is part of the root, not Voice.

Feature dissociation ([Col05] §4)

theorem Minimalist.Voice.active_theta_and_case_unified : agentive.AssignsTheta ∧ ¬agentive.ChecksCase

In active, v (= agentive Voice) assigns θ AND controls Case-checking.

theorem Minimalist.Voice.passive_theta_case_dissociated : ¬passive.AssignsTheta ∧ passive.ChecksCase

Passive dissociates them: Voice does NOT assign θ (v does), but Voice DOES check Case.

theorem Minimalist.Voice.utah_active_passive : agentive.HasD ∧ passive.HasD

UTAH: the external-argument position is present in both active and passive.

theorem Minimalist.Voice.passive_no_vDO (root : List VerbHead) : buildDecomposition passive root = root

Passive Voice does not prepend vDO: no θ, so buildDecomposition passes the root structure through unchanged.

Voice–phase bridge

theorem Minimalist.Voice.agentive_voice_is_phase_head : agentive.IsPhasal ∧ causer.IsPhasal

Agentive Voice corresponds to traditional v* (phase head); both agentive and causer Voice are phasal.

theorem Minimalist.Voice.nonthematic_voice_not_phase_head : ¬anticausative.IsPhasal ∧ ¬middle.IsPhasal

Non-thematic and expletive Voice are NOT phase heads.

Parametric decomposition ([AAS15], [Sch17])

inductive Minimalist.Voice.ExternalArgSemantics : Type

How Voice introduces an external argument semantically: [+λx] λ-abstraction (thematicArgument), [+∃x] existential binding (thematicExistential, [Sch17] medio-passive), or none (expletive).

• thematicArgument : ExternalArgSemantics
• thematicExistential : ExternalArgSemantics
• expletive : ExternalArgSemantics

@[instance_reducible]

instance Minimalist.Voice.instDecidableEqExternalArgSemantics : DecidableEq ExternalArgSemantics

Equations

• Minimalist.Voice.instDecidableEqExternalArgSemantics x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Minimalist.Voice.instReprExternalArgSemantics.repr : ExternalArgSemantics → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Minimalist.Voice.instReprExternalArgSemantics : Repr ExternalArgSemantics

Equations

• Minimalist.Voice.instReprExternalArgSemantics = { reprPrec := Minimalist.Voice.instReprExternalArgSemantics.repr }

structure Minimalist.Voice.Params : Type

The ±D/±λx decomposition ([AAS15], [Sch17]); none = underspecified (Indonesian ber- is ⟨none, none⟩, [BU22]).

• selectsSpecifier : Option Bool

  Does Voice select a syntactic specifier (DP)? some true = [+D], some false = [−D], none = underspecified.

• extArgSemantics : Option ExternalArgSemantics

  Does Voice introduce semantic agentivity/causation? none = underspecified.

def Minimalist.Voice.instDecidableEqParams.decEq (x✝ x✝¹ : Params) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Minimalist.Voice.instDecidableEqParams : DecidableEq Params

Equations

• Minimalist.Voice.instDecidableEqParams = Minimalist.Voice.instDecidableEqParams.decEq

def Minimalist.Voice.instReprParams.repr : Params → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Minimalist.Voice.instReprParams : Repr Params

Equations

• Minimalist.Voice.instReprParams = { reprPrec := Minimalist.Voice.instReprParams.repr }

def Minimalist.Voice.Flavor.toParams : Flavor → Params

Map each named flavor to its cell in the ±D/±λx parameter space.

Flavor	±D	±λx	Example
agentive	+D	+λx (arg)	English active
causer	+D	+λx (arg)	Psych causative
antipassive	+D	+λx (arg)	Mayan antipassive
reflexive	+D	+λx (arg)	Icelandic -st reflexive
reciprocal	+D	+λx (arg)	Romance reciprocal se
experiencer	+D	+λx (arg)	Icelandic subject-exp -st
nonThematic	+D	−λx	Romance anticausative SE
expletive	−D	−λx	English dispositional middle
impersonal	−D	+∃x	Finnish impersonal
passive	+D	−λx	English passive (by)

nonThematic and passive occupy the same cell [+D, −λx]; they differ in Case-checking (Head.checksCase), a property of the full Head, not of the parametric decomposition.

Equations

• Minimalist.Voice.Flavor.agentive.toParams = { selectsSpecifier := some true, extArgSemantics := some Minimalist.Voice.ExternalArgSemantics.thematicArgument }
• Minimalist.Voice.Flavor.causer.toParams = { selectsSpecifier := some true, extArgSemantics := some Minimalist.Voice.ExternalArgSemantics.thematicArgument }
• Minimalist.Voice.Flavor.antipassive.toParams = { selectsSpecifier := some true, extArgSemantics := some Minimalist.Voice.ExternalArgSemantics.thematicArgument }
• Minimalist.Voice.Flavor.reflexive.toParams = { selectsSpecifier := some true, extArgSemantics := some Minimalist.Voice.ExternalArgSemantics.thematicArgument }
• Minimalist.Voice.Flavor.reciprocal.toParams = { selectsSpecifier := some true, extArgSemantics := some Minimalist.Voice.ExternalArgSemantics.thematicArgument }
• Minimalist.Voice.Flavor.experiencer.toParams = { selectsSpecifier := some true, extArgSemantics := some Minimalist.Voice.ExternalArgSemantics.thematicArgument }
• Minimalist.Voice.Flavor.nonThematic.toParams = { selectsSpecifier := some true, extArgSemantics := some Minimalist.Voice.ExternalArgSemantics.expletive }
• Minimalist.Voice.Flavor.expletive.toParams = { selectsSpecifier := some false, extArgSemantics := some Minimalist.Voice.ExternalArgSemantics.expletive }
• Minimalist.Voice.Flavor.impersonal.toParams = { selectsSpecifier := some false, extArgSemantics := some Minimalist.Voice.ExternalArgSemantics.thematicExistential }
• Minimalist.Voice.Flavor.passive.toParams = { selectsSpecifier := some true, extArgSemantics := some Minimalist.Voice.ExternalArgSemantics.expletive }

def Minimalist.Voice.Head.params (v : Head) : Params

The parametric decomposition of a Head, derived from its flavor.

Equations

• v.params = v.flavor.toParams

def Minimalist.Voice.Head.DCoherent (v : Head) : Prop

[D]-coherence: the PF [D] feature matches the flavor's specifier selection. All canonical heads satisfy it (canonical_heads_dCoherent); a head may diverge — e.g. a .nonThematic head without SE-type PF marking — and stating the divergence makes it explicit rather than a silent encoding choice.

Equations

• v.DCoherent = ((v.params.selectsSpecifier == some true) = v.hasD)

@[instance_reducible]

instance Minimalist.Voice.instDecidableDCoherent (v : Head) : Decidable v.DCoherent

Equations

• Minimalist.Voice.instDecidableDCoherent v = Minimalist.Voice.instDecidableDCoherent._aux_1 v

theorem Minimalist.Voice.canonical_heads_dCoherent : agentive.DCoherent ∧ causer.DCoherent ∧ anticausative.DCoherent ∧ middle.DCoherent ∧ impersonal.DCoherent ∧ passive.DCoherent ∧ reflexive.DCoherent ∧ reciprocal.DCoherent ∧ experiencer.DCoherent

Every canonical head keeps hasD in sync with its flavor's specifier selection.

def Minimalist.Voice.Params.assignsTheta? (p : Params) : Option Bool

Semantic external-argument presence; none when underspecified. Broader than Head.AssignsTheta — impersonal's ∃-bound agent counts.

Equations

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

def Minimalist.Voice.Params.baselinePhasal (p : Params) : Bool

Baseline phasehood in the parameter grid: a θ-marked specifier ([+D, +λx arg]) makes a phase ([Col05]/[Cho01]).

Equations

• p.baselinePhasal = (p.selectsSpecifier == some true && p.extArgSemantics == some Minimalist.Voice.ExternalArgSemantics.thematicArgument)

def Minimalist.Voice.Params.isCompatibleWith (p q : Params) : Bool

Compatible iff agreeing on all specified dimensions.

Equations

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

def Minimalist.Voice.Params.isFullySpecified (p : Params) : Bool

Is this parameter setting fully specified?

Equations

• p.isFullySpecified = (p.selectsSpecifier.isSome && p.extArgSemantics.isSome)

Parametric bridge theorems

theorem Minimalist.Voice.flavor_params_fully_specified (f : Flavor) : f.toParams.isFullySpecified = true

All named flavors produce fully specified params.

theorem Minimalist.Voice.flavor_params_theta_consistent (f : Flavor) : f.toParams.assignsTheta? = some (match f with | Flavor.agentive => true | Flavor.causer => true | Flavor.antipassive => true | Flavor.reflexive => true | Flavor.reciprocal => true | Flavor.experiencer => true | Flavor.impersonal => true | Flavor.nonThematic => false | Flavor.expletive => false | Flavor.passive => false)

Semantic external-argument presence per flavor: the θ-assigning flavors plus impersonal.

theorem Minimalist.Voice.defaultPhasal_eq_baselinePhasal (f : Flavor) (h : f ≠ Flavor.antipassive) : f.defaultPhasal = f.toParams.baselinePhasal

defaultPhasal agrees with the parametric baseline everywhere except antipassive.

theorem Minimalist.Voice.antipassive_anomaly : Flavor.antipassive.defaultPhasal = false ∧ Flavor.antipassive.toParams.baselinePhasal = true

The antipassive anomaly, machine-checked: antipassive occupies a phasal cell of the grid ([+D, +λx arg]) yet is non-phasal by default — phasehood tracks v* transitivity ([Cho01]), and antipassive detransitivizes (its alternation has derivedTransitive = some false), though reflexive and reciprocal show the residue is not fully derivable from the alternation either.

theorem Minimalist.Voice.thetaRole_isSome_iff (f : Flavor) : f.thetaRole.isSome = true ↔ f.toParams.extArgSemantics = some ExternalArgSemantics.thematicArgument

Grid consistency: a flavor θ-marks its specifier iff its cell is [+λx arg].

theorem Minimalist.Voice.params_compatible_refl (p : Params) : p.isCompatibleWith p = true

Compatibility is reflexive.

theorem Minimalist.Voice.underspecified_compatible_with_all (f : Flavor) : have ber := { selectsSpecifier := none, extArgSemantics := none }; ber.isCompatibleWith f.toParams = true

A fully underspecified Params is compatible with every named flavor — the key property for Indonesian ber- ([BU22]).

Projection locus

inductive Minimalist.Voice.ProjectionLocus : Type

The projection a non-active exponent (Romance se, Icelandic -st, Hebrew hit-) spells out: Voice_{D}, Voice_{∅} ([AAS15], [WM17]), or v itself ([Woo15] on Icelandic -ka). Complement of Params, which parameterizes the head's own settings.

• voiceD : ProjectionLocus

  Voice carrying a [D] feature; projects a specifier ([Woo15] Voice_{D}).

• voiceBare : ProjectionLocus

  Specifierless Voice; no [D] feature ([Woo15] Voice_{∅}).

• voiceDOrBare : ProjectionLocus

  Underspecified: compatible with either voiceD or voiceBare.

• vHead : ProjectionLocus

  Exponent of v, not Voice (e.g., Icelandic -ka per [Woo15]).

@[instance_reducible]

instance Minimalist.Voice.instDecidableEqProjectionLocus : DecidableEq ProjectionLocus

Equations

• Minimalist.Voice.instDecidableEqProjectionLocus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Minimalist.Voice.instReprProjectionLocus : Repr ProjectionLocus

Equations

• Minimalist.Voice.instReprProjectionLocus = { reprPrec := Minimalist.Voice.instReprProjectionLocus.repr }

def Minimalist.Voice.instReprProjectionLocus.repr : ProjectionLocus → ℕ → Std.Format

Equations

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