Unaccusativity Diagnostic Data

@cite{burzio-1986} @cite{levin-hovav-1995} @cite{storment-2026}

Theory-neutral empirical data on unaccusativity diagnostics.

Diagnostics

• Quotative inversion (QI): "whispered Mary" vs *"spoke Mary" (@cite{storment-2026}, NLLT)
• There-insertion: "there arrived a letter" vs *"there ran a man"
• Locative inversion: "into the room walked a man"
• Resultative predication: "the river froze solid" vs *"John ran tired"
• Auxiliary selection: Italian è arrivato (be) vs ha dormito (have)

inductive Phenomena.ArgumentStructure.Unaccusativity.Data.Diagnostic : Type

Syntactic diagnostics for unaccusativity.

• quotativeInversion : Diagnostic
• thereInsertion : Diagnostic
• locativeInversion : Diagnostic
• resultativePredication : Diagnostic
• auxiliarySelection : Diagnostic
• passiveType : Diagnostic
• whAdjunctBlocking : Diagnostic

instance Phenomena.ArgumentStructure.Unaccusativity.Data.instDecidableEqDiagnostic : DecidableEq Diagnostic

Equations

• Phenomena.ArgumentStructure.Unaccusativity.Data.instDecidableEqDiagnostic x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.ArgumentStructure.Unaccusativity.Data.instReprDiagnostic.repr : Diagnostic → Nat → Std.Format

Equations

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

instance Phenomena.ArgumentStructure.Unaccusativity.Data.instReprDiagnostic : Repr Diagnostic

Equations

• Phenomena.ArgumentStructure.Unaccusativity.Data.instReprDiagnostic = { reprPrec := Phenomena.ArgumentStructure.Unaccusativity.Data.instReprDiagnostic.repr }

def Phenomena.ArgumentStructure.Unaccusativity.Data.instBEqDiagnostic.beq : Diagnostic → Diagnostic → Bool

Equations

• Phenomena.ArgumentStructure.Unaccusativity.Data.instBEqDiagnostic.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.ArgumentStructure.Unaccusativity.Data.instBEqDiagnostic : BEq Diagnostic

Equations

• Phenomena.ArgumentStructure.Unaccusativity.Data.instBEqDiagnostic = { beq := Phenomena.ArgumentStructure.Unaccusativity.Data.instBEqDiagnostic.beq }

inductive Phenomena.ArgumentStructure.Unaccusativity.Data.DiagnosticResult : Type

Result of applying a diagnostic to a verb.

• passes : DiagnosticResult
• fails : DiagnosticResult
• marginal : DiagnosticResult

instance Phenomena.ArgumentStructure.Unaccusativity.Data.instDecidableEqDiagnosticResult : DecidableEq DiagnosticResult

Equations

• Phenomena.ArgumentStructure.Unaccusativity.Data.instDecidableEqDiagnosticResult x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.ArgumentStructure.Unaccusativity.Data.instReprDiagnosticResult : Repr DiagnosticResult

Equations

• Phenomena.ArgumentStructure.Unaccusativity.Data.instReprDiagnosticResult = { reprPrec := Phenomena.ArgumentStructure.Unaccusativity.Data.instReprDiagnosticResult.repr }

def Phenomena.ArgumentStructure.Unaccusativity.Data.instReprDiagnosticResult.repr : DiagnosticResult → Nat → Std.Format

Equations

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

instance Phenomena.ArgumentStructure.Unaccusativity.Data.instBEqDiagnosticResult : BEq DiagnosticResult

Equations

• Phenomena.ArgumentStructure.Unaccusativity.Data.instBEqDiagnosticResult = { beq := Phenomena.ArgumentStructure.Unaccusativity.Data.instBEqDiagnosticResult.beq }

def Phenomena.ArgumentStructure.Unaccusativity.Data.instBEqDiagnosticResult.beq : DiagnosticResult → DiagnosticResult → Bool

Equations

• Phenomena.ArgumentStructure.Unaccusativity.Data.instBEqDiagnosticResult.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure Phenomena.ArgumentStructure.Unaccusativity.Data.DiagnosticDatum : Type

A single diagnostic judgment.

• verbForm : String
• diagnostic : Diagnostic
• result : DiagnosticResult
• sentence : String
• language : String
• note : String

instance Phenomena.ArgumentStructure.Unaccusativity.Data.instReprDiagnosticDatum : Repr DiagnosticDatum

Equations

• Phenomena.ArgumentStructure.Unaccusativity.Data.instReprDiagnosticDatum = { reprPrec := Phenomena.ArgumentStructure.Unaccusativity.Data.instReprDiagnosticDatum.repr }

def Phenomena.ArgumentStructure.Unaccusativity.Data.instReprDiagnosticDatum.repr : DiagnosticDatum → Nat → Std.Format

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.instBEqDiagnosticDatum.beq : DiagnosticDatum → DiagnosticDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.ArgumentStructure.Unaccusativity.Data.instBEqDiagnosticDatum.beq x✝¹ x✝ = false

instance Phenomena.ArgumentStructure.Unaccusativity.Data.instBEqDiagnosticDatum : BEq DiagnosticDatum

Equations

• Phenomena.ArgumentStructure.Unaccusativity.Data.instBEqDiagnosticDatum = { beq := Phenomena.ArgumentStructure.Unaccusativity.Data.instBEqDiagnosticDatum.beq }

def Phenomena.ArgumentStructure.Unaccusativity.Data.qi_whisper : DiagnosticDatum

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.qi_murmur : DiagnosticDatum

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.qi_shout : DiagnosticDatum

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.qi_cry : DiagnosticDatum

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.qi_scream : DiagnosticDatum

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.qi_mumble : DiagnosticDatum

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.qi_mutter : DiagnosticDatum

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.qi_shriek : DiagnosticDatum

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.qi_yell : DiagnosticDatum

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.qi_groan : DiagnosticDatum

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.qi_grumble : DiagnosticDatum

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.qi_hiss : DiagnosticDatum

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.qi_sigh : DiagnosticDatum

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.qi_whimper : DiagnosticDatum

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.qi_snap : DiagnosticDatum

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.qi_speak : DiagnosticDatum

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.qi_talk : DiagnosticDatum

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.qi_say : DiagnosticDatum

say passes QI (@cite{storment-2026}, ex. 9). Its VerbEntry captures the transitive indirect-speech frame ("John said that...") rather than the QI frame, so it is not connected to the smuggling bridge.

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.qi_whisper_transitive : DiagnosticDatum

MoS verb with quote complement + PP goal still permits QI. @cite{storment-2026}: QI is blocked only when multiple DP arguments compete for Case licensing. A PP goal does not need Case.

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.qi_shout_heavysubj : DiagnosticDatum

QI with heavy subject (proper name): no degradation.

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.qi_whisper_pronoun : DiagnosticDatum

Pronominal subjects degrade QI (@cite{storment-2026}, §3: pronouns resist postverbal position in QI, unlike full DPs).

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.qi_whisper_double_obj : DiagnosticDatum

QI blocked with multiple DP arguments: the transitivity constraint (@cite{storment-2026}, §5, ex. 125). T⁰ can license only one DP (the theme); a second DP argument has no Case licenser.

Equations

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

Quotative inversion and locative inversion share the same mechanism (smuggling of VP to Spec-VoiceP, @cite{storment-2026} §6) but differ in their inputs and distribution:

1. **Fronted constituent**: QI requires a quote; LI requires a locative PP
2. **Transitivity constraint**: both QI and LI are blocked with multiple
   DP arguments, due to Case licensing
3. **Pronominal subjects**: QI degrades with pronouns (§3); LI blocks them
4. **Verb class**: QI targets MoS verbs; LI applies more broadly 

def Phenomena.ArgumentStructure.Unaccusativity.Data.li_kick : DiagnosticDatum

LI with transitive verb is ungrammatical. The transitivity constraint (Case licensing) applies to both QI and LI.

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.li_arrive_pronoun : DiagnosticDatum

LI with pronominal subject is strongly ungrammatical.

Equations

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

Setswana quotative inversion data from @cite{collins-1997}, discussed extensively in @cite{storment-2026}. Setswana QI uses class 17 default subject agreement (SM17 go), never tracking the agent.

def Phenomena.ArgumentStructure.Unaccusativity.Data.qi_setswana_botsa : DiagnosticDatum

Setswana QI with 'botsa' (ask). @cite{collins-1997}, cited as Storment ex. (4).

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.qi_setswana_bua : DiagnosticDatum

Setswana QI with 'bua' (say) + depictive. Storment ex. (11).

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.qi_setswana_transitivity : DiagnosticDatum

Setswana QI blocked with two DP arguments (transitivity constraint). Storment ex. (5).

Equations

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

Structural evidence for the VP-smuggling analysis of QI (§3). These data test the positions of Theme, Agent, VP, and Quote predicted by the smuggling derivation (§4):

- **Theme** → Spec-TP (controls agreement, licenses raising)
- **Agent** → Spec-vP (in-situ, conjoint form, doesn't control agreement)
- **VP** → Spec-VoiceP (VP-internal material precedes Agent)
- **Quote** → DiscourseP (clause-external, can split, need not be grammatical) 

inductive Phenomena.ArgumentStructure.Unaccusativity.Data.QIStructuralTest : Type

Type of structural evidence for QI clause structure.

• agreement : QIStructuralTest
• parasiticGap : QIStructuralTest
• subjectRaising : QIStructuralTest
• conjointDisjoint : QIStructuralTest
• quoteCategory : QIStructuralTest
• constituentOrdering : QIStructuralTest

instance Phenomena.ArgumentStructure.Unaccusativity.Data.instDecidableEqQIStructuralTest : DecidableEq QIStructuralTest

Equations

• Phenomena.ArgumentStructure.Unaccusativity.Data.instDecidableEqQIStructuralTest x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.ArgumentStructure.Unaccusativity.Data.instReprQIStructuralTest.repr : QIStructuralTest → Nat → Std.Format

Equations

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

instance Phenomena.ArgumentStructure.Unaccusativity.Data.instReprQIStructuralTest : Repr QIStructuralTest

Equations

• Phenomena.ArgumentStructure.Unaccusativity.Data.instReprQIStructuralTest = { reprPrec := Phenomena.ArgumentStructure.Unaccusativity.Data.instReprQIStructuralTest.repr }

def Phenomena.ArgumentStructure.Unaccusativity.Data.instBEqQIStructuralTest.beq : QIStructuralTest → QIStructuralTest → Bool

Equations

• Phenomena.ArgumentStructure.Unaccusativity.Data.instBEqQIStructuralTest.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.ArgumentStructure.Unaccusativity.Data.instBEqQIStructuralTest : BEq QIStructuralTest

Equations

• Phenomena.ArgumentStructure.Unaccusativity.Data.instBEqQIStructuralTest = { beq := Phenomena.ArgumentStructure.Unaccusativity.Data.instBEqQIStructuralTest.beq }

structure Phenomena.ArgumentStructure.Unaccusativity.Data.QIStructuralDatum : Type

A structural evidence datum for QI clause structure.

• test : QIStructuralTest
• result : DiagnosticResult
• sentence : String
• language : String
• note : String

def Phenomena.ArgumentStructure.Unaccusativity.Data.instReprQIStructuralDatum.repr : QIStructuralDatum → Nat → Std.Format

Equations

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

instance Phenomena.ArgumentStructure.Unaccusativity.Data.instReprQIStructuralDatum : Repr QIStructuralDatum

Equations

• Phenomena.ArgumentStructure.Unaccusativity.Data.instReprQIStructuralDatum = { reprPrec := Phenomena.ArgumentStructure.Unaccusativity.Data.instReprQIStructuralDatum.repr }

instance Phenomena.ArgumentStructure.Unaccusativity.Data.instBEqQIStructuralDatum : BEq QIStructuralDatum

Equations

• Phenomena.ArgumentStructure.Unaccusativity.Data.instBEqQIStructuralDatum = { beq := Phenomena.ArgumentStructure.Unaccusativity.Data.instBEqQIStructuralDatum.beq }

def Phenomena.ArgumentStructure.Unaccusativity.Data.instBEqQIStructuralDatum.beq : QIStructuralDatum → QIStructuralDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.ArgumentStructure.Unaccusativity.Data.instBEqQIStructuralDatum.beq x✝¹ x✝ = false

def Phenomena.ArgumentStructure.Unaccusativity.Data.qi_agreement_english : QIStructuralDatum

English QI: verb agrees with postverbal agent, not with quote. Storment ex. (40).

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.qi_agreement_setswana : QIStructuralDatum

Setswana QI: SM surfaces as default SM17 (go), not agent's class. Storment exs. (77)–(80): go replaces ke (1sg), o (2sg), di (cl.10).

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.qi_parasitic_gap_blocked : QIStructuralDatum

QI blocks parasitic gap licensing: Theme undergoes A-movement, not Ā-movement, so it cannot license a parasitic gap. Storment ex. (62a).

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.qi_parasitic_gap_baseline : QIStructuralDatum

Non-QI preposed quote DOES license a parasitic gap: quote undergoes Ā-movement (topicalization), which licenses PGs. Storment ex. (62b).

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.qi_raising : QIStructuralDatum

QI is compatible with subject-to-subject raising: quotative Theme can A-move through embedded Spec-TP to matrix Spec-TP. Storment ex. (67a).

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.qi_conjoint_disjoint : QIStructuralDatum

Setswana: disjoint morpheme 'a' blocked in QI — Agent remains vP-internal (conjoint position). Storment ex. (87).

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.qi_quote_split : QIStructuralDatum

Quote can split around verb + agent: evidence for clause-external position (DiscourseP). Storment ex. (90).

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.qi_quote_nongrammatical : QIStructuralDatum

Quote need not be grammatical: further evidence for clause-external status. Storment ex. (96a).

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.qi_ordering_depictive : QIStructuralDatum

Setswana: depictive follows Agent — depictives are vP-external adjuncts, so they stay behind when VP smuggles. Storment ex. (11).

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.qi_ordering_manner : QIStructuralDatum

Setswana: manner adverb follows Agent — manner adverbs are vP-external, so they stay behind. Storment ex. (21).

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.qi_ordering_purpose : QIStructuralDatum

Setswana: purpose clause follows Agent — purpose clauses are vP-external adjuncts. Storment ex. (17).

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.qi_ordering_complement : QIStructuralDatum

Setswana: restructuring complement precedes Agent — VP-internal material moves with VP via smuggling. Storment ex. (27).

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.allStructuralData : List QIStructuralDatum

All QI structural evidence data points.

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.there_arrive : DiagnosticDatum

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.there_run : DiagnosticDatum

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.there_sleep : DiagnosticDatum

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.loc_arrive : DiagnosticDatum

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.loc_whisper : DiagnosticDatum

Equations

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

Japanese distinguishes direct and indirect passives. Direct passives (allowing -niyotte agent) require thematic Voice; indirect passives (-rare- adversative) are available for all verbs including unaccusatives. If a verb allows only the indirect passive, it is unaccusative.

def Phenomena.ArgumentStructure.Unaccusativity.Data.jp_hanareru_indirect : DiagnosticDatum

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.jp_hanareru_direct : DiagnosticDatum

Equations

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

Nani-o 'what-ACC' can mean 'why' with unergatives and transitives (@cite{kurafuji-1997}), but not with unaccusatives. If a verb blocks the 'why' reading of nani-o, it is unaccusative.

def Phenomena.ArgumentStructure.Unaccusativity.Data.jp_hanareru_nanio : DiagnosticDatum

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.jp_densya_nanio : DiagnosticDatum

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.allData : List DiagnosticDatum

All diagnostic data points.

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.qiData : List DiagnosticDatum

QI data only.

Equations

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

def Phenomena.ArgumentStructure.Unaccusativity.Data.liData : List DiagnosticDatum

Locative inversion data only.

Equations

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