Finnish Infinitive System [Kar18]

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 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 Finnish.Infinitives.InfClass : Type

The four Finnish infinitive classes.

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

@[implicit_reducible]

instance Finnish.Infinitives.instDecidableEqInfClass : DecidableEq InfClass

Equations

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

def Finnish.Infinitives.instReprInfClass.repr : InfClass → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Finnish.Infinitives.instReprInfClass : Repr InfClass

Equations

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

@[implicit_reducible]

instance Finnish.Infinitives.instInhabitedInfClass : Inhabited InfClass

Equations

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

structure Finnish.Infinitives.InfForm : Type

A case form available to an infinitive class.

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

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

Equations

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

@[implicit_reducible]

instance Finnish.Infinitives.instDecidableEqInfForm : DecidableEq InfForm

Equations

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

@[implicit_reducible]

instance Finnish.Infinitives.instReprInfForm : Repr InfForm

Equations

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

def Finnish.Infinitives.instReprInfForm.repr : InfForm → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Finnish.Infinitives.instInhabitedInfForm : Inhabited InfForm

Equations

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

def Finnish.Infinitives.inf1 : List InfForm

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

Equations

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

def 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 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 Finnish.Infinitives.inf4 : List InfForm

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

Equations

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

def Finnish.Infinitives.allInfForms : List InfForm

All infinitive forms across all classes.

Equations

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

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

Total number of infinitive forms.

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

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

structure 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

def Finnish.Infinitives.instReprInf3LocalMapping.repr : Inf3LocalMapping → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Finnish.Infinitives.instReprInf3LocalMapping : Repr Inf3LocalMapping

Equations

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

@[implicit_reducible]

instance Finnish.Infinitives.instInhabitedInf3LocalMapping : Inhabited Inf3LocalMapping

Equations

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

def 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 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 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 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 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 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 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 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.