Finnish Negation: The Negative Auxiliary ei @cite{karlsson-2017}

@cite{bybee-1985} @cite{miestamo-2005}

Finnish expresses sentential negation through a conjugated negative auxiliary verb ei. The negative verb inflects for person and number, while the lexical verb appears in a nonfinite connegative form that lacks tense/agreement marking.

Paradigm (present indicative)

Person	Sg	Pl
1	e-n	e-mme
2	e-t	e-tte
3	e-i	e-ivät

Key structural property

The negative auxiliary bears the inflection that the main verb would otherwise carry. This splits the @cite{bybee-1985} relevance hierarchy: negation (rank 7) hosts agreement (rank 8) and tense, while the main verb retains only the stem and aspect. This is a counter-example to strict stem-outward ordering within a single word — the ordering principle holds across the analytical construction (neg aux + main verb) rather than within a synthetic word.

structure Fragments.Finnish.Negation.NegForm : Type

Person–number features for the Finnish negative auxiliary.

• person : Nat
• number : String
• form : String

def Fragments.Finnish.Negation.instReprNegForm.repr : NegForm → Nat → Std.Format

Equations

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

instance Fragments.Finnish.Negation.instReprNegForm : Repr NegForm

Equations

• Fragments.Finnish.Negation.instReprNegForm = { reprPrec := Fragments.Finnish.Negation.instReprNegForm.repr }

instance Fragments.Finnish.Negation.instBEqNegForm : BEq NegForm

Equations

• Fragments.Finnish.Negation.instBEqNegForm = { beq := Fragments.Finnish.Negation.instBEqNegForm.beq }

def Fragments.Finnish.Negation.instBEqNegForm.beq : NegForm → NegForm → Bool

Equations

• Fragments.Finnish.Negation.instBEqNegForm.beq { person := a, number := a_1, form := a_2 } { person := b, number := b_1, form := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Fragments.Finnish.Negation.instBEqNegForm.beq x✝¹ x✝ = false

def Fragments.Finnish.Negation.negParadigm : List NegForm

Full present-tense paradigm of the negative auxiliary ei.

Equations

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

def Fragments.Finnish.Negation.connegativeRule : Core.Morphology.MorphRule Bool

The connegative MorphRule: strips tense marking from the main verb, leaving only the bare stem. The negative auxiliary carries tense instead.

Example: mene-n (I go) → en mene (I don't go)

• neg aux en carries 1sg agreement
• main verb mene is the connegative (bare stem)

Equations

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

def Fragments.Finnish.Negation.negAgreementRule (person : Nat) (number : String) : Core.Morphology.MorphRule Bool

The negative auxiliary's agreement rule: semantically vacuous, carries person/number agreement that would otherwise be on the main verb.

Equations

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

def Fragments.Finnish.Negation.finnishNegDistribution : Core.Morphology.InflDistribution

Finnish negative construction inflection distribution.

The negative auxiliary hosts: negation, tense, agreement. The main verb retains: stem, aspect (via participle choice). Uses the shared InflDistribution from Core.Morphology: onAux = negative auxiliary, onLex = main verb.

Equations

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

theorem Fragments.Finnish.Negation.paradigm_size : negParadigm.length = 6

The paradigm has exactly 6 forms (3 persons × 2 numbers).

theorem Fragments.Finnish.Negation.singular_short : ((List.filter (fun (x : NegForm) => x.number == "sg") negParadigm).all fun (f : NegForm) => decide (f.form.length ≤ 2)) = true

All singular forms are monosyllabic (≤ 2 characters).

theorem Fragments.Finnish.Negation.shared_stem : (negParadigm.all fun (f : NegForm) => f.form.get { } == 'e') = true

All forms share the stem e- (first character is 'e').

theorem Fragments.Finnish.Negation.connegative_not_vacuous : connegativeRule.isVacuous = false

The connegative rule is NOT semantically vacuous — it carries negation.

theorem Fragments.Finnish.Negation.connegative_negates : connegativeRule.semEffect true = false

The connegative rule's semantic effect is Boolean negation.

theorem Fragments.Finnish.Negation.neg_agreement_vacuous : (negAgreementRule 1 "sg").isVacuous = true

Agreement on the neg aux IS semantically vacuous.

theorem Fragments.Finnish.Negation.neg_aux_respects_bybee : Core.Morphology.MorphCategory.negation.relevanceRank < Core.Morphology.MorphCategory.agreement.relevanceRank

Negation (rank 7) hosts agreement (rank 8) on the negative auxiliary — respecting Bybee's hierarchy within the neg aux word.