Japanese Negation Fragment

@cite{miestamo-2005} @cite{dryer-haspelmath-2013}

Japanese expresses standard negation with the suffix -nai on the verb stem. This is asymmetric negation of type A/Fin+A/Cat: the negative form differs from the affirmative both in finiteness properties and in category marking.

Key asymmetries

1. A/Fin: The negative suffix -nai conjugates as an i-adjective, not as a verb. The lexical verb loses its finite inflection and appears as a stem (continuative/mizenkei form).

2. A/Cat: Past tense in the negative is formed differently:

   • Affirmative past: stem + -ta (e.g., tabe-ta 'ate')
   • Negative past: stem + -naka-tta (e.g., tabe-naka-tta 'didn't eat')

   The negative past uses the -nai → -nakatta i-adjective past, NOT the verbal past -ta directly on the stem.

Paradigm (taberu 'eat')

Form	Affirmative	Negative
Nonpast	tabe-ru	tabe-nai
Past	tabe-ta	tabe-naka-tta
Gerund	tabe-te	tabe-naku-te
Conditional	tabe-reba	tabe-nake-reba

def Fragments.Japanese.Negation.negSuffix : String

The Japanese negative suffix.

Equations

• Fragments.Japanese.Negation.negSuffix = "-nai"

structure Fragments.Japanese.Negation.NegParadigmEntry : Type

A Japanese negation paradigm entry.

• formLabel : String
• affirmative : String
• negative : String
• glossAff : String
• glossNeg : String

instance Fragments.Japanese.Negation.instReprNegParadigmEntry : Repr NegParadigmEntry

Equations

• Fragments.Japanese.Negation.instReprNegParadigmEntry = { reprPrec := Fragments.Japanese.Negation.instReprNegParadigmEntry.repr }

def Fragments.Japanese.Negation.instReprNegParadigmEntry.repr : NegParadigmEntry → Nat → Std.Format

Equations

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

def Fragments.Japanese.Negation.instBEqNegParadigmEntry.beq : NegParadigmEntry → NegParadigmEntry → Bool

Equations

• One or more equations did not get rendered due to their size.
• Fragments.Japanese.Negation.instBEqNegParadigmEntry.beq x✝¹ x✝ = false

instance Fragments.Japanese.Negation.instBEqNegParadigmEntry : BEq NegParadigmEntry

Equations

• Fragments.Japanese.Negation.instBEqNegParadigmEntry = { beq := Fragments.Japanese.Negation.instBEqNegParadigmEntry.beq }

instance Fragments.Japanese.Negation.instInhabitedNegParadigmEntry : Inhabited NegParadigmEntry

Equations

• Fragments.Japanese.Negation.instInhabitedNegParadigmEntry = { default := Fragments.Japanese.Negation.instInhabitedNegParadigmEntry.default }

def Fragments.Japanese.Negation.instInhabitedNegParadigmEntry.default : NegParadigmEntry

Equations

• Fragments.Japanese.Negation.instInhabitedNegParadigmEntry.default = { formLabel := default, affirmative := default, negative := default, glossAff := default, glossNeg := default }

def Fragments.Japanese.Negation.taberuParadigm : List NegParadigmEntry

Paradigm for taberu 'eat' (ichidan/vowel-stem verb).

Equations

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

def Fragments.Japanese.Negation.yomuParadigm : List NegParadigmEntry

Paradigm for yomu 'read' (godan/consonant-stem verb). Shows the stem-final consonant alternation.

Equations

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

structure Fragments.Japanese.Negation.NegInflDistribution : Type

Which morphological categories are affected by negation. In the affirmative, tense is marked directly on the verb stem. In the negative, tense is marked on the -nai suffix (i-adjective inflection), not on the verb stem.

• affirmativeOnStem : List Core.Morphology.MorphCategory

  Categories on verb stem in affirmative

• negativeOnStem : List Core.Morphology.MorphCategory

  Categories on verb stem in negative

• negativeOnSuffix : List Core.Morphology.MorphCategory

  Categories on the negative suffix

instance Fragments.Japanese.Negation.instReprNegInflDistribution : Repr NegInflDistribution

Equations

• Fragments.Japanese.Negation.instReprNegInflDistribution = { reprPrec := Fragments.Japanese.Negation.instReprNegInflDistribution.repr }

def Fragments.Japanese.Negation.instReprNegInflDistribution.repr : NegInflDistribution → Nat → Std.Format

Equations

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

instance Fragments.Japanese.Negation.instBEqNegInflDistribution : BEq NegInflDistribution

Equations

• Fragments.Japanese.Negation.instBEqNegInflDistribution = { beq := Fragments.Japanese.Negation.instBEqNegInflDistribution.beq }

def Fragments.Japanese.Negation.instBEqNegInflDistribution.beq : NegInflDistribution → NegInflDistribution → Bool

Equations

• One or more equations did not get rendered due to their size.
• Fragments.Japanese.Negation.instBEqNegInflDistribution.beq x✝¹ x✝ = false

def Fragments.Japanese.Negation.japaneseNegDistribution : NegInflDistribution

Equations

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

Verification

theorem Fragments.Japanese.Negation.negSuffix_is_nai : negSuffix = "-nai"

theorem Fragments.Japanese.Negation.taberu_paradigm_size : taberuParadigm.length = 5

theorem Fragments.Japanese.Negation.yomu_paradigm_size : yomuParadigm.length = 2

theorem Fragments.Japanese.Negation.neg_past_differs_from_aff_past : have affPast := (List.filter (fun (x : NegParadigmEntry) => x.formLabel == "past") taberuParadigm).head!; have negPast := affPast.negative; negPast = "tabenakatta" ∧ Fragments.Japanese.Negation.hasSubstr✝ negPast "nakatta" = true

The verb stem in negative forms differs from affirmative — asymmetry is visible: negative past tabenakatta does not contain the affirmative past suffix -ta directly on the stem.

theorem Fragments.Japanese.Negation.all_neg_contain_na : (taberuParadigm.all fun (e : NegParadigmEntry) => Fragments.Japanese.Negation.hasSubstr✝ e.negative "na") = true

All negative forms contain the negative morpheme na.

theorem Fragments.Japanese.Negation.tense_moves_to_suffix : japaneseNegDistribution.affirmativeOnStem.contains Core.Morphology.MorphCategory.tense = true ∧ japaneseNegDistribution.negativeOnStem.contains Core.Morphology.MorphCategory.tense = false ∧ japaneseNegDistribution.negativeOnSuffix.contains Core.Morphology.MorphCategory.tense = true

The distribution shows that tense moves from stem to suffix under negation.