Dekier (2021): Morphosyntax of specific and non-specific indefinite markers

[Dek21]

Glossa: a journal of general linguistics 6(1), 1–33.

This paper proposes a nanosyntactic analysis of indefinite markers, arguing that the non-specific, specific unknown, and specific known functions correspond to three layers of a universal syntactic hierarchy (the indefinite fseq):

F₁P (non-specific) ⊂ F₂P (specific unknown) ⊂ F₃P (specific known)

Using data from 45 languages, [Dek21] shows:

1. Four attested syncretism patterns: AAA (English), ABB (Yakut), AAB (Latin), ABC (Russian). The *ABA pattern is unattested.

2. *The ABA generalization ([Bob12]) holds for indefinites: the Superset and Elsewhere Principles of Nanosyntax guarantee that a single lexical entry cannot match two non-contiguous phrasal nodes.

3. Paradigm gaps are monotonic: gaps always start from the TOP of the hierarchy (SK first, then SU). No language has a gap for NS while filling SU or SK.

4. Prefix vs suffix: spellout-driven movement produces suffixes (unary foot), subderivation produces prefixes (binary foot). Russian -nibudEntry' and -to are suffixes; koeEntry- is a prefix.

Connection to linglib

This is the paper critiqued by [Bub26]. While Dekier argues that nanosyntax explains the indefinite typology via structural containment, Bubnov argues that the semantic account of [DA25] (based on team-semantic variation and constancy) provides a better explanation — one that also predicts which type is unattested (type vi) and accounts for bidirectional diachronic change.

Both papers analyze the same cross-linguistic data. This file formalizes Dekier's POSITIVE nanosyntactic analysis; Bubnov2026.lean formalizes the critique.

Dekier's hierarchy:

    F₃P  ⇒  specific known marker
   / \
  F₃  F₂P  ⇒  specific unknown marker
     / \
    F₂  F₁P  ⇒  non-specific marker
        |
        F₁

Features are ordered on a universal fseq. Each layer is characterized
by its rank (depth). A lexical entry at rank r stores F₁...Fᵣ and
matches any target of rank ≤ r via the Superset Principle —
`ExponenceRule.Matches` over the three-grade hierarchy `Fin 3`. 

def Dekier2021.nsRank : Fin 3

Fseq grades for indefinite features.

Equations

• Dekier2021.nsRank = 0

def Dekier2021.suRank : Fin 3

Equations

• Dekier2021.suRank = 1

def Dekier2021.skRank : Fin 3

Equations

• Dekier2021.skRank = 2

structure Dekier2021.ParadigmEntry : Type

A cross-linguistic indefinite paradigm entry. none in a cell indicates a paradigm gap.

• language : String
• nsForm : Option String
• suForm : Option String
• skForm : Option String

def Dekier2021.instReprParadigmEntry.repr : ParadigmEntry → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Dekier2021.instReprParadigmEntry : Repr ParadigmEntry

Equations

• Dekier2021.instReprParadigmEntry = { reprPrec := Dekier2021.instReprParadigmEntry.repr }

@[implicit_reducible]

instance Dekier2021.instDecidableEqParadigmEntry : DecidableEq ParadigmEntry

Equations

• Dekier2021.instDecidableEqParadigmEntry = Dekier2021.instDecidableEqParadigmEntry.decEq

def Dekier2021.instDecidableEqParadigmEntry.decEq (x✝ x✝¹ : ParadigmEntry) : Decidable (x✝ = x✝¹)

Equations

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

def Dekier2021.instBEqParadigmEntry.beq : ParadigmEntry → ParadigmEntry → Bool

Equations

• One or more equations did not get rendered due to their size.
• Dekier2021.instBEqParadigmEntry.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Dekier2021.instBEqParadigmEntry : BEq ParadigmEntry

Equations

• Dekier2021.instBEqParadigmEntry = { beq := Dekier2021.instBEqParadigmEntry.beq }

def Dekier2021.pEnglish : ParadigmEntry

Equations

• Dekier2021.pEnglish = { language := "English", nsForm := some "some-", suForm := some "some-", skForm := some "some-" }

def Dekier2021.pPolish : ParadigmEntry

Equations

• Dekier2021.pPolish = { language := "Polish", nsForm := some "-ś", suForm := some "-ś", skForm := some "-ś" }

def Dekier2021.pJapanese : ParadigmEntry

Equations

• Dekier2021.pJapanese = { language := "Japanese", nsForm := some "-ka", suForm := some "-ka", skForm := some "-ka" }

def Dekier2021.pKorean : ParadigmEntry

Equations

• Dekier2021.pKorean = { language := "Korean", nsForm := some "-nka", suForm := some "-nka", skForm := some "-nka" }

def Dekier2021.pLezgian : ParadigmEntry

Equations

• Dekier2021.pLezgian = { language := "Lezgian", nsForm := some "-jat'ani", suForm := some "-jat'ani", skForm := some "-jat'ani" }

def Dekier2021.pRomanian : ParadigmEntry

Equations

• Dekier2021.pRomanian = { language := "Romanian", nsForm := some "-va", suForm := some "-va", skForm := some "-va" }

def Dekier2021.pBulgarian : ParadigmEntry

Equations

• Dekier2021.pBulgarian = { language := "Bulgarian", nsForm := some "nja-", suForm := some "nja-", skForm := some "nja-" }

def Dekier2021.pSerboCro : ParadigmEntry

Equations

• Dekier2021.pSerboCro = { language := "Serbo-Croatian", nsForm := some "ne-", suForm := some "ne-", skForm := some "ne-" }

def Dekier2021.pCzech : ParadigmEntry

Equations

• Dekier2021.pCzech = { language := "Czech", nsForm := some "ně-", suForm := some "ně-", skForm := some "ně-" }

def Dekier2021.pSlovak : ParadigmEntry

Equations

• Dekier2021.pSlovak = { language := "Slovak", nsForm := some "nie-", suForm := some "nie-", skForm := some "nie-" }

def Dekier2021.pHungarian : ParadigmEntry

Equations

• Dekier2021.pHungarian = { language := "Hungarian", nsForm := some "vala-", suForm := some "vala-", skForm := some "vala-" }

def Dekier2021.pHebrew : ParadigmEntry

Equations

• Dekier2021.pHebrew = { language := "Hebrew", nsForm := some "-šehu", suForm := some "-šehu", skForm := some "-šehu" }

def Dekier2021.pTurkish : ParadigmEntry

Equations

• Dekier2021.pTurkish = { language := "Turkish", nsForm := some "bir-", suForm := some "bir-", skForm := some "bir-" }

def Dekier2021.pLatvian : ParadigmEntry

Equations

• Dekier2021.pLatvian = { language := "Latvian", nsForm := some "kaut-", suForm := some "kaut-", skForm := some "kaut-" }

def Dekier2021.pYakut : ParadigmEntry

Equations

• Dekier2021.pYakut = { language := "Yakut", nsForm := some "-eme", suForm := some "-ere", skForm := some "-ere" }

def Dekier2021.pGeorgian : ParadigmEntry

Equations

• Dekier2021.pGeorgian = { language := "Georgian", nsForm := some "-me", suForm := some "-γac", skForm := some "-γac" }

def Dekier2021.pOssetic : ParadigmEntry

Equations

• Dekier2021.pOssetic = { language := "Ossetic", nsForm := some "is-", suForm := some "-dær", skForm := some "-dær" }

def Dekier2021.pLatin : ParadigmEntry

Equations

• Dekier2021.pLatin = { language := "Latin", nsForm := some "ali-", suForm := some "ali-", skForm := some "-dam" }

def Dekier2021.pRussian : ParadigmEntry

Equations

• Dekier2021.pRussian = { language := "Russian", nsForm := some "-nibud'", suForm := some "-to", skForm := some "koe-" }

def Dekier2021.pLithuanian : ParadigmEntry

Equations

• Dekier2021.pLithuanian = { language := "Lithuanian", nsForm := some "-nors", suForm := some "kaž-", skForm := some "kai-" }

def Dekier2021.pKannada : ParadigmEntry

Equations

• Dekier2021.pKannada = { language := "Kannada", nsForm := some "-aadaruu", suForm := some "-oo", skForm := none }

def Dekier2021.pQuechua : ParadigmEntry

Equations

• Dekier2021.pQuechua = { language := "Quechua", nsForm := some "-pis", suForm := some "-chi", skForm := none }

def Dekier2021.pChinese : ParadigmEntry

Equations

• Dekier2021.pChinese = { language := "Mandarin Chinese", nsForm := some "wh-pron", suForm := none, skForm := none }

def Dekier2021.pSwahili : ParadigmEntry

Equations

• Dekier2021.pSwahili = { language := "Swahili", nsForm := none, suForm := none, skForm := none }

def Dekier2021.pIrish : ParadigmEntry

Equations

• Dekier2021.pIrish = { language := "Irish", nsForm := none, suForm := none, skForm := none }

def Dekier2021.pFilipino : ParadigmEntry

Equations

• Dekier2021.pFilipino = { language := "Filipino", nsForm := none, suForm := none, skForm := none }

def Dekier2021.fullParadigms : List ParadigmEntry

The full paradigms from Table 7 (21 languages with complete data).

Equations

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

theorem Dekier2021.full_paradigm_count : fullParadigms.length = 20

def Dekier2021.gapParadigms : List ParadigmEntry

The paradigm-gap languages from Table 8 (6 languages).

Equations

• Dekier2021.gapParadigms = [Dekier2021.pKannada, Dekier2021.pQuechua, Dekier2021.pChinese, Dekier2021.pSwahili, Dekier2021.pIrish, Dekier2021.pFilipino]

Each syncretism pattern corresponds to a particular lexicon configuration. The spellout algorithm (Superset + Minimize Junk, Morphology.Containment.spellout) derives the surface pattern from the lexicon. Entries are context-free ExponenceRules: an exponent paired with the largest grade its stored constituent spans.

def Dekier2021.englishLex : List (Morphology.Containment.ExponenceRule 3 String)

English AAA: a single entry at rank 2 covers all three layers. some- ⇔ F₃P.

Equations

• Dekier2021.englishLex = [{ exponent := "some-", spans := 2, context := none }]

theorem Dekier2021.english_spellout : Morphology.Containment.spellout englishLex nsRank = some "some-" ∧ Morphology.Containment.spellout englishLex suRank = some "some-" ∧ Morphology.Containment.spellout englishLex skRank = some "some-"

def Dekier2021.yakutLex : List (Morphology.Containment.ExponenceRule 3 String)

Yakut ABB: -emeEntry at rank 0 (F₁P), -ereEntry at rank 2 (F₃P). Elsewhere gives -emeEntry for NS, -ereEntry covers SU and SK.

Equations

• Dekier2021.yakutLex = [{ exponent := "-eme", spans := 0, context := none }, { exponent := "-ere", spans := 2, context := none }]

theorem Dekier2021.yakut_spellout : Morphology.Containment.spellout yakutLex nsRank = some "-eme" ∧ Morphology.Containment.spellout yakutLex suRank = some "-ere" ∧ Morphology.Containment.spellout yakutLex skRank = some "-ere"

def Dekier2021.latinLex : List (Morphology.Containment.ExponenceRule 3 String)

Latin AAB: aliEntry- at rank 1 (F₂P), -damEntry at rank 2 (F₃P). aliEntry- covers NS and SU via Superset; -damEntry wins for SK via Elsewhere (closer match).

Note: the nanosyntactic derivation is complex — aliEntry- is a prefix (subderivation), -damEntry is a suffix (constituent extraction).

Equations

• Dekier2021.latinLex = [{ exponent := "ali-", spans := 1, context := none }, { exponent := "-dam", spans := 2, context := none }]

theorem Dekier2021.latin_spellout : Morphology.Containment.spellout latinLex nsRank = some "ali-" ∧ Morphology.Containment.spellout latinLex suRank = some "ali-" ∧ Morphology.Containment.spellout latinLex skRank = some "-dam"

def Dekier2021.russianLex : List (Morphology.Containment.ExponenceRule 3 String)

Russian ABC: three entries, one per rank. Each layer gets its own exponent. -nibudEntry' ⇔ F₁P (suffix), -to ⇔ F₂P (suffix), koeEntry- ⇔ F₃P (prefix).

Equations

• Dekier2021.russianLex = [{ exponent := "-nibud'", spans := 0, context := none }, { exponent := "-to", spans := 1, context := none }, { exponent := "koe-", spans := 2, context := none }]

theorem Dekier2021.russian_spellout : Morphology.Containment.spellout russianLex nsRank = some "-nibud'" ∧ Morphology.Containment.spellout russianLex suRank = some "-to" ∧ Morphology.Containment.spellout russianLex skRank = some "koe-"

def Dekier2021.lithuanianLex : List (Morphology.Containment.ExponenceRule 3 String)

Lithuanian ABC: three entries at ranks 0, 1, 2. [Dek21] Table 7.

Equations

• Dekier2021.lithuanianLex = [{ exponent := "-nors", spans := 0, context := none }, { exponent := "kaž-", spans := 1, context := none }, { exponent := "kai-", spans := 2, context := none }]

theorem Dekier2021.lithuanian_spellout : Morphology.Containment.spellout lithuanianLex nsRank = some "-nors" ∧ Morphology.Containment.spellout lithuanianLex suRank = some "kaž-" ∧ Morphology.Containment.spellout lithuanianLex skRank = some "kai-"

Patterns are COMPUTED from spellout results, not stipulated. We derive the syncretism check from each Fragment file's canonical .form data rather than restating the form strings here. Note: Russian's Fragment form "-нибудь (-nibud')" differs from Dekier's Table 7 transliteration "-nibud'"; classifyTriple only inspects distinctness, so both classifications coincide as ABC.

theorem Dekier2021.english_is_aaa : Indefinite.classifyTriple English.Indefinites.someEntry.form English.Indefinites.someEntry.form English.Indefinites.someEntry.form = Indefinite.SyncretismPattern.AAA

theorem Dekier2021.yakut_is_abb : Indefinite.classifyTriple Yakut.Indefinites.emeEntry.form Yakut.Indefinites.ereEntry.form Yakut.Indefinites.ereEntry.form = Indefinite.SyncretismPattern.ABB

theorem Dekier2021.latin_is_aab : Indefinite.classifyTriple Latin.Indefinites.aliEntry.form Latin.Indefinites.aliEntry.form Latin.Indefinites.damEntry.form = Indefinite.SyncretismPattern.AAB

theorem Dekier2021.russian_is_abc : Indefinite.classifyTriple Russian.Indefinites.nibudEntry.form Russian.Indefinites.toEntry.form Russian.Indefinites.koeEntry.form = Indefinite.SyncretismPattern.ABC

theorem Dekier2021.lithuanian_is_abc : Indefinite.classifyTriple "-nors" "kaž-" "kai-" = Indefinite.SyncretismPattern.ABC

Lithuanian forms have no Fragment file yet (no Lithuanian.Indefinites), so the strings stay inline here.

The Elsewhere Principle ([Dek21]): "If several lexical items match a syntactic node, insert the entry with the fewest features unspecified for that node."

Combined with the Superset Principle this derives *ABA in general:
any antihomophonous context-free lexicon yields a contiguous
pattern (`Morphology.Containment.isContiguous_spellout`). Each
sample lexicon instantiates the theorem — *ABA is derived, not
inspected case by case. 

theorem Dekier2021.english_contiguous : Morphology.Containment.IsContiguous (Morphology.Containment.spellout englishLex)

English: contiguous spellout (no ABA configuration possible).

theorem Dekier2021.yakut_contiguous : Morphology.Containment.IsContiguous (Morphology.Containment.spellout yakutLex)

Yakut: contiguous spellout.

theorem Dekier2021.latin_contiguous : Morphology.Containment.IsContiguous (Morphology.Containment.spellout latinLex)

Latin: contiguous spellout.

theorem Dekier2021.russian_contiguous : Morphology.Containment.IsContiguous (Morphology.Containment.spellout russianLex)

Russian: contiguous spellout.

theorem Dekier2021.lithuanian_contiguous : Morphology.Containment.IsContiguous (Morphology.Containment.spellout lithuanianLex)

Lithuanian: contiguous spellout.

theorem Dekier2021.aba_unattested_pattern : ¬(Indefinite.classifyTriple "A" "B" "A").IsAttested

The ABA pattern itself is unattested cross-linguistically. This aligns with the *ABA generalization of [Bob12].

[Dek21] Table 8: paradigm gaps follow a monotonic pattern. Gaps always start from the TOP of the hierarchy (SK first, then SU). No language has a gap for NS while having a form for SU or SK.

This follows from the Superset Principle: any entry at rank r
matches ALL targets of rank ≤ r. So if ANY entry exists in the
lexicon, NS (rank 0) is always filled. 

def Dekier2021.kannadaLex : List (Morphology.Containment.ExponenceRule 3 String)

Paradigm gap lexicons: the gap position corresponds to the ABSENCE of high-rank entries.

Equations

• Dekier2021.kannadaLex = [{ exponent := "-aadaruu", spans := 0, context := none }, { exponent := "-oo", spans := 1, context := none }]

theorem Dekier2021.kannada_gap : Morphology.Containment.spellout kannadaLex nsRank = some "-aadaruu" ∧ Morphology.Containment.spellout kannadaLex suRank = some "-oo" ∧ Morphology.Containment.spellout kannadaLex skRank = none

def Dekier2021.chineseLex : List (Morphology.Containment.ExponenceRule 3 String)

Equations

• Dekier2021.chineseLex = [{ exponent := "wh-pron", spans := 0, context := none }]

theorem Dekier2021.chinese_gap : Morphology.Containment.spellout chineseLex nsRank = some "wh-pron" ∧ Morphology.Containment.spellout chineseLex suRank = none ∧ Morphology.Containment.spellout chineseLex skRank = none

def Dekier2021.emptyLex : List (Morphology.Containment.ExponenceRule 3 String)

Equations

• Dekier2021.emptyLex = []

theorem Dekier2021.empty_gap : Morphology.Containment.spellout emptyLex nsRank = none ∧ Morphology.Containment.spellout emptyLex suRank = none ∧ Morphology.Containment.spellout emptyLex skRank = none

theorem Dekier2021.no_ns_implies_no_su_sk (lex : List (Morphology.Containment.ExponenceRule 3 String)) (h : Morphology.Containment.spellout lex nsRank = none) : Morphology.Containment.spellout lex suRank = none ∧ Morphology.Containment.spellout lex skRank = none

Consequence: if NS (rank 0) has no form, nothing does.

theorem Dekier2021.no_su_implies_no_sk (lex : List (Morphology.Containment.ExponenceRule 3 String)) (h : Morphology.Containment.spellout lex suRank = none) : Morphology.Containment.spellout lex skRank = none

Consequence: if SU (rank 1) has no form, SK doesn't either.

[Dek21]: the nanosyntactic derivation predicts a structural difference between prefixes and suffixes:

- **Suffix**: formed via spellout-driven movement (roll-up).
  The stem moves above the indefinite layer, leaving a remnant
  constituent with a unary foot. Result: stem + marker.

- **Prefix**: formed via subderivation. The indefinite layers
  are built in a parallel derivation and integrated as a complex
  left branch. Result: marker + stem.

In Russian:
- *-nibudEntry'* (F₁P, rank 0): suffix — stem rolls up past F₁
- *-to* (F₂P, rank 1): suffix — stem rolls up past F₂
- *koeEntry-* (F₃P, rank 2): prefix — subderived [F₁, F₂, F₃]

Prediction: in a language with both prefixes and suffixes,
the morphological boundary (prefix/suffix break) correlates with
the derivational mechanism switch (spellout movement → subderivation).

structure Dekier2021.MarkerMorphology : Type

Russian indefinite markers with their morphological types. [Dek21].

• form : String
• rank : Fin 3
• morphType : Morphology.Nanosyntax.MorphType

@[implicit_reducible]

instance Dekier2021.instReprMarkerMorphology : Repr MarkerMorphology

Equations

• Dekier2021.instReprMarkerMorphology = { reprPrec := Dekier2021.instReprMarkerMorphology.repr }

def Dekier2021.instReprMarkerMorphology.repr : MarkerMorphology → ℕ → Std.Format

Equations

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

def Dekier2021.russianMarkers : List MarkerMorphology

Equations

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

theorem Dekier2021.russian_suffix_prefix_split (m : MarkerMorphology) : m ∈ russianMarkers → (m.morphType = Morphology.Nanosyntax.MorphType.suffix → m.rank < 2) ∧ (m.morphType = Morphology.Nanosyntax.MorphType.prefix → 2 ≤ m.rank)

In Russian, suffixes occupy the lower ranks and the prefix occupies the highest rank. This matches the spellout-movement (low) vs subderivation (high) prediction.

[Dek21]: the ordering NS < SU < SK is preferred over SK < SU < NS based on functional complexity:

- NS markers only introduce an indefinite entity (simplest)
- SU markers add specificity of the referent
- SK markers add speaker knowledge of the referent's identity

Each higher layer adds a functional property, matching the
nanosyntactic assumption that higher layers on the fseq encode
more complex functional content.

Both orderings are compatible with the syncretism data. The
functional complexity argument selects NS < SU < SK. 

theorem Dekier2021.hierarchy_ordering : nsRank < suRank ∧ suRank < skRank

The hierarchy respects the rank ordering.

Connect the nanosyntactic spellout results to the typed indefinite entries in the fragment files. The fragment entries use the [Has97] function-coverage substrate; the D&A typology is a projection living in Semantics/Quantification/DeganoAloni2025.lean. Dekier's syntactic hierarchy is the candidate counterpart on the morphological side; the bridge here pairs each Fragment entry's function coverage with the lexicon's spellout result.

theorem Dekier2021.english_bridge : English.Indefinites.someEntry.covers Indefinite.HaspelmathFunction.irrealis = true ∧ English.Indefinites.someEntry.covers Indefinite.HaspelmathFunction.specificUnknown = true ∧ English.Indefinites.someEntry.covers Indefinite.HaspelmathFunction.specificKnown = true ∧ Morphology.Containment.spellout englishLex nsRank = some "some-" ∧ Morphology.Containment.spellout englishLex suRank = some "some-" ∧ Morphology.Containment.spellout englishLex skRank = some "some-"

English some- fills all three functions — consistent with a single nanosyntactic entry at rank 2 (F₃P).

theorem Dekier2021.russian_bridge : Russian.Indefinites.nibudEntry.covers Indefinite.HaspelmathFunction.irrealis = true ∧ Russian.Indefinites.toEntry.covers Indefinite.HaspelmathFunction.specificUnknown = true ∧ Russian.Indefinites.koeEntry.covers Indefinite.HaspelmathFunction.specificKnown = true ∧ Morphology.Containment.spellout russianLex nsRank = some "-nibud'" ∧ Morphology.Containment.spellout russianLex suRank = some "-to" ∧ Morphology.Containment.spellout russianLex skRank = some "koe-"

Russian paradigm: three fragments match three spellout results.

theorem Dekier2021.yakut_bridge : Yakut.Indefinites.emeEntry.covers Indefinite.HaspelmathFunction.irrealis = true ∧ Yakut.Indefinites.ereEntry.covers Indefinite.HaspelmathFunction.specificKnown = true ∧ Yakut.Indefinites.ereEntry.covers Indefinite.HaspelmathFunction.specificUnknown = true ∧ Morphology.Containment.spellout yakutLex nsRank = some "-eme" ∧ Morphology.Containment.spellout yakutLex suRank = some "-ere" ∧ Morphology.Containment.spellout yakutLex skRank = some "-ere"

Yakut paradigm: two fragments match two spellout results.

theorem Dekier2021.latin_bridge : Latin.Indefinites.aliEntry.covers Indefinite.HaspelmathFunction.irrealis = true ∧ Latin.Indefinites.aliEntry.covers Indefinite.HaspelmathFunction.specificUnknown = true ∧ Latin.Indefinites.damEntry.covers Indefinite.HaspelmathFunction.specificKnown = true ∧ Morphology.Containment.spellout latinLex nsRank = some "ali-" ∧ Morphology.Containment.spellout latinLex suRank = some "ali-" ∧ Morphology.Containment.spellout latinLex skRank = some "-dam"

Latin paradigm: two fragments match two spellout results.

theorem Dekier2021.kannada_bridge : Kannada.Indefinites.aadaruuEntry.covers Indefinite.HaspelmathFunction.irrealis = true ∧ Kannada.Indefinites.ooEntry.covers Indefinite.HaspelmathFunction.specificUnknown = true ∧ Morphology.Containment.spellout kannadaLex nsRank = some "-aadaruu" ∧ Morphology.Containment.spellout kannadaLex suRank = some "-oo" ∧ Morphology.Containment.spellout kannadaLex skRank = none

Kannada: the SK gap in the nanosyntactic model aligns with the absence of a SK-covering form in the fragment data.

The ParadigmEntry records (Tables 7 & 8) and the nanosyntactic lexicons are two independent representations of the same data. These theorems verify they agree.

theorem Dekier2021.pEnglish_matches_spellout : pEnglish.nsForm = Morphology.Containment.spellout englishLex nsRank ∧ pEnglish.suForm = Morphology.Containment.spellout englishLex suRank ∧ pEnglish.skForm = Morphology.Containment.spellout englishLex skRank

theorem Dekier2021.pYakut_matches_spellout : pYakut.nsForm = Morphology.Containment.spellout yakutLex nsRank ∧ pYakut.suForm = Morphology.Containment.spellout yakutLex suRank ∧ pYakut.skForm = Morphology.Containment.spellout yakutLex skRank

theorem Dekier2021.pLatin_matches_spellout : pLatin.nsForm = Morphology.Containment.spellout latinLex nsRank ∧ pLatin.suForm = Morphology.Containment.spellout latinLex suRank ∧ pLatin.skForm = Morphology.Containment.spellout latinLex skRank

theorem Dekier2021.pRussian_matches_spellout : pRussian.nsForm = Morphology.Containment.spellout russianLex nsRank ∧ pRussian.suForm = Morphology.Containment.spellout russianLex suRank ∧ pRussian.skForm = Morphology.Containment.spellout russianLex skRank

theorem Dekier2021.pLithuanian_matches_spellout : pLithuanian.nsForm = Morphology.Containment.spellout lithuanianLex nsRank ∧ pLithuanian.suForm = Morphology.Containment.spellout lithuanianLex suRank ∧ pLithuanian.skForm = Morphology.Containment.spellout lithuanianLex skRank

theorem Dekier2021.pKannada_matches_spellout : pKannada.nsForm = Morphology.Containment.spellout kannadaLex nsRank ∧ pKannada.suForm = Morphology.Containment.spellout kannadaLex suRank ∧ pKannada.skForm = Morphology.Containment.spellout kannadaLex skRank

theorem Dekier2021.pChinese_matches_spellout : pChinese.nsForm = Morphology.Containment.spellout chineseLex nsRank ∧ pChinese.suForm = Morphology.Containment.spellout chineseLex suRank ∧ pChinese.skForm = Morphology.Containment.spellout chineseLex skRank

[Dek21] analyzed 45 languages total: Basque, Bulgarian, Catalan, Czech, Dutch, English, Filipino, Finnish, French, Georgian, German, Greek, Hausa, Hebrew, Hindi, Hungarian, Icelandic, Irish, Italian, Japanese, Kannada, Kazakh, Korean, Latin, Latvian, Lithuanian, Lezgian, Maltese, Mandarin Chinese, Nanay, Ossetic, Persian, Polish, Portuguese, Quechua, Romanian, Russian, Serbian/Croatian, (Colombian) Spanish, Swahili, Swedish, Turkish, and Yakut.

Of these, 20 have complete paradigms with explicit forms in
Tables 7 (formalized above). 6 have paradigm gaps (Table 8).
The remaining 19 are discussed in the appendices or show patterns
consistent with the four attested types. 

theorem Dekier2021.sample_no_aba : (fullParadigms.all fun (p : ParadigmEntry) => match p.nsForm, p.suForm, p.skForm with | some ns, some su, some sk => decide (Indefinite.classifyTriple ns su sk).IsAttested | x, x_1, x_2 => true) = true

No language in the sample violates *ABA.

theorem Dekier2021.gaps_at_top : (gapParadigms.all fun (p : ParadigmEntry) => decide ((p.skForm.isSome = true → p.suForm.isSome = true) ∧ (p.suForm.isSome = true → p.nsForm.isSome = true))) = true

All paradigm-gap languages have gaps at the TOP of the hierarchy, consistent with the monotonicity prediction.