Indefinite-pronoun typology — cross-linguistic generalizations

[Has97] [DH13b]

Typological generalizations over indefinite pronouns. The lexical object itself — IndefinitePronoun and its [Has97] feature taxonomy (HaspelmathFunction, OntologicalCategory, MorphologicalBasis) — is an object, and lives in the pronoun layer at Syntax/Pronoun/Indefinite.lean; this file imports it and adds the cross-linguistic apparatus a typological reference grammar records: a language's full paradigm, the WALS F46A bridge, and the SK/SU/NS syncretism typology.

Theory-specific apparatus (Degano & Aloni's 7-type team-semantic typology, choice-function denotations, Hamblin alternatives) lives as projections in theory files (e.g., Studies/DeganoAloni2025.lean), not in this substrate.

Schema

• MorphologicalBasis.toWALS46A: each single basis → its [DH13b] F46A cell
• IndefiniteParadigm: a language's full paradigm + ISO 639-3 code, with F46A derivation, contiguity / coverage / disjointness predicates
• SyncretismPattern: the SK/SU/NS triangle patterns, .ABA banned by the adjacency universal

WALS bridge

IndefiniteParadigm.toWALS46A derives the paradigm-level F46A classification (including the .mixed cell when forms use multiple bases) from the per-form basis distribution. Cross-linguistic bridge theorems anchored on a paper live in that paper's Studies/AuthorYear.lean.

Morphological basis → WALS F46A

def Indefinite.MorphologicalBasis.toWALS46A : MorphologicalBasis → Data.WALS.F46A.IndefinitePronouns

Forward map to the [DH13b] F46A category for a single basis. F46A's fifth cell .mixed is reserved for paradigms with multiple bases.

Equations

• Indefinite.MorphologicalBasis.interrogative.toWALS46A = Data.WALS.F46A.IndefinitePronouns.interrogativeBased
• Indefinite.MorphologicalBasis.genericNoun.toWALS46A = Data.WALS.F46A.IndefinitePronouns.genericNounBased
• Indefinite.MorphologicalBasis.special.toWALS46A = Data.WALS.F46A.IndefinitePronouns.special
• Indefinite.MorphologicalBasis.existentialConstruction.toWALS46A = Data.WALS.F46A.IndefinitePronouns.existentialConstruction

The paradigm

structure Indefinite.IndefiniteParadigm : Type

A language's full indefinite-pronoun paradigm. isoCode is ISO 639-3, the join key for [DH13b] Datapoint.iso.

• language : String
• isoCode : String
• forms : List IndefinitePronoun

def Indefinite.instDecidableEqIndefiniteParadigm.decEq (x✝ x✝¹ : IndefiniteParadigm) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Indefinite.instDecidableEqIndefiniteParadigm : DecidableEq IndefiniteParadigm

Equations

• Indefinite.instDecidableEqIndefiniteParadigm = Indefinite.instDecidableEqIndefiniteParadigm.decEq

@[implicit_reducible]

instance Indefinite.instReprIndefiniteParadigm : Repr IndefiniteParadigm

Equations

• Indefinite.instReprIndefiniteParadigm = { reprPrec := Indefinite.instReprIndefiniteParadigm.repr }

def Indefinite.instReprIndefiniteParadigm.repr : IndefiniteParadigm → ℕ → Std.Format

Equations

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

def Indefinite.IndefiniteParadigm.formsFor (p : IndefiniteParadigm) (f : HaspelmathFunction) : List IndefinitePronoun

Forms in p whose distribution covers function f.

Equations

• p.formsFor f = List.filter (fun (x : Indefinite.IndefinitePronoun) => x.covers f) p.forms

def Indefinite.IndefiniteParadigm.formAt (p : IndefiniteParadigm) (f : HaspelmathFunction) : Option String

The first form (in declaration order) covering f, if any. Used to compute the syncretism pattern over the SK/SU/NS triangle.

Equations

• p.formAt f = Option.map (fun (x : Indefinite.IndefinitePronoun) => x.form) (List.find? (fun (x : Indefinite.IndefinitePronoun) => x.covers f) p.forms)

def Indefinite.IndefiniteParadigm.basisList (p : IndefiniteParadigm) : List MorphologicalBasis

The list of distinct morphological bases used in this paradigm.

Equations

• p.basisList = (List.map (fun (x : Indefinite.IndefinitePronoun) => x.basis) p.forms).dedup

def Indefinite.IndefiniteParadigm.toWALS46A (p : IndefiniteParadigm) : Option Data.WALS.F46A.IndefinitePronouns

Derive the [DH13b] F46A classification from the paradigm's morphological-basis distribution: a single basis maps via MorphologicalBasis.toWALS46A; multiple distinct bases project to F46A's .mixed cell; an empty paradigm yields none.

Equations

• p.toWALS46A = match p.basisList with | [] => none | [b] => some b.toWALS46A | head :: head_1 :: tail => some Data.WALS.F46A.IndefinitePronouns.mixed

def Indefinite.IndefiniteParadigm.wals46A (p : IndefiniteParadigm) : Option Data.WALS.F46A.IndefinitePronouns

WALS F46A classification by lookupISO p.isoCode — independent of the paradigm's basis annotations. Use toWALS46A for the Fragment-derived classification; use wals46A for the WALS-stated classification. The two should agree (a bridge theorem typically asserts this), but for paradigms encoding multiple bases the two can diverge if the WALS encoding picks one strategy.

Equations

• p.wals46A = Option.map (fun (x : Data.WALS.Datapoint Data.WALS.F46A.IndefinitePronouns) => x.value) (Data.WALS.Datapoint.lookupISO Data.WALS.F46A.allData p.isoCode)

def Indefinite.IndefiniteParadigm.formCount (p : IndefiniteParadigm) : ℕ

Number of distinct forms in the paradigm.

Equations

• p.formCount = p.forms.length

def Indefinite.IndefiniteParadigm.allFunctions (p : IndefiniteParadigm) : List HaspelmathFunction

All distinct functions covered across all forms in the paradigm, in HaspelmathFunction.all order.

Equations

• p.allFunctions = List.filter (fun (f : Indefinite.HaspelmathFunction) => p.forms.any fun (x : Indefinite.IndefinitePronoun) => x.covers f) Indefinite.HaspelmathFunction.all

def Indefinite.IndefiniteParadigm.AllContiguous (p : IndefiniteParadigm) : Prop

Every form covers a contiguous region on the [Has97] map.

Equations

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

@[implicit_reducible]

instance Indefinite.IndefiniteParadigm.instDecidableAllContiguous (p : IndefiniteParadigm) : Decidable p.AllContiguous

Equations

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

def Indefinite.IndefiniteParadigm.CoversAllFunctions (p : IndefiniteParadigm) : Prop

The paradigm covers all nine functions on the implicational map.

Equations

• p.CoversAllFunctions = ∀ f ∈ Indefinite.HaspelmathFunction.all, (p.forms.any fun (x : Indefinite.IndefinitePronoun) => x.covers f) = true

@[implicit_reducible]

instance Indefinite.IndefiniteParadigm.instDecidableCoversAllFunctions (p : IndefiniteParadigm) : Decidable p.CoversAllFunctions

Equations

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

def Indefinite.IndefiniteParadigm.FormsDisjoint (p : IndefiniteParadigm) : Prop

The forms have disjoint function sets (no function in two forms).

Equations

• p.FormsDisjoint = ∀ f ∈ Indefinite.HaspelmathFunction.all, (List.filter (fun (x : Indefinite.IndefinitePronoun) => x.covers f) p.forms).length ≤ 1

@[implicit_reducible]

instance Indefinite.IndefiniteParadigm.instDecidableFormsDisjoint (p : IndefiniteParadigm) : Decidable p.FormsDisjoint

Equations

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

Syncretism patterns on the SK/SU/NS triangle

inductive Indefinite.SyncretismPattern : Type

Syncretism pattern on [Has97]'s SK/SU/NS triple. IsAttested excludes .ABA (banned by the implicational map's contiguity universal — NS and SK are not adjacent).

• AAA : SyncretismPattern

  All three coexpressed by a single form (English-style some-).

• ABB : SyncretismPattern

  SU+SK coexpressed, NS distinct (Yakut: ere vs eme).

• AAB : SyncretismPattern

  NS+SU coexpressed, SK distinct (Latin: ali- vs -dam).

• ABC : SyncretismPattern

  All three distinct (Russian: nibud' vs to vs koe-).

• ABA : SyncretismPattern

  NS+SK coexpressed but not SU — unattested (banned by adjacency).

@[implicit_reducible]

instance Indefinite.instDecidableEqSyncretismPattern : DecidableEq SyncretismPattern

Equations

• Indefinite.instDecidableEqSyncretismPattern x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Indefinite.instReprSyncretismPattern.repr : SyncretismPattern → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Indefinite.instReprSyncretismPattern : Repr SyncretismPattern

Equations

• Indefinite.instReprSyncretismPattern = { reprPrec := Indefinite.instReprSyncretismPattern.repr }

def Indefinite.instBEqSyncretismPattern.beq : SyncretismPattern → SyncretismPattern → Bool

Equations

• Indefinite.instBEqSyncretismPattern.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Indefinite.instBEqSyncretismPattern : BEq SyncretismPattern

Equations

• Indefinite.instBEqSyncretismPattern = { beq := Indefinite.instBEqSyncretismPattern.beq }

def Indefinite.classifyTriple (nsForm suForm skForm : String) : SyncretismPattern

Classify a triple of forms (NS, SU, SK) into a syncretism pattern.

Equations

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

def Indefinite.IndefiniteParadigm.syncretism (p : IndefiniteParadigm) : Option SyncretismPattern

The paradigm's syncretism pattern, derived from forms covering SK/SU/NS. Returns none if any of the three functions has no covering form (the paradigm has gaps in the SK/SU/NS region).

Equations

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

def Indefinite.SyncretismPattern.IsAttested (s : SyncretismPattern) : Prop

[Has97]'s adjacency universal: ABA is unattested cross-linguistically because NS and SK are non-adjacent on the map.

Equations

• s.IsAttested = (s ≠ Indefinite.SyncretismPattern.ABA)

@[implicit_reducible]

instance Indefinite.instDecidablePredSyncretismPatternIsAttested : DecidablePred SyncretismPattern.IsAttested

Equations

• Indefinite.instDecidablePredSyncretismPatternIsAttested x✝ = Indefinite.instDecidablePredSyncretismPatternIsAttested._aux_1 x✝

theorem Indefinite.aba_unattested : ¬SyncretismPattern.ABA.IsAttested

Verification

theorem Indefinite.classify_aaa : classifyTriple "A" "A" "A" = SyncretismPattern.AAA

theorem Indefinite.classify_aab : classifyTriple "A" "A" "B" = SyncretismPattern.AAB

theorem Indefinite.classify_abb : classifyTriple "A" "B" "B" = SyncretismPattern.ABB

theorem Indefinite.classify_abc : classifyTriple "A" "B" "C" = SyncretismPattern.ABC

theorem Indefinite.classify_aba : classifyTriple "A" "B" "A" = SyncretismPattern.ABA