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 Semantics.Tense.Aspect.LexicalAspect.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 Phenomena.Case.Studies.Karlsson2017.objectCaseToTelicity : Core.Case → Option Semantics.Tense.Aspect.LexicalAspect.Telicity

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

Equations

• Phenomena.Case.Studies.Karlsson2017.objectCaseToTelicity Core.Case.acc = some Semantics.Tense.Aspect.LexicalAspect.Telicity.telic
• Phenomena.Case.Studies.Karlsson2017.objectCaseToTelicity Core.Case.gen = some Semantics.Tense.Aspect.LexicalAspect.Telicity.telic
• Phenomena.Case.Studies.Karlsson2017.objectCaseToTelicity Core.Case.part = some Semantics.Tense.Aspect.LexicalAspect.Telicity.atelic
• Phenomena.Case.Studies.Karlsson2017.objectCaseToTelicity x✝ = none

inductive Phenomena.Case.Studies.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')

instance Phenomena.Case.Studies.Karlsson2017.instDecidableEqPartitiveLicensor : DecidableEq PartitiveLicensor

Equations

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

instance Phenomena.Case.Studies.Karlsson2017.instBEqPartitiveLicensor : BEq PartitiveLicensor

Equations

• Phenomena.Case.Studies.Karlsson2017.instBEqPartitiveLicensor = { beq := Phenomena.Case.Studies.Karlsson2017.instBEqPartitiveLicensor.beq }

def Phenomena.Case.Studies.Karlsson2017.instBEqPartitiveLicensor.beq : PartitiveLicensor → PartitiveLicensor → Bool

Equations

• Phenomena.Case.Studies.Karlsson2017.instBEqPartitiveLicensor.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Case.Studies.Karlsson2017.instReprPartitiveLicensor.repr : PartitiveLicensor → ℕ → Std.Format

Equations

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

instance Phenomena.Case.Studies.Karlsson2017.instReprPartitiveLicensor : Repr PartitiveLicensor

Equations

• Phenomena.Case.Studies.Karlsson2017.instReprPartitiveLicensor = { reprPrec := Phenomena.Case.Studies.Karlsson2017.instReprPartitiveLicensor.repr }

structure Phenomena.Case.Studies.Karlsson2017.PartitiveDatum : Type

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

• finnish : String
• gloss : String
• objectCase : Core.Case
• licensor : Option PartitiveLicensor
• vpTelicity : Semantics.Tense.Aspect.LexicalAspect.Telicity

def Phenomena.Case.Studies.Karlsson2017.instReprPartitiveDatum.repr : PartitiveDatum → ℕ → Std.Format

Equations

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

instance Phenomena.Case.Studies.Karlsson2017.instReprPartitiveDatum : Repr PartitiveDatum

Equations

• Phenomena.Case.Studies.Karlsson2017.instReprPartitiveDatum = { reprPrec := Phenomena.Case.Studies.Karlsson2017.instReprPartitiveDatum.repr }

def Phenomena.Case.Studies.Karlsson2017.instBEqPartitiveDatum.beq : PartitiveDatum → PartitiveDatum → Bool

Equations

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

instance Phenomena.Case.Studies.Karlsson2017.instBEqPartitiveDatum : BEq PartitiveDatum

Equations

• Phenomena.Case.Studies.Karlsson2017.instBEqPartitiveDatum = { beq := Phenomena.Case.Studies.Karlsson2017.instBEqPartitiveDatum.beq }

def Phenomena.Case.Studies.Karlsson2017.readBookComplete : PartitiveDatum

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

Equations

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

def Phenomena.Case.Studies.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 Phenomena.Case.Studies.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 Phenomena.Case.Studies.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 Phenomena.Case.Studies.Karlsson2017.allData : List PartitiveDatum

Equations

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

theorem Phenomena.Case.Studies.Karlsson2017.acc_telic : objectCaseToTelicity Core.Case.acc = some Semantics.Tense.Aspect.LexicalAspect.Telicity.telic

Accusative object maps to telic VP.

theorem Phenomena.Case.Studies.Karlsson2017.part_atelic : objectCaseToTelicity Core.Case.part = some Semantics.Tense.Aspect.LexicalAspect.Telicity.atelic

Partitive object maps to atelic VP.

theorem Phenomena.Case.Studies.Karlsson2017.gen_telic : objectCaseToTelicity Core.Case.gen = some Semantics.Tense.Aspect.LexicalAspect.Telicity.telic

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

theorem Phenomena.Case.Studies.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 Phenomena.Case.Studies.Karlsson2017.partitive_implies_atelic : ((List.filter (fun (x : PartitiveDatum) => x.objectCase == Core.Case.part) allData).all fun (x : PartitiveDatum) => x.vpTelicity == Semantics.Tense.Aspect.LexicalAspect.Telicity.atelic) = true

All partitive data have atelic VP interpretation.

theorem Phenomena.Case.Studies.Karlsson2017.accusative_implies_telic : ((List.filter (fun (x : PartitiveDatum) => x.objectCase == Core.Case.acc) allData).all fun (x : PartitiveDatum) => x.vpTelicity == Semantics.Tense.Aspect.LexicalAspect.Telicity.telic) = true

All accusative data have telic VP interpretation.

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

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

inductive Phenomena.Case.Studies.Karlsson2017.NominalSlot : Type

A morpheme slot in Finnish nominal morphology.

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

instance Phenomena.Case.Studies.Karlsson2017.instDecidableEqNominalSlot : DecidableEq NominalSlot

Equations

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

def Phenomena.Case.Studies.Karlsson2017.instBEqNominalSlot.beq : NominalSlot → NominalSlot → Bool

Equations

• Phenomena.Case.Studies.Karlsson2017.instBEqNominalSlot.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Case.Studies.Karlsson2017.instBEqNominalSlot : BEq NominalSlot

Equations

• Phenomena.Case.Studies.Karlsson2017.instBEqNominalSlot = { beq := Phenomena.Case.Studies.Karlsson2017.instBEqNominalSlot.beq }

instance Phenomena.Case.Studies.Karlsson2017.instReprNominalSlot : Repr NominalSlot

Equations

• Phenomena.Case.Studies.Karlsson2017.instReprNominalSlot = { reprPrec := Phenomena.Case.Studies.Karlsson2017.instReprNominalSlot.repr }

def Phenomena.Case.Studies.Karlsson2017.instReprNominalSlot.repr : NominalSlot → ℕ → Std.Format

Equations

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

def Phenomena.Case.Studies.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 Phenomena.Case.Studies.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

• Phenomena.Case.Studies.Karlsson2017.slotToBybeeCat Phenomena.Case.Studies.Karlsson2017.NominalSlot.stem = some Core.Morphology.MorphCategory.stem
• Phenomena.Case.Studies.Karlsson2017.slotToBybeeCat Phenomena.Case.Studies.Karlsson2017.NominalSlot.number = some Core.Morphology.MorphCategory.number
• Phenomena.Case.Studies.Karlsson2017.slotToBybeeCat Phenomena.Case.Studies.Karlsson2017.NominalSlot.case_ = none
• Phenomena.Case.Studies.Karlsson2017.slotToBybeeCat Phenomena.Case.Studies.Karlsson2017.NominalSlot.possessive = some Core.Morphology.MorphCategory.agreement
• Phenomena.Case.Studies.Karlsson2017.slotToBybeeCat Phenomena.Case.Studies.Karlsson2017.NominalSlot.clitic = none

def Phenomena.Case.Studies.Karlsson2017.bybeeSlots : List Core.Morphology.MorphCategory

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

Equations

• Phenomena.Case.Studies.Karlsson2017.bybeeSlots = List.filterMap Phenomena.Case.Studies.Karlsson2017.slotToBybeeCat Phenomena.Case.Studies.Karlsson2017.finnishNominalOrder

theorem Phenomena.Case.Studies.Karlsson2017.five_slots : finnishNominalOrder.length = 5

Finnish nominal morphology has exactly 5 suffix slots.

theorem Phenomena.Case.Studies.Karlsson2017.three_bybee_mappable : bybeeSlots.length = 3

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

theorem Phenomena.Case.Studies.Karlsson2017.bybee_slots_are : bybeeSlots = [Core.Morphology.MorphCategory.stem, Core.Morphology.MorphCategory.number, Core.Morphology.MorphCategory.agreement]

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

theorem Phenomena.Case.Studies.Karlsson2017.nominal_respects_bybee : Core.Morphology.respectsRelevanceHierarchy bybeeSlots = true

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

theorem Phenomena.Case.Studies.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 Phenomena.Case.Studies.Karlsson2017.clitic_no_bybee_category : slotToBybeeCat NominalSlot.clitic = none

Clitic is also outside Bybee's scope.

theorem Phenomena.Case.Studies.Karlsson2017.number_closer_than_agreement : Core.Morphology.MorphCategory.number.relevanceRank < Core.Morphology.MorphCategory.agreement.relevanceRank

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