Docs / Semantics / Reference / Indefinite

The implicational map of indefinite series

import Linglib.Semantics.Reference.Indefinite · namespace Indefinite

Source

An indefinite series (English some-, Russian -nibud') is used in some of nine functions, which Haspelmath arranges on an implicational map: a graph on the functions whose adjacency requirement says that the functions a series covers form a connected region. The map is implicationalMap, and a region s meets the requirement when (implicationalMap.induce ↑s).Connected, so the book's requirement is a statement of graph theory. The series themselves are IndefinitePronoun.Series.

Main declarations

Implementation notes

The empty region is not connected, as SimpleGraph.Connected requires a vertex; a series covers at least one function. The book counts the possible regions of the map differently from the graph encoded here; see the TODO of Studies/Haspelmath1997.lean.

References

The functions and the map

The nine functions of Haspelmath 1997's implicational map.

inductive HaspelmathFunctionL45–66
:
Type
  • specificKnown : HaspelmathFunction

    In the specific known function the speaker has a referent in mind.

  • specificUnknown : HaspelmathFunction

    In the specific unknown function the speaker presupposes a referent but cannot identify it.

  • irrealis : HaspelmathFunction

    In the irrealis non-specific function no specific referent is intended.

  • question : HaspelmathFunction

    The indefinite stands in a question.

  • conditional : HaspelmathFunction

    The indefinite stands in the protasis of a conditional.

  • comparative : HaspelmathFunction

    The indefinite stands in the standard of a comparative.

  • indirectNeg : HaspelmathFunction

    Indirect negation is superordinate or implicit negation (without, doubt, deny).

  • directNeg : HaspelmathFunction

    Direct negation is clause-mate negation.

  • freeChoice : HaspelmathFunction

    The indefinite is a free-choice item.

Derives DecidableEq, Fintype, Repr.

Used by HaspelmathFunction.number, HaspelmathFunction.adjacent, implicationalMap, implicationalMap_adj, SpecificityFunction.toFunction, specificityFunctions, mem_specificityFunctions

Used in Semantics/PolarityItem/LicensingContext, Dekier2021, Haspelmath1997

The book's numbering of the functions, in which it states the distribution of a series.

def HaspelmathFunction.numberL70–80
:
HaspelmathFunction → ℕ

Built from

Used in Haspelmath1997

adjacent f lists the neighbours of f on the map. The map is a chain from specific known through specific unknown to irrealis, which feeds two parallel tracks, question to indirect negation to direct negation and conditional to comparative to free choice, the tracks joined at question and conditional and at indirect negation and comparative.

                      (4) question —— (6) indirect neg —— (7) direct neg
                           |                |
(1) SK — (2) SU — (3) irr <
                           |                |
                      (5) conditional — (8) comparative — (9) free choice
def HaspelmathFunction.adjacentL82–104
:
HaspelmathFunction → List HaspelmathFunction
Equations

Built from

Used by instDecidableRelHaspelmathFunctionAdjImplicationalMap, implicationalMap_adj

Used in Haspelmath1997

The specificity functions

The three functions at the specific end of the map, which differ in whether the indefinite has a specific referent and in whether the speaker can identify it. They are ordered as the map chains them, from specific known through specific unknown to non-specific.

inductive SpecificityFunctionL125–135
:
Type

Derives DecidableEq, Fintype, Repr.

Used by SpecificityFunction.instLinearOrder, SpecificityFunction.ordConnected_iff, SpecificityFunction.instDecidableOrdConnectedCoeFinset, SpecificityFunction.toFunction, specificityFunctions, mem_specificityFunctions

Used in Bubnov2026, DeganoAloni2025, Dekier2021, Haspelmath1997

L154–155

toFunction embeds the specificity functions in the map, the non-specific function as the irrealis one.

def SpecificityFunction.toFunctionL157–162
:
SpecificityFunction → HaspelmathFunction

Built from ,

Used by SpecificityFunction.toFunction_injective, specificityFunctions, mem_specificityFunctions

Used in DeganoAloni2025, Dekier2021, Haspelmath1997

L164