Burmese Negation Fragment

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

Burmese expresses standard negation with a circumfix: prefix ma- on the verb and suffix -bu replacing the TAM markers of the affirmative.

Always asymmetric (A/Cat)

Burmese negation is always asymmetric: the negative suffix -bu replaces the TAM (tense-aspect-mood) markers used in the affirmative, neutralizing TAM distinctions. This is paradigmatic asymmetry: the negative paradigm has fewer formal distinctions than the affirmative.

Paradigm (sa 'eat')

Construction	Affirmative	Negative
Realis	sa-deh	ma-sa-bu
Irrealis	sa-meh	ma-sa-bu
Future	sa-laimeh	ma-sa-bu

The affirmative distinguishes realis (-deh), irrealis (-meh), and future (-laimeh), but the negative collapses all three to ma-...-bu.

def Fragments.Burmese.Negation.negPrefix : String

The Burmese negative prefix.

Equations

• Fragments.Burmese.Negation.negPrefix = "ma-"

def Fragments.Burmese.Negation.negSuffix : String

The Burmese negative suffix (replaces TAM markers).

Equations

• Fragments.Burmese.Negation.negSuffix = "-bu"

structure Fragments.Burmese.Negation.NegParadigmEntry : Type

A Burmese negation paradigm entry showing TAM neutralization.

• tamLabel : String
• affirmative : String
• negative : String
• glossAff : String
• glossNeg : String

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

Equations

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

instance Fragments.Burmese.Negation.instReprNegParadigmEntry : Repr NegParadigmEntry

Equations

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

instance Fragments.Burmese.Negation.instBEqNegParadigmEntry : BEq NegParadigmEntry

Equations

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

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

Equations

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

def Fragments.Burmese.Negation.saParadigm : List NegParadigmEntry

Paradigm for sa 'eat'.

Equations

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

structure Fragments.Burmese.Negation.TAMAvailability : Type

Which TAM categories are available in affirmative vs negative.

• affirmativeTAM : List String

  TAM distinctions available in affirmative

• negativeTAM : List String

  TAM distinctions available in negative

def Fragments.Burmese.Negation.instReprTAMAvailability.repr : TAMAvailability → Nat → Std.Format

Equations

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

instance Fragments.Burmese.Negation.instReprTAMAvailability : Repr TAMAvailability

Equations

• Fragments.Burmese.Negation.instReprTAMAvailability = { reprPrec := Fragments.Burmese.Negation.instReprTAMAvailability.repr }

instance Fragments.Burmese.Negation.instBEqTAMAvailability : BEq TAMAvailability

Equations

• Fragments.Burmese.Negation.instBEqTAMAvailability = { beq := Fragments.Burmese.Negation.instBEqTAMAvailability.beq }

def Fragments.Burmese.Negation.instBEqTAMAvailability.beq : TAMAvailability → TAMAvailability → Bool

Equations

• Fragments.Burmese.Negation.instBEqTAMAvailability.beq { affirmativeTAM := a, negativeTAM := a_1 } { affirmativeTAM := b, negativeTAM := b_1 } = (a == b && a_1 == b_1)
• Fragments.Burmese.Negation.instBEqTAMAvailability.beq x✝¹ x✝ = false

def Fragments.Burmese.Negation.burmeseTAM : TAMAvailability

Equations

• Fragments.Burmese.Negation.burmeseTAM = { affirmativeTAM := ["realis", "irrealis", "future"], negativeTAM := ["general negative"] }

Verification

theorem Fragments.Burmese.Negation.negPrefix_is_ma : negPrefix = "ma-"

theorem Fragments.Burmese.Negation.negSuffix_is_bu : negSuffix = "-bu"

theorem Fragments.Burmese.Negation.sa_paradigm_size : saParadigm.length = 3

theorem Fragments.Burmese.Negation.tam_neutralized : have negForms := List.map (fun (x : NegParadigmEntry) => x.negative) saParadigm; (negForms.all fun (x : String) => x == "ma-sa-bu") = true

All negative forms are identical: TAM is neutralized.

theorem Fragments.Burmese.Negation.paradigmatic_asymmetry : burmeseTAM.affirmativeTAM.length = 3 ∧ burmeseTAM.negativeTAM.length = 1

The affirmative has 3 distinct TAM forms; the negative has 1.

theorem Fragments.Burmese.Negation.affirmative_forms_distinct : have affForms := List.map (fun (x : NegParadigmEntry) => x.affirmative) saParadigm; affForms.length = 3 ∧ affForms.eraseDups.length = 3

All affirmative forms are distinct (3 TAM contrasts).

theorem Fragments.Burmese.Negation.all_neg_circumfix : (saParadigm.all fun (e : NegParadigmEntry) => Fragments.Burmese.Negation.hasSubstr✝ e.negative "ma-" && Fragments.Burmese.Negation.hasSubstr✝¹ e.negative "-bu") = true

All negative forms contain the circumfix ma-...-bu.