Documentation

Studies.BeaversUdayana2022

Beavers & Udayana (2022): Middle voice as generalized argument suppression #

This file formalizes Beavers and Udayana's analysis of the Indonesian middle prefix ber-.

The prefix saturates the first open argument of its VP with a free variable. Which argument that is depends on how the object is realized. An object DP combines with the verb first, so ber- suppresses the agent and the patient is the subject. An incorporated noun is predicated of the patient without saturating it, so ber- suppresses the patient and the agent is the subject. The free variable is read as coreferent with the subject or as disjoint from it, which gives the four middles of the paper.

Main definitions #

ber, incorporate: the denotation of ber- and the incorporating variant of a verb.
MiddleType, MiddleType.denote: a cell of the two-by-two classification, and the truth conditions that ber- derives for it.
RootClass: the classes of root that fix the default reading.
Voice, Voice.LicensesOleh, Voice.LicensesRationale, Voice.LicensesSendirinya: the voice forms and the licensing conditions of the three diagnostics.

Main results #

denote_dispositional, denote_reflexive, denote_incorporation, denote_incorporationReflexive: the truth conditions of the four middles.
denote_incorporationReflexive_iff_reflexive: incorporated diri and an inherent reflexive have the same truth conditions.
causerSuppress_eq_ber, denote_reflexive_iff_resolve: ber- generalizes the causer suppression of Beavers and Zubair.
subjectIsAgent_iff, separateAgent_of_dispositional: the subject is the agent in every cell but the dispositional one, which entails an agent other than the subject.
licensesOleh_iff, licensesSendirinya_not_licensesRationale_iff: only di- licenses oleh, and only anticausative ter- licenses dengan sendirinya without a rationale clause.

References #

The middles #

inductive BeaversUdayana2022.Reading :

How the variable that ber- leaves free is read relative to the subject.

coreferent : Reading
disjoint : Reading

Instances For

@[instance_reducible]

instance BeaversUdayana2022.instDecidableEqReading :

DecidableEq Reading

Equations

BeaversUdayana2022.instDecidableEqReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance BeaversUdayana2022.instReprReading :

Equations

BeaversUdayana2022.instReprReading = { reprPrec := BeaversUdayana2022.instReprReading.repr }

def BeaversUdayana2022.instReprReading.repr :

Reading → ℕ → Std.Format

Equations

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

Instances For

inductive BeaversUdayana2022.ObjectRealization :

How the object of the base verb is realized, as an incorporated noun or as a DP that is promoted to subject.

incorporation : ObjectRealization
promotion : ObjectRealization

Instances For

@[instance_reducible]

instance BeaversUdayana2022.instDecidableEqObjectRealization :

DecidableEq ObjectRealization

Equations

BeaversUdayana2022.instDecidableEqObjectRealization x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance BeaversUdayana2022.instReprObjectRealization :

Repr ObjectRealization

Equations

BeaversUdayana2022.instReprObjectRealization = { reprPrec := BeaversUdayana2022.instReprObjectRealization.repr }

def BeaversUdayana2022.instReprObjectRealization.repr :

ObjectRealization → ℕ → Std.Format

Equations

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

Instances For

structure BeaversUdayana2022.MiddleType :

A cell of the classification of middles by object realization and reading.

objRealization : ObjectRealization
reading : Reading

Instances For

def BeaversUdayana2022.instDecidableEqMiddleType.decEq (x✝ x✝¹ : MiddleType) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

@[instance_reducible]

instance BeaversUdayana2022.instDecidableEqMiddleType :

DecidableEq MiddleType

Equations

BeaversUdayana2022.instDecidableEqMiddleType = BeaversUdayana2022.instDecidableEqMiddleType.decEq

@[instance_reducible]

instance BeaversUdayana2022.instReprMiddleType :

Repr MiddleType

Equations

BeaversUdayana2022.instReprMiddleType = { reprPrec := BeaversUdayana2022.instReprMiddleType.repr }

def BeaversUdayana2022.instReprMiddleType.repr :

MiddleType → ℕ → Std.Format

Equations

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

Instances For

def BeaversUdayana2022.dispositional :

The dispositional or passive middle, as in Mobil itu berjual dengan mudah 'The car sells easily'.

Equations

BeaversUdayana2022.dispositional = { objRealization := BeaversUdayana2022.ObjectRealization.promotion, reading := BeaversUdayana2022.Reading.disjoint }

Instances For

def BeaversUdayana2022.reflexive :

The inherent reflexive, as in Ali berdandan 'Ali dressed'.

Equations

BeaversUdayana2022.reflexive = { objRealization := BeaversUdayana2022.ObjectRealization.promotion, reading := BeaversUdayana2022.Reading.coreferent }

Instances For

def BeaversUdayana2022.incorporation :

The incorporation middle, as in Orang itu bercuci mata 'The man washed his eyes'.

Equations

BeaversUdayana2022.incorporation = { objRealization := BeaversUdayana2022.ObjectRealization.incorporation, reading := BeaversUdayana2022.Reading.disjoint }

Instances For

def BeaversUdayana2022.incorporationReflexive :

The incorporated reflexive, as in Orang itu berjual diri 'The man sold himself'.

Equations

BeaversUdayana2022.incorporationReflexive = { objRealization := BeaversUdayana2022.ObjectRealization.incorporation, reading := BeaversUdayana2022.Reading.coreferent }

Instances For

Composition #

A dyadic root is a relation V patient agent, with the event variable closed off.

def BeaversUdayana2022.ber {E α : Type} (z : E) (vp : E → α) :

α

ber- saturates the first open argument of its VP with the free variable z (43).

Equations

BeaversUdayana2022.ber z vp = vp z

Instances For

def BeaversUdayana2022.incorporate {E : Type} (V : E → E → Prop) (P : E → Prop) :

E → E → Prop

An incorporating verb predicates the noun of its patient and keeps the patient as an argument (49).

Equations

BeaversUdayana2022.incorporate V P x y = (V x y ∧ P x)

Instances For

def BeaversUdayana2022.vp {E : Type} (V : E → E → Prop) (P : E → Prop) (s : E) :

ObjectRealization → E → Prop

The VP of a middle before ber- applies, as a function of its first open argument. With a promoted object, whose trace the verb has combined with, that argument is the agent, and with an incorporated noun it is the patient.

Equations

BeaversUdayana2022.vp V P s BeaversUdayana2022.ObjectRealization.promotion = V s
BeaversUdayana2022.vp V P s BeaversUdayana2022.ObjectRealization.incorporation = fun (x : E) => BeaversUdayana2022.incorporate V P x s

Instances For

def BeaversUdayana2022.Reading.resolve {E : Type} (s : E) (φ : E → Prop) :

Reading → Prop

A reading resolves the free variable, to the subject or to something else.

Equations

BeaversUdayana2022.Reading.resolve s φ BeaversUdayana2022.Reading.coreferent = φ s
BeaversUdayana2022.Reading.resolve s φ BeaversUdayana2022.Reading.disjoint = ∃ (z : E), z ≠ s ∧ φ z

Instances For

def BeaversUdayana2022.MiddleType.denote {E : Type} (V : E → E → Prop) (P : E → Prop) (s : E) (m : MiddleType) :

The truth conditions of a middle with subject s, which are those of ber- applied to the VP, with the free variable resolved by the reading.

Equations

BeaversUdayana2022.MiddleType.denote V P s m = BeaversUdayana2022.Reading.resolve s (fun (z : E) => BeaversUdayana2022.ber z (BeaversUdayana2022.vp V P s m.objRealization)) m.reading

Instances For

def BeaversUdayana2022.diri {E : Type} :

E → Prop

As an incorporated noun diri 'self' is semantically vacuous.

Equations

BeaversUdayana2022.diri x = ∃ (y : E), y = x

Instances For

theorem BeaversUdayana2022.denote_dispositional {E : Type} (V : E → E → Prop) (P : E → Prop) (s : E) :

MiddleType.denote V P s dispositional ↔ ∃ (z : E), z ≠ s ∧ V s z

A dispositional middle says that something other than the subject acted on it.

theorem BeaversUdayana2022.denote_reflexive {E : Type} (V : E → E → Prop) (P : E → Prop) (s : E) :

MiddleType.denote V P s reflexive ↔ V s s

An inherent reflexive says that the subject acted on itself.

theorem BeaversUdayana2022.denote_incorporation {E : Type} (V : E → E → Prop) (P : E → Prop) (s : E) :

MiddleType.denote V P s incorporation ↔ ∃ (z : E), z ≠ s ∧ V z s ∧ P z

An incorporation middle says that the subject acted on something else that the noun describes.

theorem BeaversUdayana2022.denote_incorporationReflexive {E : Type} (V : E → E → Prop) (P : E → Prop) (s : E) :

MiddleType.denote V P s incorporationReflexive ↔ V s s ∧ P s

An incorporated reflexive says that the subject acted on itself and that the noun describes it.

theorem BeaversUdayana2022.denote_incorporationReflexive_iff_reflexive {E : Type} (V : E → E → Prop) (P : E → Prop) (s : E) :

MiddleType.denote V diri s incorporationReflexive ↔ MiddleType.denote V P s reflexive

With diri incorporated, the reflexive incorporation middle has the truth conditions of an inherent reflexive.

def BeaversUdayana2022.MiddleType.SubjectIsAgent (m : MiddleType) :

The subject of a middle is understood as the agent of the base verb in every cell but the dispositional one.

Equations

m.SubjectIsAgent = (m.objRealization = BeaversUdayana2022.ObjectRealization.incorporation ∨ m.reading = BeaversUdayana2022.Reading.coreferent)

Instances For

@[instance_reducible]

instance BeaversUdayana2022.instDecidablePredMiddleTypeSubjectIsAgent :

DecidablePred MiddleType.SubjectIsAgent

Equations

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

theorem BeaversUdayana2022.exists_patient_of_subjectIsAgent {E : Type} (V : E → E → Prop) (P : E → Prop) (s : E) {m : MiddleType} (hm : m.SubjectIsAgent) (h : MiddleType.denote V P s m) :

∃ (x : E), V x s

Where the subject is the agent, the middle entails that it acted on something.

theorem BeaversUdayana2022.subjectIsAgent_iff (m : MiddleType) :

m.SubjectIsAgent ↔ m ≠ dispositional

The subject is the agent exactly when the cell is not the dispositional one.

theorem BeaversUdayana2022.separateAgent_of_dispositional {E : Type} (V : E → E → Prop) (P : E → Prop) (s : E) (h : MiddleType.denote V P s dispositional) :

∃ (z : E), z ≠ s ∧ V s z

A dispositional middle entails an agent other than its subject.

Causer suppression (§3.3) #

ber- generalizes the causer suppression of Beavers and Zubair, which applies to a causer of the individual sort alone. Their verbs take the causer first.

theorem BeaversUdayana2022.causerSuppress_eq_ber {E : Type} {c : BeaversZubair2013.CauserSort} (h : BeaversZubair2013.CauserSort.individual ≤ c) {α : Type} (z : E) (vp : E → α) :

BeaversZubair2013.causerSuppress c h z vp = ber z vp

Causer suppression is ber- under a condition on the sort of the causer.

theorem BeaversUdayana2022.denote_reflexive_iff_resolve {E : Type} {c : BeaversZubair2013.CauserSort} (h : BeaversZubair2013.CauserSort.individual ≤ c) (V : E → E → Prop) (P : E → Prop) (s : E) :

MiddleType.denote V P s reflexive ↔ BeaversZubair2013.Reading.reflexive.resolve h (flip V) s

An inherent reflexive is the reflexive resolution of a suppressed causer.

theorem BeaversUdayana2022.resolve_existential_of_dispositional {E : Type} {c : BeaversZubair2013.CauserSort} (h : BeaversZubair2013.CauserSort.individual ≤ c) (V : E → E → Prop) (P : E → Prop) (s : E) (hs : MiddleType.denote V P s dispositional) :

BeaversZubair2013.Reading.existential.resolve h (flip V) s

A dispositional middle entails the existential resolution of a suppressed causer, to which it adds that the causer is not the subject.

A model #

Tono sold the car, and Ali dressed himself.

inductive BeaversUdayana2022.Entity :

The individuals of the model.

tono : Entity
ali : Entity
car : Entity

Instances For

@[instance_reducible]

instance BeaversUdayana2022.instDecidableEqEntity :

DecidableEq Entity

Equations

BeaversUdayana2022.instDecidableEqEntity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance BeaversUdayana2022.instReprEntity :

Equations

BeaversUdayana2022.instReprEntity = { reprPrec := BeaversUdayana2022.instReprEntity.repr }

def BeaversUdayana2022.instReprEntity.repr :

Entity → ℕ → Std.Format

Equations

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

Instances For

def BeaversUdayana2022.acted :

Entity → Entity → Prop

The selling and dressing events of the model, as one relation of patient and agent.

Equations

BeaversUdayana2022.acted BeaversUdayana2022.Entity.car BeaversUdayana2022.Entity.tono = True
BeaversUdayana2022.acted BeaversUdayana2022.Entity.ali BeaversUdayana2022.Entity.ali = True
BeaversUdayana2022.acted x✝¹ x✝ = False

Instances For

@[instance_reducible]

instance BeaversUdayana2022.instFintypeEntity :

Fintype Entity

Equations

BeaversUdayana2022.instFintypeEntity = { elems := {BeaversUdayana2022.Entity.tono, BeaversUdayana2022.Entity.ali, BeaversUdayana2022.Entity.car}, complete := ⋯ }

@[instance_reducible]

instance BeaversUdayana2022.instDecidableRelEntityActed :

DecidableRel acted

Equations

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

theorem BeaversUdayana2022.model :

MiddleType.denote acted diri Entity.car dispositional ∧ ¬MiddleType.denote acted diri Entity.car reflexive ∧ MiddleType.denote acted diri Entity.ali reflexive ∧ ¬MiddleType.denote acted diri Entity.ali dispositional ∧ MiddleType.denote acted (fun (x : Entity) => x = Entity.car) Entity.tono incorporation ∧ ¬MiddleType.denote acted (fun (x : Entity) => x = Entity.car) Entity.ali incorporation

The car has a dispositional middle and no reflexive one, Ali a reflexive one and no dispositional one, and Tono the incorporation middle with a noun true of the car.

Root classes (§3.5, §5) #

The default reading of a plain ber- form follows the class of its root. The members are the paper's own roots, as entries of Fragments/Indonesian/Verbs.lean.

inductive BeaversUdayana2022.RootClass :

The classes of dyadic root.

naturallyReflexive : RootClass
The conventional expectation is self-action, as with verbs of body care.
obviative : RootClass
The conventional expectation is disjoint reference, as with every other dyadic root.
causerUnspecified : RootClass
A change of state whose root entails no external causer.

Instances For

@[instance_reducible]

instance BeaversUdayana2022.instDecidableEqRootClass :

DecidableEq RootClass

Equations

BeaversUdayana2022.instDecidableEqRootClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def BeaversUdayana2022.instReprRootClass.repr :

RootClass → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance BeaversUdayana2022.instReprRootClass :

Equations

BeaversUdayana2022.instReprRootClass = { reprPrec := BeaversUdayana2022.instReprRootClass.repr }

def BeaversUdayana2022.RootClass.roots :

RootClass → List Indonesian.Verb

The paper's roots of each class, which are the body-care verbs of (15), the roots of (4) with a dispositional or passive ber- form, and buka 'open' and pecah 'break' of §5.

Equations

Instances For

def BeaversUdayana2022.RootClass.defaultMiddle :

RootClass → Option MiddleType

The default middle of a plain ber- form, which matches the conventional expectation of the root class. A causer-unspecified root has no ber- form.

Equations

Instances For

theorem BeaversUdayana2022.RootClass.ber_iff_defaultMiddle (c : RootClass) (v : Indonesian.Verb) :

v ∈ c.roots → (v.ber = true ↔ c.defaultMiddle.isSome = true) ∧ (v.terClass.isSome = true ↔ ¬v.ber = true)

A root has a ber- form exactly when its class has a default middle, and a form in ter- otherwise.

theorem BeaversUdayana2022.jual_incorporatesDiri :

Indonesian.jual.IncorporatesDiri

An obviative root gets its reflexive reading from incorporated diri 'self', as in berjual diri (26b), the marked form that blocks the reading for the plain ber- form.

The diagnostics (§2, §5) #

A di- passive projects a weak implicit argument, which an oleh phrase realizes and which can control into a rationale clause. A ber- form has a free variable in the semantics and no such argument in the syntax.

inductive BeaversUdayana2022.Voice :

The voice forms that the diagnostics compare.

meN : Voice
The active in meN-.
di : Voice
The passive in di-.
ber (m : MiddleType) : Voice
A middle in ber-.
ter : Voice
The anticausative in ter- of a causer-unspecified root.

Instances For

@[instance_reducible]

instance BeaversUdayana2022.instDecidableEqVoice :

DecidableEq Voice

Equations

BeaversUdayana2022.instDecidableEqVoice = BeaversUdayana2022.instDecidableEqVoice.decEq

def BeaversUdayana2022.instDecidableEqVoice.decEq (x✝ x✝¹ : Voice) :

Decidable (x✝ = x✝¹)

Equations

Instances For

def BeaversUdayana2022.instReprVoice.repr :

Voice → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance BeaversUdayana2022.instReprVoice :

Repr Voice

Equations

BeaversUdayana2022.instReprVoice = { reprPrec := BeaversUdayana2022.instReprVoice.repr }

def BeaversUdayana2022.Voice.SubjectIsAgent :

The subject is the agent in the active and in the middles where ber- leaves it so.

Equations

BeaversUdayana2022.Voice.meN.SubjectIsAgent = True
(BeaversUdayana2022.Voice.ber m).SubjectIsAgent = m.SubjectIsAgent
BeaversUdayana2022.Voice.di.SubjectIsAgent = False
BeaversUdayana2022.Voice.ter.SubjectIsAgent = False

Instances For

def BeaversUdayana2022.Voice.SeparateAgentEntailed :

An agent other than the subject is entailed by the passive and by the dispositional middle. A causer-unspecified root entails none.

Equations

BeaversUdayana2022.Voice.di.SeparateAgentEntailed = True
(BeaversUdayana2022.Voice.ber m).SeparateAgentEntailed = (m = BeaversUdayana2022.dispositional)
BeaversUdayana2022.Voice.meN.SeparateAgentEntailed = False
BeaversUdayana2022.Voice.ter.SeparateAgentEntailed = False

Instances For

def BeaversUdayana2022.Voice.LicensesOleh (v : Voice) :

An oleh 'by' phrase realizes the weak implicit argument of di-.

Equations

v.LicensesOleh = (v = BeaversUdayana2022.Voice.di)

Instances For

def BeaversUdayana2022.Voice.LicensesRationale (v : Voice) :

The null subject of a rationale clause is controlled by an agentive subject or by the weak implicit argument of di-.

Equations

v.LicensesRationale = (v.SubjectIsAgent ∨ v = BeaversUdayana2022.Voice.di)

Instances For

def BeaversUdayana2022.Voice.LicensesSendirinya (v : Voice) :

dengan sendirinya 'by itself' denies an agent other than the subject.

Equations

v.LicensesSendirinya = ¬v.SeparateAgentEntailed

Instances For

@[instance_reducible]

instance BeaversUdayana2022.Voice.instDecidablePredSubjectIsAgent :

DecidablePred SubjectIsAgent

Equations

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

@[instance_reducible]

instance BeaversUdayana2022.Voice.instDecidablePredSeparateAgentEntailed :

DecidablePred SeparateAgentEntailed

Equations

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

@[instance_reducible]

instance BeaversUdayana2022.Voice.instDecidablePredLicensesOleh :

DecidablePred LicensesOleh

Equations

x✝.instDecidablePredLicensesOleh = BeaversUdayana2022.Voice.instDecidablePredLicensesOleh._aux_1 x✝

@[instance_reducible]

instance BeaversUdayana2022.Voice.instDecidablePredLicensesRationale :

DecidablePred LicensesRationale

Equations

x✝.instDecidablePredLicensesRationale = { decide := decide x✝.SubjectIsAgent || decide (x✝ = BeaversUdayana2022.Voice.di), reflects_decide := ⋯ }

@[instance_reducible]

instance BeaversUdayana2022.Voice.instDecidablePredLicensesSendirinya :

DecidablePred LicensesSendirinya

Equations

x✝.instDecidablePredLicensesSendirinya = { decide := !decide x✝.SeparateAgentEntailed, reflects_decide := ⋯ }

theorem BeaversUdayana2022.Voice.licensesOleh_iff (v : Voice) :

v.LicensesOleh ↔ v = di

Only di- licenses oleh.

theorem BeaversUdayana2022.Voice.dispositional_rejects :

¬(ber dispositional).LicensesOleh ∧ ¬(ber dispositional).LicensesRationale ∧ ¬(ber dispositional).LicensesSendirinya

The dispositional middle fails all three diagnostics.

theorem BeaversUdayana2022.Voice.ber_of_subjectIsAgent {m : MiddleType} (hm : m.SubjectIsAgent) :

¬(ber m).LicensesOleh ∧ (ber m).LicensesRationale ∧ (ber m).LicensesSendirinya

The middles whose subject is the agent license a rationale clause and dengan sendirinya and no oleh phrase.

theorem BeaversUdayana2022.Voice.licensesSendirinya_not_licensesRationale_iff (v : Voice) :

v.LicensesSendirinya ∧ ¬v.LicensesRationale ↔ v = ter

Among the forms without an agent subject, anticausative ter- alone licenses dengan sendirinya, and it licenses no rationale clause.

theorem BeaversUdayana2022.Voice.judgments :

The paper's judgments agree with the licensing conditions on an oleh phrase with di- (11), on dengan sendirinya with a dispositional middle (10c) and with a reflexive one (17b), and on a rationale clause with a dispositional middle (13).

Relational nouns (§4) #

theorem BeaversUdayana2022.ber_relationalNoun {E : Type} (π : E → E → Prop) (possessum possessor : E) :

ber possessum π possessor ↔ π possessum possessor

A relational noun such as topi 'hat' denotes a relation of possessum and possessor, and ber- suppresses the possessum, so that Tono bertopi says that Tono has some hat on. A sortal noun has one argument, and suppressing it leaves none for a subject.

The voice typology of Alexiadou and Schäfer (§7.3) #

def BeaversUdayana2022.meNParams :

Minimalist.Voice.Params

meN- corresponds to the thematic active voice.

Equations

BeaversUdayana2022.meNParams = Minimalist.Voice.agentive.params

Instances For

def BeaversUdayana2022.diParams :

Minimalist.Voice.Params

di- corresponds to the passive.

Equations

BeaversUdayana2022.diParams = Minimalist.Voice.passive.params

Instances For

def BeaversUdayana2022.berParams :

Minimalist.Voice.Params

ber- fixes neither whether a specifier is selected nor whether an agent is introduced.

Equations

BeaversUdayana2022.berParams = { hasD := none, thematic := none }

Instances For

theorem BeaversUdayana2022.berParams_compatible (v : Minimalist.Voice.Head) :

berParams.Compatible v.params ∧ ¬meNParams.Compatible diParams

ber- is compatible with every voice of the typology, and meN- and di- with each other are not.