Haspelmath (1997): indefinite pronoun typology

[Has97]'s implicational map arranges nine indefinite-series functions so that every series covers a connected region (Fig. 4.4 — the geometry of Indefinite.HaspelmathFunction.adjacent). Two samples:

• a Fragment-derived six-language sample (English, German, Yakut, Latin, Kannada, Russian) with per-language bridge theorems verifying that each Fragment's morphological-basis encoding derives the [DH13b] F46A classification of the same language (ISO 639-3 join), plus SK/SU/NS syncretism witnesses;
• a stipulated 17-language polarity-side sample of IndefiniteParadigms with contiguity, coverage, and overlap theorems, and decide-checks connecting the paradigms to Fragments/{Lang}/PolarityItems.lean.

The German, Hungarian, Japanese, Korean, Mandarin, and Quechua (Ancash) paradigms are verified against the book (appendix A.1, A.26, A.36–A.39; Table 4.1); the rest are hand-stipulated pending the same pass. English in particular follows a narrower polarity-view allocation than both the book's coding (Table 4.1: some- 12345, any- 456789) and the [DA25]-shaped Fragments/English/Indefinites.lean; the Fragment-vs-Studies divergence is theorem-ized in Studies/Bubnov2026.lean §11 ([Bub26] reads coverage distributionally, net of paradigmatic competition).

Main results

• english_matches_wals_F46A … kannada_matches_wals_F46A, mandarin_matches_wals_F46A — F46A classifications (Fragment-derived, plus the stipulated Mandarin paradigm) agree with WALS.
• all_languages_contiguous, all_languages_cover_all_functions — the map hypothesis and full coverage on the 17-language sample.
• russian_not_disjoint, german_not_disjoint, hungarian_not_disjoint, mandarin_not_disjoint — series overlap is attested and normal (p. 76).
• freeChoice_multifunction_implies_comparative, japanese_comparative_patterns_with_negation — free choice's only map neighbour is the comparative, which may instead pattern with negation.
• bridges_negation, bridges_question, bridges_npiFci — licensing checks against the polarity Fragments.

Implementation notes

The 17 polarity-side paradigms are stipulated rather than derived from Fragments/{Lang}/Indefinites.lean: the per-form functions field commits to one analysis of the map partition, and the contiguity-driven encoding here genuinely differs from the Fragments' competition-driven one (English, German, Russian). Studies/Chierchia2006.lean consumes the english/italian/german/mandarin paradigms. Latin is absent from F46A's 326-language sample; German and Kannada have SK/SU/NS gaps, so no syncretism witnesses. Substrate: Features/Indefinite.lean (map, morphological bases) and Syntax/Category/Pronoun/IndefiniteParadigm.lean (paradigms, WALS converters, the decidable contiguity / coverage / disjointness predicates).

WALS F46A bridges

theorem Haspelmath1997.yakut_matches_wals_F46A : Yakut.Indefinites.paradigm.toWALS46A = Option.map (fun (x : Data.WALS.Datapoint Data.WALS.F46A.IndefinitePronouns) => x.value) (Data.WALS.Datapoint.lookupISO Data.WALS.F46A.allData "sah")

All four Yakut forms host on interrogative kim, deriving .interrogativeBased, matching WALS for iso "sah".

theorem Haspelmath1997.english_matches_wals_F46A : English.Indefinites.paradigm.toWALS46A = Option.map (fun (x : Data.WALS.Datapoint Data.WALS.F46A.IndefinitePronouns) => x.value) (Data.WALS.Datapoint.lookupISO Data.WALS.F46A.allData "eng")

some- on generic-noun stems derives .genericNounBased, matching WALS for iso "eng".

theorem Haspelmath1997.german_matches_wals_F46A : German.Indefinites.paradigm.toWALS46A = Option.map (fun (x : Data.WALS.Datapoint Data.WALS.F46A.IndefinitePronouns) => x.value) (Data.WALS.Datapoint.lookupISO Data.WALS.F46A.allData "deu")

Special irgend- plus generic-noun jemand/etwas derives .mixed, matching WALS for iso "deu".

theorem Haspelmath1997.russian_matches_wals_F46A : Russian.Indefinites.paradigm.toWALS46A = Option.map (fun (x : Data.WALS.Datapoint Data.WALS.F46A.IndefinitePronouns) => x.value) (Data.WALS.Datapoint.lookupISO Data.WALS.F46A.allData "rus")

All three Russian forms attach to interrogative bases, deriving .interrogativeBased, matching WALS for iso "rus".

theorem Haspelmath1997.kannada_matches_wals_F46A : Kannada.Indefinites.paradigm.toWALS46A = Option.map (fun (x : Data.WALS.Datapoint Data.WALS.F46A.IndefinitePronouns) => x.value) (Data.WALS.Datapoint.lookupISO Data.WALS.F46A.allData "kan")

Both Kannada forms attach to interrogative yāru, deriving .interrogativeBased, matching WALS for iso "kan".

Syncretism witnesses

theorem Haspelmath1997.english_paradigm_AAA : English.Indefinites.paradigm.syncretism = some Indefinite.SyncretismPattern.AAA

theorem Haspelmath1997.yakut_paradigm_ABB : Yakut.Indefinites.paradigm.syncretism = some Indefinite.SyncretismPattern.ABB

theorem Haspelmath1997.latin_paradigm_AAB : Latin.Indefinites.paradigm.syncretism = some Indefinite.SyncretismPattern.AAB

theorem Haspelmath1997.russian_paradigm_ABC : Russian.Indefinites.paradigm.syncretism = some Indefinite.SyncretismPattern.ABC

The 17-language sample

def Haspelmath1997.english : Indefinite.IndefiniteParadigm

English: 4 generic-noun-based series in the polarity-view allocation (narrower than Table 4.1 — see the module docstring).

Equations

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

def Haspelmath1997.russian : Indefinite.IndefiniteParadigm

Russian: 6 interrogative-based series. Coverage follows [DA25] Table 2 (кое- SK; -то epistemic; -то and -нибудь both admit non-specific uses, so Russian fails FormsDisjoint); the Fragment encodes -то more narrowly per [Bub26], and both readings coexist by design (Studies/Bubnov2026.lean §11).

Equations

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

def Haspelmath1997.german : Indefinite.IndefiniteParadigm

German: 4 person-form series (A.1; Table 4.1: etwas 123456, irgend 2345689, jeder 689, n- 7). The temporal je-series (4568) has no person form; the series overlap heavily (p. 76).

Equations

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

def Haspelmath1997.japanese : Indefinite.IndefiniteParadigm

Japanese: 3 interrogative-based series (A.38): -ka non-negative; -mo the negations plus comparative (dare-yori-mo, A284), with verbal negation under direct negation; -demo free choice only (A287).

Equations

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

def Haspelmath1997.mandarin : Indefinite.IndefiniteParadigm

Mandarin: the four regions of Fig. A.36 (A.36.1): generic nouns (rén 'person', typically in the existential frame yǒu rén) for the specific functions, bare interrogatives "in all non-specific non-emphatic functions", the emphatic dōu~yě series on direct negation, and the free-choice determiner rènhé.

Equations

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

theorem Haspelmath1997.mandarin_matches_wals_F46A : mandarin.toWALS46A = Option.map (fun (x : Data.WALS.Datapoint Data.WALS.F46A.IndefinitePronouns) => x.value) (Data.WALS.Datapoint.lookupISO Data.WALS.F46A.allData "cmn")

Mandarin's generic-noun, interrogative, and special bases derive .mixed, matching WALS for iso "cmn".

def Haspelmath1997.turkish : Indefinite.IndefiniteParadigm

Turkish: 5 generic-noun-based series (bir- 'one').

Equations

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

def Haspelmath1997.hindi : Indefinite.IndefiniteParadigm

Hindi-Urdu: 3 series on the special base koii.

Equations

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

def Haspelmath1997.italian : Indefinite.IndefiniteParadigm

Italian: 3 generic-noun-based series.

Equations

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

def Haspelmath1997.finnish : Indefinite.IndefiniteParadigm

Finnish: 4 series on the special joku/kukaan morphemes.

Equations

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

def Haspelmath1997.korean : Indefinite.IndefiniteParadigm

Korean: wh + particle (A.39): bare wh and -nka non-negative (split into a specific and a non-specific row); -to the negations plus comparative (A294); -na free choice (A291).

Equations

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

def Haspelmath1997.hungarian : Indefinite.IndefiniteParadigm

Hungarian: 3 interrogative-based series (A.26; Table 4.1: akár 4589): vala- from specific through indirect negation, sem direct negation, akár-~bár- question/conditional/comparative/free choice — contiguous precisely via the map's question–conditional edge.

Equations

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

def Haspelmath1997.georgian : Indefinite.IndefiniteParadigm

Georgian: 4 interrogative-based series.

Equations

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

def Haspelmath1997.quechua : Indefinite.IndefiniteParadigm

Quechua (Ancash): 2 series (A.37): bare interrogatives for the merged specific node, -pis ('also, even') for all non-specific functions (direct negation with mana … -tsu, A279). Absent from WALS F46A, whose Quechua datapoint is Imbabura.

Equations

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

def Haspelmath1997.yoruba : Indefinite.IndefiniteParadigm

Yoruba: 2 generic-noun-based series (ẹnìkan 'person').

Equations

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

def Haspelmath1997.thai : Indefinite.IndefiniteParadigm

Thai: 3 interrogative-based series.

Equations

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

def Haspelmath1997.tagalog : Indefinite.IndefiniteParadigm

Tagalog: 4 series built on the existential construction.

Equations

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

def Haspelmath1997.swahili : Indefinite.IndefiniteParadigm

Swahili: 3 generic-noun-based series (mtu 'person').

Equations

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

def Haspelmath1997.allLanguages : List Indefinite.IndefiniteParadigm

The polarity-typology sample.

Equations

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

Contiguity and coverage

theorem Haspelmath1997.all_languages_contiguous (p : Indefinite.IndefiniteParadigm) : p ∈ allLanguages → p.AllContiguous

The map hypothesis (Fig. 4.4): every form covers a contiguous region.

theorem Haspelmath1997.all_languages_cover_all_functions (p : Indefinite.IndefiniteParadigm) : p ∈ allLanguages → p.CoversAllFunctions

Every language in the sample covers all nine functions.

theorem Haspelmath1997.russian_not_disjoint : ¬russian.FormsDisjoint

Russian fails FormsDisjoint: -то and -нибудь overlap on non-specific uses ([DA25] Table 2).

theorem Haspelmath1997.german_not_disjoint : ¬german.FormsDisjoint

German fails FormsDisjoint: jemand and irgendwer overlap from SU through indirect negation (A.1).

theorem Haspelmath1997.hungarian_not_disjoint : ¬hungarian.FormsDisjoint

Hungarian fails FormsDisjoint: valaki and akárki overlap on question and conditional (A.26).

theorem Haspelmath1997.mandarin_not_disjoint : ¬mandarin.FormsDisjoint

Mandarin fails FormsDisjoint maximally: the bare-interrogative span contains both emphatic series' regions outright (Fig. A.36).

Typological generalizations

theorem Haspelmath1997.freeChoice_multifunction_implies_comparative (p : Indefinite.IndefiniteParadigm) : p ∈ allLanguages → ∀ e ∈ p.forms, e.covers Indefinite.HaspelmathFunction.freeChoice = true → e.coverage > 1 → e.covers Indefinite.HaspelmathFunction.comparative = true

A form covering free choice plus anything else covers the comparative — free choice's only neighbour on the map.

theorem Haspelmath1997.japanese_comparative_patterns_with_negation : ∃ e ∈ japanese.forms, e.covers Indefinite.HaspelmathFunction.comparative = true ∧ e.covers Indefinite.HaspelmathFunction.directNeg = true ∧ ¬e.covers Indefinite.HaspelmathFunction.freeChoice = true

The comparative need not pattern with free choice: -mo covers it with the negations and without free choice (A.38, §4.7.1).

Map-geometry facts

theorem Haspelmath1997.non_contiguous_pairs : ([[Indefinite.HaspelmathFunction.specificKnown, Indefinite.HaspelmathFunction.directNeg], [Indefinite.HaspelmathFunction.specificKnown, Indefinite.HaspelmathFunction.freeChoice], [Indefinite.HaspelmathFunction.specificKnown, Indefinite.HaspelmathFunction.comparative], [Indefinite.HaspelmathFunction.specificUnknown, Indefinite.HaspelmathFunction.directNeg]].all fun (x : List Indefinite.HaspelmathFunction) => decide (Indefinite.HaspelmathFunction.isContiguous x = false)) = true

Regions skipping the map's intermediate functions are non-contiguous.

theorem Haspelmath1997.named_regions_contiguous : ([[Indefinite.HaspelmathFunction.specificKnown, Indefinite.HaspelmathFunction.specificUnknown], [Indefinite.HaspelmathFunction.specificKnown, Indefinite.HaspelmathFunction.specificUnknown, Indefinite.HaspelmathFunction.irrealis], [Indefinite.HaspelmathFunction.question, Indefinite.HaspelmathFunction.conditional, Indefinite.HaspelmathFunction.indirectNeg], [Indefinite.HaspelmathFunction.question, Indefinite.HaspelmathFunction.conditional, Indefinite.HaspelmathFunction.indirectNeg, Indefinite.HaspelmathFunction.directNeg], [Indefinite.HaspelmathFunction.comparative, Indefinite.HaspelmathFunction.freeChoice], [Indefinite.HaspelmathFunction.question, Indefinite.HaspelmathFunction.conditional, Indefinite.HaspelmathFunction.indirectNeg, Indefinite.HaspelmathFunction.directNeg, Indefinite.HaspelmathFunction.comparative, Indefinite.HaspelmathFunction.freeChoice], Indefinite.HaspelmathFunction.all].all fun (x : List Indefinite.HaspelmathFunction) => Indefinite.HaspelmathFunction.isContiguous x) = true

The map's named regions — specific, NPI, FC, the polarity-sensitive span, and the whole map — are contiguous.

Fragment bridges

Each paradigm's polarity-sensitive forms correspond to Fragments/{Lang}/PolarityItems.lean entries licensed in the matching contexts.

theorem Haspelmath1997.bridges_negation (e : Polarity.Item) : e ∈ [Italian.PolarityItems.nessuno, Russian.PolarityItems.nikto, Japanese.PolarityItems.dareMo, Korean.PolarityItems.nwukwuTo, Hungarian.PolarityItems.senki, Georgian.PolarityItems.aravin, Quechua.PolarityItems.piPis, Mandarin.PolarityItems.sheiDou] → Polarity.LicensingContext.negation ∈ e.licensingContexts

Every direct-negation form with a Fragment counterpart is licensed under clausal negation.

theorem Haspelmath1997.bridges_question (e : Polarity.Item) : e ∈ [English.PolarityItems.any, Turkish.PolarityItems.kimse, Finnish.PolarityItems.kukaan] → Polarity.LicensingContext.question ∈ e.licensingContexts

Every question-span form's Fragment counterpart is licensed in questions.

theorem Haspelmath1997.bridges_npiFci (e : Polarity.Item) : e ∈ [German.PolarityItems.irgendein, Mandarin.PolarityItems.shei] → e.licensor = some Polarity.DEStrength.weak ∧ e.freeChoice = true

The single-form wide-coverage items are dual NPI/FCIs in their Fragments: weak-strength licensor plus free-choice licensing.