Voice heads

Voice introduces, or fails to introduce, the external argument of the verbal phrase it takes, as Kratzer proposed. A head is a cell of Alexiadou and Schäfer's typology after Schäfer: thematic Voice introduces an external-argument variable with an instruction for interpreting it, as an agent, a causer or a holder, and expletive Voice introduces nothing; active Voice bears a D-feature and projects a specifier, non-active Voice does not, its variable, if any, existentially bound and implicit. The four cells are the active and non-active thematic heads, the transitive and the passive, and the active and non-active expletive heads, the se-marked anticausative and the non-active middle. Beyond its cell a head may bind the internal argument to the external one, reflexively or reciprocally, or demote it to an oblique, the antipassive; may check the accusative Case that v otherwise checks; and may carry Agree features.

Every property consumers read is derived from the cell: Head.IsThematic, Head.AssignsTheta, Head.ExternalImplicit, Head.IsPhasal, and the underspecified cell Head.params that Beavers and Udayana's Indonesian ber- leaves open.

Main definitions

• Instruction, Operation, Head: the thematic instruction, the valency operation and the head.
• Head.IsThematic, Head.HasD, Head.ExternalImplicit, Head.AssignsTheta, Head.IsPhasal, Head.ChecksCase, Head.DCoherent: the predicate API.
• agentive, causer, experiencer, anticausative, middle, passive, impersonal, reflexive, reciprocal, antipassive: the named cells.
• Params, Head.params, Params.Compatible: the ±D/±λx cell with either coordinate left open.

Main results

• Head.AssignsTheta.isThematic, Head.IsPhasal.assignsTheta: θ-assignment entails a thematic head, and phasehood entails θ-assignment.
• canonical_dCoherent: every named cell realizes its variable in its specifier exactly when it has one.
• antipassive_not_phasal: the antipassive is thematic and active yet not a phase.
• Params.Compatible.refl, underspecified_compatible_with_all.

Implementation notes

• The passive is the thematic non-active cell, its agent implicit, with the Finnish impersonal in the same cell; Collins's passive Voice, which assigns no θ-role and checks Case, is statable here as an expletive active head with checksCase.
• Phasehood is that of Chomsky's v*, a θ-assigning active head, with the antipassive excepted because it detransitivizes. A study that separates the phase head v from Voice reads its own v off the Voice head below it.
• Cuervo's inchoatives have no Voice at all, and the event structure below Voice is Minimalist.LittleV.

References

• [AAS15]
• [BU22]
• [Cho01]
• [Col05]
• [Cue03]
• [Kra96]
• [MSK25]
• [MP26]
• [Sch08a]
• [Sch17]
• [Sco23]
• [Sil12]
• [Woo15]

The cell

inductive Minimalist.Voice.Instruction : Type

The instruction a thematic Voice head gives for interpreting its external-argument variable ([AAS15]).

• agent : Instruction
• causer : Instruction
• holder : Instruction

@[instance_reducible]

instance Minimalist.Voice.instDecidableEqInstruction : DecidableEq Instruction

Equations

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

def Minimalist.Voice.instReprInstruction.repr : Instruction → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Minimalist.Voice.instReprInstruction : Repr Instruction

Equations

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

inductive Minimalist.Voice.Operation : Type

What a head does to the internal argument beyond introducing an external one, binding it to the external argument reflexively or reciprocally ([Sil12]) or demoting it to an oblique ([Sco23]).

• reflexive : Operation
• reciprocal : Operation
• antipassive : Operation

@[instance_reducible]

instance Minimalist.Voice.instDecidableEqOperation : DecidableEq Operation

Equations

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

def Minimalist.Voice.instReprOperation.repr : Operation → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Minimalist.Voice.instReprOperation : Repr Operation

Equations

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

structure Minimalist.Voice.Head : Type

A Voice head, with its cell in the thematic/expletive × active/non-active typology, whether its variable is implicit, its valency operation, and its per-construction properties.

• thematic : Option Instruction

  The external-argument variable λx with its instruction, none for expletive Voice.

• hasD : Bool

  The head bears D and projects a specifier.

• implicit : Bool

  The variable is existentially bound rather than saturated by a specifier DP.

• operation : Option Operation

  The operation on the internal argument, if any.

• checksCase : Bool

  Checks the accusative Case that v otherwise checks, as [Col05]'s passive Voice does.

• features : FeatureBundle

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

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

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

The head is thematic when it introduces an external-argument variable, and so has semantics.

Equations

• v.IsThematic = (v.thematic.isSome = true)

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

Projects a specifier.

Equations

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

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

The external argument is existentially bound.

Equations

• v.ExternalImplicit = (v.implicit = true)

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

Assigns a θ-role to a DP in its specifier: thematic, with its variable not implicit.

Equations

• v.AssignsTheta = (v.IsThematic ∧ ¬v.ExternalImplicit)

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

Checks Case.

Equations

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

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

The head is a phase head, [Cho01]'s v*, when it assigns a θ-role and is active, unless it is the antipassive, which detransitivizes.

Equations

• v.IsPhasal = (v.AssignsTheta ∧ v.HasD ∧ v.operation ≠ some Minimalist.Voice.Operation.antipassive)

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

A thematic head's variable is implicit exactly when the head projects no specifier, as in [AAS15]'s grid; a head may diverge, and stating the divergence makes it explicit.

Equations

• v.DCoherent = (v.IsThematic → v.implicit = !v.hasD)

@[instance_reducible]

instance Minimalist.Voice.Head.instDecidableIsThematic (v : Head) : Decidable v.IsThematic

Equations

• v.instDecidableIsThematic = Minimalist.Voice.Head.instDecidableIsThematic._aux_1 v

@[instance_reducible]

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

Equations

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

@[instance_reducible]

instance Minimalist.Voice.Head.instDecidableExternalImplicit (v : Head) : Decidable v.ExternalImplicit

Equations

• v.instDecidableExternalImplicit = Minimalist.Voice.Head.instDecidableExternalImplicit._aux_1 v

@[instance_reducible]

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

Equations

• v.instDecidableAssignsTheta = { decide := decide v.IsThematic && decide ¬v.ExternalImplicit, reflects_decide := ⋯ }

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

• v.instDecidableIsPhasal = { decide := decide v.AssignsTheta && decide (v.HasD ∧ v.operation ≠ some Minimalist.Voice.Operation.antipassive), reflects_decide := ⋯ }

@[instance_reducible]

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

Equations

• v.instDecidableDCoherent = { decide := if h : v.IsThematic then decide ((fun (a : v.IsThematic) => v.implicit = !v.hasD) h) else true, reflects_decide := ⋯ }

theorem Minimalist.Voice.Head.AssignsTheta.isThematic {v : Head} (h : v.AssignsTheta) : v.IsThematic

theorem Minimalist.Voice.Head.IsPhasal.assignsTheta {v : Head} (h : v.IsPhasal) : v.AssignsTheta

The underspecified cell

structure Minimalist.Voice.Params : Type

The ±D/±λx cell with either coordinate left open ([AAS15], [Sch17]): none is underspecified, as Indonesian ber- is on both ([BU22]).

• hasD : Option Bool

  Does the head project a specifier?

• thematic : Option Bool

  Does the head introduce an external-argument variable?

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

Equations

• Minimalist.Voice.instDecidableEqParams.decEq { hasD := a, thematic := a_1 } { hasD := b, thematic := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[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.Head.params (v : Head) : Params

The cell of a head, fully specified.

Equations

• v.params = { hasD := some v.hasD, thematic := some v.thematic.isSome }

def Minimalist.Voice.Params.Compatible (p q : Params) : Prop

Two cells are compatible when they agree on every coordinate both specify.

Equations

• p.Compatible q = ((∀ s ∈ p.hasD, ∀ t ∈ q.hasD, s = t) ∧ ∀ s ∈ p.thematic, ∀ t ∈ q.thematic, s = t)

@[instance_reducible]

instance Minimalist.Voice.instDecidableRelParamsCompatible : DecidableRel Params.Compatible

Equations

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

theorem Minimalist.Voice.Params.Compatible.refl (p : Params) : p.Compatible p

theorem Minimalist.Voice.underspecified_compatible_with_all (v : Head) : { hasD := none, thematic := none }.Compatible v.params

A cell open on both coordinates is compatible with every head.

The named cells

def Minimalist.Voice.agentive : Head

Thematic active Voice introducing an agent, the transitive and unergative head v*.

Equations

• Minimalist.Voice.agentive = { thematic := some Minimalist.Voice.Instruction.agent, hasD := true }

def Minimalist.Voice.causer : Head

Thematic active Voice introducing a causer.

Equations

• Minimalist.Voice.causer = { thematic := some Minimalist.Voice.Instruction.causer, hasD := true }

def Minimalist.Voice.experiencer : Head

Thematic active Voice introducing a holder, the experiencer subject of a psych causative.

Equations

• Minimalist.Voice.experiencer = { thematic := some Minimalist.Voice.Instruction.holder, hasD := true }

def Minimalist.Voice.anticausative : Head

Expletive active Voice, with no variable and a specifier for a marker such as Romance se, the marked anticausative ([MP26]).

Equations

• Minimalist.Voice.anticausative = { thematic := none, hasD := true }

def Minimalist.Voice.middle : Head

Expletive non-active Voice, with neither variable nor specifier, the dispositional middle.

Equations

• Minimalist.Voice.middle = { thematic := none, hasD := false }

def Minimalist.Voice.passive : Head

Thematic non-active Voice, its agent existentially bound and implicit, the passive.

Equations

• Minimalist.Voice.passive = { thematic := some Minimalist.Voice.Instruction.agent, hasD := false, implicit := true }

def Minimalist.Voice.impersonal : Head

The Finnish impersonal, the same cell as the passive, with an implicit generic agent.

Equations

• Minimalist.Voice.impersonal = Minimalist.Voice.passive

def Minimalist.Voice.reflexive : Head

Agentive Voice binding the internal argument to the agent, Romance reflexive se ([MSK25]). [Woo15]'s Icelandic -st is a SpecpP clitic, not an exponent of this head.

Equations

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

def Minimalist.Voice.reciprocal : Head

Agentive Voice putting the agent in the mutual relation with the internal argument, [Sil12]'s syntactic reciprocalization. Lexically reciprocal verbs enter the syntax symmetric and are not exponents of this head.

Equations

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

def Minimalist.Voice.antipassive : Head

Agentive Voice demoting the object to an oblique, with absolutive on the agent ([Sco23]).

Equations

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

Verification

theorem Minimalist.Voice.assignsTheta_cells : agentive.AssignsTheta ∧ causer.AssignsTheta ∧ experiencer.AssignsTheta ∧ reflexive.AssignsTheta ∧ reciprocal.AssignsTheta ∧ antipassive.AssignsTheta ∧ ¬anticausative.AssignsTheta ∧ ¬middle.AssignsTheta ∧ ¬passive.AssignsTheta

The θ-assigning heads are the thematic active ones; the anticausative, the middle and the passive assign none.

theorem Minimalist.Voice.passive_anticausative : passive.IsThematic ∧ passive.ExternalImplicit ∧ ¬anticausative.IsThematic ∧ anticausative.HasD

The passive is thematic with an implicit agent; the anticausative is expletive with a specifier, the core claim of [MP26] that se is a PF phenomenon.

theorem Minimalist.Voice.canonical_dCoherent : agentive.DCoherent ∧ causer.DCoherent ∧ experiencer.DCoherent ∧ anticausative.DCoherent ∧ middle.DCoherent ∧ passive.DCoherent ∧ reflexive.DCoherent ∧ reciprocal.DCoherent ∧ antipassive.DCoherent

Every named thematic cell keeps its variable implicit exactly when it lacks a specifier.

theorem Minimalist.Voice.phasal_cells : agentive.IsPhasal ∧ causer.IsPhasal ∧ ¬anticausative.IsPhasal ∧ ¬middle.IsPhasal ∧ ¬passive.IsPhasal

Agentive and causer Voice are phase heads, v*; the anticausative, the middle and the passive are not.

theorem Minimalist.Voice.antipassive_not_phasal : antipassive.AssignsTheta ∧ ¬antipassive.IsPhasal

The antipassive is a thematic active head that is no phase, phasehood tracking v* transitivity ([Cho01]) and the antipassive detransitivizing.