Finnish Verb Entries @cite{karlsson-2017}

Finnish verbs illustrate two phenomena that exercise linglib's infrastructure:

1. The impersonal "passive" — Finnish lacks a true passive. What is traditionally called the passive is an impersonal construction: the agent is demoted to an implicit generic human referent, not promoted to a by-phrase. The subject position remains empty.

   Active: Mies avasi oven. 'The man opened the door.' "Passive": Ovi avattiin. 'The door was opened (by someone).'

   This is formalized using VoiceFlavor.impersonal, distinct from both nonThematic (anticausative, no agent at all) and agentive (syntactically projected agent).

2. Verb type classification — Finnish has 6 productive verb types (conjugation classes) based on infinitive stem shape (Karlsson §10.1). We record the type as data, not as separate MorphRules, since the classification is lexical.

inductive Fragments.Finnish.Predicates.VerbType : Type

Finnish verb type (conjugation class, Karlsson §10.1).

• type1 : VerbType
• type2 : VerbType
• type3 : VerbType
• type4 : VerbType
• type5 : VerbType
• type6 : VerbType

instance Fragments.Finnish.Predicates.instDecidableEqVerbType : DecidableEq VerbType

Equations

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

instance Fragments.Finnish.Predicates.instBEqVerbType : BEq VerbType

Equations

• Fragments.Finnish.Predicates.instBEqVerbType = { beq := Fragments.Finnish.Predicates.instBEqVerbType.beq }

def Fragments.Finnish.Predicates.instBEqVerbType.beq : VerbType → VerbType → Bool

Equations

• Fragments.Finnish.Predicates.instBEqVerbType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Fragments.Finnish.Predicates.instReprVerbType.repr : VerbType → ℕ → Std.Format

Equations

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

instance Fragments.Finnish.Predicates.instReprVerbType : Repr VerbType

Equations

• Fragments.Finnish.Predicates.instReprVerbType = { reprPrec := Fragments.Finnish.Predicates.instReprVerbType.repr }

structure Fragments.Finnish.Predicates.FinnishVerb : Type

A Finnish verb entry with active and impersonal "passive" forms.

• infinitive : String

  Infinitive (dictionary form, I infinitive)

• gloss : String

  English gloss

• verbType : VerbType

  Verb type (conjugation class)

• pres3sgAct : String

  3sg present active

• presImpersonal : String

  Impersonal "passive" present

def Fragments.Finnish.Predicates.instReprFinnishVerb.repr : FinnishVerb → ℕ → Std.Format

Equations

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

instance Fragments.Finnish.Predicates.instReprFinnishVerb : Repr FinnishVerb

Equations

• Fragments.Finnish.Predicates.instReprFinnishVerb = { reprPrec := Fragments.Finnish.Predicates.instReprFinnishVerb.repr }

instance Fragments.Finnish.Predicates.instBEqFinnishVerb : BEq FinnishVerb

Equations

• Fragments.Finnish.Predicates.instBEqFinnishVerb = { beq := Fragments.Finnish.Predicates.instBEqFinnishVerb.beq }

def Fragments.Finnish.Predicates.instBEqFinnishVerb.beq : FinnishVerb → FinnishVerb → Bool

Equations

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

def Fragments.Finnish.Predicates.avata : FinnishVerb

Equations

• Fragments.Finnish.Predicates.avata = { infinitive := "avata", gloss := "to open", verbType := Fragments.Finnish.Predicates.VerbType.type4, pres3sgAct := "avaa", presImpersonal := "avataan" }

def Fragments.Finnish.Predicates.lukea : FinnishVerb

Equations

• Fragments.Finnish.Predicates.lukea = { infinitive := "lukea", gloss := "to read", verbType := Fragments.Finnish.Predicates.VerbType.type1, pres3sgAct := "lukee", presImpersonal := "luetaan" }

def Fragments.Finnish.Predicates.tulla : FinnishVerb

Equations

• Fragments.Finnish.Predicates.tulla = { infinitive := "tulla", gloss := "to come", verbType := Fragments.Finnish.Predicates.VerbType.type3, pres3sgAct := "tulee", presImpersonal := "tullaan" }

def Fragments.Finnish.Predicates.haluta : FinnishVerb

Equations

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

def Fragments.Finnish.Predicates.finnishActive : Minimalism.VoiceHead

Active Finnish voice: agentive, projects a syntactic agent.

Equations

• Fragments.Finnish.Predicates.finnishActive = Minimalism.voiceAgent

def Fragments.Finnish.Predicates.finnishPassive : Minimalism.VoiceHead

Finnish "passive" voice: impersonal, no syntactic agent specifier. The agent is existentially closed — someone performs the action, but the someone is not a syntactic argument.

Equations

• Fragments.Finnish.Predicates.finnishPassive = Minimalism.voiceImpersonal

theorem Fragments.Finnish.Predicates.active_has_agent : finnishActive.assignsTheta = true

Active Finnish verbs project an agent.

theorem Fragments.Finnish.Predicates.passive_no_agent : finnishPassive.assignsTheta = false

Finnish "passive" does NOT project an agent syntactically.

theorem Fragments.Finnish.Predicates.passive_has_semantics : finnishPassive.hasSemantics = true

Finnish "passive" HAS semantic content (existential closure over agent), unlike true anticausatives which are semantically vacuous.

theorem Fragments.Finnish.Predicates.passive_not_phase : finnishPassive.phaseHead = false

Finnish "passive" is NOT a phase head.

theorem Fragments.Finnish.Predicates.impersonal_vs_anticausative : finnishPassive.hasSemantics = true ∧ Minimalism.voiceAnticausative.hasSemantics = false

Finnish "passive" is distinct from anticausative — both lack a syntactic agent, but impersonal Voice has semantics while nonThematic does not.

theorem Fragments.Finnish.Predicates.impersonal_suffix : ([avata, lukea, tulla, haluta].all fun (v : FinnishVerb) => v.presImpersonal.endsWith "aan") = true

All impersonal forms end in -aan or -ään (back or front harmony on the passive marker).

theorem Fragments.Finnish.Predicates.verb_types_distinct : avata.verbType ≠ lukea.verbType ∧ lukea.verbType ≠ tulla.verbType ∧ tulla.verbType ≠ haluta.verbType

All 4 sample verbs have distinct verb types.

def Fragments.Finnish.Predicates.finnishVoiceSystem : Interfaces.VoiceSystemProfile

Finnish voice system: two-way asymmetrical (active/impersonal).

Finnish lacks a true passive — what is traditionally called the passive is an impersonal construction where the agent is demoted to an implicit generic human referent, not promoted to a by-phrase (@cite{karlsson-2017} Ch. 11). Active is the basic form.

Equations

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

theorem Fragments.Finnish.Predicates.finnish_voice_system_asymmetrical : finnishVoiceSystem.symmetry = Interfaces.VoiceSystemSymmetry.asymmetrical

theorem Fragments.Finnish.Predicates.finnish_voice_count : finnishVoiceSystem.voiceCount = 2

theorem Fragments.Finnish.Predicates.finnish_is_active_passive : finnishVoiceSystem.isActivePassive = true

Finnish is the ideal testing ground for implicative verb semantics because it has a much richer inventory of lexically-specific implicatives than English. Where English has primarily manage (underspecified) and dare (courage), Finnish has ~12 common implicatives that each lexicalize a different prerequisite type.

The structure extends `FinnishVerb` with implicative fields. 

structure Fragments.Finnish.Predicates.FinnishImplicativeVerbextends Fragments.Finnish.Predicates.FinnishVerb : Type

A Finnish implicative verb entry, extending the base verb with implicative classification from @cite{nadathur-2024}.

• infinitive : String
• gloss : String
• verbType : VerbType
• pres3sgAct : String
• presImpersonal : String
• implicativeBuilder : Nadathur2024.Implicative.ImplicativeBuilder

  Positive (entails complement) or negative (entails ¬complement)

• directionality : Nadathur2024.Implicative.Directionality

  One-way or two-way complement entailment

• prerequisite : Nadathur2024.Implicative.Prerequisite

  The lexically-specified prerequisite type

• neg3sgAct : String

  Negative 3sg present (with negation verb ei)

instance Fragments.Finnish.Predicates.instReprFinnishImplicativeVerb : Repr FinnishImplicativeVerb

Equations

• Fragments.Finnish.Predicates.instReprFinnishImplicativeVerb = { reprPrec := Fragments.Finnish.Predicates.instReprFinnishImplicativeVerb.repr }

def Fragments.Finnish.Predicates.instReprFinnishImplicativeVerb.repr : FinnishImplicativeVerb → ℕ → Std.Format

Equations

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

instance Fragments.Finnish.Predicates.instBEqFinnishImplicativeVerb : BEq FinnishImplicativeVerb

Equations

• Fragments.Finnish.Predicates.instBEqFinnishImplicativeVerb = { beq := Fragments.Finnish.Predicates.instBEqFinnishImplicativeVerb.beq }

def Fragments.Finnish.Predicates.instBEqFinnishImplicativeVerb.beq : FinnishImplicativeVerb → FinnishImplicativeVerb → Bool

Equations

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

def Fragments.Finnish.Predicates.onnistua : FinnishImplicativeVerb

onnistua 'succeed, manage' — two-way positive, unspecified prerequisite. "Eman onnistui pakenema-an" → 'Eman fled.' "Eman ei onnistunut pakenema-an" → 'Eman did not flee.' (@cite{nadathur-2024} ex. 2)

Equations

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

def Fragments.Finnish.Predicates.uskaltaa : FinnishImplicativeVerb

uskaltaa 'dare' — two-way positive, prerequisite = courage. "Juno uskaltaa avata oven" → 'Juno opens the door.' "Juno ei uskaltanut avata ovea" → 'Juno did not open the door.' (@cite{nadathur-2024} ex. 4)

Equations

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

def Fragments.Finnish.Predicates.viitsia : FinnishImplicativeVerb

viitsiä 'bother' — two-way positive, prerequisite = engagement. (@cite{nadathur-2024} ex. 10)

Equations

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

def Fragments.Finnish.Predicates.malttaa : FinnishImplicativeVerb

malttaa 'have the patience' — two-way positive, prerequisite = patience. "Marja malttoi odottaa" → 'Marja waited.' "Marja ei malttanut odottaa" → 'Marja did not wait.' (@cite{nadathur-2024} ex. 11)

Equations

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

def Fragments.Finnish.Predicates.hennoa : FinnishImplicativeVerb

hennoa 'have the heart' — two-way positive, prerequisite = hard-heartedness. (@cite{nadathur-2024} ex. 27)

Equations

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

def Fragments.Finnish.Predicates.kehdata : FinnishImplicativeVerb

kehdata 'act without shame, be unembarrassed' — two-way positive. (@cite{nadathur-2024} ex. 40)

Equations

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

def Fragments.Finnish.Predicates.ehtia : FinnishImplicativeVerb

ehtiä 'find/make time' — two-way positive, prerequisite = time. (@cite{nadathur-2024} ex. 39)

Equations

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

def Fragments.Finnish.Predicates.jaksaa : FinnishImplicativeVerb

jaksaa 'have the strength' — one-way positive, prerequisite = strength. Positive: "Sampo jaksoi nousta" ↛ 'Sampo rose.' (only implicature) Negative: "Sampo ei jaksanut nousta" → 'Sampo did not rise.' (@cite{nadathur-2024} ex. 5)

Equations

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

def Fragments.Finnish.Predicates.mahtua : FinnishImplicativeVerb

mahtua 'fit, be small enough' — one-way positive, prerequisite = fitness. "Freija mahtui kulkemaan oven" ↛ 'Freija went through the door.' "Freija ei mahtunut kulkemaan oven" → 'Freija did not go through the door.' (@cite{nadathur-2024} ex. 30)

Equations

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

def Fragments.Finnish.Predicates.pystya : FinnishImplicativeVerb

pystyä 'be able' — one-way positive (the Finnish counterpart of be able). "Maarit pystyi tappelema-an" ↛ 'Maarit fought.' "Maarit ei pystynyt tappelema-an" → 'Maarit did not fight.' (@cite{nadathur-2024} ex. 29)

Equations

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

def Fragments.Finnish.Predicates.laiminlyoda : FinnishImplicativeVerb

laiminlyödä 'neglect' — polarity-reversing two-way. "Hän laiminlöi korjata virheen" → 'He did not correct the error.' "Hän ei laiminlyönyt korjata virhettä" → 'He corrected the error.' (@cite{nadathur-2024} ex. 44)

Equations

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

def Fragments.Finnish.Predicates.eparoida : FinnishImplicativeVerb

epäröidä 'hesitate' — polarity-reversing one-way. "Juno epäröi ottaa osaa kilpailuun" ↛ 'Juno did not take part.' "Juno ei epäröinyt ottaa osaa kilpailuun" → 'Juno took part.' (@cite{nadathur-2024} §6.4, ex. 46)

Equations

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

theorem Fragments.Finnish.Predicates.twoWay_verbs_correct : onnistua.directionality = Nadathur2024.Implicative.Directionality.twoWay ∧ uskaltaa.directionality = Nadathur2024.Implicative.Directionality.twoWay ∧ viitsia.directionality = Nadathur2024.Implicative.Directionality.twoWay ∧ malttaa.directionality = Nadathur2024.Implicative.Directionality.twoWay ∧ hennoa.directionality = Nadathur2024.Implicative.Directionality.twoWay ∧ kehdata.directionality = Nadathur2024.Implicative.Directionality.twoWay ∧ ehtia.directionality = Nadathur2024.Implicative.Directionality.twoWay ∧ laiminlyoda.directionality = Nadathur2024.Implicative.Directionality.twoWay

All two-way implicatives have .twoWay directionality.

theorem Fragments.Finnish.Predicates.oneWay_verbs_correct : jaksaa.directionality = Nadathur2024.Implicative.Directionality.oneWay ∧ mahtua.directionality = Nadathur2024.Implicative.Directionality.oneWay ∧ pystya.directionality = Nadathur2024.Implicative.Directionality.oneWay ∧ eparoida.directionality = Nadathur2024.Implicative.Directionality.oneWay

All one-way implicatives have .oneWay directionality.

theorem Fragments.Finnish.Predicates.prerequisites_distinct : uskaltaa.prerequisite = Nadathur2024.Implicative.Prerequisite.courage ∧ viitsia.prerequisite = Nadathur2024.Implicative.Prerequisite.engagement ∧ malttaa.prerequisite = Nadathur2024.Implicative.Prerequisite.patience ∧ hennoa.prerequisite = Nadathur2024.Implicative.Prerequisite.hardHeartedness ∧ jaksaa.prerequisite = Nadathur2024.Implicative.Prerequisite.strength ∧ mahtua.prerequisite = Nadathur2024.Implicative.Prerequisite.fitness ∧ ehtia.prerequisite = Nadathur2024.Implicative.Prerequisite.time ∧ kehdata.prerequisite = Nadathur2024.Implicative.Prerequisite.shamelessness

Each specific implicative has a distinct prerequisite type.

theorem Fragments.Finnish.Predicates.bleached_unspecified : onnistua.prerequisite = Nadathur2024.Implicative.Prerequisite.unspecified ∧ pystya.prerequisite = Nadathur2024.Implicative.Prerequisite.unspecified

Bleached implicatives (manage-type) have unspecified prerequisites.

theorem Fragments.Finnish.Predicates.polarity_reversing : laiminlyoda.implicativeBuilder = Nadathur2024.Implicative.ImplicativeBuilder.negative ∧ eparoida.implicativeBuilder = Nadathur2024.Implicative.ImplicativeBuilder.negative

Polarity-reversing verbs have negative polarity.

theorem Fragments.Finnish.Predicates.polarity_preserving : onnistua.implicativeBuilder = Nadathur2024.Implicative.ImplicativeBuilder.positive ∧ uskaltaa.implicativeBuilder = Nadathur2024.Implicative.ImplicativeBuilder.positive ∧ viitsia.implicativeBuilder = Nadathur2024.Implicative.ImplicativeBuilder.positive ∧ malttaa.implicativeBuilder = Nadathur2024.Implicative.ImplicativeBuilder.positive ∧ hennoa.implicativeBuilder = Nadathur2024.Implicative.ImplicativeBuilder.positive ∧ jaksaa.implicativeBuilder = Nadathur2024.Implicative.ImplicativeBuilder.positive ∧ mahtua.implicativeBuilder = Nadathur2024.Implicative.ImplicativeBuilder.positive ∧ pystya.implicativeBuilder = Nadathur2024.Implicative.ImplicativeBuilder.positive ∧ kehdata.implicativeBuilder = Nadathur2024.Implicative.ImplicativeBuilder.positive ∧ ehtia.implicativeBuilder = Nadathur2024.Implicative.ImplicativeBuilder.positive

Polarity-preserving verbs have positive polarity.

def Fragments.Finnish.Predicates.FinnishImplicativeVerb.toImplicativeClass (v : FinnishImplicativeVerb) : Nadathur2024.Implicative.ImplicativeClass

Convert a Finnish implicative verb to an ImplicativeClass.

Equations

• v.toImplicativeClass = { polarity := v.implicativeBuilder, directionality := v.directionality, aspectGoverned := false, prerequisite := some v.prerequisite }

theorem Fragments.Finnish.Predicates.uskaltaa_matches_dare : uskaltaa.toImplicativeClass = Nadathur2024.Implicative.ImplicativeClass.dare

Uskaltaa and English dare have the same classification.