Japanese Negation Fragment

@cite{miestamo-2005} @cite{haspelmath-2013} @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 : Typology.Negation.NegMarkerEntry

-nai — Japanese's negative verbal suffix. Attaches to the verb stem (mizenkei/continuative form) and itself inflects as an i-adjective: tabe-nai (NPST), tabe-naka-tta (PST), tabe-naku-te (GER). The shift of TAM marking from the stem to the -nai suffix is the A/Fin+A/Cat asymmetry captured by japaneseNegDistribution below.

Equations

• Fragments.Japanese.Negation.negSuffix = { form := "-nai", morphemeType := Typology.Negation.NegMorphemeType.affix, position := Typology.Negation.NegMarkerPosition.morphological }

def Fragments.Japanese.Negation.negationSystem : Typology.Negation.NegationSystem

The Japanese negation system: a single verbal affix with rich morphological redistribution (see japaneseNegDistribution). The Fragment-side joint consumed by Phenomena/Negation/Studies/Dryer2013.lean.

Equations

• Fragments.Japanese.Negation.negationSystem = Typology.Negation.NegationSystem.ofISO "jpn" [Fragments.Japanese.Negation.negSuffix]

structure Fragments.Japanese.Negation.NegParadigmEntry : Type

A Japanese negation paradigm entry.

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

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

Equations

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

@[implicit_reducible]

instance Fragments.Japanese.Negation.instReprNegParadigmEntry : Repr NegParadigmEntry

Equations

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

@[implicit_reducible]

instance Fragments.Japanese.Negation.instBEqNegParadigmEntry : BEq NegParadigmEntry

Equations

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

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

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

Equations

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

@[implicit_reducible]

instance Fragments.Japanese.Negation.instInhabitedNegParadigmEntry : Inhabited NegParadigmEntry

Equations

• Fragments.Japanese.Negation.instInhabitedNegParadigmEntry = { default := Fragments.Japanese.Negation.instInhabitedNegParadigmEntry.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

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

Equations

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

@[implicit_reducible]

instance Fragments.Japanese.Negation.instReprNegInflDistribution : Repr NegInflDistribution

Equations

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

@[implicit_reducible]

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.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.

def Fragments.Japanese.Negation.negationProfile : Typology.Negation.NegationProfile

Japanese negation profile (WALS Ch 112-115 + Greco/JinKoenig fields).

Equations

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