Differential Indexing Typology @cite{just-2024}

@cite{aissen-2003} @cite{haspelmath-2019} @cite{siewierska-2004} @cite{harris-1981} @cite{laka-1996} @cite{haspelmath-2021}

Formalizes the typological survey from:

• Just, E. (2024). A structural and functional comparison of differential A and P indexing. Linguistics 62(2): 295–321.

Key Distinction: Flagging vs. Indexing (@cite{haspelmath-2019}, Just §2)

Flagging = case morphology on the NP (e.g., accusative suffix). Indexing = verbal agreement / cross-referencing (e.g., Bantu object markers).

These serve different functions:

• Flagging: disambiguate thematic roles (who did what to whom)
• Indexing: track prominent referents through discourse

Both channels are governed by the same prominence scales (person, animacy, definiteness) but because they serve different functions, the patterns are not redundant.

Core Claim: Same Scales, Opposite Polarity

The same referential properties condition both differential P and A indexing. The directions form a mirror image (§4.2, p. 311):

• P indexing targets prominent Ps (high person, animacy, definiteness)
• A indexing targets non-prominent As (low person, animacy, definiteness)

This follows from the unified functional principle (§6, p. 315): prominent arguments tend to be indexed more readily, regardless of role. A arguments are prominent by default; P arguments are not. Differential marking targets departures from these defaults.

inductive Phenomena.Agreement.DifferentialIndexing.IndexingPersonLevel : Type

Person prominence for differential indexing.

The person scale for indexing is a binary split between speech act participants (SAP: 1st/2nd person) and non-participants (3rd person). This mirrors @cite{preminger-2014}'s [±participant] feature decomposition.

This is coarser than Core.Prominence.PersonLevel (1st > 2nd > 3rd), which is needed for scenario splits. The binary split suffices for indexing because indexing does not distinguish 1st from 2nd.

• sap : IndexingPersonLevel

  Speech act participants: 1st and 2nd person

• third : IndexingPersonLevel

  Non-participants: 3rd person

instance Phenomena.Agreement.DifferentialIndexing.instDecidableEqIndexingPersonLevel : DecidableEq IndexingPersonLevel

Equations

• Phenomena.Agreement.DifferentialIndexing.instDecidableEqIndexingPersonLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Agreement.DifferentialIndexing.instBEqIndexingPersonLevel : BEq IndexingPersonLevel

Equations

• Phenomena.Agreement.DifferentialIndexing.instBEqIndexingPersonLevel = { beq := Phenomena.Agreement.DifferentialIndexing.instBEqIndexingPersonLevel.beq }

def Phenomena.Agreement.DifferentialIndexing.instBEqIndexingPersonLevel.beq : IndexingPersonLevel → IndexingPersonLevel → Bool

Equations

• Phenomena.Agreement.DifferentialIndexing.instBEqIndexingPersonLevel.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Agreement.DifferentialIndexing.instReprIndexingPersonLevel.repr : IndexingPersonLevel → Nat → Std.Format

Equations

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

instance Phenomena.Agreement.DifferentialIndexing.instReprIndexingPersonLevel : Repr IndexingPersonLevel

Equations

• Phenomena.Agreement.DifferentialIndexing.instReprIndexingPersonLevel = { reprPrec := Phenomena.Agreement.DifferentialIndexing.instReprIndexingPersonLevel.repr }

instance Phenomena.Agreement.DifferentialIndexing.instInhabitedIndexingPersonLevel : Inhabited IndexingPersonLevel

Equations

• Phenomena.Agreement.DifferentialIndexing.instInhabitedIndexingPersonLevel = { default := Phenomena.Agreement.DifferentialIndexing.instInhabitedIndexingPersonLevel.default }

def Phenomena.Agreement.DifferentialIndexing.instInhabitedIndexingPersonLevel.default : IndexingPersonLevel

Equations

• Phenomena.Agreement.DifferentialIndexing.instInhabitedIndexingPersonLevel.default = Phenomena.Agreement.DifferentialIndexing.IndexingPersonLevel.sap

def Phenomena.Agreement.DifferentialIndexing.IndexingPersonLevel.rank : IndexingPersonLevel → Nat

Rank on the indexing person scale: SAP (1) > 3rd (0).

Equations

• Phenomena.Agreement.DifferentialIndexing.IndexingPersonLevel.sap.rank = 1
• Phenomena.Agreement.DifferentialIndexing.IndexingPersonLevel.third.rank = 0

def Phenomena.Agreement.DifferentialIndexing.IndexingPersonLevel.all : List IndexingPersonLevel

All indexing person levels.

Equations

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

theorem Phenomena.Agreement.DifferentialIndexing.person_sap_gt_third : IndexingPersonLevel.sap.rank > IndexingPersonLevel.third.rank

structure Phenomena.Agreement.DifferentialIndexing.IndexingFragmentextends Core.Prominence.DifferentialMarkingProfile : Type

A differential indexing fragment for a single language.

Extends DifferentialMarkingProfile with language metadata and per-dimension marking predicates. The 2D marks predicate is computed from animacyIndexed and definitenessIndexed by the mk' constructor, and the channel is always .indexing.

For P indexing: true at a level means "P arguments at this level ARE indexed." The expectation (Just §4.2) is that P indexing targets the prominent end of each scale.

For A indexing: true at a level means "A arguments at this level ARE indexed." The expectation is that A indexing targets the non-prominent end.

• name : String
• role : ArgumentRole
• channel : MarkingChannel
• marks : AnimacyLevel → DefinitenessLevel → Bool
• iso639 : String

  ISO 639-3 code

• family : String

  Language family

• personIndexed : IndexingPersonLevel → Bool

  Which person levels trigger indexing

• animacyIndexed : Core.Prominence.AnimacyLevel → Bool

  Which animacy levels trigger indexing

• definitenessIndexed : Core.Prominence.DefinitenessLevel → Bool

  Which definiteness levels trigger indexing

def Phenomena.Agreement.DifferentialIndexing.IndexingFragment.mk' (name iso639 family : String) (role : Core.Prominence.ArgumentRole) (personIndexed : IndexingPersonLevel → Bool) (animacyIndexed : Core.Prominence.AnimacyLevel → Bool) (definitenessIndexed : Core.Prominence.DefinitenessLevel → Bool) : IndexingFragment

Smart constructor for IndexingFragment. Computes the 2D marks predicate as the product of animacyIndexed and definitenessIndexed, and sets channel :=.indexing.

Equations

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

def Phenomena.Agreement.DifferentialIndexing.IndexingFragment.personConditioned (f : IndexingFragment) : Bool

A dimension is conditioning if the marking predicate is non-uniform: some levels are indexed and some are not.

Equations

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

def Phenomena.Agreement.DifferentialIndexing.IndexingFragment.animacyConditioned (f : IndexingFragment) : Bool

Equations

• f.animacyConditioned = (Core.Prominence.AnimacyLevel.all.any f.animacyIndexed && !Core.Prominence.AnimacyLevel.all.all f.animacyIndexed)

def Phenomena.Agreement.DifferentialIndexing.IndexingFragment.definitenessConditioned (f : IndexingFragment) : Bool

Equations

• f.definitenessConditioned = (Core.Prominence.DefinitenessLevel.all.any f.definitenessIndexed && !Core.Prominence.DefinitenessLevel.all.all f.definitenessIndexed)

def Phenomena.Agreement.DifferentialIndexing.IndexingFragment.isDifferential (f : IndexingFragment) : Bool

At least one dimension conditions the indexing (i.e., is non-uniform).

Equations

• f.isDifferential = (f.personConditioned || f.animacyConditioned || f.definitenessConditioned)

def Phenomena.Agreement.DifferentialIndexing.IndexingFragment.pPolarityCorrect (f : IndexingFragment) : Bool

P indexing has correct polarity if it targets the PROMINENT end: SAP over 3rd, human over inanimate, definite over nonspecific.

Equations

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

def Phenomena.Agreement.DifferentialIndexing.IndexingFragment.aPolarityCorrect (f : IndexingFragment) : Bool

A indexing has correct polarity if it targets the NON-PROMINENT end: 3rd over SAP, inanimate over human, nonspecific over definite.

Equations

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

def Phenomena.Agreement.DifferentialIndexing.IndexingFragment.polarityCorrect (f : IndexingFragment) : Bool

Role-appropriate polarity check. T behaves like P (targets prominent), R behaves like A (targets non-prominent). S is vacuously correct.

Equations

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

Languages where the P argument is differentially indexed. Prominent Ps (SAP, human, definite) are MORE likely to be indexed.

Marking predicates encode the actual pattern per scale. For scales that
are not conditioning, the predicate is uniformly `true` (all levels
indexed). For conditioning scales, the predicate marks the prominent
end as `true` and the non-prominent end as `false`.

Source references are from @cite{just-2024}. 

def Phenomena.Agreement.DifferentialIndexing.abkhaz : IndexingFragment

Abkhaz (NW Caucasian): P indexed only for SAP.

Equations

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

def Phenomena.Agreement.DifferentialIndexing.amharic : IndexingFragment

Amharic (Semitic): P indexed for SAP and definite objects.

Equations

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

def Phenomena.Agreement.DifferentialIndexing.basque : IndexingFragment

Basque (Isolate): object agreement only for SAP objects.

Equations

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

def Phenomena.Agreement.DifferentialIndexing.georgian : IndexingFragment

Georgian (Kartvelian): P agreement conditioned by person — indirect objects (dative) are indexed for SAP only.

Equations

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

def Phenomena.Agreement.DifferentialIndexing.hungarian : IndexingFragment

Hungarian (Uralic): definite conjugation triggered by definite objects; indefinite conjugation for indefinite objects. See also Fragments.Hungarian.Predicates for the conjugation split.

Equations

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

def Phenomena.Agreement.DifferentialIndexing.kagulu : IndexingFragment

Kagulu (Bantu): object marker for animate+ objects.

Equations

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

def Phenomena.Agreement.DifferentialIndexing.kinzadi : IndexingFragment

KiNzadi (Bantu): P indexed for SAP only.

Equations

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

def Phenomena.Agreement.DifferentialIndexing.koorete : IndexingFragment

Koorete (Omotic): P indexed for SAP only.

Equations

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

def Phenomena.Agreement.DifferentialIndexing.maltese : IndexingFragment

Maltese (Semitic): definite object agreement — verb agrees with definite objects via suffixed object markers (Just & Čéplö 2022).

Equations

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

def Phenomena.Agreement.DifferentialIndexing.nkoreKiga : IndexingFragment

Nkore-Kiga (Bantu): object marker for SAP objects.

Equations

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

def Phenomena.Agreement.DifferentialIndexing.romanian : IndexingFragment

Romanian (Romance): clitic doubling conditioned by person, animacy, and definiteness. SAP + human + definite = doubled.

Equations

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

def Phenomena.Agreement.DifferentialIndexing.somali : IndexingFragment

Somali (Cushitic): P indexed for SAP — full paradigm for SAP objects, reduced for 3rd person. Focus/topicality also plays a role but is not captured in the prominence grid.

Equations

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

def Phenomena.Agreement.DifferentialIndexing.swahili : IndexingFragment

Swahili (Bantu): object marker obligatory for human objects, optional/ absent for non-human.

Equations

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

def Phenomena.Agreement.DifferentialIndexing.teiwa : IndexingFragment

Teiwa (Trans-New Guinea): P indexed for animate objects.

Equations

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

def Phenomena.Agreement.DifferentialIndexing.welsh : IndexingFragment

Welsh (Celtic): synthetic agreement only with pronominal (SAP) objects; analytic (no agreement) with 3rd person full NPs.

Equations

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

def Phenomena.Agreement.DifferentialIndexing.zulu : IndexingFragment

Zulu (Bantu): object marker for animate objects.

Equations

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

def Phenomena.Agreement.DifferentialIndexing.spokenArabic : IndexingFragment

Spoken Arabic varieties (Semitic): P indexed for SAP only — object suffixes restricted to pronominal objects.

Equations

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

Languages where the A argument is differentially indexed. Non-prominent As (3rd person, inanimate, indefinite) are MORE likely to be indexed. The polarity is REVERSED relative to P indexing.

Source references from @cite{just-2024}. 

def Phenomena.Agreement.DifferentialIndexing.jamsay : IndexingFragment

Jamsay (Dogon): A indexed only for 3rd person agents — SAP agents are not cross-referenced on the verb.

Equations

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

def Phenomena.Agreement.DifferentialIndexing.kharia : IndexingFragment

Kharia (Munda): A indexed for 3rd person agents.

Equations

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

def Phenomena.Agreement.DifferentialIndexing.mundari : IndexingFragment

Mundari (Munda): A indexed for 3rd person agents.

Equations

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

def Phenomena.Agreement.DifferentialIndexing.juang : IndexingFragment

Juang (Munda): A indexed for 3rd person agents.

Equations

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

def Phenomena.Agreement.DifferentialIndexing.anywa : IndexingFragment

Anywa (Nilotic): A indexed for 3rd person agents only — SAP agents are not cross-referenced.

Equations

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

def Phenomena.Agreement.DifferentialIndexing.reyesano : IndexingFragment

Reyesano (Tacanan): A indexed for 3rd person and non-human agents.

Equations

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

def Phenomena.Agreement.DifferentialIndexing.easternMansi : IndexingFragment

Eastern Mansi (Uralic): A indexed for indefinite/non-topical agents.

Equations

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

def Phenomena.Agreement.DifferentialIndexing.pIndexingLanguages : List IndexingFragment

All differential P indexing languages in the sample.

Equations

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

def Phenomena.Agreement.DifferentialIndexing.aIndexingLanguages : List IndexingFragment

All differential A indexing languages in the sample.

Equations

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

def Phenomena.Agreement.DifferentialIndexing.allIndexingLanguages : List IndexingFragment

All differential indexing languages.

Equations

• Phenomena.Agreement.DifferentialIndexing.allIndexingLanguages = Phenomena.Agreement.DifferentialIndexing.pIndexingLanguages ++ Phenomena.Agreement.DifferentialIndexing.aIndexingLanguages

theorem Phenomena.Agreement.DifferentialIndexing.pIndexing_all_roleP : (pIndexingLanguages.all fun (x : IndexingFragment) => x.role == Core.Prominence.ArgumentRole.P) = true

All P indexing languages have role P.

theorem Phenomena.Agreement.DifferentialIndexing.aIndexing_all_roleA : (aIndexingLanguages.all fun (x : IndexingFragment) => x.role == Core.Prominence.ArgumentRole.A) = true

All A indexing languages have role A.

theorem Phenomena.Agreement.DifferentialIndexing.all_differential : (allIndexingLanguages.all fun (x : IndexingFragment) => x.isDifferential) = true

All profiles are genuinely differential (at least one conditioning factor is non-uniform). Derived from the marking predicates.

The counts below are COMPUTED from the marking predicates via personConditioned, animacyConditioned, definitenessConditioned. No hard-coded numbers — if a language's marking predicate changes, the counts update automatically.

def Phenomena.Agreement.DifferentialIndexing.pPersonConditioned : List IndexingFragment

P indexing languages conditioned by person (derived).

Equations

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

def Phenomena.Agreement.DifferentialIndexing.pAnimacyConditioned : List IndexingFragment

P indexing languages conditioned by animacy (derived).

Equations

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

def Phenomena.Agreement.DifferentialIndexing.pDefinitenessConditioned : List IndexingFragment

P indexing languages conditioned by definiteness (derived).

Equations

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

def Phenomena.Agreement.DifferentialIndexing.aPersonConditioned : List IndexingFragment

A indexing languages conditioned by person (derived).

Equations

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

"The very same referential properties condition both differential P and differential A indexing."

Person is the most frequent conditioning factor for BOTH P and A
indexing. This is derived from the marking predicates. 

theorem Phenomena.Agreement.DifferentialIndexing.person_dominates_P : pPersonConditioned.length > pAnimacyConditioned.length ∧ pPersonConditioned.length > pDefinitenessConditioned.length

Person is the most common conditioning factor for P indexing: more P-indexing languages are person-conditioned than animacy- or definiteness-conditioned.

theorem Phenomena.Agreement.DifferentialIndexing.person_dominates_A : aPersonConditioned.length > (List.filter (fun (x : IndexingFragment) => x.animacyConditioned) aIndexingLanguages).length ∧ aPersonConditioned.length > (List.filter (fun (x : IndexingFragment) => x.definitenessConditioned) aIndexingLanguages).length

Person is the most common conditioning factor for A indexing: more A-indexing languages are person-conditioned than animacy- or definiteness-conditioned.

"The very same referential properties condition both differential P and differential A indexing."

theorem Phenomena.Agreement.DifferentialIndexing.person_conditions_both : ((pIndexingLanguages.any fun (x : IndexingFragment) => x.personConditioned) && decide ((aIndexingLanguages.any fun (x : IndexingFragment) => x.personConditioned) = true)) = true

Person conditions both P and A indexing.

theorem Phenomena.Agreement.DifferentialIndexing.animacy_conditions_both : ((pIndexingLanguages.any fun (x : IndexingFragment) => x.animacyConditioned) && decide ((aIndexingLanguages.any fun (x : IndexingFragment) => x.animacyConditioned) = true)) = true

Animacy conditions both P and A indexing.

theorem Phenomena.Agreement.DifferentialIndexing.definiteness_conditions_both : ((pIndexingLanguages.any fun (x : IndexingFragment) => x.definitenessConditioned) && decide ((aIndexingLanguages.any fun (x : IndexingFragment) => x.definitenessConditioned) = true)) = true

Definiteness conditions both P and A indexing.

"The directions in which these scales operate form a mirror image: indexing targets prominent P arguments on the one hand and non-prominent A arguments on the other."

theorem Phenomena.Agreement.DifferentialIndexing.p_indexing_targets_prominent : (pIndexingLanguages.all fun (x : IndexingFragment) => x.pPolarityCorrect) = true

All P indexing languages have correct polarity: they target the prominent end of each conditioning scale.

theorem Phenomena.Agreement.DifferentialIndexing.a_indexing_targets_nonprominent : (aIndexingLanguages.all fun (x : IndexingFragment) => x.aPolarityCorrect) = true

All A indexing languages have correct polarity: they target the non-prominent end of each conditioning scale.

theorem Phenomena.Agreement.DifferentialIndexing.mirror_image_universal : (allIndexingLanguages.all fun (x : IndexingFragment) => x.polarityCorrect) = true

The mirror image holds universally across the sample: every language has role-appropriate polarity.

For languages where animacy and/or definiteness condition indexing, we verify monotonicity of the inherited DifferentialMarkingProfile on the 2D grid. The marks predicate is derived from the fragment's animacyIndexed and definitenessIndexed — no separate stipulation.

theorem Phenomena.Agreement.DifferentialIndexing.hungarian_monotone : hungarian.isMonotone = true

All animacy/definiteness-conditioned profiles are monotone.

theorem Phenomena.Agreement.DifferentialIndexing.swahili_monotone : swahili.isMonotone = true

theorem Phenomena.Agreement.DifferentialIndexing.kagulu_monotone : kagulu.isMonotone = true

theorem Phenomena.Agreement.DifferentialIndexing.easternMansi_monotone : easternMansi.isMonotone = true

theorem Phenomena.Agreement.DifferentialIndexing.swahili_animacy_only : swahili.isAnimacyOnly = true

Swahili P indexing depends only on animacy (definiteness is irrelevant).

theorem Phenomena.Agreement.DifferentialIndexing.kagulu_animacy_only : kagulu.isAnimacyOnly = true

Kagulu P indexing depends only on animacy.

theorem Phenomena.Agreement.DifferentialIndexing.hungarian_definiteness_only : hungarian.isDefinitenessOnly = true

Hungarian P indexing depends only on definiteness (animacy is irrelevant).

theorem Phenomena.Agreement.DifferentialIndexing.easternMansi_definiteness_only : easternMansi.isDefinitenessOnly = true

Eastern Mansi A indexing depends only on definiteness.

theorem Phenomena.Agreement.DifferentialIndexing.bantu_all_P : (allIndexingLanguages.all fun (p : IndexingFragment) => if (p.family == "Bantu") = true then p.role == Core.Prominence.ArgumentRole.P else true) = true

Bantu languages in the sample all show P indexing.

theorem Phenomena.Agreement.DifferentialIndexing.munda_all_A : (allIndexingLanguages.all fun (p : IndexingFragment) => if (p.family == "Austroasiatic (Munda)") = true then p.role == Core.Prominence.ArgumentRole.A else true) = true

Munda languages in the sample all show A indexing.

theorem Phenomena.Agreement.DifferentialIndexing.family_diversity : (List.map (fun (x : IndexingFragment) => x.family) allIndexingLanguages).eraseDups.length ≥ 10

The sample covers at least 10 distinct language families.

"Prominent arguments, be it A or P (or probably any other role), tend to be indexed more readily than arguments which are low in identifiability, animacy or topicality."

The mirror image is NOT a coincidence — it follows from a single
principle (indexing tracks prominent referents) combined with different
default prominence per role (A defaults high, P defaults low). 

theorem Phenomena.Agreement.DifferentialIndexing.prominent_P_indexed : (pPersonConditioned.all fun (x : IndexingFragment) => x.personIndexed IndexingPersonLevel.sap) = true

For every person-conditioned P-indexing language, SAP is indexed (= prominent P gets indexed).

theorem Phenomena.Agreement.DifferentialIndexing.nonprominent_A_indexed : (aPersonConditioned.all fun (x : IndexingFragment) => x.personIndexed IndexingPersonLevel.third) = true

For every person-conditioned A-indexing language, 3rd person is indexed (= non-prominent A gets indexed, because A's default is prominent).

theorem Phenomena.Agreement.DifferentialIndexing.complement_differs_by_role : (pPersonConditioned.all fun (f : IndexingFragment) => !f.personIndexed IndexingPersonLevel.third) = true ∧ (aPersonConditioned.all fun (f : IndexingFragment) => !f.personIndexed IndexingPersonLevel.sap) = true

The unified principle predicts that the COMPLEMENT of "indexed" differs by role: P-indexing excludes 3rd person, A-indexing excludes SAP. Both follow from "index the prominent referent" + role defaults.