Constructions and the types of voice alternation

import Linglib.Syntax.Voice.Construction

A construction of a verb gives each potential participant a status: a nominal term with a transitivity-related role, a dative oblique, an incorporated noun, an implied participant, or absent. Comparing an initial and a derived construction of one verb, a participant is nucleativized when it becomes a core term and denucleativized when it ceases to be one, and a denucleativized participant is maintained in participant structure or suppressed from it. The oriented types of voice alternation, passivization, antipassivization, decausativization and the rest, are defined from these notions, after Creissels.

Main definitions

Voice.Status, Voice.Construction: a participant's status, and a construction.
Voice.Construction.Nucleativized, Denucleativized, Suppressed, fate: comparing two constructions.
Voice.Construction.IsPassivization, IsAntipassivization, IsDecausativization, IsASNucleativization, IsCumulation, IsApplicativization, …: the types of voice alternation.
ArgumentFrame.status, Diathesis.construction: the construction of a diathesis.

Main statements

Voice.Construction.valency_eq_of_nucleativized_of_denucleativized: nucleativization is not valency increase.
Voice.Construction.fate_eq_denucleativized_iff: a participant's fate is denucleativized exactly when it is denucleativized within participant structure.
Voice.Construction.IsPassivization.not_isDecausativization: passivization keeps the initial A in participant structure, decausativization does not.

References

Creissels 2024, Transitivity, Valency, and Voice formalized
Levin 1993, English Verb Classes and Alternations: A Preliminary Investigation formalized

Participant fate

L48–61

L63–66

L68–69

Constructions

Comparing an initial construction c with a derived construction d of the same verb.

A construction expresses a potential participant of its verb as a nominal term with a transitivity-related role, as a dative oblique or as an incorporated noun, leaves it implied but unexpressed, or has it outside participant structure.

inductive Voice.Status L73–82

Type

term (r : TermRole) : Status
dative : Status
incorporated : Status
implicit : Status
absent : Status

Derives DecidableEq, Repr.

Used by Voice.Status.role, Voice.Status.Nuclear, Voice.Construction, ArgumentFrame.status

Used in Creissels2024

L86–90

L92–95

L97

A construction of a verb gives each of its potential participants a status.

@[reducible, inline] abbrev Voice.Construction L101–102

(ι : Type u_1) :

Type u_1

Voice.Construction ι = (ι → Voice.Status)

Built from

Used in Creissels2024

L108–109

L111–112

L115–116

A participant that is not a core term of the initial construction is one of the derived construction.

def Voice.Construction.Nucleativized L120–122

{ι : Type u_1} (c d : Construction ι) (i : ι) :

Prop

c.Nucleativized d i = (¬(c i).Nuclear ∧ (d i).Nuclear)

Built from ,

Used by Voice.Construction.Nucleativizes, Voice.Construction.instDecidableNucleativized, Voice.Construction.instDecidableNucleativizes, Voice.Construction.valency_eq_of_nucleativized_of_denucleativized, Voice.Construction.IsASNucleativization, Voice.Construction.IsPortative, Voice.Construction.isASNucleativization_iff, Voice.Construction.isPortative_iff

A core term of the initial construction is not one of the derived construction.

def Voice.Construction.Denucleativized L124–125

{ι : Type u_1} (c d : Construction ι) (i : ι) :

Prop

c.Denucleativized d i = ((c i).Nuclear ∧ ¬(d i).Nuclear)

Built from ,

A core term of the initial construction is removed from participant structure.

def Voice.Construction.Suppressed L127–128

{ι : Type u_1} (c d : Construction ι) (i : ι) :

Prop

c.Suppressed d i = ((c i).Nuclear ∧ d i = Voice.Status.absent)

Built from ,

Used by Voice.Construction.instDecidableSuppressed, Voice.Construction.fate_eq_suppressed_iff, Voice.Construction.IsDecausativization, Voice.Construction.isDecausativization_iff

An initial core term is suppressed when it leaves participant structure, cumulated when it shares its derived core term with another, maintained when it remains a core term, and denucleativized otherwise.

def Voice.Construction.fate L217–225

{ι : Type u_1} (c d : Construction ι) [Fintype ι] [DecidableEq ι] (i : ι) :

ParticipantFate

The definition is too large to print here; read it in the source.

Built from ,

Used by Voice.Construction.fate_eq_denucleativized_iff, Voice.Construction.fate_eq_suppressed_iff

Used in Syntax/Voice/Basic

theorem Voice.Construction.fate_eq_denucleativized_iff L227–230

{ι : Type u_1} (c d : Construction ι) [Fintype ι] [DecidableEq ι] (i : ι) :

c.fate d i = ParticipantFate.denucleativized ↔ c.Denucleativized d i ∧ d i ≠ Status.absent

Built from , ,

L232–234

An alternation may nucleativize one participant and denucleativize another, keeping the valency, so nucleativization is not valency increase (Creissels 2024 §8.1.3).

theorem Voice.Construction.valency_eq_of_nucleativized_of_denucleativized L236–247

{ι : Type u_1} [Fintype ι] [DecidableEq ι] {c d : Construction ι} {i j : ι} (hi : c.Nucleativized d i) (hj : c.Denucleativized d j) (h : ∀ (k : ι), k ≠ i → k ≠ j → ((c k).Nuclear ↔ (d k).Nuclear)) :

c.valency = d.valency

Built from , , , ,

The types of voice alternation

L253–254

In passivization the initial construction is transitive, its A is denucleativized but maintained in participant structure, and no participant is nucleativized (Creissels 2024 §8.3.2.1).

structure Voice.Construction.IsPassivization L256–270

{ι : Type u_1} (c d : Construction ι) :

Prop

transitive : c.Transitive
The initial construction is transitive.
denucleativized_A (i : ι) : c i = Status.term TermRole.A → c.Denucleativized d i
The initial A is not a core term of the derived construction.
maintained_A (i : ι) : c i = Status.term TermRole.A → d i ≠ Status.absent
The initial A stays in participant structure.
not_nucleativizes : ¬c.Nucleativizes d
No participant becomes a core term.
nuclear_P (i : ι) : c i = Status.term TermRole.P → (d i).Nuclear
The initial P remains a core term, as S in the canonical case and as P after a double-P construction (footnote 1 of §8.1.3).

Built from , , , ,

Used by Voice.Construction.IsImpersonalPassivization, Voice.Construction.isPassivization_iff, Voice.Construction.isImpersonalPassivization_iff, Voice.Construction.instDecidableIsPassivization, Voice.Construction.instDecidableIsImpersonalPassivization, Voice.Construction.IsPassivization.not_isDecausativization, Voice.Construction.IsSymmetrical.not_isPassivization

Used in Syntax/Voice/Basic, Creissels2024

L272–276

In antipassivization the initial construction is transitive, participant structure is unchanged, the initial P is denucleativized and no participant is nucleativized, and the initial A becomes the S of an intransitive construction, or keeps the role of A after a double-P construction (Creissels 2024 §8.3.2).

structure Voice.Construction.IsAntipassivization L278–292

{ι : Type u_1} (c d : Construction ι) :

Prop

transitive : c.Transitive
The initial construction is transitive.
preservesStructure : c.PreservesStructure d
Participant structure is unchanged.
denucleativized_P : ∃ (i : ι), c i = Status.term TermRole.P ∧ c.Denucleativized d i
An initial P is not a core term of the derived construction.
not_nucleativizes : ¬c.Nucleativizes d
No participant becomes a core term.
A_to_S_or_A (i : ι) : c i = Status.term TermRole.A → d i = Status.term TermRole.S ∨ d i = Status.term TermRole.A
The initial A becomes S, or stays A.

Built from , , , ,

Used by Voice.Construction.isAntipassivization_iff, Voice.Construction.instDecidableIsAntipassivization

Used in Syntax/Voice/Basic, Creissels2024

L294–307

In decausativization the initial construction is transitive, its A is suppressed from participant structure, and its P becomes the S of an intransitive construction (Creissels 2024 §8.3.1.2).

structure Voice.Construction.IsDecausativization L309–318

{ι : Type u_1} (c d : Construction ι) :

Prop

transitive : c.Transitive
The initial construction is transitive.
suppressed_A (i : ι) : c i = Status.term TermRole.A → c.Suppressed d i
The initial A leaves participant structure.
P_to_S (i : ι) : c i = Status.term TermRole.P → d i = Status.term TermRole.S
The initial P becomes S.

Built from , ,

Used by Voice.Construction.isDecausativization_iff, Voice.Construction.instDecidableIsDecausativization, Voice.Construction.IsDecausativization.not_preservesStructure, Voice.Construction.IsPassivization.not_isDecausativization

Used in Syntax/Voice/Basic, Creissels2024

In A/S-nucleativization a participant is nucleativized and takes over the role of A or S, the initial A or S coded as P or denucleativized. Causativization, where the new participant instigates or controls the event, the A/S-nucleativization of an oblique, and concernativization, where it is a concernee of the initial S or P, share this structure (Creissels 2024 §8.3.1.1, §8.3.4).

structure Voice.Construction.IsASNucleativization L320–331

{ι : Type u_1} (c d : Construction ι) (i : ι) :

Prop

nucleativized : c.Nucleativized d i
The participant becomes a core term.
eq_A_or_S : d i = Status.term TermRole.A ∨ d i = Status.term TermRole.S
The participant is the derived A or S.
A_or_S_to_P (j : ι) : c j = Status.term TermRole.A ∨ c j = Status.term TermRole.S → d j = Status.term TermRole.P ∨ ¬(d j).Nuclear
The initial A or S becomes P or is denucleativized.

Built from , ,

Used by Voice.Construction.isASNucleativization_iff, Voice.Construction.instDecidableIsASNucleativization, Voice.Construction.IsPortative.not_isASNucleativization, Voice.Construction.IsSymmetrical.not_isASNucleativization

Used in Syntax/Voice/Basic, Creissels2024

In reflexivization and reciprocalization two participant roles expressed as A and P, or as S and a dative oblique, are cumulated by the S term of the derived construction (Creissels 2024 §8.3.3).

def Voice.Construction.IsCumulation L333–338

{ι : Type u_1} (c d : Construction ι) :

Prop

The definition is too large to print here; read it in the source.

Built from

Used by Voice.Construction.instDecidableIsCumulation

Used in Syntax/Voice/Basic, Creissels2024

In applicativization the initial A or S keeps the role of A or S, and the derived construction introduces, in a role other than A or S, an applied participant (Creissels 2024 §8.3.5).

structure Voice.Construction.IsApplicativization L340–351

{ι : Type u_1} (c d : Construction ι) (applied : ι) :

Prop

A_or_S_to_A_or_S (j : ι) : c j = Status.term TermRole.A ∨ c j = Status.term TermRole.S → d j = Status.term TermRole.A ∨ d j = Status.term TermRole.S
The initial A or S stays A or S.
introduced : c.Introduced d applied
The applied participant is introduced.
ne_A : d applied ≠ Status.term TermRole.A
The applied participant is not the derived A.
ne_S : d applied ≠ Status.term TermRole.S
The applied participant is not the derived S.

Built from ,

Used by Voice.Construction.IsPApplicativization, Voice.Construction.IsDApplicativization, Voice.Construction.IsXApplicativization, Voice.Construction.isApplicativization_iff, Voice.Construction.isPApplicativization_iff, Voice.Construction.isDApplicativization_iff, Voice.Construction.isXApplicativization_iff, Voice.Construction.instDecidableIsApplicativization, Voice.Construction.instDecidableIsDApplicativization, Voice.Construction.instDecidableIsXApplicativization

theorem Voice.Construction.IsPassivization.not_isDecausativization L473–476

{ι : Type u_1} {c d : Construction ι} (h : c.IsPassivization d) :

¬c.IsDecausativization d

Built from , ,

The status a frame gives the participant of slot s is its transitivity-related role if s is a core slot, X if it is an expressed oblique, and absent if it is an expletive or unfilled. An incorporated noun expresses its participant without a term (Creissels 2024 §17.2.2). An implicit slot leaves its participant implied, unless it is understood as the subject itself or as its members; then the subject's term cumulates the two roles (Creissels 2024 §8.3.3). Levin's understood reflexive and reciprocal objects are therefore cumulations, not implied participants.

def ArgumentFrame.status L502–516

(fr : ArgumentFrame) (s : Slot) :

Voice.Status

The definition is too large to print here; read it in the source.

Built from

Used by Diathesis.construction

Used in Syntax/Voice/Basic, Bohnemeyer2004

The construction of a diathesis gives each participant the status of its slot, absent where the diathesis leaves it out.

def Diathesis.construction L518–521

{n : ℕ} (d : Diathesis n) :

Voice.Construction (Fin n)

d.construction i = (d.links.get i).elim Voice.Status.absent d.status

Built from ,

Used in Syntax/Voice/Basic, Coon2019, Creissels2024