Finnish infinitives

Karlsson names the Finnish infinitives after their function endings, as the Iso suomen kielioppi does. There are the A infinitive, which is the dictionary form, the E infinitive, the MA infinitive and the rare MINEN infinitive, traditionally the first to the fourth. Infinitives take case endings as nouns do, but few of them. The A infinitive has its basic form, a nominative, and a translative that takes a possessive ending, as in sano-a-kse-ni 'in order for me to say'. The E infinitive has an inessive of time, as in sano-e-ssa 'while saying', and an instructive of manner, as in itki-e-n 'crying'. The MA infinitive has the inessive, elative, illative, adessive and abessive, as in luke-ma-ssa 'reading', and a rare instructive of necessity, as in tule-ma-n. The MINEN infinitive has only a nominative and a partitive, both of obligation.

The A and E infinitives are built on the infinitive stem, and the MA and MINEN infinitives on the inflectional stem, the stem of the present, as ole-ma- against ol-la 'be'. The ending of the A infinitive depends on how its stem ends. It is -dA after a long vowel or a diphthong, as in saa-da 'get', and -tA after s, as in juos-ta 'run'. After l, n or r it repeats that consonant, as in tul-la 'come', and after a short vowel or a t it is -A, as in sano-a 'say' and huomat-a 'notice'. The E infinitive changes the -A to -e, as in sano-e- and juos-te-, and a final -e of the stem to -i, as in luki-e-ssa 'while reading'.

Main definitions

• Finnish.Infinitive: the four infinitives.
• Finnish.Infinitive.cases: the cases an infinitive takes.
• Finnish.Infinitive.aEnding: the ending of the A infinitive after its stem.
• Finnish.Infinitive.base: a stem with an infinitive's function ending, before a case ending.

Main results

• Finnish.Infinitive.toCase_mem_cases_ma_iff: of the local cases the MA infinitive takes the interior series and, of the exterior series, the adessive alone.
• Finnish.Infinitive.surface_base_e: the E infinitive of Karlsson's stems in -e.

Implementation notes

The stems teh- 'do' and näh- 'see' take -dA, which Karlsson lists among the exceptions, and this is not represented. The partitive of the MINEN infinitive is built on -mis-, as in mene-mis-tä, and a case ending after it is not derived.

References

• [Kar18]

inductive Finnish.Infinitive : Type

The Finnish infinitives, named by their function endings.

• a : Infinitive

  The A infinitive, the first, is the dictionary form, as in sano-a 'say'.

• e : Infinitive

  The E infinitive is the second, as in sano-e-ssa 'while saying'.

• ma : Infinitive

  The MA infinitive is the third, as in sano-ma-an 'to say'.

• minen : Infinitive

  The MINEN infinitive is the fourth, as in tietä-minen 'knowing'.

@[instance_reducible]

instance Finnish.instDecidableEqInfinitive : DecidableEq Infinitive

Equations

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

@[instance_reducible]

instance Finnish.instReprInfinitive : Repr Infinitive

Equations

• Finnish.instReprInfinitive = { reprPrec := Finnish.instReprInfinitive.repr }

def Finnish.instReprInfinitive.repr : Infinitive → ℕ → Std.Format

Equations

• Finnish.instReprInfinitive.repr Finnish.Infinitive.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Finnish.Infinitive.a")).group prec✝
• Finnish.instReprInfinitive.repr Finnish.Infinitive.e prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Finnish.Infinitive.e")).group prec✝
• Finnish.instReprInfinitive.repr Finnish.Infinitive.ma prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Finnish.Infinitive.ma")).group prec✝
• Finnish.instReprInfinitive.repr Finnish.Infinitive.minen prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Finnish.Infinitive.minen")).group prec✝

@[instance_reducible]

instance Finnish.instFintypeInfinitive : Fintype Infinitive

Equations

• Finnish.instFintypeInfinitive = { elems := { val := ↑Finnish.Infinitive.enumList, nodup := Finnish.Infinitive.enumList_nodup }, complete := Finnish.instFintypeInfinitive._proof_1 }

def Finnish.Infinitive.cases : Infinitive → Finset Case

The cases an infinitive takes.

Equations

• Finnish.Infinitive.a.cases = {Finnish.Case.nom, Finnish.Case.transl}
• Finnish.Infinitive.e.cases = {Finnish.Case.ine, Finnish.Case.instr}
• Finnish.Infinitive.ma.cases = {Finnish.Case.ine, Finnish.Case.ela, Finnish.Case.ill, Finnish.Case.ade, Finnish.Case.abess, Finnish.Case.instr}
• Finnish.Infinitive.minen.cases = {Finnish.Case.nom, Finnish.Case.part}

theorem Finnish.Infinitive.toCase_mem_cases_ma_iff {r : Spatial.Localization} {d : Spatial.Path.Direction} {c : _root_.Case} (h : Case.toCase r d = some c) : c ∈ Finset.image Case.label ma.cases ↔ r = Spatial.Localization.interior ∨ r = Spatial.Localization.exterior ∧ d = Spatial.Path.Direction.place

Of the local cases the MA infinitive takes the interior series and, of the exterior series, the adessive alone.

def Finnish.Infinitive.aEnding (w : List Phonology.Segment) : List Phonology.Segment

The A infinitive ends in -dA after a long vowel or a diphthong, -tA after s, the stem's final consonant with -A after l, n or r, and -A otherwise.

Equations

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

def Finnish.Infinitive.eStem (w : List Phonology.Segment) : List Phonology.Segment

The stem of the E infinitive is the infinitive stem with its final -e changed to -i, as in luki-e- 'read' from luke-a (§22.3.1).

Equations

• Finnish.Infinitive.eStem w = if w.getLast? = some Finnish.e then w.dropLast ++ [Finnish.i] else w

def Finnish.Infinitive.base : Infinitive → List Phonology.Segment → List Phonology.Segment

The stem w with the function ending of an infinitive, before a case ending.

Equations

• Finnish.Infinitive.a.base x✝ = x✝ ++ Finnish.Infinitive.aEnding x✝
• Finnish.Infinitive.e.base x✝ = Finnish.Infinitive.eStem x✝ ++ (Finnish.Infinitive.aEnding x✝).dropLast ++ [Finnish.e]
• Finnish.Infinitive.ma.base x✝ = x✝ ++ [Finnish.m, Finnish.A]
• Finnish.Infinitive.minen.base x✝ = x✝ ++ [Finnish.m, Finnish.i, Finnish.n, Finnish.e, Finnish.n]

theorem Finnish.Infinitive.surface_base_e : surface (e.base [l, u, k, Finnish.e]) = [l, u, k, i, Finnish.e] ∧ surface (e.base [i, t, k, Finnish.e]) = [i, t, k, i, Finnish.e] ∧ surface (e.base [t, u, n, t, Finnish.e]) = [t, u, n, t, i, Finnish.e] ∧ surface (e.base [k, o, k, Finnish.e]) = [k, o, k, i, Finnish.e] ∧ surface (e.base [s, Finnish.a, n, o]) = [s, Finnish.a, n, o, Finnish.e]

The E infinitive of luke-a 'read', itke-ä 'cry', tunte-a 'feel' and koke-a 'experience' is built on luki-, itki-, tunti- and koki-, and that of sano-a 'say' on sano-.