Finnish Case System @cite{karlsson-2017}

@cite{krifka-1989}

The Finnish partitive case is the primary formal link between case marking and aspectual interpretation in the language (@cite{karlsson-2017}, Chs. 9, 12–13). The case of the direct object determines — or reflects — the telicity of the VP:

• Accusative/genitive object → telic (bounded, resultative): Luin kirja-n. 'I read the book (completely).'

• Partitive object → atelic (unbounded, irresultative): Luin kirja-a. 'I read the book / was reading the book (partially).'

The partitive also appears obligatorily under negation: En lukenut kirja-a. 'I didn't read the book.'

This is the first bridge in linglib connecting Core.Case to Features.Telicity, making the case–aspect interaction formally verifiable.

Theoretical significance

Finnish partitive is evidence for the Incremental Theme hypothesis: the object's referential properties (bounded vs. unbounded) compose with the verb's event structure to determine VP-level telicity. The case morphology makes this composition visible.

def Karlsson2017.objectCaseToTelicity : Core.Case → Option Features.Telicity

The case of the Finnish direct object maps to VP telicity. Accusative/genitive → telic; partitive → atelic.

Equations

• Karlsson2017.objectCaseToTelicity UD.Case.Acc = some Features.Telicity.telic
• Karlsson2017.objectCaseToTelicity UD.Case.Gen = some Features.Telicity.telic
• Karlsson2017.objectCaseToTelicity UD.Case.Par = some Features.Telicity.atelic
• Karlsson2017.objectCaseToTelicity x✝ = none

inductive Karlsson2017.PartitiveLicensor : Type

Context in which partitive case is obligatory (Karlsson §12.3).

• negation : PartitiveLicensor

  Negation: en lukenut kirja-a

• unboundedQuantity : PartitiveLicensor

  Unbounded quantity: join vettä ('I drank water')

• irresultative : PartitiveLicensor

  Irresultative action: luin kirjaa ('I was reading the book')

@[implicit_reducible]

instance Karlsson2017.instDecidableEqPartitiveLicensor : DecidableEq PartitiveLicensor

Equations

• Karlsson2017.instDecidableEqPartitiveLicensor x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Karlsson2017.instReprPartitiveLicensor.repr : PartitiveLicensor → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Karlsson2017.instReprPartitiveLicensor : Repr PartitiveLicensor

Equations

• Karlsson2017.instReprPartitiveLicensor = { reprPrec := Karlsson2017.instReprPartitiveLicensor.repr }

structure Karlsson2017.PartitiveDatum : Type

A partitive licensing datum: object case + licensing context + telicity.

• finnish : String
• gloss : String
• objectCase : Core.Case
• licensor : Option PartitiveLicensor
• vpTelicity : Features.Telicity

@[implicit_reducible]

instance Karlsson2017.instReprPartitiveDatum : Repr PartitiveDatum

Equations

• Karlsson2017.instReprPartitiveDatum = { reprPrec := Karlsson2017.instReprPartitiveDatum.repr }

def Karlsson2017.instReprPartitiveDatum.repr : PartitiveDatum → ℕ → Std.Format

Equations

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

def Karlsson2017.instBEqPartitiveDatum.beq : PartitiveDatum → PartitiveDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Karlsson2017.instBEqPartitiveDatum.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Karlsson2017.instBEqPartitiveDatum : BEq PartitiveDatum

Equations

• Karlsson2017.instBEqPartitiveDatum = { beq := Karlsson2017.instBEqPartitiveDatum.beq }

def Karlsson2017.readBookComplete : PartitiveDatum

Accusative object, telic VP: 'I read the book (completely).'

Equations

• Karlsson2017.readBookComplete = { finnish := "Luin kirjan", gloss := "I read the book (completely)", objectCase := UD.Case.acc, licensor := none, vpTelicity := Features.Telicity.telic }

def Karlsson2017.readBookPartial : PartitiveDatum

Partitive object, atelic VP (irresultative): 'I was reading the book.'

Equations

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

def Karlsson2017.readBookNegated : PartitiveDatum

Partitive under negation: 'I didn't read the book.'

Equations

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

def Karlsson2017.drankWater : PartitiveDatum

Partitive with mass noun (unbounded quantity): 'I drank water.'

Equations

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

def Karlsson2017.allData : List PartitiveDatum

Equations

• Karlsson2017.allData = [Karlsson2017.readBookComplete, Karlsson2017.readBookPartial, Karlsson2017.readBookNegated, Karlsson2017.drankWater]

theorem Karlsson2017.acc_telic : objectCaseToTelicity UD.Case.acc = some Features.Telicity.telic

Accusative object maps to telic VP.

theorem Karlsson2017.part_atelic : objectCaseToTelicity UD.Case.part = some Features.Telicity.atelic

Partitive object maps to atelic VP.

theorem Karlsson2017.gen_telic : objectCaseToTelicity UD.Case.gen = some Features.Telicity.telic

Genitive object (used for total objects in some environments) maps to telic, same as accusative.

theorem Karlsson2017.mapping_agrees_with_data : (allData.all fun (d : PartitiveDatum) => objectCaseToTelicity d.objectCase == some d.vpTelicity) = true

For every datum, the objectCaseToTelicity mapping agrees with the annotated vpTelicity.

theorem Karlsson2017.partitive_implies_atelic : ((List.filter (fun (x : PartitiveDatum) => x.objectCase == UD.Case.part) allData).all fun (x : PartitiveDatum) => x.vpTelicity == Features.Telicity.atelic) = true

All partitive data have atelic VP interpretation.

theorem Karlsson2017.accusative_implies_telic : ((List.filter (fun (x : PartitiveDatum) => x.objectCase == UD.Case.acc) allData).all fun (x : PartitiveDatum) => x.vpTelicity == Features.Telicity.telic) = true

All accusative data have telic VP interpretation.

theorem Karlsson2017.partitive_has_licensor : ((List.filter (fun (x : PartitiveDatum) => x.objectCase == UD.Case.part) allData).all fun (d : PartitiveDatum) => d.licensor.isSome) = true

Every partitive datum has a licensor (negation, quantity, or aspect).

inductive Karlsson2017.NominalSlot : Type

A morpheme slot in Finnish nominal morphology.

• stem : NominalSlot
• number : NominalSlot
• case_ : NominalSlot
• possessive : NominalSlot
• clitic : NominalSlot

@[implicit_reducible]

instance Karlsson2017.instDecidableEqNominalSlot : DecidableEq NominalSlot

Equations

• Karlsson2017.instDecidableEqNominalSlot x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Karlsson2017.instReprNominalSlot.repr : NominalSlot → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Karlsson2017.instReprNominalSlot : Repr NominalSlot

Equations

• Karlsson2017.instReprNominalSlot = { reprPrec := Karlsson2017.instReprNominalSlot.repr }

def Karlsson2017.finnishNominalOrder : List NominalSlot

Finnish nominal suffix order (Karlsson §7.1).

Equations

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

def Karlsson2017.slotToBybeeCat : NominalSlot → Option Core.Morphology.MorphCategory

Map nominal slots to Bybee MorphCategory where possible. Case has no Bybee equivalent — this is the gap.

Equations

• Karlsson2017.slotToBybeeCat Karlsson2017.NominalSlot.stem = some Core.Morphology.MorphCategory.stem
• Karlsson2017.slotToBybeeCat Karlsson2017.NominalSlot.number = some Core.Morphology.MorphCategory.number
• Karlsson2017.slotToBybeeCat Karlsson2017.NominalSlot.case_ = none
• Karlsson2017.slotToBybeeCat Karlsson2017.NominalSlot.possessive = some (Core.Morphology.MorphCategory.agreement Core.Agreement.Controller.poss)
• Karlsson2017.slotToBybeeCat Karlsson2017.NominalSlot.clitic = none

def Karlsson2017.bybeeSlots : List Core.Morphology.MorphCategory

The Bybee-mappable subset of Finnish nominal slots, in suffix order.

Equations

• Karlsson2017.bybeeSlots = List.filterMap Karlsson2017.slotToBybeeCat Karlsson2017.finnishNominalOrder

theorem Karlsson2017.five_slots : finnishNominalOrder.length = 5

Finnish nominal morphology has exactly 5 suffix slots.

theorem Karlsson2017.three_bybee_mappable : bybeeSlots.length = 3

Only 3 of 5 nominal slots have Bybee equivalents (stem, number, agreement).

theorem Karlsson2017.bybee_slots_are : bybeeSlots = [Core.Morphology.MorphCategory.stem, Core.Morphology.MorphCategory.number, Core.Morphology.MorphCategory.agreement Core.Agreement.Controller.poss]

The Bybee-mappable slots are: stem, number, agreement.

theorem Karlsson2017.nominal_respects_bybee : Core.Morphology.RespectsRelevanceHierarchy bybeeSlots

The Bybee-mappable nominal slots respect the relevance hierarchy: stem (0) < number (3) < agreement (8).

theorem Karlsson2017.case_no_bybee_category : slotToBybeeCat NominalSlot.case_ = none

Case has no Bybee category — this is the gap that Finnish nominal morphology reveals in Bybee's verb-centric hierarchy.

theorem Karlsson2017.clitic_no_bybee_category : slotToBybeeCat NominalSlot.clitic = none

Clitic is also outside Bybee's scope.

theorem Karlsson2017.number_closer_than_agreement : Core.Morphology.MorphCategory.number.peripherality < (Core.Morphology.MorphCategory.agreement Core.Agreement.Controller.poss).peripherality

Number (rank 3) is more stem-relevant than possessive agreement (rank 8), consistent with number appearing closer to the stem in Finnish.