Voice Head Flavors

@cite{chomsky-2001} @cite{coon-2019} @cite{cuervo-2003} @cite{harley-2014} @cite{kratzer-1996} @cite{legate-2003} @cite{schaefer-2008} @cite{wood-2015}

Voice heads introduce (or fail to introduce) external arguments. The key typology from @cite{schaefer-2008}:

• Agentive: Introduces an agent external argument (@cite{kratzer-1996} Voice_AG)
• Causer: Introduces a causer (@cite{schaefer-2008} Voice_CAUSE)
• NonThematic: Semantically vacuous — no θ-role, but has a [D] feature requiring PF realization (anticausative SE in Romance; Muñoz @cite{munoz-perez-2026})
• Expletive: No specifier, no semantics (middle voice, dispositionals)
• Reflexive: [+θ, +D] with reflexive binding (@cite{wood-2015} Icelandic -st)
• Experiencer: [+θ, +D] introducing experiencer (@cite{wood-2015} subject-exp -st)

Key Claim

Non-thematic Voice contributes no semantics. SE is a PF marker of absent external argument, not a semantic operator. Evidence: SE is optional in Chilean Spanish when Fission produces a syncretic clitic.

Voice–VerbHead Bridge (§§ 5–6)

Voice and VerbHead are both "little-v" but encode different dimensions: Voice determines whether an external argument is introduced; VerbHead decomposes the event structure into subevents.

Following @cite{cuervo-2003} and @cite{pylkkanen-2008}, the CAUSE relation is modeled here as an independent VerbHead in the root's event decomposition — present in both causative and anticausative alternants. Voice contributes vDO (the agent's activity subevent) when it assigns a θ-role, but does NOT contribute the causal relation.

Note: @cite{wood-2015} uses a SINGLE v head whose interpretation introduces CAUSE, rather than @cite{cuervo-2003}'s multi-headed decomposition. The VerbHead decomposition used here is a linglib modeling choice that captures the same Voice–CAUSE independence using @cite{cuervo-2003}'s notation. See Fragments.Icelandic.Predicates for the Icelandic fragment.

inductive Minimalism.VoiceFlavor : Type

Typology of Voice head flavors.

Agentive Voice introduces an agent; causer Voice introduces a causer; non-thematic Voice has no semantics (anticausative SE); expletive Voice has neither specifier nor semantics (middles); passive Voice checks Case without assigning θ (@cite{collins-2005}: by); reflexive Voice introduces agent that binds internal argument (@cite{wood-2015}); experiencer Voice introduces experiencer external argument (@cite{wood-2015}).

• agentive : VoiceFlavor
• causer : VoiceFlavor
• nonThematic : VoiceFlavor
• expletive : VoiceFlavor
• impersonal : VoiceFlavor
• passive : VoiceFlavor
• antipassive : VoiceFlavor
• reflexive : VoiceFlavor
• experiencer : VoiceFlavor

instance Minimalism.instDecidableEqVoiceFlavor : DecidableEq VoiceFlavor

Equations

• Minimalism.instDecidableEqVoiceFlavor x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Minimalism.instBEqVoiceFlavor.beq : VoiceFlavor → VoiceFlavor → Bool

Equations

• Minimalism.instBEqVoiceFlavor.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Minimalism.instBEqVoiceFlavor : BEq VoiceFlavor

Equations

• Minimalism.instBEqVoiceFlavor = { beq := Minimalism.instBEqVoiceFlavor.beq }

def Minimalism.instReprVoiceFlavor.repr : VoiceFlavor → ℕ → Std.Format

Equations

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

instance Minimalism.instReprVoiceFlavor : Repr VoiceFlavor

Equations

• Minimalism.instReprVoiceFlavor = { reprPrec := Minimalism.instReprVoiceFlavor.repr }

structure Minimalism.VoiceHead : Type

A Voice head with its properties.

• flavor : VoiceFlavor

  The flavor determining argument introduction and semantics

• hasD : Bool

  [D] subcategorization feature: requires a specifier at PF

• phaseHead : Bool

  Is this Voice head a phase head? (v* = agentive Voice)

• checksCase : Bool

  Does this Voice head check Case? In active, v checks accusative; in passive, Voice/by checks it (@cite{collins-2005}, p. 96: feature dissociation). Default false — only passive Voice checks Case.

• features : FeatureBundle

  Agree-relevant features on Voice (e.g., [uOblique] for Mam =(y)a'). Default empty — most Voice heads carry no probe features.

instance Minimalism.instDecidableEqVoiceHead : DecidableEq VoiceHead

Equations

• Minimalism.instDecidableEqVoiceHead = Minimalism.instDecidableEqVoiceHead.decEq

def Minimalism.instDecidableEqVoiceHead.decEq (x✝ x✝¹ : VoiceHead) : Decidable (x✝ = x✝¹)

Equations

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

instance Minimalism.instBEqVoiceHead : BEq VoiceHead

Equations

• Minimalism.instBEqVoiceHead = { beq := Minimalism.instBEqVoiceHead.beq }

def Minimalism.instBEqVoiceHead.beq : VoiceHead → VoiceHead → Bool

Equations

• One or more equations did not get rendered due to their size.
• Minimalism.instBEqVoiceHead.beq x✝¹ x✝ = false

def Minimalism.instReprVoiceHead.repr : VoiceHead → ℕ → Std.Format

Equations

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

instance Minimalism.instReprVoiceHead : Repr VoiceHead

Equations

• Minimalism.instReprVoiceHead = { reprPrec := Minimalism.instReprVoiceHead.repr }

def Minimalism.VoiceHead.assignsTheta (v : VoiceHead) : Bool

Does this Voice head introduce a θ-role?

Equations

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

def Minimalism.VoiceHead.hasSemantics (v : VoiceHead) : Bool

Does this Voice head have semantic content?

Equations

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

def Minimalism.voiceAgent : VoiceHead

Agentive Voice (transitive/unergative): introduces agent, is a phase head.

Equations

• Minimalism.voiceAgent = { flavor := Minimalism.VoiceFlavor.agentive, hasD := true, phaseHead := true }

def Minimalism.voiceCauser : VoiceHead

Causer Voice: introduces causer, is a phase head.

Equations

• Minimalism.voiceCauser = { flavor := Minimalism.VoiceFlavor.causer, hasD := true, phaseHead := true }

def Minimalism.voiceAnticausative : VoiceHead

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

Equations

• Minimalism.voiceAnticausative = { flavor := Minimalism.VoiceFlavor.nonThematic, hasD := true, phaseHead := false }

def Minimalism.voiceMiddle : VoiceHead

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

Equations

• Minimalism.voiceMiddle = { flavor := Minimalism.VoiceFlavor.expletive, hasD := false, phaseHead := false }

def Minimalism.voiceImpersonal : VoiceHead

Impersonal Voice (Finnish "passive"): demotes agent to an implicit generic human referent. Has semantics (existential closure over agent) but does not assign a θ-role to a syntactic specifier.

Equations

• Minimalism.voiceImpersonal = { flavor := Minimalism.VoiceFlavor.impersonal, hasD := false, phaseHead := false }

def Minimalism.voicePassive : VoiceHead

Passive Voice: headed by by, checks Case but does not assign a θ-role — v assigns the θ-role to the external argument in Spec,vP. Passive v is NOT a phase head: the Case-checking feature that makes v* a strong phase head has been dissociated onto Voice/by.

This is why PartP (complement of v) remains accessible for smuggling: passive v is a defective v, not v*. Cf. @cite{chomsky-2001}: "only v* (transitive) is a strong phase."

Contested: @cite{legate-2003} argues passive v IS a phase head based on reconstruction and parasitic gap data. The current formalization follows @cite{collins-2005} and @cite{chomsky-2001}.

Equations

• Minimalism.voicePassive = { flavor := Minimalism.VoiceFlavor.passive, hasD := true, phaseHead := false, checksCase := true }

def Minimalism.voiceReflexive : VoiceHead

Reflexive Voice (@cite{wood-2015}): introduces agent that is coreferent with the internal argument. [+θ, +D], phase head (assigns θ). Icelandic -st spells out this Voice in reflexive constructions.

Equations

• Minimalism.voiceReflexive = { flavor := Minimalism.VoiceFlavor.reflexive, hasD := true, phaseHead := true }

def Minimalism.voiceExperiencer : VoiceHead

Experiencer Voice (@cite{wood-2015}): introduces experiencer external argument. [+θ, +D], phase head. Icelandic subject-experiencer -st verbs (e.g., leiðast 'be bored').

Equations

• Minimalism.voiceExperiencer = { flavor := Minimalism.VoiceFlavor.experiencer, hasD := true, phaseHead := true }

theorem Minimalism.agentive_assigns_theta : voiceAgent.assignsTheta = true

Agentive Voice assigns a θ-role.

theorem Minimalism.nonThematic_no_theta : voiceAnticausative.assignsTheta = false

Non-thematic Voice does NOT assign a θ-role (Muñoz Pérez's key claim).

theorem Minimalism.nonThematic_no_semantics : voiceAnticausative.hasSemantics = false

Non-thematic Voice has no semantic contribution. This is the core claim of Muñoz @cite{munoz-perez-2026}: SE is a PF phenomenon.

theorem Minimalism.agentive_is_phase : voiceAgent.phaseHead = true

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

theorem Minimalism.anticausative_not_phase : voiceAnticausative.phaseHead = false

Non-thematic Voice is NOT a phase head.

theorem Minimalism.impersonal_no_theta : voiceImpersonal.assignsTheta = false

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

theorem Minimalism.impersonal_has_semantics : voiceImpersonal.hasSemantics = true

Impersonal Voice HAS semantics: it contributes an existential closure over the agent variable, unlike non-thematic Voice which is vacuous.

theorem Minimalism.passive_no_theta : voicePassive.assignsTheta = false

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

theorem Minimalism.passive_not_phase : voicePassive.phaseHead = false

Passive Voice IS NOT a phase head.

theorem Minimalism.passive_has_semantics : voicePassive.hasSemantics = true

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

theorem Minimalism.passive_checks_case : voicePassive.checksCase = true

Passive Voice checks Case (@cite{collins-2005}, p. 96: feature dissociation).

theorem Minimalism.reflexive_assigns_theta : voiceReflexive.assignsTheta = true

Reflexive Voice assigns a θ-role (@cite{wood-2015}).

theorem Minimalism.experiencer_assigns_theta : voiceExperiencer.assignsTheta = true

Experiencer Voice assigns a θ-role (@cite{wood-2015}).

theorem Minimalism.theta_implies_active_flavor (v : VoiceHead) : v.assignsTheta = true → v.flavor = VoiceFlavor.agentive ∨ v.flavor = VoiceFlavor.causer ∨ v.flavor = VoiceFlavor.antipassive ∨ v.flavor = VoiceFlavor.reflexive ∨ v.flavor = VoiceFlavor.experiencer

Only θ-assigning Voice flavors assign θ-roles.

def Minimalism.buildDecomposition (voice : VoiceHead) (rootStructure : List VerbHead) : List VerbHead

Build the full verbal decomposition by combining Voice's contribution with the root-determined lower event structure.

Voice contributes vDO when it assigns a θ-role (agentive, causer, antipassive). The root supplies the lower structure, which now includes vCAUSE for change-of-state roots (@cite{wood-2015}, @cite{pylkkanen-2008}). CAUSE is independent of Voice:

• Voice_AG + [vCAUSE, vGO, vBE] → [vDO, vCAUSE, vGO, vBE] (causative)
• Voice_nonTh + [vCAUSE, vGO, vBE] → [vCAUSE, vGO, vBE] (anticausative)
• Voice_AG + [] → [vDO] (unergative activity)
• Voice_nonTh + [vBE] → [vBE] (stative)

Equations

• Minimalism.buildDecomposition voice rootStructure = if voice.assignsTheta = true then Minimalism.VerbHead.vDO :: rootStructure else rootStructure

theorem Minimalism.theta_voice_prepends_vDO (v : VoiceHead) (root : List VerbHead) (h : v.assignsTheta = true) : buildDecomposition v root = VerbHead.vDO :: root

θ-assigning Voice prepends vDO to the root structure.

theorem Minimalism.no_theta_passthrough (v : VoiceHead) (root : List VerbHead) (h : v.assignsTheta = false) : buildDecomposition v root = root

Non-θ Voice leaves the root structure unchanged.

theorem Minimalism.agent_plus_change_is_causative : isCausative (buildDecomposition voiceAgent [VerbHead.vCAUSE, VerbHead.vGO, VerbHead.vBE]) = true

Causative pattern: agentive Voice + [vCAUSE, vGO, vBE] yields a causative decomposition.

theorem Minimalism.nonthematic_plus_change_is_inchoative : isInchoative (buildDecomposition voiceAnticausative [VerbHead.vCAUSE, VerbHead.vGO, VerbHead.vBE]) = true

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

theorem Minimalism.agent_plus_nothing_is_activity : isActivity (buildDecomposition voiceAgent []) = true

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

theorem Minimalism.nonthematic_plus_state_is_state : isState (buildDecomposition voiceAnticausative [VerbHead.vBE]) = true

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

theorem Minimalism.causative_alternation : isCausative (buildDecomposition voiceAgent [VerbHead.vCAUSE, VerbHead.vGO, VerbHead.vBE]) = true ∧ isInchoative (buildDecomposition voiceAnticausative [VerbHead.vCAUSE, VerbHead.vGO, VerbHead.vBE]) = true

The causative alternation: same root structure [vCAUSE, vGO, vBE] is causative under agentive Voice but inchoative under non-thematic Voice. CAUSE is shared across both alternants — only vDO (from Voice) differs. This formalizes the @cite{wood-2015}/@cite{pylkkanen-2008} insight: CAUSE is independent of Voice.

theorem Minimalism.voice_determines_causativity (v : VoiceHead) : isCausative (buildDecomposition v [VerbHead.vCAUSE, VerbHead.vGO, VerbHead.vBE]) = v.assignsTheta

Voice determines causativity: if the root structure is [vCAUSE, vGO, vBE], then whether the result is causative tracks exactly whether Voice assigns a θ-role.

theorem Minimalism.cause_independent_of_voice : hasCause (buildDecomposition voiceAgent [VerbHead.vCAUSE, VerbHead.vGO, VerbHead.vBE]) = true ∧ hasCause (buildDecomposition voiceAnticausative [VerbHead.vCAUSE, VerbHead.vGO, VerbHead.vBE]) = true

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

theorem Minimalism.active_theta_and_case_unified : voiceAgent.assignsTheta = true ∧ voiceAgent.checksCase = false

In active, v (= agentive Voice) assigns θ AND controls Case-checking (Case is checked by v, not by Voice). In passive, these functions dissociate: v assigns θ (external argument in Spec,vP), while Voice/by checks Case.

theorem Minimalism.passive_theta_case_dissociated : voicePassive.assignsTheta = false ∧ voicePassive.checksCase = true

Passive: θ-assignment and Case-checking are dissociated. Voice does NOT assign θ (v does), but Voice DOES check Case.

theorem Minimalism.utah_active_passive : voiceAgent.hasD = true ∧ voicePassive.hasD = true

UTAH compliance: the external argument is structurally present (hasD = true) in BOTH active and passive. The external argument occupies the same position (Spec,vP) regardless of voice — satisfying the Uniformity of Theta Assignment Hypothesis.

theorem Minimalism.passive_no_vDO (root : List VerbHead) : buildDecomposition voicePassive root = root

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

theorem Minimalism.agentive_voice_is_phase_head : voiceAgent.phaseHead = true ∧ voiceCauser.phaseHead = true

Agentive Voice corresponds to traditional v* (phase head). In the @cite{kratzer-1996}/Schäfer framework, agentive Voice replaces v*. Both agentive and causer Voice are phase heads.

theorem Minimalism.nonthematic_voice_not_phase_head : voiceAnticausative.phaseHead = false ∧ voiceMiddle.phaseHead = false

Non-thematic and expletive Voice are NOT phase heads. Only θ-role-assigning Voice heads (agentive, causer) are phases.

theorem Minimalism.phase_iff_theta (v : VoiceHead) (h : v = voiceAgent ∨ v = voiceCauser ∨ v = voiceAnticausative ∨ v = voiceMiddle ∨ v = voiceReflexive ∨ v = voiceExperiencer) : v.phaseHead = v.assignsTheta

Phase-head-ness correlates with θ-role assignment: Voice is a phase head iff it assigns a θ-role.

inductive Minimalism.ExternalArgSemantics : Type

How a Voice head introduces (or fails to introduce) an external argument semantically.

• thematicArgument: [+λx] — introduces agent/causer via λ-abstraction; the external argument occupies Spec,VoiceP
• thematicExistential: [+∃x] — introduces agent/causer via ∃-binding; agent is semantically present but syntactically implicit (@cite{schaefer-2017} (31b)/(31e): "medio-passive Voice" {λe∃x[agent(e,x)]})
• expletive: [−λx] — no semantic contribution; Voice is semantically vacuous (anticausative SE, middles)

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

instance Minimalism.instDecidableEqExternalArgSemantics : DecidableEq ExternalArgSemantics

Equations

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

def Minimalism.instBEqExternalArgSemantics.beq : ExternalArgSemantics → ExternalArgSemantics → Bool

Equations

• Minimalism.instBEqExternalArgSemantics.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Minimalism.instBEqExternalArgSemantics : BEq ExternalArgSemantics

Equations

• Minimalism.instBEqExternalArgSemantics = { beq := Minimalism.instBEqExternalArgSemantics.beq }

def Minimalism.instReprExternalArgSemantics.repr : ExternalArgSemantics → ℕ → Std.Format

Equations

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

instance Minimalism.instReprExternalArgSemantics : Repr ExternalArgSemantics

Equations

• Minimalism.instReprExternalArgSemantics = { reprPrec := Minimalism.instReprExternalArgSemantics.repr }

structure Minimalism.VoiceParams : Type

The ±D / ±λx parametric decomposition of Voice heads.

From @cite{alexiadou-schaefer-2015} (p. 109, ex. (12)), extended by @cite{schaefer-2017}. Two binary parameters generate the core cross-linguistic typology of Voice:

• ±D (selectsSpecifier): does Voice select a syntactic specifier?
• ±λx (extArgSemantics): does Voice introduce an external argument variable?

none values represent underspecification: the morpheme is compatible with multiple parameter settings, with the actual setting determined by independent factors (argument realization, verb class, pragmatics). Indonesian ber- is fully underspecified ⟨none, none⟩ (@cite{beavers-udayana-2022}); Spanish se is underspecified for ±D.

• 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 Minimalism.instDecidableEqVoiceParams.decEq (x✝ x✝¹ : VoiceParams) : Decidable (x✝ = x✝¹)

Equations

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

instance Minimalism.instDecidableEqVoiceParams : DecidableEq VoiceParams

Equations

• Minimalism.instDecidableEqVoiceParams = Minimalism.instDecidableEqVoiceParams.decEq

def Minimalism.instBEqVoiceParams.beq : VoiceParams → VoiceParams → Bool

Equations

• Minimalism.instBEqVoiceParams.beq { selectsSpecifier := a, extArgSemantics := a_1 } { selectsSpecifier := b, extArgSemantics := b_1 } = (a == b && a_1 == b_1)
• Minimalism.instBEqVoiceParams.beq x✝¹ x✝ = false

instance Minimalism.instBEqVoiceParams : BEq VoiceParams

Equations

• Minimalism.instBEqVoiceParams = { beq := Minimalism.instBEqVoiceParams.beq }

instance Minimalism.instReprVoiceParams : Repr VoiceParams

Equations

• Minimalism.instReprVoiceParams = { reprPrec := Minimalism.instReprVoiceParams.repr }

def Minimalism.instReprVoiceParams.repr : VoiceParams → ℕ → Std.Format

Equations

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

def Minimalism.VoiceFlavor.toParams : VoiceFlavor → VoiceParams

Map each named VoiceFlavor to its position in the ±D / ±λx parameter space.

Flavor	±D	±λx	Example
agentive	+D	+λx (arg)	English active
causer	+D	+λx (arg)	Psych causative
reflexive	+D	+λx (arg)	Icelandic -st reflexive
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)

Note: nonThematic and passive occupy the same cell [+D, −λx]. They differ in Case-checking (VoiceHead.checksCase), which is a property of the full VoiceHead, not of the parametric decomposition.

Equations

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

def Minimalism.VoiceHead.params (v : VoiceHead) : VoiceParams

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

Equations

• v.params = v.flavor.toParams

def Minimalism.VoiceParams.assignsTheta? (p : VoiceParams) : Option Bool

Does this parameter setting assign a theta role? Returns none when underspecified.

Equations

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

def Minimalism.VoiceParams.isCompatibleWith (p q : VoiceParams) : Bool

Are two VoiceParams settings compatible? Two settings are compatible if they agree on all specified dimensions. An underspecified dimension (none) is compatible with anything.

Equations

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

def Minimalism.VoiceParams.isFullySpecified (p : VoiceParams) : Bool

Is this parameter setting fully specified (no underspecification)?

Equations

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

theorem Minimalism.flavor_params_fully_specified (f : VoiceFlavor) : f.toParams.isFullySpecified = true

All named VoiceFlavors produce fully specified params.

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

VoiceHead.assignsTheta is consistent with VoiceParams.assignsTheta?: for fully-specified params, they agree.

theorem Minimalism.params_compatible_refl (p : VoiceParams) : p.isCompatibleWith p = true

Compatibility is reflexive.

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

A fully underspecified VoiceParams is compatible with every named VoiceFlavor — the key property for Indonesian ber-.