Comrie (1989) [Com89]

Language Universals and Linguistic Typology: Syntax and Morphology. 2nd ed. University of Chicago Press.

Bridge study file connecting linglib's independently formalized typological hierarchies and proving they cohere as [Com89]'s synthesis claims.

Cross-hierarchy unity (Chs 5–9)

[Com89]'s central methodological point: the same prominence hierarchies (animacy, definiteness, person) recur across multiple grammatical domains:

• Case marking (Ch 6): Differential Object Marking driven by animacy/definiteness ([Ais03] in Case.Studies.Aissen2003). Features.Prominence.AnimacyLevel is the shared type.
• Alignment (Ch 5–6): Split ergativity conditioned by [Sil76]'s hierarchy (Alignment.Typology). Same AnimacyLevel type governs the split threshold.
• Relativization (Ch 7): The [KC77] Accessibility Hierarchy orders grammatical relations by extraction accessibility (Syntax.RelativeClause.Basic, FillerGap.Studies.KeenanComrie1977). The AH positions (Subject > DO > IO > OBL) mirror the GR hierarchy that governs causee demotion.
• Causatives (Ch 8): Morphological complexity correlates with semantic directness (Causation.Morphological); causee marking follows the GR hierarchy (CauseeSlot).

The shared infrastructure in Features.Prominence ensures the animacy connection is structural — by construction, not by theorem. The GR hierarchy parallel between the AH and causee demotion is proved below.

Subject as a cluster concept (Ch 5)

[Com89] argues that "subject" is not a primitive grammatical relation but a bundle of coding and behavioral properties that converge in accusative languages and diverge under ergativity (§1a below). Coding properties (case, agreement, word order) are the "surface" identification of the subject NP; behavioral properties (conjunction reduction, reflexivization, raising, equi-deletion, relativization accessibility) are the "deep" cross-clausal tests. In morphologically ergative languages the two diverge: coding picks out S=P (absolutive) while behavioral tests still pick out S=A. Full convergence on S=P (syntactic ergativity, Dyirbal subordinate clauses) is rare.

Relative clauses and the AH (Ch 7)

Relativization typology is formalized in KeenanComrie1977 and Syntax.RelativeClause.Basic. The AH concerns accessibility to extraction — a filler-gap dependency — which is why the study file lives under FillerGap/. Non-extraction relative clause types (correlatives, internally-headed RCs) fall outside the AH's scope: [Com89] discusses them but they do not participate in the hierarchy.

Cross-domain unity of the animacy hierarchy

The AnimacyLevel type in Features.Prominence is imported by both Dixon1994 (Silverstein's split ergativity) and Aissen2003 (DOM via OT). This is structural grounding: the same 3-level hierarchy (human > animate > inanimate) governs both phenomena, with no possibility of drift between separate definitions.

The same pattern holds for DefinitenessLevel and Person — all three prominence scales are defined once in Features.Prominence and imported by every downstream module.

inductive Comrie1989.CodingProperty : Type

Coding properties: how the subject NP is morphologically marked. These are "surface" properties visible from case and agreement alone.

• caseMarking : CodingProperty
• verbAgreement : CodingProperty
• wordOrderPosition : CodingProperty

@[implicit_reducible]

instance Comrie1989.instDecidableEqCodingProperty : DecidableEq CodingProperty

Equations

• Comrie1989.instDecidableEqCodingProperty x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Comrie1989.instReprCodingProperty.repr : CodingProperty → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Comrie1989.instReprCodingProperty : Repr CodingProperty

Equations

• Comrie1989.instReprCodingProperty = { reprPrec := Comrie1989.instReprCodingProperty.repr }

inductive Comrie1989.BehavioralProperty : Type

Behavioral properties: how the subject NP participates in syntactic operations that span clause boundaries. These are the "deep" properties that motivate a grammatical-relation analysis.

• conjunctionReduction : BehavioralProperty
• reflexivization : BehavioralProperty
• raisingTarget : BehavioralProperty
• equiDeletion : BehavioralProperty
• relativizationAccess : BehavioralProperty

@[implicit_reducible]

instance Comrie1989.instDecidableEqBehavioralProperty : DecidableEq BehavioralProperty

Equations

• Comrie1989.instDecidableEqBehavioralProperty x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Comrie1989.instReprBehavioralProperty.repr : BehavioralProperty → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Comrie1989.instReprBehavioralProperty : Repr BehavioralProperty

Equations

• Comrie1989.instReprBehavioralProperty = { reprPrec := Comrie1989.instReprBehavioralProperty.repr }

def Comrie1989.CodingProperty.all : List CodingProperty

All coding properties (for finite enumeration).

Equations

• Comrie1989.CodingProperty.all = [Comrie1989.CodingProperty.caseMarking, Comrie1989.CodingProperty.verbAgreement, Comrie1989.CodingProperty.wordOrderPosition]

def Comrie1989.BehavioralProperty.all : List BehavioralProperty

All behavioral properties (for finite enumeration).

Equations

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

structure Comrie1989.SubjectPropertyBundle : Type

A subject property bundle: for each property, which NP grouping it picks out in a given language.

• true = S=A grouping (accusative pattern for that property)
• false = S=P grouping (ergative pattern for that property)

A language's "subject" is well-defined when all properties agree; it is a non-primitive cluster concept when they diverge.

• coding : CodingProperty → Bool
• behavioral : BehavioralProperty → Bool

def Comrie1989.accusativeBundle : SubjectPropertyBundle

Accusative convergence: all properties pick out S=A. English, Latin, Russian, Japanese, etc.

Equations

• Comrie1989.accusativeBundle = { coding := fun (x : Comrie1989.CodingProperty) => true, behavioral := fun (x : Comrie1989.BehavioralProperty) => true }

def Comrie1989.morphErgativityBundle : SubjectPropertyBundle

Morphological ergativity with accusative syntax: coding picks S=P (absolutive case/agreement), but behavioral tests pick S=A. This is the common pattern in "ergative" languages: Dyirbal main clauses, many Australian and Mayan languages.

Equations

• Comrie1989.morphErgativityBundle = { coding := fun (x : Comrie1989.CodingProperty) => false, behavioral := fun (x : Comrie1989.BehavioralProperty) => true }

def Comrie1989.syntacticErgativityBundle : SubjectPropertyBundle

Full (syntactic) ergativity: both coding AND behavioral properties pick out S=P. Rare cross-linguistically; Dyirbal subordinate clauses are the classic example.

Equations

• Comrie1989.syntacticErgativityBundle = { coding := fun (x : Comrie1989.CodingProperty) => false, behavioral := fun (x : Comrie1989.BehavioralProperty) => false }

def Comrie1989.SubjectPropertyBundle.converges (b : SubjectPropertyBundle) : Bool

Whether all subject properties converge on the same NP. Convergence means all coding and behavioral properties agree on either S=A (accusative) or S=P (ergative). Divergence — some properties picking S=A and others S=P — means "subject" is not a unitary concept in that language.

Equations

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

theorem Comrie1989.accusative_marks_P : Alignment.AlignmentType.accusative.marksPatient

Accusative alignment implies P is differentially marked (the patient receives overt case marking to distinguish it from S). This connects [Com89] Ch 5–6 to the DOM patterns in [Ais03]: in an accusative language, it is the P role whose marking is sensitive to prominence (animate/definite Ps get marked, inanimates don't).

theorem Comrie1989.ergative_marks_A : Alignment.AlignmentType.ergative.marksAgent

Ergative alignment implies A is differentially marked. In an ergative language, it is the A role whose marking is prominence-sensitive — less prominent As (full NPs, inanimates) get ergative marking.

theorem Comrie1989.neutral_marks_neither : ¬Alignment.AlignmentType.neutral.marksAgent ∧ ¬Alignment.AlignmentType.neutral.marksPatient

Neutral alignment marks neither A nor P distinctly.

theorem Comrie1989.marking_polarity_matches_alignment : Features.Prominence.ArgumentRole.P.lowDefault = true ∧ Features.Prominence.ArgumentRole.A.highDefault = true

The directionality of differential marking follows from alignment: accusative systems differentially mark the low-default role (P), ergative systems differentially mark the high-default role (A). This mirrors the polarity of marking in Features.Prominence: P is lowDefault, A is highDefault.

Alignment predicts subject property convergence

[Com89] Ch 5: alignment type predicts whether subject properties converge. In accusative languages, all properties pick S=A. In ergative languages, coding properties pick S=P; whether behavioral properties also pick S=P (syntactic ergativity, rare) or S=A (morphological ergativity, common) is a parametric dimension.

The toSubjectBundle function derives the predicted subject property bundle from alignment type, so the three canonical bundles of §1a become consequences of alignment classification rather than independent definitions.

def Comrie1989.toSubjectBundle (a : Alignment.AlignmentType) (syntacticErg : Bool := false) : SubjectPropertyBundle

Derive the predicted subject property bundle from alignment type. Non-ergative alignment → all properties S=A (accusative bundle). Ergative → coding S=P, behavioral parametric.

Equations

• Comrie1989.toSubjectBundle Alignment.AlignmentType.ergative syntacticErg = if syntacticErg = true then Comrie1989.syntacticErgativityBundle else Comrie1989.morphErgativityBundle
• Comrie1989.toSubjectBundle a syntacticErg = Comrie1989.accusativeBundle

theorem Comrie1989.accusative_derives_bundle : toSubjectBundle Alignment.AlignmentType.accusative = accusativeBundle

Accusative alignment derives the accusative bundle.

theorem Comrie1989.morphErg_derives_bundle : toSubjectBundle Alignment.AlignmentType.ergative = morphErgativityBundle

Ergative alignment (default) derives morphological ergativity bundle.

theorem Comrie1989.syntacticErg_derives_bundle : toSubjectBundle Alignment.AlignmentType.ergative true = syntacticErgativityBundle

Ergative alignment with syntacticErg=true derives syntactic ergativity.

theorem Comrie1989.accusative_subject_converges : accusativeBundle.converges = true

In accusative languages, all subject properties converge on S=A. [Com89] Ch 5: "In accusative languages... the notion of subject is reasonably clear."

theorem Comrie1989.morphErg_subject_diverges : morphErgativityBundle.converges = false

In morphologically ergative languages, subject properties diverge: coding picks S=P (absolutive), behavioral picks S=A. [Com89] Ch 5: "In ergative languages, the various properties do not necessarily converge."

theorem Comrie1989.syntacticErg_subject_converges : syntacticErgativityBundle.converges = true

In syntactically ergative languages (Dyirbal subordinate clauses), subject properties converge on S=P — full ergativity. This is the rare case where even behavioral tests track absolutive.

Alignment profiles predict subject property convergence

Each language's alignment profile (from Dixon1994) generates a predicted subject property bundle via toSubjectBundle. These theorems verify the predictions against the known typological facts for each language:

• Accusative languages (English, Japanese): derived bundle converges.
• Morphologically ergative languages (Basque, Dargwa, Hindi-Urdu): derived bundle diverges (coding ≠ behavioral).
• Syntactically ergative languages (Dyirbal): must set syntacticErg := true to get a converging bundle.

The syntacticErg parameter captures the rare/common ergativity distinction that [Com89] Ch 5 identifies as central.

theorem Comrie1989.english_subject_from_alignment : (toSubjectBundle Dixon1994.english.npAlignment).converges = true

English: accusative NP alignment → derived bundle converges.

theorem Comrie1989.japanese_subject_from_alignment : (toSubjectBundle Dixon1994.japanese.npAlignment).converges = true

Japanese: accusative NP alignment → derived bundle converges.

theorem Comrie1989.basque_morphErg_diverges : (toSubjectBundle Dixon1994.basque.npAlignment).converges = false

Basque: ergative alignment → default (morphological) derived bundle diverges, correctly predicting that coding and behavioral properties pick different NPs.

theorem Comrie1989.basque_bundle_is_morphErg : toSubjectBundle Dixon1994.basque.npAlignment = morphErgativityBundle

Basque's derived bundle is exactly the morphological ergativity bundle: coding picks S=P, behavioral picks S=A.

theorem Comrie1989.dargwa_bundle_is_morphErg : toSubjectBundle Dixon1994.dargwa.npAlignment = morphErgativityBundle

Dargwa: consistently ergative → morphological ergativity predicted.

theorem Comrie1989.hindiUrdu_morphErg_diverges : (toSubjectBundle Dixon1994.hindiUrdu.npAlignment).converges = false

Hindi-Urdu: ergative NP alignment → morphological ergativity predicted. The split-ergative conditioning (perfective → ERG) is orthogonal to subject property convergence: even in perfective clauses, behavioral properties track S=A.

theorem Comrie1989.dyirbal_default_diverges : (toSubjectBundle Dixon1994.dyirbal.npAlignment).converges = false

Dyirbal: ergative NP alignment → default (morphological) prediction diverges. But Dyirbal is one of the rare syntactically ergative languages ([Dix72]): even behavioral properties (coordination deletion) track S=P.

theorem Comrie1989.dyirbal_syntacticErg_converges : (toSubjectBundle Dixon1994.dyirbal.npAlignment true).converges = true

Dyirbal with syntacticErg=true → derived bundle converges, correctly predicting full syntactic ergativity.

theorem Comrie1989.compact_direct_vs_periphrastic_indirect : Causation.Morphological.comrie_monotone { complexity := Causation.Morphological.CausativeComplexity.lexical, mediation := Causation.Morphological.Mediation.direct, causerRestriction := none, causeeRestriction := none } { complexity := Causation.Morphological.CausativeComplexity.periphrastic, mediation := Causation.Morphological.Mediation.indirect, causerRestriction := none, causeeRestriction := none }

[Com89]'s compact-to-analytic and direct-to-indirect dimensions are connected: a compact+direct construction and a periphrastic+indirect construction satisfy the monotonicity predicate.

theorem Comrie1989.intransitive_causee_above_transitive_causee : (Causation.Morphological.causeeDemotion 1).rank > (Causation.Morphological.causeeDemotion 2).rank

Causee demotion: intransitive base → causee gets DO (rank 2), transitive base → causee gets IO (rank 1). The causee is demoted as base valency increases.

theorem Comrie1989.subject_is_ah_top : RelativeClause.AHPosition.subject.rank = 6 ∧ ∀ (p : RelativeClause.AHPosition), p.rank ≤ RelativeClause.AHPosition.subject.rank

The top of the AH is the subject position — [Com89] Ch 7: "A language must be able to relativize subjects" (HC₁). The subject is the most accessible position on the hierarchy.

theorem Comrie1989.ah_mirrors_causee_hierarchy : RelativeClause.AHPosition.subject.rank > RelativeClause.AHPosition.directObject.rank ∧ RelativeClause.AHPosition.directObject.rank > RelativeClause.AHPosition.indirectObject.rank ∧ RelativeClause.AHPosition.indirectObject.rank > RelativeClause.AHPosition.oblique.rank

The AH mirrors the GR hierarchy used in causee marking: Subject > Direct Object > Indirect Object > Oblique. The same ordering governs both relativization accessibility and causee demotion — positions higher on the hierarchy are both more accessible to relativization and filled first in causativization.

The GR hierarchy underlying both causee demotion and relativization

[Com89] observes that the same grammatical relation hierarchy governs both causee demotion (Ch 8) and relativization accessibility (Ch 7):

Subject > Direct Object > Indirect Object > Oblique

CauseeSlot (in Causation.Morphological) and AHPosition (in Syntax.RelativeClause.Basic) encode overlapping portions of this hierarchy independently. The bridge function causeeToAH maps causee slots to their corresponding AH positions, and the order-preservation theorem proves the mapping is monotone — confirming that the two hierarchies are structurally the same.

def Comrie1989.causeeToAH : Causation.Morphological.CauseeSlot → RelativeClause.AHPosition

Map causee slots to their corresponding AH positions. Both encode the same GR hierarchy; this bridge makes the connection explicit.

Equations

• Comrie1989.causeeToAH Causation.Morphological.CauseeSlot.directObject = RelativeClause.AHPosition.directObject
• Comrie1989.causeeToAH Causation.Morphological.CauseeSlot.indirectObject = RelativeClause.AHPosition.indirectObject
• Comrie1989.causeeToAH Causation.Morphological.CauseeSlot.oblique = RelativeClause.AHPosition.oblique

theorem Comrie1989.causee_ah_order_preserved (s1 s2 : Causation.Morphological.CauseeSlot) : s1.rank > s2.rank ↔ (causeeToAH s1).rank > (causeeToAH s2).rank

The mapping preserves ordering: higher causee rank ↔ higher AH rank.

theorem Comrie1989.causeeDemotion_maps_to_ah : causeeToAH (Causation.Morphological.causeeDemotion 1) = RelativeClause.AHPosition.directObject ∧ causeeToAH (Causation.Morphological.causeeDemotion 2) = RelativeClause.AHPosition.indirectObject ∧ causeeToAH (Causation.Morphological.causeeDemotion 3) = RelativeClause.AHPosition.oblique

Causee demotion follows the AH: the slots assigned by causeeDemotion correspond to exactly the AH positions below subject.

Dargwa causative system bridges to Comrie's causee hierarchy

Dargwa (Tanti) has a productive causative morpheme -aq ([Sum21] §4.5.7). The Dargwa fragment (Dargwa.ComplexPredicates) records:

• Intransitive base: causee appears in absolutive = direct object slot
• Transitive base: causee appears in elative = oblique slot

Comrie's hierarchy predicts IO for transitive bases, but Dargwa skips the IO position and demotes directly to oblique (elative). This is consistent with monotonicity — the actual slot is at most as high as the predicted slot — but represents a language-specific choice to use a spatial case rather than a dative/IO.

def Comrie1989.dargwaCauseeSlot (e : Dargwa.ComplexPredicates.CausativeEntry) : Causation.Morphological.CauseeSlot

Map Dargwa causee case to CauseeSlot based on base verb transitivity. Intransitive base → DO (absolutive in Dargwa); transitive base → OBL (elative in Dargwa).

Equations

• Comrie1989.dargwaCauseeSlot e = if e.baseTransitive = true then Causation.Morphological.CauseeSlot.oblique else Causation.Morphological.CauseeSlot.directObject

theorem Comrie1989.dargwa_intr_matches_prediction : dargwaCauseeSlot Dargwa.ComplexPredicates.causStandUp = Causation.Morphological.causeeDemotion 1

Dargwa intransitive causative: causee = DO, exactly matching Comrie's prediction (causeeDemotion 1).

theorem Comrie1989.dargwa_tr_more_demoted : (dargwaCauseeSlot Dargwa.ComplexPredicates.causDig).rank < (Causation.Morphological.causeeDemotion 2).rank

Dargwa transitive causative: causee = OBL, one step below Comrie's prediction of IO (causeeDemotion 2). Dargwa uses elative (a spatial/oblique case) rather than dative/IO.

theorem Comrie1989.dargwa_causee_monotone : (dargwaCauseeSlot Dargwa.ComplexPredicates.causStandUp).rank > (dargwaCauseeSlot Dargwa.ComplexPredicates.causDig).rank

Dargwa preserves Comrie's monotonicity: intransitive causee outranks transitive causee on the GR hierarchy.

theorem Comrie1989.dargwa_causee_on_ah : causeeToAH (dargwaCauseeSlot Dargwa.ComplexPredicates.causStandUp) = RelativeClause.AHPosition.directObject ∧ causeeToAH (dargwaCauseeSlot Dargwa.ComplexPredicates.causDig) = RelativeClause.AHPosition.oblique

Dargwa causee slots map to the same AH positions as the cross-linguistic generalization.

The alignment–DOM correlation ([Com89] Ch 6)

[Com89] observes that alignment type determines which argument role undergoes differential marking:

• Accusative (S=A vs P): P is the distinctly-marked role → DOM expected
• Ergative (S=P vs A): A is the distinctly-marked role → DSM expected
• Neutral (S=A=P): no role distinction → no differential marking
• Tripartite (S≠A≠P): both A and P distinct → both possible

This correlation was later derived formally by [dHM08] via the Primary Actant Immunity Principle: the argument encoded like the intransitive S resists differential marking, leaving the non-primary argument available for prominence-sensitive marking.

The critical structural point: the same prominence hierarchies (AnimacyLevel, DefinitenessLevel) that condition split ergativity ([Sil76]) also condition DOM ([Ais03]). This connection is built in by construction — both import Features.Prominence.

@[reducible, inline]

abbrev Comrie1989.domExpected (a : Alignment.AlignmentType) : Prop

Whether DOM (differential P marking) is expected given alignment. Structurally identical to AlignmentType.marksPatient: exactly the alignments that mark P distinctly from S predict DOM.

Equations

• Comrie1989.domExpected a = a.marksPatient

@[reducible, inline]

abbrev Comrie1989.dsmExpected (a : Alignment.AlignmentType) : Prop

Whether DSM (differential A marking) is expected given alignment. Structurally identical to AlignmentType.marksAgent.

Equations

• Comrie1989.dsmExpected a = a.marksAgent

theorem Comrie1989.dom_iff_marks_patient (a : Alignment.AlignmentType) : domExpected a ↔ a.marksPatient

DOM expectation = patient marking.

theorem Comrie1989.dsm_iff_marks_agent (a : Alignment.AlignmentType) : dsmExpected a ↔ a.marksAgent

DSM expectation = agent marking.

theorem Comrie1989.acc_dom_erg_dsm : domExpected Alignment.AlignmentType.accusative ∧ ¬dsmExpected Alignment.AlignmentType.accusative ∧ ¬domExpected Alignment.AlignmentType.ergative ∧ dsmExpected Alignment.AlignmentType.ergative

Accusative predicts DOM (not DSM); ergative predicts DSM (not DOM). [Com89] Ch 6 / [dHM08] §4.

def Comrie1989.hasAnyMarking (dom : Aissen2003.DOMProfile) : Bool

Whether a DOMProfile has any differential marking (at least one prominence cell is overtly marked).

Equations

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

Testing the alignment–DOM prediction against language data

Languages with both an AlignmentProfile (from Alignment.Typology) and a DOMProfile (from Case.Typology) can be tested: accusative alignment predicts DOM; ergative predicts DSM instead.

• Turkish: accusative + DOM (definiteness-based) → consistent
• Russian: accusative + DOM (animacy-based) → consistent
• Hindi-Urdu: ergative NP alignment + DOM (ko) — addressed in §7b
• Spanish: neutral NP alignment + DOM (a-marking) — DOM operates independently of the alignment system (on top of a caseless base)

theorem Comrie1989.turkish_dom_consistent : domExpected Dixon1994.turkish.npAlignment ∧ hasAnyMarking Aissen2003.turkishDOM = true

Turkish: accusative alignment → DOM expected; DOM present.

theorem Comrie1989.russian_dom_consistent : domExpected Dixon1994.russian.npAlignment ∧ hasAnyMarking Aissen2003.russianDOM = true

Russian: accusative alignment → DOM expected; DOM present.

theorem Comrie1989.neutral_no_dom : ¬domExpected Alignment.AlignmentType.neutral ∧ hasAnyMarking Aissen2003.noDOMProfile = false

No-DOM languages with neutral alignment: DOM not expected, and no DOM exists. Doubly consistent.

Split ergativity creates alignment zones with different DOM predictions

In split-ergative languages, alignment varies across conditions (aspect, animacy, person). Each zone has its own prediction:

• Accusative zone: P is distinct → DOM expected
• Ergative zone: P groups with S → DOM not expected (DSM instead)

Hindi-Urdu is the key test case: perfective → ergative (subject gets -ne), imperfective → accusative. Per-zone PaIP prediction: DOM expected only in the imperfective. But Hindi's -ko marking applies in both aspects. The ko-marked object receives differential marking regardless of whether the clause is ergative or accusative.

The split-ergativity × DOM interaction demonstrates that the same prominence hierarchies operate at two levels simultaneously:

1. Macro level: aspect conditions the alignment split
2. Micro level: animacy/definiteness conditions DOM within each zone

def Comrie1989.domInZone (family : Features.AlignmentFamily) : Bool

In a split-ergative system, DOM availability in each zone tracks the alignment of that zone.

Equations

• Comrie1989.domInZone Features.AlignmentFamily.accusative = true
• Comrie1989.domInZone Features.AlignmentFamily.ergative = false

theorem Comrie1989.hindi_impfv_dom : domInZone (Alignment.hindiSplit.alignment Alignment.Aspect.imperfective) = true

Hindi imperfective: accusative zone → DOM expected.

theorem Comrie1989.hindi_pfv_no_dom : domInZone (Alignment.hindiSplit.alignment Alignment.Aspect.perfective) = false

Hindi perfective: ergative zone → DOM not expected.

theorem Comrie1989.hindi_has_dom_across_aspects : hasAnyMarking Aissen2003.hindiDOM = true

Hindi actually has DOM (ko-marking) that applies across both aspects. The empirical profile exceeds the per-zone prediction: ko operates on top of the case system, not within it.

theorem Comrie1989.dyirbal_split_dom_zones : domInZone (Dixon1994.dyirbalSplit.alignment Features.Prominence.AnimacyLevel.inanimate) = false ∧ domInZone (Dixon1994.dyirbalSplit.alignment Features.Prominence.AnimacyLevel.human) = true

Dyirbal's animacy-based split creates analogous zones: inanimates get ergative alignment (DOM not expected), animates get accusative (DOM expected). The split threshold and DOM threshold operate over the same AnimacyLevel type.

Structural unity: same hierarchies condition both phenomena

The animacy hierarchy operates in two independent grammatical systems:

1. Split ergativity ([Sil76]): AnimacyLevel determines which NPs get ergative vs accusative alignment. In Dyirbal, inanimate → ergative, human/animate → accusative.
2. DOM ([Ais03]): AnimacyLevel determines which objects get overt marking. In Spanish, human → marked, non-human → unmarked.

Both are monotone cutoffs on the same linearly ordered type. A change to AnimacyLevel propagates automatically to both systems. This is [Com89]'s central methodological point: the same hierarchies recur across grammatical domains.

theorem Comrie1989.animacy_governs_split_and_dom : Dixon1994.dyirbalSplit.alignment Features.Prominence.AnimacyLevel.inanimate = Features.AlignmentFamily.ergative ∧ Dixon1994.dyirbalSplit.alignment Features.Prominence.AnimacyLevel.human = Features.AlignmentFamily.accusative ∧ Aissen2003.spanishDOM.marks Features.Prominence.AnimacyLevel.human Features.Prominence.DefinitenessLevel.nonSpecific = true ∧ Aissen2003.spanishDOM.marks Features.Prominence.AnimacyLevel.inanimate Features.Prominence.DefinitenessLevel.nonSpecific = false

The animacy hierarchy governs both split ergativity and DOM. Dyirbal uses it for the ergative split; Spanish uses it for DOM. Both are monotone cutoffs on the same ordered type.

theorem Comrie1989.hindi_bidimensional_dom : Aissen2003.hindiDOM.marks Features.Prominence.AnimacyLevel.human Features.Prominence.DefinitenessLevel.indefiniteSpecific = true ∧ Aissen2003.hindiDOM.marks Features.Prominence.AnimacyLevel.animate Features.Prominence.DefinitenessLevel.indefiniteSpecific = false ∧ Aissen2003.hindiDOM.marks Features.Prominence.AnimacyLevel.animate Features.Prominence.DefinitenessLevel.definite = true ∧ Aissen2003.hindiDOM.marks Features.Prominence.AnimacyLevel.inanimate Features.Prominence.DefinitenessLevel.personalPronoun = false

Hindi-Urdu's bidimensional DOM uses BOTH prominence scales: human objects need only indefinite-specific status for ko-marking, while animate objects require definite status. The staircase cutoff operates jointly on AnimacyLevel × DefinitenessLevel.