Documentation

Linglib.Phenomena.Case.Studies.Caha2009

Caha (2009) — The Nanosyntax of Case #

@cite{caha-2009} @cite{blake-1994}

Caha's central proposal (@cite{caha-2009} §1.1): the morphosyntactic representation of each case literally contains the representations of all cases below it on the universal hierarchy: [[[[[ NOM ] ACC ] GEN ] DAT ] P ]. This study file defines the Caha-specific containment predicate RespectsCahaContainment and applies it to each Fragment case inventory.

Caha's Universal Case sequence is NOM – ACC – GEN – DAT – INST – COM (@cite{caha-2009} (10b), p. 10); the Russian-specific sequence inserts a "prepositional" between GEN and DAT (@cite{caha-2009} (16), p. 12). Vocatives are explicitly excluded from Caha's scope (@cite{caha-2009} §1.1 fn. 4, p. 9). For the substrate's encoding of this hierarchy and how it relates to Caha's actual sequence, see Core/Case/Order.lean.

Of 22 Fragment case inventories, 19 conform; the three principled exceptions are: Dargwa (ergative — Caha is keyed to accusative alignment), Finnish (DAT-less, ALL → DAT extension per @cite{blake-1994} Ch. 6), and Hungarian (GEN-less, dative-as-possessor syncretism per @cite{caha-2008} §5).

Caha containment-respect predicate #

Does an inventory respect Caha's containment hierarchy? True iff inv is downward-closed under the canonical PartialOrder Case (Caha containment) defined in Core/Case/Order.lean: whenever c ∈ inv and d ≤ c, then d ∈ inv. Off-hierarchy cases (ERG, ABS, INST, COM, …) impose no constraint — in the Caha order they only have c ≤ c, so the downward-closure condition is vacuous. On-hierarchy c of rank r forces every lower on-hierarchy case (ranks 0, …, r-1) into inv, which is exactly the prefix-contiguity Caha demands.

Mathlib's IsLowerSet would suffice for the same content; the Caha-named predicate is kept here for grep-ability and because the substantive claim is Caha-specific.

def Phenomena.Case.Studies.Caha2009.RespectsCahaContainment (inv : Finset Core.Case) :

Equations

Phenomena.Case.Studies.Caha2009.RespectsCahaContainment inv = ∀ c ∈ inv, ∀ d ≤ c, d ∈ inv

Instances For

@[implicit_reducible]

instance Phenomena.Case.Studies.Caha2009.instDecidableRespectsCahaContainment (inv : Finset Core.Case) :

Decidable (RespectsCahaContainment inv)

Equations

Phenomena.Case.Studies.Caha2009.instDecidableRespectsCahaContainment inv = id inferInstance

Slavic substrate: containment lemmas #

Decoupled from Fragments/Slavic/Case.lean so that the Fragment substrate file does not pull in the Caha-specific containment predicate (which lives here in this study file, not in Core/).

theorem Phenomena.Case.Studies.Caha2009.slavicCore_respectsCaha :

RespectsCahaContainment Fragments.Slavic.Case.coreInventory

theorem Phenomena.Case.Studies.Caha2009.slavicSeven_respectsCaha :

RespectsCahaContainment Fragments.Slavic.Case.sevenCaseInventory

Vacuous: Core.Case.Order.containmentRank .voc = none faithfully encodes Caha's own scope choice (@cite{caha-2009} §1.1 fn. 4, p. 9: "Vocatives ... are ignored throughout this dissertation").

§ 1: Conformers (non-Slavic) #

theorem Phenomena.Case.Studies.Caha2009.german_respectsCaha :

RespectsCahaContainment Fragments.German.Case.caseInventory

theorem Phenomena.Case.Studies.Caha2009.greek_respectsCaha :

RespectsCahaContainment Fragments.Greek.Case.caseInventory

theorem Phenomena.Case.Studies.Caha2009.hindi_respectsCaha :

RespectsCahaContainment Fragments.Hindi.Case.caseInventory

theorem Phenomena.Case.Studies.Caha2009.icelandic_respectsCaha :

RespectsCahaContainment Fragments.Icelandic.Case.caseInventory

theorem Phenomena.Case.Studies.Caha2009.japanese_respectsCaha :

RespectsCahaContainment Fragments.Japanese.Case.caseInventory

theorem Phenomena.Case.Studies.Caha2009.korean_respectsCaha :

RespectsCahaContainment Fragments.Korean.Case.caseInventory

theorem Phenomena.Case.Studies.Caha2009.latin_respectsCaha :

RespectsCahaContainment Fragments.Latin.Case.caseInventory

theorem Phenomena.Case.Studies.Caha2009.mongolian_respectsCaha :

RespectsCahaContainment Fragments.Mongolian.Case.caseInventory

theorem Phenomena.Case.Studies.Caha2009.swissgerman_respectsCaha :

RespectsCahaContainment Fragments.SwissGerman.Case.caseInventory

theorem Phenomena.Case.Studies.Caha2009.tamil_respectsCaha :

RespectsCahaContainment Fragments.Tamil.Case.caseInventory

theorem Phenomena.Case.Studies.Caha2009.telugu_respectsCaha :

RespectsCahaContainment Fragments.Telugu.Case.caseInventory

theorem Phenomena.Case.Studies.Caha2009.turkish_respectsCaha :

RespectsCahaContainment Fragments.Turkish.Case.caseInventory

theorem Phenomena.Case.Studies.Caha2009.yakut_respectsCaha :

RespectsCahaContainment Fragments.Yakut.Case.caseInventory

§ 2: Slavic conformers (one substrate proof, ten aliases) #

Each per-language caseInventory abbrev-aliases coreInventory, so the ten theorems below all reduce to slavicCore_respectsCaha. Cross-Slavic agreement is structural, not coincidental — covers every modern Slavic language with productive case morphology (Bulgarian and Macedonian, which lost case in the noun system, have no Case.lean file).

theorem Phenomena.Case.Studies.Caha2009.belarusian_respectsCaha :

RespectsCahaContainment Fragments.Slavic.Belarusian.Case.caseInventory

theorem Phenomena.Case.Studies.Caha2009.cassubian_respectsCaha :

RespectsCahaContainment Fragments.Slavic.Cassubian.Case.caseInventory

theorem Phenomena.Case.Studies.Caha2009.czech_respectsCaha :

RespectsCahaContainment Fragments.Slavic.Czech.Case.caseInventory

theorem Phenomena.Case.Studies.Caha2009.polish_respectsCaha :

RespectsCahaContainment Fragments.Slavic.Polish.Case.caseInventory

theorem Phenomena.Case.Studies.Caha2009.russian_respectsCaha :

RespectsCahaContainment Fragments.Slavic.Russian.Case.caseInventory

theorem Phenomena.Case.Studies.Caha2009.serbian_respectsCaha :

RespectsCahaContainment Fragments.Slavic.Serbian.Case.caseInventory

theorem Phenomena.Case.Studies.Caha2009.slovak_respectsCaha :

RespectsCahaContainment Fragments.Slavic.Slovak.Case.caseInventory

theorem Phenomena.Case.Studies.Caha2009.slovenian_respectsCaha :

RespectsCahaContainment Fragments.Slavic.Slovenian.Case.caseInventory

theorem Phenomena.Case.Studies.Caha2009.sorbian_respectsCaha :

RespectsCahaContainment Fragments.Slavic.Sorbian.Case.caseInventory

theorem Phenomena.Case.Studies.Caha2009.ukrainian_respectsCaha :

RespectsCahaContainment Fragments.Slavic.Ukrainian.Case.caseInventory

§ 3: Predicted violators #

theorem Phenomena.Case.Studies.Caha2009.dargwa_not_respectsCaha :

¬RespectsCahaContainment Fragments.Dargwa.Case.caseInventory

Dargwa is ergative; Caha's containment is keyed to accusative alignment. ABS/ERG are off-hierarchy in containmentRank, so Dargwa's [abs, erg, gen, dat, com, ess] fails downward closure (GEN/DAT present without NOM/ACC).

theorem Phenomena.Case.Studies.Caha2009.finnish_not_respectsCaha :

¬RespectsCahaContainment Fragments.Finnish.Case.caseInventory

Finnish has no dedicated dative — the allative (-lle) covers recipient function (@cite{blake-1994} Ch. 6, ALL → DAT extension; @cite{karlsson-2017} confirms). The inventory has rank 4 (LOC) without rank 3 (DAT).

theorem Phenomena.Case.Studies.Caha2009.hungarian_not_respectsCaha :

¬RespectsCahaContainment Fragments.Hungarian.Case.caseInventory

Hungarian has no morphological genitive — both standard reference grammars (@cite{kenesei-vago-fenyvesi-1998} §1.10, @cite{rounds-2001} ch. 6) gloss -nak / -nek exclusively as dative; @cite{caha-2008} §5 (pp. 266–267) explicitly addresses Hungarian as the textbook Blake-hierarchy surface counterexample, citing Blake's own footnote that the GEN-less inventory is resolved by treating the dative as expressing possessor function. The inventory has rank 3 (DAT) on Caha's containment hierarchy without rank 2 (GEN), failing downward closure. (Note: this is a counterexample to the containmentRank-based downward-closure predicate, which encodes Blake's hierarchy in Caha's notation; it is not a counterexample to Caha 2008's (28), which is about suffix-vs-postposition ordering and holds vacuously here since Hungarian marks all cases suffixally.)

§ 4: Slavic paradigm-shape syncretism (Caha §§8.3.1-4) #

The conformer theorems above only check inventory cardinality — a trivial agreement, since every Slavic 6-case set obviously satisfies downward-closure. Caha's substantive prediction is about paradigm shape: which morphological cells syncretize within a noun's declension. This section formalizes the paradigm-shape predictions for all four Slavic languages Caha analyses in detail. Distinct shapes are factored into Slavic.SyncretismPatterns (§ 4.1) so per-language sections are docstring + attestation lists.

Per-language sub-sections appear in encoding order (Serbian, Slovene, Ukrainian, Czech), not Caha's chapter order (which has Czech §8.3.3 before Ukrainian §8.3.4) — file structure follows the order shapes were added; cross-Slavic narrative closes in § 4.6.

@[reducible, inline]

abbrev Phenomena.Case.Studies.Caha2009.Slavic.slavicRank :

Core.Case → Option (Fin 6)

Caha's Slavic-specific Case sequence (@cite{caha-2009} (16), p. 12 for Russian; (7) p. 238 confirms the same for Serbian): NOM – ACC – GEN – PREP/LOC – DAT – INS. Re-export from Core.Case.Order.cahaSlavicRank (the substrate definition). For the relationship to containmentRank (LOC at top, INST off-hierarchy), see Core.Case.Order.cahaSlavicRank_vs_containmentRank.

Equations

Phenomena.Case.Studies.Caha2009.Slavic.slavicRank = Core.Case.cahaSlavicRank

Instances For

@[reducible, inline]

abbrev Phenomena.Case.Studies.Caha2009.Slavic.Paradigm :

A morphological paradigm encoded as a form-class index per cell. Indices correspond to the Slavic case sequence: 0=NOM, 1=ACC, 2=GEN, 3=PREP/LOC, 4=DAT, 5=INS. Two cells share a form iff their indices are equal.

Equations

Phenomena.Case.Studies.Caha2009.Slavic.Paradigm = (Fin 6 → ℕ)

Instances For

def Phenomena.Case.Studies.Caha2009.Slavic.IsContiguous (p : Paradigm) :

Caha's Universal Contiguity (@cite{caha-2009} (10), p. 10) on a Slavic paradigm. Defers to the domain-independent Morphology.Containment.isContiguous substrate (which Core.Case.Allomorphy.AllomorphyPattern.IsContiguous specializes at n=4 — same engine, n=6 specialization here).

Equations

Phenomena.Case.Studies.Caha2009.Slavic.IsContiguous p = (Morphology.Containment.isContiguous [p 0, p 1, p 2, p 3, p 4, p 5] = true)

Instances For

@[implicit_reducible]

instance Phenomena.Case.Studies.Caha2009.Slavic.instDecidableIsContiguous (p : Paradigm) :

Decidable (IsContiguous p)

Equations

Phenomena.Case.Studies.Caha2009.Slavic.instDecidableIsContiguous p = id inferInstance

§ 4.1: Distinct syncretism patterns attested in Caha's Slavic data #

Each pattern is a Paradigm (form-class index per cell, indexed 0=NOM, 1=ACC, 2=GEN, 3=LOC/PREP, 4=DAT, 5=INS). Same pattern across languages = same def here; per-language sections below attest which Caha-cited noun in which language exemplifies each pattern. Names classify by syncretism structure, not witness lexeme.

Contiguous patterns (UC-respecting) #

def Phenomena.Case.Studies.Caha2009.Slavic.SyncretismPatterns.animMascSg :

Animate masculine singular: ACC=GEN + PREP=DAT (Serbian son sîn / man muž; Slovene farmer kmèt / I jaz; Ukrainian cashier kasír / me ja). Caha 11b + 11d (Serbian); 15b + 15c (Slovene).

Equations

Instances For

def Phenomena.Case.Studies.Caha2009.Slavic.SyncretismPatterns.inanimMascSg :

Inanimate masculine / neuter / m-sg-adjective: NOM=ACC + PREP=DAT. Serbian city grâd / village sèlo / heart srce; Slovene apple jábolko / peach brêskev; Ukrainian big velík (m sg adj). Caha 11a + 11d (Serbian); 15a + 15c (Slovene).

Equations

Instances For

def Phenomena.Case.Studies.Caha2009.Slavic.SyncretismPatterns.femAStemSg :

Feminine a-stem singular: just PREP=DAT (Serbian sheep òvca). Caha 11d.

Equations

Instances For

def Phenomena.Case.Studies.Caha2009.Slavic.SyncretismPatterns.femIStemSg :

Feminine i-stem singular: NOM=ACC + GEN=PREP=DAT triple. Serbian death smrt (the (11c) GEN-PREP paradigm Caha cites by name); Slovene thread nìt.

Equations

Instances For

def Phenomena.Case.Studies.Caha2009.Slavic.SyncretismPatterns.plDistinct :

Plural with NOM≠ACC + PREP=DAT=INS triple. Serbian son sînovi. Caha 11d + 11e.

Equations

Instances For

def Phenomena.Case.Studies.Caha2009.Slavic.SyncretismPatterns.plNomAcc :

Plural with NOM=ACC + PREP=DAT=INS triple. Serbian village sèla / sheep ôvce / death smrti. Caha 11a + 11d + 11e.

Equations

Instances For

def Phenomena.Case.Studies.Caha2009.Slavic.SyncretismPatterns.dualNomAccDatIns :

Dual with NOM=ACC + DAT=INS. Slovene table mîz / farmer kmèt (dual). Caha 15a + 15d.

Equations

Instances For

def Phenomena.Case.Studies.Caha2009.Slavic.SyncretismPatterns.threePairs :

Maximally syncretic contiguous: NOM=ACC + GEN=PREP + DAT=INS (three pair-syncretisms). Slovene 'both' dva.

Equations

Instances For

def Phenomena.Case.Studies.Caha2009.Slavic.SyncretismPatterns.adjPlNomAccGenPrep :

Adjective plural: NOM=ACC + GEN=PREP. Ukrainian big velík (pl).

Equations

Instances For

def Phenomena.Case.Studies.Caha2009.Slavic.SyncretismPatterns.nomAccGenTripleSg :

Singular with NOM=ACC=GEN triple. Ukrainian knowledge znannjá.

Equations

Instances For

def Phenomena.Case.Studies.Caha2009.Slavic.SyncretismPatterns.genPrepDatTripleSg :

Singular with GEN=PREP=DAT triple, no NOM=ACC. Ukrainian mother mátir (Caha (69) p. 269).

Equations

Instances For

def Phenomena.Case.Studies.Caha2009.Slavic.SyncretismPatterns.nomAccObliqueQuadSg :

Maximally syncretic of all attested: NOM=ACC + GEN=PREP=DAT=INS quadruple. Ukrainian '100' sto.

Equations

Instances For

def Phenomena.Case.Studies.Caha2009.Slavic.SyncretismPatterns.nomAccObliquesDistinct :

NOM=ACC with all 4 oblique cells distinct. Czech window okno sg, machine stroj pl, castle kost pl (Caha (29), (30) p. 248). The most "minimal" attested non-trivial Slavic paradigm shape — only the universal NOM=ACC syncretism, nothing else.

Equations

Instances For

def Phenomena.Case.Studies.Caha2009.Slavic.SyncretismPatterns.accGenPrepInsSkipDat :

ACC=GEN (contiguous) plus PREP=INS skipping DAT (non-contiguous). Czech bigger m.sg větší (Caha (25) p. 246, (67)i p. 266 prep-ins case in m/n adjectives sg). Caha defends the prep-ins component as phonological conflation.

Equations

Instances For

def Phenomena.Case.Studies.Caha2009.Slavic.SyncretismPatterns.streetDoubleABA :

TWO non-contiguous syncretisms in one paradigm: NOM=GEN (ABA over ACC) + ACC=PREP=DAT (ABA over GEN). Czech ulice 'street' sg (Caha (29) p. 248, analyzed via pronominal-vs-nominal endings split in (40)–(41) p. 252–253; treated as two accidental homophonies restricted to this single paradigm).

Equations

Instances For

Attested non-contiguous patterns (Caha-acknowledged #

counterexamples to UC, defended in Caha's prose as phonological or accidental — see per-language Counterexamples sub-namespaces for witness attribution).

def Phenomena.Case.Studies.Caha2009.Slavic.SyncretismPatterns.prepInsSkipDat :

PREP=INS skipping DAT — Slovene 'this n.' tô (Caha (18) p. 241, defended via -em vs -im phonological collapse in (19) p. 242); Ukrainian 'endless' bezkrájij less-frequent variant (Caha (71) p. 269, same defense).

Equations

Instances For

def Phenomena.Case.Studies.Caha2009.Slavic.SyncretismPatterns.nomInsExtremeEnds :

NOM=INS at the extreme ends of the sequence — Slovene 'traveller' pótniki pl (Caha (18) p. 241, defended via tonal differences and otrôc-i / otrók-i stem alternation, p. 243).

Equations

Instances For

def Phenomena.Case.Studies.Caha2009.Slavic.SyncretismPatterns.accInsRestricted :

ACC=INS skipping GEN/PREP/DAT — Slovene 'this f.' tâ (Caha (18) p. 241, admitted as accidental homophony in restricted lexical niche, p. 243).

Equations

Instances For

Contiguity / non-contiguity proofs (decide-checked once per #

shape; per-language attestedShapes lists below inherit these).

theorem Phenomena.Case.Studies.Caha2009.Slavic.SyncretismPatterns.animMascSg_contiguous :

IsContiguous animMascSg

theorem Phenomena.Case.Studies.Caha2009.Slavic.SyncretismPatterns.inanimMascSg_contiguous :

IsContiguous inanimMascSg

theorem Phenomena.Case.Studies.Caha2009.Slavic.SyncretismPatterns.femAStemSg_contiguous :

IsContiguous femAStemSg

theorem Phenomena.Case.Studies.Caha2009.Slavic.SyncretismPatterns.femIStemSg_contiguous :

IsContiguous femIStemSg

theorem Phenomena.Case.Studies.Caha2009.Slavic.SyncretismPatterns.plDistinct_contiguous :

IsContiguous plDistinct

theorem Phenomena.Case.Studies.Caha2009.Slavic.SyncretismPatterns.plNomAcc_contiguous :

IsContiguous plNomAcc

theorem Phenomena.Case.Studies.Caha2009.Slavic.SyncretismPatterns.dualNomAccDatIns_contiguous :

IsContiguous dualNomAccDatIns

theorem Phenomena.Case.Studies.Caha2009.Slavic.SyncretismPatterns.threePairs_contiguous :

IsContiguous threePairs

theorem Phenomena.Case.Studies.Caha2009.Slavic.SyncretismPatterns.adjPlNomAccGenPrep_contiguous :

IsContiguous adjPlNomAccGenPrep

theorem Phenomena.Case.Studies.Caha2009.Slavic.SyncretismPatterns.nomAccGenTripleSg_contiguous :

IsContiguous nomAccGenTripleSg

theorem Phenomena.Case.Studies.Caha2009.Slavic.SyncretismPatterns.genPrepDatTripleSg_contiguous :

IsContiguous genPrepDatTripleSg

theorem Phenomena.Case.Studies.Caha2009.Slavic.SyncretismPatterns.nomAccObliqueQuadSg_contiguous :

IsContiguous nomAccObliqueQuadSg

theorem Phenomena.Case.Studies.Caha2009.Slavic.SyncretismPatterns.nomAccObliquesDistinct_contiguous :

IsContiguous nomAccObliquesDistinct

theorem Phenomena.Case.Studies.Caha2009.Slavic.SyncretismPatterns.prepInsSkipDat_not_contiguous :

¬IsContiguous prepInsSkipDat

theorem Phenomena.Case.Studies.Caha2009.Slavic.SyncretismPatterns.nomInsExtremeEnds_not_contiguous :

¬IsContiguous nomInsExtremeEnds

theorem Phenomena.Case.Studies.Caha2009.Slavic.SyncretismPatterns.accInsRestricted_not_contiguous :

¬IsContiguous accInsRestricted

theorem Phenomena.Case.Studies.Caha2009.Slavic.SyncretismPatterns.accGenPrepInsSkipDat_not_contiguous :

¬IsContiguous accGenPrepInsSkipDat

theorem Phenomena.Case.Studies.Caha2009.Slavic.SyncretismPatterns.streetDoubleABA_not_contiguous :

¬IsContiguous streetDoubleABA

Hypothetical (non-attested) ABA patterns #

Showing the predicate has bite for arbitrary ABA shapes beyond the specific patterns Caha addresses. Caha predicts these patterns are unattested in any language.

def Phenomena.Case.Studies.Caha2009.Slavic.Refutations.nomGenSkipAcc :

NOM=GEN with distinct ACC — would skip an intermediate cell.

Equations

Instances For

theorem Phenomena.Case.Studies.Caha2009.Slavic.Refutations.nomGenSkipAcc_not_contiguous :

¬IsContiguous nomGenSkipAcc

def Phenomena.Case.Studies.Caha2009.Slavic.Refutations.hypotheticalPrepInsSkipDat :

PREP=INS with distinct DAT — would skip the intervening DAT.

Equations

Instances For

theorem Phenomena.Case.Studies.Caha2009.Slavic.Refutations.hypotheticalPrepInsSkipDat_not_contiguous :

¬IsContiguous hypotheticalPrepInsSkipDat

def Phenomena.Case.Studies.Caha2009.Slavic.Refutations.nomDatSkipMiddle :

NOM=DAT with all 3 cells between distinct from NOM — long-range ABA spanning four positions.

Equations

Instances For

theorem Phenomena.Case.Studies.Caha2009.Slavic.Refutations.nomDatSkipMiddle_not_contiguous :

¬IsContiguous nomDatSkipMiddle

§ 4.2: Serbian (§8.3.1, p. 238-240). Caha's headline: "Serbian can be #

thought of as another poster child for Universal Contiguity, with no violations thereof" (p. 239). Caha's five named syncretism types (Caha (11), p. 239):

(a) NOM-ACC: neuters in sg+pl; feminine plurals (b) ACC-GEN: singular masculine animates (c) GEN-PREP: singular of the 'death' paradigm (d) PREP-DAT: almost omnipresent (Caha p. 238 notes PREP/DAT differ only in stress on monosyllabic nouns, segmentally identical — entertains "in fact only a single 'surface' dat/prep case in Serbian") (e) DAT-INS: plurals

Serbian attests no Caha-acknowledged counterexamples.

def Phenomena.Case.Studies.Caha2009.Slavic.Serbian.attestedShapes :

All Serbian shapes attested in Caha (9) p. 238 (singular, 7 nouns) and (10) p. 239 (plural, 7 nouns). The 7 sg paradigms reduce to 4 distinct shapes; the 7 pl reduce to 2.

Equations

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

Instances For

theorem Phenomena.Case.Studies.Caha2009.Slavic.Serbian.all_attested_contiguous (p : Paradigm) :

p ∈ attestedShapes → IsContiguous p

§ 4.3: Slovene (§8.3.2, p. 240-244). Per Caha (13) p. 240, Slovene uses #

the same Slavic sequence NOM-ACC-GEN-PREP-DAT-INS but, unlike Serbian, "keeps all the six cases distinct: there is no prep – dat annexion." Slovene also has dual number — paradigms below are per-noun-and-number-cell.

Caha's four widespread syncretism types in (15) p. 240:

(a) NOM-ACC: widespread; in all neuters, in all duals (b) ACC-GEN: most pronouns, all masculine animate sg nouns (c) PREP-DAT: all singular nouns (d) DAT-INS: all duals

Plus the rarer GEN-PREP syncretism (16) p. 241, attested in plural adjectives, plural/dual personal pronouns, and certain feminine sg declensions.

Crucially, Slovene also has three Caha-acknowledged counterexamples (Caha (18) p. 241–242) — see Counterexamples sub-namespace below.

def Phenomena.Case.Studies.Caha2009.Slavic.Slovene.attestedShapes :

All Slovene contiguous shapes attested in Caha (14) p. 240, (16) p. 241, (17) p. 241.

Equations

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

Instances For

theorem Phenomena.Case.Studies.Caha2009.Slavic.Slovene.all_attested_contiguous (p : Paradigm) :

p ∈ attestedShapes → IsContiguous p

Three paradigms (Caha (18) p. 241–242) that violate Universal Contiguity at the segmental level. Caha defends each in the surrounding prose (p. 242–243) as either phonological conflation ((19): 'this n.' PREP=INS via -em vs -im tonal collapse, visible distinctly in 'that' tîst-em vs tîst-im where prefixation strips the tone; tonal: 'traveller' NOM=INS via acute/circumflex pl tone plus the otrôc-i / otrók-i 'child' stem alternation evidence) or accidental homophony (ACC=INS in 'this f.', restricted to one declension of feminine singulars).

def Phenomena.Case.Studies.Caha2009.Slavic.Slovene.Counterexamples.attestedShapes :

Slovene attestations of non-contiguous patterns:

prepInsSkipDat ← 'this' n. tô
nomInsExtremeEnds ← 'traveller' pótniki pl
accInsRestricted ← 'this' f. tâ

Equations

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

Instances For

theorem Phenomena.Case.Studies.Caha2009.Slavic.Slovene.Counterexamples.all_attested_not_contiguous (p : Paradigm) :

p ∈ attestedShapes → ¬IsContiguous p

§ 4.4: Ukrainian (§8.3.4, p. 268-271). Per Caha §8.3.4 p. 268, Ukrainian #

also conforms to the Slavic Universal Contiguity sequence NOM-ACC-GEN-PREP-DAT-INS. Caha's data (68) p. 268 illustrates NOM-ACC, ACC-GEN, GEN-PREP, and PREP-DAT pairs. Two "possibly offensive" syncretisms exist (paradigm variants of 'region' (70) and adjective 'endless' (71)), but Caha argues they are paradigm-variant-conditioned and isolated.

Caha (74b) p. 271 highlights that Ukrainian has removed a contiguity violation that earlier stages of the language showed, "in a way that is predicted by the Superset Principle."

def Phenomena.Case.Studies.Caha2009.Slavic.Ukrainian.attestedShapes :

All Ukrainian contiguous shapes attested in Caha (68) p. 268 and (69) p. 269.

Equations

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

Instances For

theorem Phenomena.Case.Studies.Caha2009.Slavic.Ukrainian.all_attested_contiguous (p : Paradigm) :

p ∈ attestedShapes → IsContiguous p

The "less frequently found alternative" variant of the soft-stem adjective 'endless' (bezkrájij) shows PREP=INS skipping DAT — identical shape to Slovene's Counterexamples.thisN, addressable by the same phonological-conflation analysis Caha applies to Slovene (Caha p. 271, "the homophony represents a phonological conflation of two underlyingly distinct patterns").

def Phenomena.Case.Studies.Caha2009.Slavic.Ukrainian.Counterexamples.attestedShapes :

Ukrainian attestation of prepInsSkipDat ← 'endless' bezkrájij m sg less-frequent variant.

Equations

Phenomena.Case.Studies.Caha2009.Slavic.Ukrainian.Counterexamples.attestedShapes = [Phenomena.Case.Studies.Caha2009.Slavic.SyncretismPatterns.prepInsSkipDat]

Instances For

theorem Phenomena.Case.Studies.Caha2009.Slavic.Ukrainian.Counterexamples.all_attested_not_contiguous (p : Paradigm) :

p ∈ attestedShapes → ¬IsContiguous p

§ 4.5: Czech (§8.3.3, p. 244-267). Caha's most permissive Slavic #

language for syncretism: "When it comes to syncretism, it seems at first blush that 'anything goes'" (p. 244). Three of Czech's six cases (ACC, PREP, INS) show 4 of the 5 logically possible syncretisms with other cases. Caha then argues that most apparent violations are phonological conflations of distinct underlying representations or accidental homophonies in restricted niches; Czech "in fact provides good support for the Universal Contiguity" (p. 267).

Caha's (67) p. 266 summary table — 10 attested syncretism types in Czech with extension and status:

(a) NOM-ACC: widespread, non-accidental (b) NOM-GEN: 'street' sg only, accidental homophony (c) NOM-INS: soft C-final m anim Ns, phonological conflation (d) ACC-GEN: m anim sg, pronouns, non-accidental (e) ACC-PREP: 'street' sg only, accidental homophony (f) ACC-INS: f.sg adjs, 'sir' pl, phonological conflation (g) GEN-PREP: As in pl, Num 'two', some Ns sg, non-accidental (h) PREP-DAT: nouns sg, non-accidental (i) PREP-INS: m/n As sg, phonological conflation (j) DAT-INS: Num 'two', for all-oblique conflation, non-accidental

The 5 contiguous types (a, d, g, h, j) all reuse existing SyncretismPatterns shapes attested in Serbian/Slovene/Ukrainian. The 5 non-contiguous types (b, c, e, f, i) include three already- encoded shapes (nomInsExtremeEnds for c, accInsRestricted for f, prepInsSkipDat-style for i) plus two Czech-distinctive shapes (streetDoubleABA for b+e bundled in the ulice paradigm, accGenPrepInsSkipDat for i with ACC=GEN context).

def Phenomena.Case.Studies.Caha2009.Slavic.Czech.attestedShapes :

Czech contiguous shapes attested per Caha (29)–(33) and (67) p. 266. Witness lexemes: machine stroj sg/pl, both oba, that f.pl ty, man muž sg, good adj pl m dobrý, etc.

Equations

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

Instances For

theorem Phenomena.Case.Studies.Caha2009.Slavic.Czech.all_attested_contiguous (p : Paradigm) :

p ∈ attestedShapes → IsContiguous p

Czech (67b, c, e, f, i) — five non-contiguous syncretism types. Caha defends each in §8.3.3 prose:

NOM-INS (67c): phonological conflation -y → -i after soft consonants (Caha p. 248-251, see paradigm 'man' muž pl)
NOM-GEN + ACC-PREP (67b+e): both accidental homophonies in the ulice 'street' paradigm; Caha (40)-(41) p. 252-253 argues pronominal vs nominal ending series split -e1 vs -e2 and -i1 vs -i2
ACC-INS (67f): phonological conflation in f.sg adjectives like dobrá 'good' (= same shape as Slovene 'this f.' tâ)
PREP-INS (67i): phonological conflation in m/n sg adjectives like větší 'bigger' (= same shape as Slovene 'this n.' tô, plus contiguous ACC=GEN context)

def Phenomena.Case.Studies.Caha2009.Slavic.Czech.Counterexamples.attestedShapes :

Equations

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

Instances For

theorem Phenomena.Case.Studies.Caha2009.Slavic.Czech.Counterexamples.all_attested_not_contiguous (p : Paradigm) :

p ∈ attestedShapes → ¬IsContiguous p

§ 4.6: Cross-Slavic summary (Caha §8.3.5, p. 271) #

Caha (73) p. 271 presents a unified table: all five investigated Slavic languages (Russian, Serbian, Slovene, Czech, Ukrainian) share the same Universal Adjacency template NOM-ACC-GEN-PREP-DAT-INS. Non-contiguous attestations are addressed as phonological conflations of distinct underlying representations (most cases) or accidental homophonies in restricted niches (a few).

All four detailed sub-sections (§§ 4.2-4.5) are now formalized: Serbian (no counterexamples — "poster child"), Slovene (3 in (18) p. 241), Czech (5 in (67) p. 266 — the most permissive language), Ukrainian (1 in (71) p. 269). Per-language all_attested_contiguous lemmas establish UC for each; per-language Counterexamples.all_attested_not_contiguous lemmas confirm the predicate has bite on Caha-acknowledged violators.

The cross-Slavic claim is documented here rather than asserted as a bundled ∧-theorem: per-language lemmas already carry the substantive content, and bundling them was the caha_poster_child smell prior audits twice removed.

Russian is implicit: Caha (16) p. 12 establishes the same NOM-ACC-GEN-PREP-DAT-INS sequence for Russian as for Serbian (7) p. 238, with paradigm shapes shared (Russian's data appears in §§1.1, 5.1-5.4 as Caha's running example, but §8.3.x focuses on the four other Slavic languages).