Japanese Negation Fragment

[Mie05] [Has13b] [DH13a]

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 Japanese.Negation.negSuffix : Syntax.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

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

def Japanese.Negation.negationSystem : Syntax.Negation.NegationSystem

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

Equations

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

structure Japanese.Negation.NegParadigmEntry : Type

A Japanese negation paradigm entry.

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

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

Equations

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

@[implicit_reducible]

instance Japanese.Negation.instReprNegParadigmEntry : Repr NegParadigmEntry

Equations

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

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

Equations

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

@[implicit_reducible]

instance Japanese.Negation.instBEqNegParadigmEntry : BEq NegParadigmEntry

Equations

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

@[implicit_reducible]

instance Japanese.Negation.instInhabitedNegParadigmEntry : Inhabited NegParadigmEntry

Equations

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

def 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 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 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 Morphology.MorphCategory

  Categories on verb stem in affirmative

• negativeOnStem : List Morphology.MorphCategory

  Categories on verb stem in negative

• negativeOnSuffix : List Morphology.MorphCategory

  Categories on the negative suffix

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

Equations

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

@[implicit_reducible]

instance Japanese.Negation.instReprNegInflDistribution : Repr NegInflDistribution

Equations

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

@[implicit_reducible]

instance Japanese.Negation.instBEqNegInflDistribution : BEq NegInflDistribution

Equations

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

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

Equations

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

def Japanese.Negation.japaneseNegDistribution : NegInflDistribution

Equations

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

Verification

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

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

theorem Japanese.Negation.neg_past_form : (List.filter (fun (x : NegParadigmEntry) => x.formLabel == "past") taberuParadigm).head!.negative = "tabenakatta"

The negative past form is tabenakatta — built on the negative stem, not the affirmative past tabeta.

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

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

def Japanese.Negation.negationProfile : Syntax.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.