Indefinite-pronoun typology — consensus substrate

@cite{haspelmath-1997} @cite{wals-2013}

Theory-neutral types for cross-linguistic indefinite-pronoun data, following the same Typology/{Domain}.lean pattern as WordOrder.lean, Adposition.lean, MorphProfile.lean. Plugged into per-language LanguageProfile.indefinites via withIndefinites (see Typology/LanguageProfile.lean).

Theory-specific apparatus (Degano & Aloni's 7-type team-semantic typology, choice-function denotations, Hamblin alternatives, …) lives as projections in theory files (e.g., Theories/Semantics/Quantification/DeganoAloni2025.lean), not in this substrate. This follows the consensus-only Fragment-schema discipline: the substrate carries only what a typological reference grammar would record.

Schema

• HaspelmathFunction: 9 functions on @cite{haspelmath-1997}'s implicational map
• MorphologicalBasis: 4 morphological strategies (= 4 of WALS F46A's 5 cells)
• IndefiniteEntry: a form's gloss + basis + function-coverage
• IndefiniteParadigm: a language's full paradigm + ISO 639-3 code

WALS bridge

MorphologicalBasis.toWALS46A maps each basis to its WALS F46A cell; 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 live in Phenomena/Indefinites/Typology.lean.

inductive Typology.Indefinite.HaspelmathFunction : Type

The 9 indefinite-pronoun functions on @cite{haspelmath-1997}'s implicational map. A single form covers a contiguous region of the map.

• specificKnown : HaspelmathFunction

  Function 1: Specific known. Speaker has a referent in mind.

• specificUnknown : HaspelmathFunction

  Function 2: Specific unknown. Speaker presupposes a referent but cannot identify it.

• irrealis : HaspelmathFunction

  Function 3: Irrealis non-specific. No specific referent intended.

• question : HaspelmathFunction

  Function 4: Polar / content question.

• conditional : HaspelmathFunction

  Function 5: Conditional protasis.

• comparative : HaspelmathFunction

  Function 6: Standard of comparison.

• indirectNeg : HaspelmathFunction

  Function 7: Indirect (clause-mate) negation.

• directNeg : HaspelmathFunction

  Function 8: Direct negation.

• freeChoice : HaspelmathFunction

  Function 9: Free choice.

@[implicit_reducible]

instance Typology.Indefinite.instDecidableEqHaspelmathFunction : DecidableEq HaspelmathFunction

Equations

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

@[implicit_reducible]

instance Typology.Indefinite.instReprHaspelmathFunction : Repr HaspelmathFunction

Equations

• Typology.Indefinite.instReprHaspelmathFunction = { reprPrec := Typology.Indefinite.instReprHaspelmathFunction.repr }

def Typology.Indefinite.instReprHaspelmathFunction.repr : HaspelmathFunction → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.Indefinite.instBEqHaspelmathFunction : BEq HaspelmathFunction

Equations

• Typology.Indefinite.instBEqHaspelmathFunction = { beq := Typology.Indefinite.instBEqHaspelmathFunction.beq }

def Typology.Indefinite.instBEqHaspelmathFunction.beq : HaspelmathFunction → HaspelmathFunction → Bool

Equations

• Typology.Indefinite.instBEqHaspelmathFunction.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Typology.Indefinite.HaspelmathFunction.all : List HaspelmathFunction

All nine functions, listed in map order.

Equations

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

def Typology.Indefinite.HaspelmathFunction.adjacent : HaspelmathFunction → List HaspelmathFunction

Adjacency on @cite{haspelmath-1997}'s implicational map.

specKnown — specUnknown — irrealis — question — conditional — indNeg — dirNeg
                                                                          |
                                                freeChoice — comparative —+

Crucial typological claim: any pronoun series covers a contiguous region.

Equations

• Typology.Indefinite.HaspelmathFunction.specificKnown.adjacent = [Typology.Indefinite.HaspelmathFunction.specificUnknown]
• Typology.Indefinite.HaspelmathFunction.specificUnknown.adjacent = [Typology.Indefinite.HaspelmathFunction.specificKnown, Typology.Indefinite.HaspelmathFunction.irrealis]
• Typology.Indefinite.HaspelmathFunction.irrealis.adjacent = [Typology.Indefinite.HaspelmathFunction.specificUnknown, Typology.Indefinite.HaspelmathFunction.question]
• Typology.Indefinite.HaspelmathFunction.question.adjacent = [Typology.Indefinite.HaspelmathFunction.irrealis, Typology.Indefinite.HaspelmathFunction.conditional]
• Typology.Indefinite.HaspelmathFunction.conditional.adjacent = [Typology.Indefinite.HaspelmathFunction.question, Typology.Indefinite.HaspelmathFunction.indirectNeg]
• Typology.Indefinite.HaspelmathFunction.indirectNeg.adjacent = [Typology.Indefinite.HaspelmathFunction.conditional, Typology.Indefinite.HaspelmathFunction.directNeg]
• Typology.Indefinite.HaspelmathFunction.directNeg.adjacent = [Typology.Indefinite.HaspelmathFunction.indirectNeg, Typology.Indefinite.HaspelmathFunction.comparative]
• Typology.Indefinite.HaspelmathFunction.comparative.adjacent = [Typology.Indefinite.HaspelmathFunction.directNeg, Typology.Indefinite.HaspelmathFunction.freeChoice]
• Typology.Indefinite.HaspelmathFunction.freeChoice.adjacent = [Typology.Indefinite.HaspelmathFunction.comparative]

def Typology.Indefinite.HaspelmathFunction.isDE : HaspelmathFunction → Bool

Is f a downward-entailing / nonveridical context (the classical NPI-licensing region: question, conditional, indirect/direct negation)? Used by @cite{chierchia-2006}-style polarity-item typologies to predict NPI distribution.

Equations

• Typology.Indefinite.HaspelmathFunction.question.isDE = true
• Typology.Indefinite.HaspelmathFunction.conditional.isDE = true
• Typology.Indefinite.HaspelmathFunction.indirectNeg.isDE = true
• Typology.Indefinite.HaspelmathFunction.directNeg.isDE = true
• x✝.isDE = false

def Typology.Indefinite.HaspelmathFunction.isFC : HaspelmathFunction → Bool

Is f a free-choice context (comparative + freeChoice)? Comparative standards are universal-flavored and pattern with FC cross-linguistically (@cite{haspelmath-1997}).

Equations

• Typology.Indefinite.HaspelmathFunction.comparative.isFC = true
• Typology.Indefinite.HaspelmathFunction.freeChoice.isFC = true
• x✝.isFC = false

def Typology.Indefinite.HaspelmathFunction.bfsReachable (funcs : List HaspelmathFunction) (start : HaspelmathFunction) (fuel : ℕ := 10) : List HaspelmathFunction

BFS on the implicational map restricted to a given set of functions. Returns the set of nodes reachable from start through edges whose endpoints both lie in funcs.

Equations

• Typology.Indefinite.HaspelmathFunction.bfsReachable funcs start fuel = Typology.Indefinite.HaspelmathFunction.bfsReachable.go funcs [start] [start] fuel

def Typology.Indefinite.HaspelmathFunction.bfsReachable.go (funcs queue visited : List HaspelmathFunction) (fuel : ℕ) : List HaspelmathFunction

Equations

• One or more equations did not get rendered due to their size.
• Typology.Indefinite.HaspelmathFunction.bfsReachable.go funcs queue visited 0 = visited
• Typology.Indefinite.HaspelmathFunction.bfsReachable.go funcs [] visited fuel = visited

def Typology.Indefinite.HaspelmathFunction.isContiguous (funcs : List HaspelmathFunction) : Bool

A list of functions is contiguous on the implicational map iff BFS from any element reaches all others. @cite{haspelmath-1997}'s key constraint: every pronoun series must cover a contiguous region.

Equations

• Typology.Indefinite.HaspelmathFunction.isContiguous [] = true
• Typology.Indefinite.HaspelmathFunction.isContiguous (f :: tail) = (f :: tail).all (Typology.Indefinite.HaspelmathFunction.bfsReachable (f :: tail) f 15).contains

inductive Typology.Indefinite.MorphologicalBasis : Type

@cite{haspelmath-1997}'s four morphological strategies for deriving indefinite pronouns. Aligns with the four single-strategy values of @cite{wals-2013} F46A; F46A's .mixed cell arises only at the paradigm level (see IndefiniteParadigm.toWALS46A).

• interrogative : MorphologicalBasis

  Built from interrogative pronouns (who-, what-, …).

• genericNoun : MorphologicalBasis

  Built from generic nouns ('person', 'thing', 'place').

• special : MorphologicalBasis

  A dedicated indefinite morpheme.

• existentialConstruction : MorphologicalBasis

  An existential predication construction.

@[implicit_reducible]

instance Typology.Indefinite.instDecidableEqMorphologicalBasis : DecidableEq MorphologicalBasis

Equations

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

@[implicit_reducible]

instance Typology.Indefinite.instReprMorphologicalBasis : Repr MorphologicalBasis

Equations

• Typology.Indefinite.instReprMorphologicalBasis = { reprPrec := Typology.Indefinite.instReprMorphologicalBasis.repr }

def Typology.Indefinite.instReprMorphologicalBasis.repr : MorphologicalBasis → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.Indefinite.instBEqMorphologicalBasis : BEq MorphologicalBasis

Equations

• Typology.Indefinite.instBEqMorphologicalBasis = { beq := Typology.Indefinite.instBEqMorphologicalBasis.beq }

def Typology.Indefinite.instBEqMorphologicalBasis.beq : MorphologicalBasis → MorphologicalBasis → Bool

Equations

• Typology.Indefinite.instBEqMorphologicalBasis.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

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

Forward map to the @cite{wals-2013} F46A category for a single basis. F46A's fifth cell .mixed is reserved for paradigms with multiple bases.

Equations

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

structure Typology.Indefinite.IndefiniteEntry : Type

A single indefinite-pronoun form: surface form, gloss, morphological basis, and the @cite{haspelmath-1997} functions it covers.

functions is the realized cross-linguistic distribution (textbook-consensus data). Theory-specific predictions about which functions a form should cover (Degano & Aloni 7-type team-semantics, choice-function denotation, Hamblin alternatives) are projections of this entry into theory-side types, not fields of the entry.

• language : String
• form : String

  Surface form including any required host (e.g., "kim ere", "irgend-").

• gloss : String
• basis : MorphologicalBasis
• functions : Finset HaspelmathFunction

def Typology.Indefinite.instDecidableEqIndefiniteEntry.decEq (x✝ x✝¹ : IndefiniteEntry) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Typology.Indefinite.instDecidableEqIndefiniteEntry : DecidableEq IndefiniteEntry

Equations

• Typology.Indefinite.instDecidableEqIndefiniteEntry = Typology.Indefinite.instDecidableEqIndefiniteEntry.decEq

@[implicit_reducible]

instance Typology.Indefinite.instReprIndefiniteEntry : Repr IndefiniteEntry

Manual Repr showing just language.form to avoid the unsafe Repr (Finset α) instance from Mathlib.Data.Finset.Sort, which would propagate unsafety into every consumer of IndefiniteEntry.

Equations

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

def Typology.Indefinite.IndefiniteEntry.covers (e : IndefiniteEntry) (f : HaspelmathFunction) : Bool

Does this entry cover function f?

Equations

• e.covers f = decide (f ∈ e.functions)

structure Typology.Indefinite.IndefiniteParadigm : Type

A language's full indefinite-pronoun paradigm. isoCode is ISO 639-3, the join key for @cite{wals-2013} Datapoint.iso.

• language : String
• isoCode : String
• forms : List IndefiniteEntry

def Typology.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 Typology.Indefinite.instDecidableEqIndefiniteParadigm : DecidableEq IndefiniteParadigm

Equations

• Typology.Indefinite.instDecidableEqIndefiniteParadigm = Typology.Indefinite.instDecidableEqIndefiniteParadigm.decEq

@[implicit_reducible]

instance Typology.Indefinite.instReprIndefiniteParadigm : Repr IndefiniteParadigm

Equations

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

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

Equations

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

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

Forms in p whose distribution covers function f.

Equations

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

def Typology.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 : Typology.Indefinite.IndefiniteEntry) => x.form) (List.find? (fun (x : Typology.Indefinite.IndefiniteEntry) => x.covers f) p.forms)

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

The list of distinct morphological bases used in this paradigm.

Equations

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

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

Derive the @cite{wals-2013} 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 Typology.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 Typology.Indefinite.IndefiniteParadigm.formCount (p : IndefiniteParadigm) : ℕ

Number of distinct forms in the paradigm.

Equations

• p.formCount = p.forms.length

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

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

Equations

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

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

Every form covers a contiguous region on the @cite{haspelmath-1997} map.

Equations

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

@[implicit_reducible]

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

Equations

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

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

The paradigm covers all nine functions on the implicational map.

Equations

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

@[implicit_reducible]

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

Equations

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

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

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

Equations

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

@[implicit_reducible]

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

Equations

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

def Typology.Indefinite.IndefiniteEntry.functionList (e : IndefiniteEntry) : List HaspelmathFunction

For each form, the list of functions it covers, in HaspelmathFunction.all order.

Equations

• e.functionList = List.filter (fun (x : Typology.Indefinite.HaspelmathFunction) => e.covers x) Typology.Indefinite.HaspelmathFunction.all

def Typology.Indefinite.IndefiniteEntry.coverage (e : IndefiniteEntry) : ℕ

Coverage of a single form: number of functions it spans.

Equations

• e.coverage = e.functionList.length

inductive Typology.Indefinite.SyncretismPattern : Type

Syncretism pattern on @cite{haspelmath-1997}'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 Typology.Indefinite.instDecidableEqSyncretismPattern : DecidableEq SyncretismPattern

Equations

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

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

Equations

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

@[implicit_reducible]

instance Typology.Indefinite.instReprSyncretismPattern : Repr SyncretismPattern

Equations

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

@[implicit_reducible]

instance Typology.Indefinite.instBEqSyncretismPattern : BEq SyncretismPattern

Equations

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

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

Equations

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

def Typology.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 Typology.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 Typology.Indefinite.SyncretismPattern.IsAttested (s : SyncretismPattern) : Prop

@cite{haspelmath-1997}'s adjacency universal: ABA is unattested cross-linguistically because NS and SK are non-adjacent on the map.

Equations

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

@[implicit_reducible]

instance Typology.Indefinite.instDecidablePredSyncretismPatternIsAttested : DecidablePred SyncretismPattern.IsAttested

Equations

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

theorem Typology.Indefinite.aba_unattested : ¬SyncretismPattern.ABA.IsAttested

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

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

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

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

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