Voice systems #

A language's voices are a finite set of Voices. The symmetrical voices of Western Austronesian and of a few languages elsewhere code which participant is the pivot, the syntactically privileged term, without affecting the transitivity of the construction, and a system is symmetrical when every voice does so ([Cre24] §8.1.7); it is multiple rather than binary when some voice selects an oblique as pivot (§8.5.1, §8.5.2). Of the four characteristics of an Austronesian-type voice system in [ELvU17], the privileged argument realized in one form or position whatever its function (4a) is Voice.pivot, and verb morphology varying with its choice, obliques included (4b), is Voice.marker and Multiple; the extraction restriction to the pivot (4c) and the marking of non-pivot subjects (4d) are recorded where a fragment states them.

Main definitions #

Voice.Symmetrical, Voice.Multiple, Voice.Equipollent — properties of a set of voices

Main results #

Voice.Symmetrical.not_isValencyIncreasing, Symmetrical.not_isValencyDecreasing — no voice of a symmetrical system changes valency
Voice.symmetrical_image, multiple_image, equipollent_image — the properties over a system indexed by a language's voice names

Implementation notes #

[Cre24] §8.1.7 reports two rival criteria for symmetry: equipollent marking (Himmelmann) and equal transitivity of all voices (Riesberg), and adopts the second. Symmetrical is the book's criterion and Equipollent, every voice coded and so none derived from an unmarked one, the first; Balinese separates them (Studies/Creissels2024.lean).
A language whose names outrun the frames, two passives or two oblique voices of one relation, keeps its own name type and states the properties of the image of its map into Voice.

References #

source

def Voice.Symmetrical (S : Finset Voice) :

Prop

Every voice selects a pivot without affecting transitivity: the book's criterion for a symmetrical voice system ([Cre24] §8.1.7).

Equations

Voice.Symmetrical S = ∀ v ∈ S, v.IsSymmetrical

Instances For

source

def Voice.Multiple (S : Finset Voice) :

Prop

Some voice selects an oblique as pivot: a multiple system, as against a binary one whose pivot is always a nuclear participant ([Cre24] §8.5.1, §8.5.2).

Equations

Voice.Multiple S = ∃ v ∈ S, v.SelectsOblique

Instances For

source

def Voice.Equipollent (S : Finset Voice) :

Prop

Every voice is coded, none derived from an unmarked one by adding marking: the criterion for symmetry [Cre24] §8.1.7 attributes to Himmelmann and does not adopt.

Equations

Voice.Equipollent S = ∀ v ∈ S, v.IsCoded

Instances For

source

@[instance_reducible]

instance Voice.instDecidableSymmetrical (S : Finset Voice) :

Decidable (Symmetrical S)

Equations

Voice.instDecidableSymmetrical S = { decide := decide (∀ a ∈ S.val.attach, (fun (x : Voice) (a : x ∈ S) => x.IsSymmetrical) ↑a ⋯), reflects_decide := ⋯ }