Finnish Case Inventory [Bla94b]

[Kar18]

Finnish has 15 morphological cases, one of the richest case systems in Europe:

• Grammatical (3): nominative, genitive, partitive (+ accusative for pronouns/total objects, often syncretic with NOM or GEN)
• Internal local (3): inessive (-ssA, 'in'), elative (-stA, 'out of'), illative (-Vn, 'into')
• External local (3): adessive (-llA, 'on/at'), ablative (-ltA, 'from'), allative (-lle, 'to/onto')
• Other (5–6): essive (-nA, 'as'), translative (-ksi, 'becoming'), abessive (-ttA, 'without'), comitative (-ine-, 'with'), instructive (-n, 'by means of')

Our 19-value Case represents 12 of the 15 Finnish cases. The three Finnish-specific semantic cases (essive, translative, abessive) are included directly; the internal/external local pairs (inessive/adessive → LOC, elative/ablative → ABL, illative/allative → ALL) are collapsed into a single rank.

Finnish lacks a dedicated dative case — the allative covers recipient function ([Bla94b], Ch. 6: ALL → DAT extension). This creates a gap at rank 4 (DAT) on Blake's hierarchy, making Finnish a known exception to strict contiguity.

def Finnish.Case.caseInventory : Finset Case

Finnish case inventory mapped to Case.

All 15 Finnish cases now have Case equivalents (essive, translative, abessive added to Case; internal/external local pairs collapsed):

• NOM →.nom, ACC →.acc (pronoun/total-object accusative)
• GEN →.gen, PART →.part
• the 6 local cases as distinct cells: INE/ELA/ILL (interior), ADE/ABL/ALL (exterior) — via the shared Region × PathDir decomposition (Syntax/Case/Order.lean)
• ESS →.ess, TRANSL →.transl, ABESS →.abess
• INSTR →.inst, COM →.com

Equations

• Finnish.Case.caseInventory = {Case.nom, Case.acc, Case.gen, Case.part, Case.ine, Case.ade, Case.ela, Case.abl, Case.ill, Case.all, Case.ess, Case.transl, Case.abess, Case.inst, Case.com}

theorem Finnish.Case.inventory_fails_strict : ¬Case.IsValidInventory caseInventory

Finnish's inventory fails strict contiguity: the spatial tier (rank ≤ 2) and GEN/core (rank ≥ 5) have no LOC (rank 3) or DAT (rank 4) between them. Finnish uses allative for recipient function instead of a dedicated dative.

This illustrates Blake's hedge: the hierarchy holds "usually" but languages like Finnish fill the dative slot with a local case extension (ALL → DAT, formalized in Case.Extends).

theorem Finnish.Case.allative_extends_to_dative : Case.all.Extends Case.dat

The allative-for-dative substitution is exactly the extension path in [Hei09a] Table 29.6, formalized in Case.Extends.

def Finnish.Case.finnishNomAccSync : Morphology.Case.Allomorphy.Syncretism

Finnish NOM/ACC syncretism: the accusative of non-pronominal singular nouns is identical to the nominative. Uses the cross-linguistic pattern from Morphology.Case.Allomorphy.

Equations

• Finnish.Case.finnishNomAccSync = Morphology.Case.Allomorphy.nomAccSyncretism

theorem Finnish.Case.abl_inst_distinct : Case.abl.HierarchyAdjacent Case.inst

Finnish ABL/INST are not syncretic — ablative (-ltA) and instructive (-n) are distinct forms. Unlike many IE languages where ABL and INST merge, Finnish keeps them separate.

inductive Finnish.Case.Direction : Type

Direction of motion/relation in the Finnish local case system. [Kar18]: the three directional dimensions — static location, source of motion, and goal of motion.

• static : Direction
• source : Direction
• goal : Direction

@[implicit_reducible]

instance Finnish.Case.instDecidableEqDirection : DecidableEq Direction

Equations

• Finnish.Case.instDecidableEqDirection x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Finnish.Case.instReprDirection : Repr Direction

Equations

• Finnish.Case.instReprDirection = { reprPrec := Finnish.Case.instReprDirection.repr }

def Finnish.Case.instReprDirection.repr : Direction → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Finnish.Case.instInhabitedDirection : Inhabited Direction

Equations

• Finnish.Case.instInhabitedDirection = { default := Finnish.Case.instInhabitedDirection.default }

inductive Finnish.Case.LocationType : Type

Location type: whether the spatial relation is conceptualized as internal (containment) or external (surface/proximity). [Kar18]: Finnish systematically distinguishes "inside" (inessive/elative/illative) from "at/on" (adessive/ablative/allative).

• internal : LocationType
• external : LocationType

@[implicit_reducible]

instance Finnish.Case.instDecidableEqLocationType : DecidableEq LocationType

Equations

• Finnish.Case.instDecidableEqLocationType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Finnish.Case.instReprLocationType.repr : LocationType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Finnish.Case.instReprLocationType : Repr LocationType

Equations

• Finnish.Case.instReprLocationType = { reprPrec := Finnish.Case.instReprLocationType.repr }

@[implicit_reducible]

instance Finnish.Case.instInhabitedLocationType : Inhabited LocationType

Equations

• Finnish.Case.instInhabitedLocationType = { default := Finnish.Case.instInhabitedLocationType.default }

structure Finnish.Case.LocalCase : Type

A cell in the Finnish local case matrix: the case name, suffix, directional coordinates, and mapping to Case.

• name : String
• suffix : String
• direction : Direction
• locationType : LocationType
• coreCase : Case

@[implicit_reducible]

instance Finnish.Case.instDecidableEqLocalCase : DecidableEq LocalCase

Equations

• Finnish.Case.instDecidableEqLocalCase = Finnish.Case.instDecidableEqLocalCase.decEq

def Finnish.Case.instDecidableEqLocalCase.decEq (x✝ x✝¹ : LocalCase) : Decidable (x✝ = x✝¹)

Equations

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

def Finnish.Case.instReprLocalCase.repr : LocalCase → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Finnish.Case.instReprLocalCase : Repr LocalCase

Equations

• Finnish.Case.instReprLocalCase = { reprPrec := Finnish.Case.instReprLocalCase.repr }

@[implicit_reducible]

instance Finnish.Case.instInhabitedLocalCase : Inhabited LocalCase

Equations

• Finnish.Case.instInhabitedLocalCase = { default := Finnish.Case.instInhabitedLocalCase.default }

def Finnish.Case.Direction.toPathDir : Direction → Case.PathDir

The Finnish directional dimension as the shared Case.PathDir (static = the locative Place base).

Equations

• Finnish.Case.Direction.static.toPathDir = Case.PathDir.place
• Finnish.Case.Direction.source.toPathDir = Case.PathDir.source
• Finnish.Case.Direction.goal.toPathDir = Case.PathDir.goal

def Finnish.Case.LocationType.toRegion : LocationType → Case.Region

The Finnish location type as the shared Case.Region.

Equations

• Finnish.Case.LocationType.internal.toRegion = Case.Region.interior
• Finnish.Case.LocationType.external.toRegion = Case.Region.exterior

def Finnish.Case.localCaseMatrix : Direction → LocationType → LocalCase

The 3×2 local case matrix, mapping each cell to its distinct Case via the shared Region × PathDir decomposition (Syntax/Case/Order.lean) — no longer collapsing internal/external (cf. the deleted static_collapses_to_loc).

	Internal	External
Static	inessive -ssA	adessive -llA
Source	elative -stA	ablative -ltA
Goal	illative -Vn	allative -lle

Equations

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

def Finnish.Case.allLocalCases : List LocalCase

All 6 local cases as a flat list.

Equations

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

theorem Finnish.Case.coreCase_eq_toCase (d : Direction) (l : LocationType) : some (localCaseMatrix d l).coreCase = Case.toCase l.toRegion d.toPathDir

Each cell's Case is exactly what the shared Case.toCase decomposition builds from its Region × PathDir coordinates — the matrix is the shared spatial decomposition, not a private table.

theorem Finnish.Case.localCases_distinct : (List.map LocalCase.coreCase allLocalCases).Nodup

The 6 local cases are 6 distinct Case cells — the faithful decomposition keeps internal and external apart (the lossy collapse of the old *_collapses_to_* theorems is gone).

theorem Finnish.Case.localCases_subset_inventory (lc : LocalCase) : lc ∈ allLocalCases → lc.coreCase ∈ caseInventory

All 6 local cases appear in the full Finnish inventory.

theorem Finnish.Case.internal_external_distinct (d : Direction) : (localCaseMatrix d LocationType.internal).suffix ≠ (localCaseMatrix d LocationType.external).suffix

Within each direction, internal and external suffixes differ.