@cite{everdell-2023} — Applicativization in O'dam (Southeastern Tepiman)

Everdell, Michael. 2023. Arguments and adjuncts in O'dam: language-specific realization of a cross-linguistic distinction. PhD dissertation, University of Texas at Austin.

Chapter 5 formalizes O'dam applicativization, which provides evidence that thematic hierarchies cannot be fully eliminated from argument realization theory — a key counterpoint to purely content-based linking (MAP alone).

Core claims

1. O'dam has two applicative suffixes: -dha and -tuda, which are specific about which verbs they combine with and which function they serve. Unlike Kinyarwanda -ish, O'dam applicatives are unambiguous in their function with a given verb.

2. Thematic hierarchy of applied arguments (the dissertation's (273)):

   Agent > Promoted object [+ANIM] > Beneficiary
   

   The applied argument's thematic role is hierarchically determined: agent-introduction takes priority over promotion, which takes priority over beneficiary introduction. Beneficiary is the elsewhere case.

3. Applicative function is predictable from two properties of the base verb: (a) its transitivity and (b) its semantic participants.

4. Animacy entailment is the consistent semantic contribution of promotion. Unlike Kinyarwanda (which adds change-of-possession), O'dam promotion simply adds an animacy entailment to the promoted participant. Benefactive/malefactive inferences are pragmatic.

5. Applicativization is a valency test: the applied form always has valency = base valency + 1. This explains the hypertransitivity ban: ditransitives (makia' 'give', tikka' 'ask') cannot be applicativized because O'dam caps syntactic arguments at three.

6. Locatives are always adjuncts: they don't count toward transitivity, evidenced by motion verbs behaving as intransitives under applicativization.

7. Instruments are always adjuncts AND always inanimate: they cannot be promoted because promotion requires animacy, and instruments in O'dam are categorically inanimate.

Cross-references

• Studies/Pylkkanen2008.lean: O'dam applicatives don't fit the high/low dichotomy cleanly — they perform agent-introduction (high-like), promotion, AND beneficiary licensing depending on the base verb.
• Studies/Beavers2010.lean: The affectedness hierarchy and MAP operate on direct/oblique alternations. O'dam shows a different dimension of argument realization: thematic hierarchies governing which participant gets promoted by an applicative.
• Studies/BeaversUdayana2022.lean: Indonesian ber- middles suppress arguments; O'dam -dha and -tuda ADD arguments. Both are valency operations that probe base argument structure.

inductive Phenomena.ArgumentStructure.Studies.Everdell2024.BaseTransitivity : Type

Base transitivity of an O'dam verb. Everdell's analysis treats motion verbs with only a locative participant as intransitive (the locative is an adjunct).

• intransitive : BaseTransitivity
• transitive : BaseTransitivity
• ditransitive : BaseTransitivity

instance Phenomena.ArgumentStructure.Studies.Everdell2024.instDecidableEqBaseTransitivity : DecidableEq BaseTransitivity

Equations

• Phenomena.ArgumentStructure.Studies.Everdell2024.instDecidableEqBaseTransitivity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.ArgumentStructure.Studies.Everdell2024.instBEqBaseTransitivity : BEq BaseTransitivity

Equations

• Phenomena.ArgumentStructure.Studies.Everdell2024.instBEqBaseTransitivity = { beq := Phenomena.ArgumentStructure.Studies.Everdell2024.instBEqBaseTransitivity.beq }

def Phenomena.ArgumentStructure.Studies.Everdell2024.instBEqBaseTransitivity.beq : BaseTransitivity → BaseTransitivity → Bool

Equations

• Phenomena.ArgumentStructure.Studies.Everdell2024.instBEqBaseTransitivity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.ArgumentStructure.Studies.Everdell2024.instReprBaseTransitivity : Repr BaseTransitivity

Equations

• Phenomena.ArgumentStructure.Studies.Everdell2024.instReprBaseTransitivity = { reprPrec := Phenomena.ArgumentStructure.Studies.Everdell2024.instReprBaseTransitivity.repr }

def Phenomena.ArgumentStructure.Studies.Everdell2024.instReprBaseTransitivity.repr : BaseTransitivity → ℕ → Std.Format

Equations

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

inductive Phenomena.ArgumentStructure.Studies.Everdell2024.EntailedParticipantType : Type

The type of non-argument entailed participant (if any) that a transitive verb has. These are participants entailed by the verb's semantics but NOT syntactic arguments of the base form.

• implicitObject : EntailedParticipantType
• locative : EntailedParticipantType
• instrument : EntailedParticipantType
• none : EntailedParticipantType

instance Phenomena.ArgumentStructure.Studies.Everdell2024.instDecidableEqEntailedParticipantType : DecidableEq EntailedParticipantType

Equations

• Phenomena.ArgumentStructure.Studies.Everdell2024.instDecidableEqEntailedParticipantType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.ArgumentStructure.Studies.Everdell2024.instBEqEntailedParticipantType.beq : EntailedParticipantType → EntailedParticipantType → Bool

Equations

• Phenomena.ArgumentStructure.Studies.Everdell2024.instBEqEntailedParticipantType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.ArgumentStructure.Studies.Everdell2024.instBEqEntailedParticipantType : BEq EntailedParticipantType

Equations

• Phenomena.ArgumentStructure.Studies.Everdell2024.instBEqEntailedParticipantType = { beq := Phenomena.ArgumentStructure.Studies.Everdell2024.instBEqEntailedParticipantType.beq }

def Phenomena.ArgumentStructure.Studies.Everdell2024.instReprEntailedParticipantType.repr : EntailedParticipantType → ℕ → Std.Format

Equations

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

instance Phenomena.ArgumentStructure.Studies.Everdell2024.instReprEntailedParticipantType : Repr EntailedParticipantType

Equations

• Phenomena.ArgumentStructure.Studies.Everdell2024.instReprEntailedParticipantType = { reprPrec := Phenomena.ArgumentStructure.Studies.Everdell2024.instReprEntailedParticipantType.repr }

inductive Phenomena.ArgumentStructure.Studies.Everdell2024.AnimateCompatibility : Type

Whether a locative participant is compatible with an animate referent. This determines whether the locative can be promoted by an applicative, since promotion requires adding an animacy entailment.

• compatible : AnimateCompatibility
• incompatible : AnimateCompatibility

instance Phenomena.ArgumentStructure.Studies.Everdell2024.instDecidableEqAnimateCompatibility : DecidableEq AnimateCompatibility

Equations

• Phenomena.ArgumentStructure.Studies.Everdell2024.instDecidableEqAnimateCompatibility x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.ArgumentStructure.Studies.Everdell2024.instBEqAnimateCompatibility : BEq AnimateCompatibility

Equations

• Phenomena.ArgumentStructure.Studies.Everdell2024.instBEqAnimateCompatibility = { beq := Phenomena.ArgumentStructure.Studies.Everdell2024.instBEqAnimateCompatibility.beq }

def Phenomena.ArgumentStructure.Studies.Everdell2024.instBEqAnimateCompatibility.beq : AnimateCompatibility → AnimateCompatibility → Bool

Equations

• Phenomena.ArgumentStructure.Studies.Everdell2024.instBEqAnimateCompatibility.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.ArgumentStructure.Studies.Everdell2024.instReprAnimateCompatibility : Repr AnimateCompatibility

Equations

• Phenomena.ArgumentStructure.Studies.Everdell2024.instReprAnimateCompatibility = { reprPrec := Phenomena.ArgumentStructure.Studies.Everdell2024.instReprAnimateCompatibility.repr }

def Phenomena.ArgumentStructure.Studies.Everdell2024.instReprAnimateCompatibility.repr : AnimateCompatibility → ℕ → Std.Format

Equations

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

inductive Phenomena.ArgumentStructure.Studies.Everdell2024.VerbClass : Type

Semantic class of an O'dam verb, relevant to applicativization.

• unaccusative : VerbClass
• unergative : VerbClass
• motionIntransitive : VerbClass
• ingestion : VerbClass
• perception : VerbClass
• lexicalMiddle : VerbClass
• simpleTransitive : VerbClass
• denominalCreation : VerbClass
• ditransitive : VerbClass

instance Phenomena.ArgumentStructure.Studies.Everdell2024.instDecidableEqVerbClass : DecidableEq VerbClass

Equations

• Phenomena.ArgumentStructure.Studies.Everdell2024.instDecidableEqVerbClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.ArgumentStructure.Studies.Everdell2024.instBEqVerbClass.beq : VerbClass → VerbClass → Bool

Equations

• Phenomena.ArgumentStructure.Studies.Everdell2024.instBEqVerbClass.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.ArgumentStructure.Studies.Everdell2024.instBEqVerbClass : BEq VerbClass

Equations

• Phenomena.ArgumentStructure.Studies.Everdell2024.instBEqVerbClass = { beq := Phenomena.ArgumentStructure.Studies.Everdell2024.instBEqVerbClass.beq }

instance Phenomena.ArgumentStructure.Studies.Everdell2024.instReprVerbClass : Repr VerbClass

Equations

• Phenomena.ArgumentStructure.Studies.Everdell2024.instReprVerbClass = { reprPrec := Phenomena.ArgumentStructure.Studies.Everdell2024.instReprVerbClass.repr }

def Phenomena.ArgumentStructure.Studies.Everdell2024.instReprVerbClass.repr : VerbClass → ℕ → Std.Format

Equations

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

structure Phenomena.ArgumentStructure.Studies.Everdell2024.OdamVerb : Type

An O'dam verb entry for applicativization analysis.

• baseForm : String

  Base form (citation)

• gloss : String

  Gloss

• appliedForm : String

  Applied form (with -dha or -tuda)

• verbClass : VerbClass

  Verb class

• transitivity : BaseTransitivity

  Syntactic transitivity of the base form

• entailedParticipant : EntailedParticipantType

  Type of entailed non-argument participant (if any)

• animateLocative : AnimateCompatibility

  Whether the locative (if any) is compatible with an animate referent

instance Phenomena.ArgumentStructure.Studies.Everdell2024.instReprOdamVerb : Repr OdamVerb

Equations

• Phenomena.ArgumentStructure.Studies.Everdell2024.instReprOdamVerb = { reprPrec := Phenomena.ArgumentStructure.Studies.Everdell2024.instReprOdamVerb.repr }

def Phenomena.ArgumentStructure.Studies.Everdell2024.instReprOdamVerb.repr : OdamVerb → ℕ → Std.Format

Equations

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

instance Phenomena.ArgumentStructure.Studies.Everdell2024.instBEqOdamVerb : BEq OdamVerb

Equations

• Phenomena.ArgumentStructure.Studies.Everdell2024.instBEqOdamVerb = { beq := Phenomena.ArgumentStructure.Studies.Everdell2024.instBEqOdamVerb.beq }

def Phenomena.ArgumentStructure.Studies.Everdell2024.instBEqOdamVerb.beq : OdamVerb → OdamVerb → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.ArgumentStructure.Studies.Everdell2024.instBEqOdamVerb.beq x✝¹ x✝ = false

inductive Phenomena.ArgumentStructure.Studies.Everdell2024.ApplFunction : Type

The function an O'dam applicative performs with a given verb.

These are ordered by the thematic hierarchy (273): Agent > Promoted object [+ANIM] > Beneficiary.

blocked covers the hypertransitivity ban (ditransitives).

• agentIntroduction : ApplFunction
• promotion : ApplFunction
• beneficiary : ApplFunction
• blocked : ApplFunction

instance Phenomena.ArgumentStructure.Studies.Everdell2024.instDecidableEqApplFunction : DecidableEq ApplFunction

Equations

• Phenomena.ArgumentStructure.Studies.Everdell2024.instDecidableEqApplFunction x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.ArgumentStructure.Studies.Everdell2024.instBEqApplFunction : BEq ApplFunction

Equations

• Phenomena.ArgumentStructure.Studies.Everdell2024.instBEqApplFunction = { beq := Phenomena.ArgumentStructure.Studies.Everdell2024.instBEqApplFunction.beq }

def Phenomena.ArgumentStructure.Studies.Everdell2024.instBEqApplFunction.beq : ApplFunction → ApplFunction → Bool

Equations

• Phenomena.ArgumentStructure.Studies.Everdell2024.instBEqApplFunction.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.ArgumentStructure.Studies.Everdell2024.instReprApplFunction : Repr ApplFunction

Equations

• Phenomena.ArgumentStructure.Studies.Everdell2024.instReprApplFunction = { reprPrec := Phenomena.ArgumentStructure.Studies.Everdell2024.instReprApplFunction.repr }

def Phenomena.ArgumentStructure.Studies.Everdell2024.instReprApplFunction.repr : ApplFunction → ℕ → Std.Format

Equations

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

def Phenomena.ArgumentStructure.Studies.Everdell2024.predictFunction (v : OdamVerb) : ApplFunction

The central prediction: the applicative's function is determined by the base verb's transitivity and entailed participants.

This implements Everdell's thematic hierarchy (273):

1. If the base is intransitive → agent introduction
2. If the base is transitive AND has a promotable participant → promotion
3. If the base is transitive AND has no promotable participant → beneficiary
4. If the base is ditransitive → blocked

A participant is "promotable" if it is either:

• An implicit object (not expressible in base form), OR
• A locative compatible with an animate interpretation

Instruments are NEVER promotable: they are inanimate in O'dam, and promotion adds an animacy entailment.

Equations

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

def Phenomena.ArgumentStructure.Studies.Everdell2024.effectiveTransitivity (v : OdamVerb) : BaseTransitivity

"Exceptional transitives" (ingestion, perception, lexical middles) are syntactically transitive but pattern with intransitives under applicativization because their subject is not maximally distinct from the object.

This function computes the effective transitivity for applicativization purposes.

Equations

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

def Phenomena.ArgumentStructure.Studies.Everdell2024.predictFunctionRefined (v : OdamVerb) : ApplFunction

The refined prediction accounting for exceptional transitives.

Equations

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

def Phenomena.ArgumentStructure.Studies.Everdell2024.tuklhia : OdamVerb

Equations

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

def Phenomena.ArgumentStructure.Studies.Everdell2024.koxia : OdamVerb

Equations

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

def Phenomena.ArgumentStructure.Studies.Everdell2024.miiya_burn : OdamVerb

Equations

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

def Phenomena.ArgumentStructure.Studies.Everdell2024.miiya_ignite : OdamVerb

Equations

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

def Phenomena.ArgumentStructure.Studies.Everdell2024.tisdia : OdamVerb

Equations

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

def Phenomena.ArgumentStructure.Studies.Everdell2024.aaya : OdamVerb

Equations

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

def Phenomena.ArgumentStructure.Studies.Everdell2024.kikbo : OdamVerb

Equations

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

def Phenomena.ArgumentStructure.Studies.Everdell2024.bhaya_swallow : OdamVerb

Ingestion verbs: syntactically transitive but applicativize like intransitives because subject is not maximally distinct from object.

Equations

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

def Phenomena.ArgumentStructure.Studies.Everdell2024.iya_drink : OdamVerb

Equations

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

def Phenomena.ArgumentStructure.Studies.Everdell2024.tigia_see : OdamVerb

Perception verbs: also transitive but pattern intransitively.

Equations

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

def Phenomena.ArgumentStructure.Studies.Everdell2024.kaaya_hear : OdamVerb

Equations

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

def Phenomena.ArgumentStructure.Studies.Everdell2024.saabu_fast : OdamVerb

Lexical middles: subject and object are co-identified.

Equations

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

def Phenomena.ArgumentStructure.Studies.Everdell2024.namkia_meet : OdamVerb

Equations

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

def Phenomena.ArgumentStructure.Studies.Everdell2024.tulhiina_suffer : OdamVerb

Equations

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

def Phenomena.ArgumentStructure.Studies.Everdell2024.oncho_hide : OdamVerb

Equations

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

def Phenomena.ArgumentStructure.Studies.Everdell2024.gara_sell : OdamVerb

Verbs with implicit objects (promoted by applicative).

Equations

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

def Phenomena.ArgumentStructure.Studies.Everdell2024.jotsa_send : OdamVerb

Equations

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

def Phenomena.ArgumentStructure.Studies.Everdell2024.aga_say : OdamVerb

Equations

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

def Phenomena.ArgumentStructure.Studies.Everdell2024.bua_throw : OdamVerb

Verbs with locative participants compatible with animate referents (promoted to object with animacy entailment).

Equations

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

def Phenomena.ArgumentStructure.Studies.Everdell2024.baabu_take_out : OdamVerb

Equations

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

def Phenomena.ArgumentStructure.Studies.Everdell2024.nuina_push : OdamVerb

Equations

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

def Phenomena.ArgumentStructure.Studies.Everdell2024.mukda_sharpen : OdamVerb

Equations

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

def Phenomena.ArgumentStructure.Studies.Everdell2024.sooma_sew : OdamVerb

Equations

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

def Phenomena.ArgumentStructure.Studies.Everdell2024.sarna_tear : OdamVerb

Equations

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

def Phenomena.ArgumentStructure.Studies.Everdell2024.uana_clean : OdamVerb

Equations

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

def Phenomena.ArgumentStructure.Studies.Everdell2024.uana_write : OdamVerb

Equations

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

def Phenomena.ArgumentStructure.Studies.Everdell2024.kuagia_cut_firewood : OdamVerb

Transitive with entailed instrument (not promotable).

Equations

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

def Phenomena.ArgumentStructure.Studies.Everdell2024.bulhia_tie : OdamVerb

Equations

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

def Phenomena.ArgumentStructure.Studies.Everdell2024.bakta_hang : OdamVerb

Transitive with locative incompatible with animate referent.

Equations

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

def Phenomena.ArgumentStructure.Studies.Everdell2024.gammu_put_inside : OdamVerb

Equations

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

def Phenomena.ArgumentStructure.Studies.Everdell2024.makia_give : OdamVerb

Equations

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

def Phenomena.ArgumentStructure.Studies.Everdell2024.tikka_ask : OdamVerb

Equations

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

def Phenomena.ArgumentStructure.Studies.Everdell2024.junmada_make_mole : OdamVerb

Denominal verbs of creation: syntactically transitive (they take the resultative -xim) but gain a beneficiary, not an agent. The incorporated noun satisfies one thematic role.

Equations

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

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.tuklhia_gains_agent : predictFunction tuklhia = ApplFunction.agentIntroduction

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.koxia_gains_agent : predictFunction koxia = ApplFunction.agentIntroduction

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.miiya_burn_gains_agent : predictFunction miiya_burn = ApplFunction.agentIntroduction

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.tisdia_gains_agent : predictFunction tisdia = ApplFunction.agentIntroduction

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.aaya_gains_agent : predictFunction aaya = ApplFunction.agentIntroduction

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.kikbo_gains_agent : predictFunction kikbo = ApplFunction.agentIntroduction

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.bhaya_refined_agent : predictFunctionRefined bhaya_swallow = ApplFunction.agentIntroduction

Ingestion: syntactically transitive, but the refined predictor recognizes it as effectively intransitive.

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.iya_refined_agent : predictFunctionRefined iya_drink = ApplFunction.agentIntroduction

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.tigia_refined_agent : predictFunctionRefined tigia_see = ApplFunction.agentIntroduction

Perception: same pattern.

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.kaaya_refined_agent : predictFunctionRefined kaaya_hear = ApplFunction.agentIntroduction

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.saabu_refined_agent : predictFunctionRefined saabu_fast = ApplFunction.agentIntroduction

Lexical middles: same pattern.

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.namkia_refined_agent : predictFunctionRefined namkia_meet = ApplFunction.agentIntroduction

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.tulhiina_refined_agent : predictFunctionRefined tulhiina_suffer = ApplFunction.agentIntroduction

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.oncho_refined_agent : predictFunctionRefined oncho_hide = ApplFunction.agentIntroduction

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.naive_wrong_for_exceptionals : predictFunction bhaya_swallow = ApplFunction.beneficiary ∧ predictFunction tigia_see = ApplFunction.beneficiary ∧ predictFunction saabu_fast = ApplFunction.beneficiary

The naive predictor gets exceptional transitives WRONG — it would predict beneficiary, not agent. This motivates the refined predictor.

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.gara_promotes : predictFunction gara_sell = ApplFunction.promotion

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.jotsa_promotes : predictFunction jotsa_send = ApplFunction.promotion

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.aga_promotes : predictFunction aga_say = ApplFunction.promotion

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.bua_promotes : predictFunction bua_throw = ApplFunction.promotion

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.baabu_promotes : predictFunction baabu_take_out = ApplFunction.promotion

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.nuina_promotes : predictFunction nuina_push = ApplFunction.promotion

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.mukda_gets_beneficiary : predictFunction mukda_sharpen = ApplFunction.beneficiary

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.sooma_gets_beneficiary : predictFunction sooma_sew = ApplFunction.beneficiary

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.sarna_gets_beneficiary : predictFunction sarna_tear = ApplFunction.beneficiary

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.uana_gets_beneficiary : predictFunction uana_clean = ApplFunction.beneficiary

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.uana_write_gets_beneficiary : predictFunction uana_write = ApplFunction.beneficiary

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.kuagia_instrument_not_promoted : predictFunction kuagia_cut_firewood = ApplFunction.beneficiary

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.bulhia_instrument_not_promoted : predictFunction bulhia_tie = ApplFunction.beneficiary

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.bakta_inanimate_loc_not_promoted : predictFunction bakta_hang = ApplFunction.beneficiary

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.gammu_inanimate_loc_not_promoted : predictFunction gammu_put_inside = ApplFunction.beneficiary

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.junmada_gets_beneficiary : predictFunction junmada_make_mole = ApplFunction.beneficiary

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.makia_blocked : predictFunction makia_give = ApplFunction.blocked

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.tikka_blocked : predictFunction tikka_ask = ApplFunction.blocked

structure Phenomena.ArgumentStructure.Studies.Everdell2024.ApplDatum : Type

The observed applicative function for each verb.

• verb : OdamVerb
• observedFunction : ApplFunction

def Phenomena.ArgumentStructure.Studies.Everdell2024.instReprApplDatum.repr : ApplDatum → ℕ → Std.Format

Equations

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

instance Phenomena.ArgumentStructure.Studies.Everdell2024.instReprApplDatum : Repr ApplDatum

Equations

• Phenomena.ArgumentStructure.Studies.Everdell2024.instReprApplDatum = { reprPrec := Phenomena.ArgumentStructure.Studies.Everdell2024.instReprApplDatum.repr }

instance Phenomena.ArgumentStructure.Studies.Everdell2024.instBEqApplDatum : BEq ApplDatum

Equations

• Phenomena.ArgumentStructure.Studies.Everdell2024.instBEqApplDatum = { beq := Phenomena.ArgumentStructure.Studies.Everdell2024.instBEqApplDatum.beq }

def Phenomena.ArgumentStructure.Studies.Everdell2024.instBEqApplDatum.beq : ApplDatum → ApplDatum → Bool

Equations

• Phenomena.ArgumentStructure.Studies.Everdell2024.instBEqApplDatum.beq { verb := a, observedFunction := a_1 } { verb := b, observedFunction := b_1 } = (a == b && a_1 == b_1)
• Phenomena.ArgumentStructure.Studies.Everdell2024.instBEqApplDatum.beq x✝¹ x✝ = false

def Phenomena.ArgumentStructure.Studies.Everdell2024.allData : List ApplDatum

Equations

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

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.prediction_matches_all_nonexceptional : (allData.all fun (d : ApplDatum) => predictFunction d.verb == d.observedFunction) = true

The deepest theorem: predictFunction matches the observed applicative function for all non-exceptional verbs.

The prediction succeeds for all verbs that are NOT exceptional transitives (ingestion, perception, lexical middles). For those, predictFunctionRefined is needed.

def Phenomena.ArgumentStructure.Studies.Everdell2024.baseValency : BaseTransitivity → ℕ

Valency change is always +1. The applied form has exactly one more syntactic argument than the base.

Equations

• Phenomena.ArgumentStructure.Studies.Everdell2024.baseValency Phenomena.ArgumentStructure.Studies.Everdell2024.BaseTransitivity.intransitive = 1
• Phenomena.ArgumentStructure.Studies.Everdell2024.baseValency Phenomena.ArgumentStructure.Studies.Everdell2024.BaseTransitivity.transitive = 2
• Phenomena.ArgumentStructure.Studies.Everdell2024.baseValency Phenomena.ArgumentStructure.Studies.Everdell2024.BaseTransitivity.ditransitive = 3

def Phenomena.ArgumentStructure.Studies.Everdell2024.appliedValency (v : OdamVerb) : Option ℕ

Equations

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

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.intransitive_becomes_transitive : appliedValency tuklhia = some 2

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.transitive_becomes_ditransitive : appliedValency mukda_sharpen = some 3

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.ditransitive_is_blocked : appliedValency makia_give = none

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.no_hypertransitivity (v : OdamVerb) (h : v.transitivity = BaseTransitivity.ditransitive) : predictFunction v = ApplFunction.blocked

The hypertransitivity ban: no verb can have more than 3 syntactic arguments. This follows from the fact that ditransitives cannot applicativize and the +1 valency change.

def Phenomena.ArgumentStructure.Studies.Everdell2024.isPromotable : EntailedParticipantType → AnimateCompatibility → Bool

Whether a participant type is promotable by the applicative. Promotion requires adding an animacy entailment. Instruments are categorically inanimate in O'dam, so they cannot be promoted.

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.ArgumentStructure.Studies.Everdell2024.isPromotable Phenomena.ArgumentStructure.Studies.Everdell2024.EntailedParticipantType.implicitObject x✝ = true
• Phenomena.ArgumentStructure.Studies.Everdell2024.isPromotable Phenomena.ArgumentStructure.Studies.Everdell2024.EntailedParticipantType.instrument x✝ = false
• Phenomena.ArgumentStructure.Studies.Everdell2024.isPromotable Phenomena.ArgumentStructure.Studies.Everdell2024.EntailedParticipantType.none x✝ = false

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.instruments_never_promotable (ac : AnimateCompatibility) : isPromotable EntailedParticipantType.instrument ac = false

Instruments are never promotable.

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.implicit_objects_always_promotable (ac : AnimateCompatibility) : isPromotable EntailedParticipantType.implicitObject ac = true

Implicit objects are always promotable.

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.animate_locatives_promotable : isPromotable EntailedParticipantType.locative AnimateCompatibility.compatible = true

Animate-compatible locatives are promotable.

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.inanimate_locatives_not_promotable : isPromotable EntailedParticipantType.locative AnimateCompatibility.incompatible = false

Inanimate locatives are not promotable.

def Phenomena.ArgumentStructure.Studies.Everdell2024.isExceptionalTransitive : VerbClass → Bool

The exceptional transitive classes are exactly those where the subject is not maximally distinct from the object.

This captures @cite{naess-2007}'s observation: ingestion/perception verbs and lexical middles minimize the affector-affectee distinction, making them functionally intransitive.

Equations

• Phenomena.ArgumentStructure.Studies.Everdell2024.isExceptionalTransitive Phenomena.ArgumentStructure.Studies.Everdell2024.VerbClass.ingestion = true
• Phenomena.ArgumentStructure.Studies.Everdell2024.isExceptionalTransitive Phenomena.ArgumentStructure.Studies.Everdell2024.VerbClass.perception = true
• Phenomena.ArgumentStructure.Studies.Everdell2024.isExceptionalTransitive Phenomena.ArgumentStructure.Studies.Everdell2024.VerbClass.lexicalMiddle = true
• Phenomena.ArgumentStructure.Studies.Everdell2024.isExceptionalTransitive x✝ = false

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.exceptionals_are_transitive : bhaya_swallow.transitivity = BaseTransitivity.transitive ∧ tigia_see.transitivity = BaseTransitivity.transitive ∧ saabu_fast.transitivity = BaseTransitivity.transitive

Exceptional transitives are syntactically transitive.

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.exceptionals_effectively_intransitive : effectiveTransitivity bhaya_swallow = BaseTransitivity.intransitive ∧ effectiveTransitivity tigia_see = BaseTransitivity.intransitive ∧ effectiveTransitivity saabu_fast = BaseTransitivity.intransitive

But they are effectively intransitive for applicativization.

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.predictFunction_depends_only (v w : OdamVerb) (ht : v.transitivity = w.transitivity) (he : v.entailedParticipant = w.entailedParticipant) (ha : v.animateLocative = w.animateLocative) : predictFunction v = predictFunction w

predictFunction depends only on transitivity, entailedParticipant, and animateLocative.

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.refined_agrees_on_nonexceptional (v : OdamVerb) (h : isExceptionalTransitive v.verbClass = false) : predictFunctionRefined v = predictFunction v

predictFunctionRefined agrees with predictFunction on all non-exceptional verb classes. The refinement only changes the prediction for ingestion, perception, and lexical middles.

@cite{krejci-2012} proposes a hierarchy of causativizability:

    unaccusatives > middles/ingestives > unergatives > simple transitives

O'dam's exceptional transitives are exactly middles and ingestives —
the verb classes that cross-linguistically pattern with intransitives
in causativization. This explains why O'dam applicatives (which are
syncretic with causatives) treat them as intransitive:
causative-applicative syncretism + the causativizability hierarchy
predicts the exceptional transitive class.

The hierarchy data and implicational validation are formalized in
`Semantics.Causation.MorphologicalCausation` (§11). 

O'dam applicatives challenge the @cite{pylkknen-2008} binary high/low classification. They exhibit properties of BOTH types:

- **High-like**: can applicativize unergatives (agent introduction)
  and static verbs (lexical middles gain agents)
- **Low-like**: can promote a locative to an applied object with
  a transfer-like interpretation

However, O'dam applicatives are NOT ambiguous in the way Kinyarwanda
*-ish* is: with a given verb, the function is deterministic. 

def Phenomena.ArgumentStructure.Studies.Everdell2024.odam_appl : Pylkkanen2008.ApplClassification

O'dam passes both high-applicative diagnostics from Table 2.1.

Equations

• Phenomena.ArgumentStructure.Studies.Everdell2024.odam_appl = { language := "O'dam", applType := Minimalism.ApplType.high, unergativeOK := some true, staticVerbOK := some true }

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.odam_diagnostics_predict_high : Pylkkanen2008.diagnosticPredictsHigh odam_appl = true

O'dam patterns as high by the diagnostics.

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.odam_also_promotes : predictFunction jotsa_send = ApplFunction.promotion ∧ predictFunction baabu_take_out = ApplFunction.promotion

But O'dam also performs promotion (a low-like function). The dissertation shows this dual behavior is NOT ambiguity — the function is deterministic based on the base verb. This suggests that high/low is not a single binary parameter but a cluster of partially independent properties.

@cite{beavers-2023-sag-lectures} argues that argument realization is governed by a "soup" of factors: truth-conditional strength (MAP), event-structural templates, convention, and discourse/pragmatics. Beavers acknowledges that thematic hierarchies play SOME role but argues they are largely reducible to truth-conditional content.

O'dam applicatives provide evidence that the thematic hierarchy
(273) is NOT fully reducible to content:

1. The hierarchy Agent > Promoted [+ANIM] > Beneficiary determines
   which applicative function is selected, NOT the truth-conditional
   strength of the applied argument.

2. Instruments cannot be promoted even though they may be entailed
   (truth-conditionally strong) — the blocking comes from a
   representational property (animacy), not from content-based MAP.

3. The exceptional transitives (ingestion, perception, middles) are
   blocked from beneficiary licensing by a representational property
   (subject-object distinctness), not by content strength.

This makes O'dam a key test case for the "soup" theory: thematic
hierarchies are one ingredient that cannot be fully eliminated. 

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.hierarchy_deterministic : predictFunction gara_sell = ApplFunction.promotion ∧ predictFunction jotsa_send = ApplFunction.promotion ∧ predictFunction mukda_sharpen = ApplFunction.beneficiary ∧ predictFunction sooma_sew = ApplFunction.beneficiary

The thematic hierarchy makes a prediction that pure MAP cannot: the same verb form (sell, send) always promotes the same participant, regardless of context or truth-conditional strength of other potential applied arguments. See §19 for the deeper analysis of why this is orthogonal to MAP.

A central claim: locative participants in O'dam are ALWAYS syntactic adjuncts. Evidence:

1. Motion verbs with one non-locative participant (e.g., *aaya'*
   'arrive') are intransitive under applicativization — they gain
   an agent, not a beneficiary.

2. Motion verbs with two non-locative participants are transitive —
   the locative doesn't count toward valency.

3. Under the promotative function, entailed locatives are promoted
   to object status, gaining an animacy entailment. If locatives
   were already arguments, promotion of an argument to... argument
   would be incoherent.

This connects to head-marking and preverbal quantification (Ch. 3–4):
locatives fail every argumenthood test in O'dam. 

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.motion_verbs_intransitive : tisdia.transitivity = BaseTransitivity.intransitive ∧ aaya.transitivity = BaseTransitivity.intransitive

Motion verbs are intransitive despite having locative participants. Their locatives are adjuncts, so they don't count toward valency.

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.motion_verbs_gain_agents : predictFunction tisdia = ApplFunction.agentIntroduction ∧ predictFunction aaya = ApplFunction.agentIntroduction

Therefore motion verbs gain agents under applicativization, just like other intransitives.

O'dam applicative promotion is orthogonal to MAP. MAP governs direct/oblique alternations based on truth-conditional strength (affectedness degree). O'dam promotion is governed by animacy, a representational property independent of change-of-state entailments.

This creates a two-dimensional space for argument realization:

| Dimension        | Governing property     | Framework       |
|------------------|------------------------|-----------------|
| Direct vs oblique| Truth-conditional strength| MAP (Beavers)  |
| Promoted vs not  | Animacy compatibility  | Hierarchy (273) |

Instruments can be truth-conditionally strong (entailed by the
verb) but STILL not promotable, because they are categorically
inanimate. This is a content-independent constraint that MAP
cannot capture. 

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.promotion_orthogonal_to_entailment : kuagia_cut_firewood.entailedParticipant = EntailedParticipantType.instrument ∧ predictFunction kuagia_cut_firewood = ApplFunction.beneficiary ∧ bulhia_tie.entailedParticipant = EntailedParticipantType.instrument ∧ predictFunction bulhia_tie = ApplFunction.beneficiary

Instruments are entailed (potentially high affectedness) but not promotable. This witnesses a dimension of argument realization orthogonal to MAP: animacy governs promotion, not truth-conditional strength.

theorem Phenomena.ArgumentStructure.Studies.Everdell2024.animacy_gates_promotion : baabu_take_out.entailedParticipant = EntailedParticipantType.locative ∧ baabu_take_out.animateLocative = AnimateCompatibility.compatible ∧ predictFunction baabu_take_out = ApplFunction.promotion ∧ bakta_hang.entailedParticipant = EntailedParticipantType.locative ∧ bakta_hang.animateLocative = AnimateCompatibility.incompatible ∧ predictFunction bakta_hang = ApplFunction.beneficiary

The thematic hierarchy makes categorical predictions that cannot be derived from truth-conditional strength alone: the SAME type of entailed participant (locative) gets different treatment based solely on animate compatibility.