Ozaki (2026): Japanese Accusative/Ablative Alternation Verbs Are Unaccusative

This file formalizes Ozaki's argument that the Japanese verbs of departure whose source argument is marked either accusative o or ablative kara, hanareru 'leave' and deru 'exit', project one dyadic unaccusative structure under both markings. The source is an argument whatever its marking, since it elides under an overt adjunct, the argumenthood diagnostic of Funakoshi, and scrambles long-distance, that of Saito; and the verbs project no thematic Voice (Kratzer) under either marking, since their passive is the indirect passive, the direct passive with niyotte being ungrammatical, and the accusative wh-adjunct nani-o 'why' of Kurafuji is unavailable, as with unaccusatives. Each diagnostic returns the same verdict for both markings (verdict, judgment_eq_verdict, diagnostics_both_markings). The alternation is then a matter of case assignment: kara is a lexical ablative assigned by an optional postposition, and o is the dependent accusative assigned to a caseless noun phrase c-commanded by another, which the ablative bleeds (acc_variant, abl_variant, accusative_without_voice).

Implementation notes

The examples are the generated rows of Data/Examples/Ozaki2026, the (9), (13), and (26) pairs split into an accusative and an ablative row. The case algorithm is the one-domain dependent-case assignment of Syntax/Case/Dependent, and the absence of thematic Voice is the non-thematic Voice head of Syntax/Minimalist/Verbal/Voice, which the Japanese Fragment records for both verbs and from which it derives their unaccusativity.

References

• [Oza26]
• [Fun16]
• [Sai85]
• [Kur97]
• [Kra96]

The diagnostics

def Ozaki2026.diagnostic (e : Datum) : Option String

The diagnostic an example applies.

Equations

• Ozaki2026.diagnostic e = e.feature? "diagnostic"

def Ozaki2026.marking (e : Datum) : Option String

The marking of the source in an example.

Equations

• Ozaki2026.marking e = e.feature? "marking"

def Ozaki2026.verdict : Option String → Judgment

The verdict the argument assigns to each diagnostic: the alternation, the argumenthood diagnostics, and the indirect passive succeed, the direct passive and the wh-adjunct fail.

Equations

• Ozaki2026.verdict (some "direct_passive") = Judgment.ungrammatical
• Ozaki2026.verdict (some "nani_o") = Judgment.ungrammatical
• Ozaki2026.verdict x✝ = Judgment.acceptable

theorem Ozaki2026.judgment_eq_verdict (e : Datum) : e ∈ Examples.all → e.judgment = verdict (diagnostic e)

Every example's judgment is its diagnostic's verdict: the marking of the source plays no role.

theorem Ozaki2026.diagnostics_both_markings (m : String) : m ∈ ["acc", "abl"] → (∃ e ∈ Examples.all, marking e = some m ∧ diagnostic e = some "ellipsis" ∧ e.judgment = Judgment.acceptable) ∧ (∃ e ∈ Examples.all, marking e = some m ∧ diagnostic e = some "scrambling" ∧ e.judgment = Judgment.acceptable) ∧ ∃ e ∈ Examples.all, marking e = some m ∧ diagnostic e = some "nani_o" ∧ e.judgment = Judgment.ungrammatical

Both markings are attested with each marking-sensitive diagnostic: the source elides and scrambles, and the wh-adjunct is out, under accusative and under ablative alike.

theorem Ozaki2026.alternation_verbs_unaccusative (v : Japanese.Verb) : v ∈ [Japanese.hanareru, Japanese.deru] → v.voiceType = some VoiceType.nonThematic ∧ v.IsUnaccusative ∧ v.passivizable = false

The Fragment records both verbs with non-thematic Voice, from which their unaccusativity is derived, and as non-passivizable.

theorem Ozaki2026.not_directPassivizable : ¬Japanese.DirectPassivizable Japanese.hanareru.toVerb ∧ ¬Minimalist.Voice.anticausative.AssignsTheta

The direct passive requires a verb introducing an external argument, which the non-thematic head does not provide: (20) is out.

Case assignment (§3)

inductive Ozaki2026.Participant : Type

The participants of hanareru 'leave': the leaver and the source, the leaver c-commanding the source in the one Spell-Out domain.

• leaver : Participant
• source : Participant

@[instance_reducible]

instance Ozaki2026.instDecidableEqParticipant : DecidableEq Participant

Equations

• Ozaki2026.instDecidableEqParticipant x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Ozaki2026.instReprParticipant.repr : Participant → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Ozaki2026.instReprParticipant : Repr Participant

Equations

• Ozaki2026.instReprParticipant = { reprPrec := Ozaki2026.instReprParticipant.repr }

def Ozaki2026.accVariant : Participant → Option Case

The accusative variant (28): leaver and source are caseless noun phrases.

Equations

• Ozaki2026.accVariant x✝ = none

def Ozaki2026.ablVariant : Participant → Option Case

The ablative variant (29): the postposition has valued the source ablative.

Equations

• Ozaki2026.ablVariant Ozaki2026.Participant.leaver = none
• Ozaki2026.ablVariant Ozaki2026.Participant.source = some Case.abl

def Ozaki2026.cases (lex : Participant → Option Case) : Case.Valuation Participant (Case × Case.Mechanism)

The cases of a variant.

Equations

• Ozaki2026.cases lex = DependentCase.assignCases Alignment.AlignmentType.accusative lex [Ozaki2026.Participant.leaver, Ozaki2026.Participant.source]

theorem Ozaki2026.acc_variant : Case.Valuation.valueOf Participant.source (cases accVariant) = some (Case.acc, Case.Mechanism.dependent) ∧ Case.Valuation.valueOf Participant.leaver (cases accVariant) = some (Case.nom, Case.Mechanism.unmarked)

In the accusative variant the source receives dependent accusative by (27) and the leaver unmarked nominative.

theorem Ozaki2026.abl_variant : Case.Valuation.valueOf Participant.source (cases ablVariant) = some (Case.abl, Case.Mechanism.lexical) ∧ Case.Valuation.valueOf Participant.leaver (cases ablVariant) = some (Case.nom, Case.Mechanism.unmarked)

In the ablative variant the lexical ablative bleeds dependent accusative, and the leaver is unaffected.

theorem Ozaki2026.accusative_without_voice : ¬Minimalist.Voice.anticausative.AssignsTheta ∧ Option.map (fun (x : Case × Case.Mechanism) => x.2) (Case.Valuation.valueOf Participant.source (cases accVariant)) = some Case.Mechanism.dependent

Accusative without thematic Voice: the non-thematic head assigns no θ-role, and the source's accusative is configurational rather than assigned by a functional head.