Finnish Case Inventory @cite{blake-1994}

@cite{karlsson-2017}

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 Core.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 (@cite{blake-1994}, 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 Fragments.Finnish.Case.caseInventory : List Core.Case

Finnish case inventory mapped to Core.Case.

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

• NOM →.nom, ACC →.acc (pronoun/total-object accusative)
• GEN →.gen, PART →.part
• INE/ADE →.loc, ELA/ABL →.abl, ILL/ALL →.all
• ESS →.ess, TRANSL →.transl, ABESS →.abess
• INSTR →.inst, COM →.com

Equations

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

theorem Fragments.Finnish.Case.inventory_fails_strict : Core.validInventory caseInventory = false

Finnish's mapped inventory fails strict contiguity: GEN (rank 5) and LOC (rank 3) have no 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 Core.caseExtension).

theorem Fragments.Finnish.Case.allative_extends_to_dative : Core.Case.dat ∈ Core.caseExtension Core.Case.all

The allative-for-dative substitution is exactly the extension path in @cite{heine-2009} Table 29.6, formalized in Core.caseExtension.

def Fragments.Finnish.Case.finnishNomAccSync : Theories.Morphology.CaseContainment.Syncretism

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

Equations

• Fragments.Finnish.Case.finnishNomAccSync = Theories.Morphology.CaseContainment.nomAccSyncretism

theorem Fragments.Finnish.Case.abl_inst_distinct : Theories.Morphology.CaseContainment.hierarchyAdjacent Core.Case.abl Core.Case.inst = true

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 Fragments.Finnish.Case.Direction : Type

Direction of motion/relation in the Finnish local case system. @cite{karlsson-2017}: the three directional dimensions — static location, source of motion, and goal of motion.

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

instance Fragments.Finnish.Case.instDecidableEqDirection : DecidableEq Direction

Equations

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

def Fragments.Finnish.Case.instBEqDirection.beq : Direction → Direction → Bool

Equations

• Fragments.Finnish.Case.instBEqDirection.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Finnish.Case.instBEqDirection : BEq Direction

Equations

• Fragments.Finnish.Case.instBEqDirection = { beq := Fragments.Finnish.Case.instBEqDirection.beq }

instance Fragments.Finnish.Case.instReprDirection : Repr Direction

Equations

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

def Fragments.Finnish.Case.instReprDirection.repr : Direction → Nat → Std.Format

Equations

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

def Fragments.Finnish.Case.instInhabitedDirection.default : Direction

Equations

• Fragments.Finnish.Case.instInhabitedDirection.default = Fragments.Finnish.Case.Direction.static

instance Fragments.Finnish.Case.instInhabitedDirection : Inhabited Direction

Equations

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

inductive Fragments.Finnish.Case.LocationType : Type

Location type: whether the spatial relation is conceptualized as internal (containment) or external (surface/proximity). @cite{karlsson-2017}: Finnish systematically distinguishes "inside" (inessive/elative/illative) from "at/on" (adessive/ablative/allative).

• internal : LocationType
• external : LocationType

instance Fragments.Finnish.Case.instDecidableEqLocationType : DecidableEq LocationType

Equations

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

def Fragments.Finnish.Case.instBEqLocationType.beq : LocationType → LocationType → Bool

Equations

• Fragments.Finnish.Case.instBEqLocationType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Finnish.Case.instBEqLocationType : BEq LocationType

Equations

• Fragments.Finnish.Case.instBEqLocationType = { beq := Fragments.Finnish.Case.instBEqLocationType.beq }

def Fragments.Finnish.Case.instReprLocationType.repr : LocationType → Nat → Std.Format

Equations

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

instance Fragments.Finnish.Case.instReprLocationType : Repr LocationType

Equations

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

def Fragments.Finnish.Case.instInhabitedLocationType.default : LocationType

Equations

• Fragments.Finnish.Case.instInhabitedLocationType.default = Fragments.Finnish.Case.LocationType.internal

instance Fragments.Finnish.Case.instInhabitedLocationType : Inhabited LocationType

Equations

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

structure Fragments.Finnish.Case.LocalCase : Type

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

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

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

Equations

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

instance Fragments.Finnish.Case.instDecidableEqLocalCase : DecidableEq LocalCase

Equations

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

def Fragments.Finnish.Case.instBEqLocalCase.beq : LocalCase → LocalCase → Bool

Equations

• One or more equations did not get rendered due to their size.
• Fragments.Finnish.Case.instBEqLocalCase.beq x✝¹ x✝ = false

instance Fragments.Finnish.Case.instBEqLocalCase : BEq LocalCase

Equations

• Fragments.Finnish.Case.instBEqLocalCase = { beq := Fragments.Finnish.Case.instBEqLocalCase.beq }

def Fragments.Finnish.Case.instReprLocalCase.repr : LocalCase → Nat → Std.Format

Equations

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

instance Fragments.Finnish.Case.instReprLocalCase : Repr LocalCase

Equations

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

def Fragments.Finnish.Case.instInhabitedLocalCase.default : LocalCase

Equations

• Fragments.Finnish.Case.instInhabitedLocalCase.default = { name := default, suffix := default, direction := default, locationType := default, coreCase := default }

instance Fragments.Finnish.Case.instInhabitedLocalCase : Inhabited LocalCase

Equations

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

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

The 3×2 local case matrix.

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

Core.Case collapses each row into a single value (static →.loc, source →.abl, goal →.all). The matrix reveals the full structure.

Equations

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

def Fragments.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 Fragments.Finnish.Case.localCases_count : allLocalCases.length = 6

The matrix has exactly 6 cells.

theorem Fragments.Finnish.Case.static_collapses_to_loc : (localCaseMatrix Direction.static LocationType.internal).coreCase = (localCaseMatrix Direction.static LocationType.external).coreCase

Core.Case collapses each direction row: both internal and external static cases map to.loc.

theorem Fragments.Finnish.Case.source_collapses_to_abl : (localCaseMatrix Direction.source LocationType.internal).coreCase = (localCaseMatrix Direction.source LocationType.external).coreCase

Both source cases map to.abl.

theorem Fragments.Finnish.Case.goal_collapses_to_all : (localCaseMatrix Direction.goal LocationType.internal).coreCase = (localCaseMatrix Direction.goal LocationType.external).coreCase

Both goal cases map to.all.

theorem Fragments.Finnish.Case.localCases_subset_inventory : (allLocalCases.all fun (lc : LocalCase) => caseInventory.any fun (x : Core.Case) => x == lc.coreCase) = true

All 6 local cases appear in the full Finnish inventory.

theorem Fragments.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.