Finnish Infinitive System @cite{karlsson-2017}

Finnish has four productive infinitive forms, each built from the verb stem plus a characteristic marker and case suffix:

Infinitive	Marker	Case forms
I (A)	-a / -ä	translative only (basic citation form)
II (E)	-e-	inessive, instructive
III (MA)	-ma-	inessive, elative, illative, adessive, abessive
IV (MINEN)	-minen	nominative (verbal noun)

The III infinitive is linguistically remarkable: it takes local case suffixes on verbal stems, mirroring the nominal local case system. Four of its five case forms correspond exactly to cells in the 3×2 local case matrix (see Fragments.Finnish.Case.localCaseMatrix):

• inessive -massa = static + internal
• elative -masta = source + internal
• illative -maan = goal + internal
• adessive -malla = static + external

The fifth, abessive -matta ('without V-ing'), comes from outside the local case matrix — abessive is a "marginal" case.

This structural parallel — the same case paradigm applying to both nouns and nonfinite verbs — is evidence that Finnish local cases are genuine morphosyntactic features, not frozen adverbial suffixes.

inductive Fragments.Finnish.Infinitives.InfClass : Type

The four Finnish infinitive classes.

• i : InfClass
• ii : InfClass
• iii : InfClass
• iv : InfClass

instance Fragments.Finnish.Infinitives.instDecidableEqInfClass : DecidableEq InfClass

Equations

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

instance Fragments.Finnish.Infinitives.instBEqInfClass : BEq InfClass

Equations

• Fragments.Finnish.Infinitives.instBEqInfClass = { beq := Fragments.Finnish.Infinitives.instBEqInfClass.beq }

def Fragments.Finnish.Infinitives.instBEqInfClass.beq : InfClass → InfClass → Bool

Equations

• Fragments.Finnish.Infinitives.instBEqInfClass.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Fragments.Finnish.Infinitives.instReprInfClass.repr : InfClass → Nat → Std.Format

Equations

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

instance Fragments.Finnish.Infinitives.instReprInfClass : Repr InfClass

Equations

• Fragments.Finnish.Infinitives.instReprInfClass = { reprPrec := Fragments.Finnish.Infinitives.instReprInfClass.repr }

def Fragments.Finnish.Infinitives.instInhabitedInfClass.default : InfClass

Equations

• Fragments.Finnish.Infinitives.instInhabitedInfClass.default = Fragments.Finnish.Infinitives.InfClass.i

instance Fragments.Finnish.Infinitives.instInhabitedInfClass : Inhabited InfClass

Equations

• Fragments.Finnish.Infinitives.instInhabitedInfClass = { default := Fragments.Finnish.Infinitives.instInhabitedInfClass.default }

structure Fragments.Finnish.Infinitives.InfForm : Type

A case form available to an infinitive class.

• infClass : InfClass
• caseName : String
• suffix : String
• gloss : String

def Fragments.Finnish.Infinitives.instDecidableEqInfForm.decEq (x✝ x✝¹ : InfForm) : Decidable (x✝ = x✝¹)

Equations

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

instance Fragments.Finnish.Infinitives.instDecidableEqInfForm : DecidableEq InfForm

Equations

• Fragments.Finnish.Infinitives.instDecidableEqInfForm = Fragments.Finnish.Infinitives.instDecidableEqInfForm.decEq

def Fragments.Finnish.Infinitives.instBEqInfForm.beq : InfForm → InfForm → Bool

Equations

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

instance Fragments.Finnish.Infinitives.instBEqInfForm : BEq InfForm

Equations

• Fragments.Finnish.Infinitives.instBEqInfForm = { beq := Fragments.Finnish.Infinitives.instBEqInfForm.beq }

instance Fragments.Finnish.Infinitives.instReprInfForm : Repr InfForm

Equations

• Fragments.Finnish.Infinitives.instReprInfForm = { reprPrec := Fragments.Finnish.Infinitives.instReprInfForm.repr }

def Fragments.Finnish.Infinitives.instReprInfForm.repr : InfForm → Nat → Std.Format

Equations

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

def Fragments.Finnish.Infinitives.instInhabitedInfForm.default : InfForm

Equations

• Fragments.Finnish.Infinitives.instInhabitedInfForm.default = { infClass := default, caseName := default, suffix := default, gloss := default }

instance Fragments.Finnish.Infinitives.instInhabitedInfForm : Inhabited InfForm

Equations

• Fragments.Finnish.Infinitives.instInhabitedInfForm = { default := Fragments.Finnish.Infinitives.instInhabitedInfForm.default }

def Fragments.Finnish.Infinitives.inf1 : List InfForm

I infinitive (A-infinitive): the basic citation form. "lukea" = 'to read'. Only appears in translative.

Equations

• Fragments.Finnish.Infinitives.inf1 = [{ infClass := Fragments.Finnish.Infinitives.InfClass.i, caseName := "translative", suffix := "-a / -ä", gloss := "to V" }]

def Fragments.Finnish.Infinitives.inf2 : List InfForm

II infinitive (E-infinitive): -e- + inessive or instructive. "lukiessa" = 'while reading', "lukien" = 'by reading'.

Equations

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

def Fragments.Finnish.Infinitives.inf3 : List InfForm

III infinitive (MA-infinitive): -ma- + local case suffixes. The paradigm that mirrors the nominal local case matrix. "lukemassa" = 'reading' (at it), "lukemasta" = 'from reading', "lukemaan" = 'to read' (goal), "lukemalla" = 'by reading', "lukematta" = 'without reading'.

Equations

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

def Fragments.Finnish.Infinitives.inf4 : List InfForm

IV infinitive (MINEN-infinitive): verbal noun, nominative only. "lukeminen" = 'reading' (the act).

Equations

• Fragments.Finnish.Infinitives.inf4 = [{ infClass := Fragments.Finnish.Infinitives.InfClass.iv, caseName := "nominative", suffix := "-minen", gloss := "the act of V-ing" }]

def Fragments.Finnish.Infinitives.allInfForms : List InfForm

All infinitive forms across all classes.

Equations

• Fragments.Finnish.Infinitives.allInfForms = Fragments.Finnish.Infinitives.inf1 ++ Fragments.Finnish.Infinitives.inf2 ++ Fragments.Finnish.Infinitives.inf3 ++ Fragments.Finnish.Infinitives.inf4

theorem Fragments.Finnish.Infinitives.allInfForms_count : allInfForms.length = 9

Total number of infinitive forms.

theorem Fragments.Finnish.Infinitives.inf3_richest : inf3.length = 5

The III infinitive has the richest paradigm (5 forms).

structure Fragments.Finnish.Infinitives.Inf3LocalMapping : Type

A III-infinitive case form paired with the local case matrix cell it mirrors. none for abessive (outside the local matrix).

• infForm : InfForm
• localCell : Option Case.LocalCase

instance Fragments.Finnish.Infinitives.instReprInf3LocalMapping : Repr Inf3LocalMapping

Equations

• Fragments.Finnish.Infinitives.instReprInf3LocalMapping = { reprPrec := Fragments.Finnish.Infinitives.instReprInf3LocalMapping.repr }

def Fragments.Finnish.Infinitives.instReprInf3LocalMapping.repr : Inf3LocalMapping → Nat → Std.Format

Equations

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

def Fragments.Finnish.Infinitives.instInhabitedInf3LocalMapping.default : Inf3LocalMapping

Equations

• Fragments.Finnish.Infinitives.instInhabitedInf3LocalMapping.default = { infForm := default, localCell := default }

instance Fragments.Finnish.Infinitives.instInhabitedInf3LocalMapping : Inhabited Inf3LocalMapping

Equations

• Fragments.Finnish.Infinitives.instInhabitedInf3LocalMapping = { default := Fragments.Finnish.Infinitives.instInhabitedInf3LocalMapping.default }

def Fragments.Finnish.Infinitives.inf3LocalMappings : List Inf3LocalMapping

The mapping from III infinitive forms to local case matrix cells. Four of five forms correspond to matrix cells; abessive does not.

Equations

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

theorem Fragments.Finnish.Infinitives.inf3_local_overlap : (List.filter (fun (x : Inf3LocalMapping) => x.localCell.isSome) inf3LocalMappings).length = 4

Exactly 4 of 5 III-infinitive forms map to local case matrix cells.

theorem Fragments.Finnish.Infinitives.inf3_unmapped_is_abessive : (List.filter (fun (x : Inf3LocalMapping) => x.localCell.isNone) inf3LocalMappings).length = 1 ∧ (List.filter (fun (x : Inf3LocalMapping) => x.localCell.isNone) inf3LocalMappings)[0]!.infForm.caseName = "abessive"

The one unmapped form is abessive.

theorem Fragments.Finnish.Infinitives.inf3_inessive_matches_nominal : (Case.localCaseMatrix Case.Direction.static Case.LocationType.internal).name = "inessive" ∧ inf3[0]!.caseName = "inessive"

The III infinitive's inessive matches the nominal inessive (static + internal cell of the matrix).

theorem Fragments.Finnish.Infinitives.inf3_elative_matches_nominal : (Case.localCaseMatrix Case.Direction.source Case.LocationType.internal).name = "elative" ∧ inf3[1]!.caseName = "elative"

The III infinitive's elative matches the nominal elative (source + internal cell of the matrix).

theorem Fragments.Finnish.Infinitives.inf3_illative_matches_nominal : (Case.localCaseMatrix Case.Direction.goal Case.LocationType.internal).name = "illative" ∧ inf3[2]!.caseName = "illative"

The III infinitive's illative matches the nominal illative (goal + internal cell of the matrix).

theorem Fragments.Finnish.Infinitives.inf3_adessive_matches_nominal : (Case.localCaseMatrix Case.Direction.static Case.LocationType.external).name = "adessive" ∧ inf3[3]!.caseName = "adessive"

The III infinitive's adessive matches the nominal adessive (static + external cell of the matrix).

theorem Fragments.Finnish.Infinitives.inf3_covers_internal_column : have mapped := List.filterMap (fun (x : Inf3LocalMapping) => x.localCell) inf3LocalMappings; (mapped.all fun (lc : Case.LocalCase) => lc.locationType == Case.LocationType.internal || lc.direction == Case.Direction.static && lc.locationType == Case.LocationType.external) = true

The 4 mapped III-infinitive forms cover 3 of the 6 local case matrix cells (the 3 internal cases + adessive), leaving ablative and allative unused.

This asymmetry — all internal cases but only one external case — reflects that the III infinitive is primarily about containment ("in the process of"), departure ("from the process"), and goal ("into doing"), with adessive ("by means of") as the sole external form.