Miestamo (2005): Standard Negation

@cite{miestamo-2005}

@cite{miestamo-2005} refines the WALS symmetric/asymmetric classification (Ch 113-114) with two orthogonal theoretical distinctions:

1. Constructional vs Paradigmatic Asymmetry

WALS Ch 113 collapses these into a single "asymmetric" category, but Miestamo decomposes asymmetry into two independent dimensions:

• Constructional: the syntactic structure of the negative clause differs from the affirmative beyond just adding the negation marker. E.g., Finnish uses a negative auxiliary + connegative, restructuring the clause.

• Paradigmatic: the paradigm (set of available formal distinctions) is different in the negative. E.g., Burmese -bu replaces all TAM suffixes, collapsing three distinctions to one.

These are orthogonal: a language can have constructional asymmetry with full paradigmatic symmetry (Finnish), or paradigmatic asymmetry without major constructional changes (Turkish aorist).

2. Derived vs Independent Asymmetry

• Derived: the asymmetry is a structural consequence of the negation marker's properties. A negative verb necessarily creates A/Fin because it takes over the finite verb slot — the asymmetry follows from the morphological type.

• Independent: the asymmetry is not structurally predictable from the negation marker type. E.g., Burmese TAM neutralization does not follow from having a circumfix — other circumfixing languages maintain TAM.

WALS Consistency

Every datum here is consistent with the coarser WALS classification:

• Symmetric-only → no constructional or paradigmatic asymmetry
• Asymmetric A/Fin → constructional asymmetry (almost always; 44/45 in Table 5)
• Asymmetric A/Cat → paradigmatic or constructional or both
• SymAsy → some constructions symmetric, others asymmetric

Quantitative Data

The book's representative sample (RS) covers 179 languages (Table 3, p. 171): Sym 72 (40%), SymAsy 76 (42%), Asy 31 (17%). Note: the WALS Ch 113 sample (also by Miestamo) covers 297 languages with different numbers; those are captured separately via Data.WALS.F113A.

inductive Miestamo2005.AsymmetryDimension : Type

@cite{miestamo-2005}'s two dimensions of asymmetry. WALS Ch 113 collapses these into a single symmetric/asymmetric distinction; Miestamo decomposes asymmetry into two independent dimensions. Local to this study file because the dimensions are framework-distinctive.

• constructional : AsymmetryDimension

  The negative clause has a different syntactic structure than the affirmative, beyond just the negation marker. E.g., Finnish neg aux restructures the clause; Japanese -nai changes verb to i-adjective.

• paradigmatic : AsymmetryDimension

  The negative paradigm has fewer formal distinctions than the affirmative. E.g., Burmese -bu neutralizes TAM; Turkish aorist uses a different marker.

@[implicit_reducible]

instance Miestamo2005.instDecidableEqAsymmetryDimension : DecidableEq AsymmetryDimension

Equations

• Miestamo2005.instDecidableEqAsymmetryDimension x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Miestamo2005.instBEqAsymmetryDimension.beq : AsymmetryDimension → AsymmetryDimension → Bool

Equations

• Miestamo2005.instBEqAsymmetryDimension.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Miestamo2005.instBEqAsymmetryDimension : BEq AsymmetryDimension

Equations

• Miestamo2005.instBEqAsymmetryDimension = { beq := Miestamo2005.instBEqAsymmetryDimension.beq }

def Miestamo2005.instReprAsymmetryDimension.repr : AsymmetryDimension → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Miestamo2005.instReprAsymmetryDimension : Repr AsymmetryDimension

Equations

• Miestamo2005.instReprAsymmetryDimension = { reprPrec := Miestamo2005.instReprAsymmetryDimension.repr }

inductive Miestamo2005.AsymmetrySource : Type

Whether the asymmetry is derived from the negation marker type or independent of it (@cite{miestamo-2005}).

• derived : AsymmetrySource

  The asymmetry follows structurally from the negation marker's properties. A negative verb necessarily creates A/Fin.

• independent : AsymmetrySource

  The asymmetry is not predictable from the marker type alone. E.g., TAM neutralization in Burmese is independent of circumfixing.

@[implicit_reducible]

instance Miestamo2005.instDecidableEqAsymmetrySource : DecidableEq AsymmetrySource

Equations

• Miestamo2005.instDecidableEqAsymmetrySource x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Miestamo2005.instBEqAsymmetrySource : BEq AsymmetrySource

Equations

• Miestamo2005.instBEqAsymmetrySource = { beq := Miestamo2005.instBEqAsymmetrySource.beq }

def Miestamo2005.instBEqAsymmetrySource.beq : AsymmetrySource → AsymmetrySource → Bool

Equations

• Miestamo2005.instBEqAsymmetrySource.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Miestamo2005.instReprAsymmetrySource.repr : AsymmetrySource → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Miestamo2005.instReprAsymmetrySource : Repr AsymmetrySource

Equations

• Miestamo2005.instReprAsymmetrySource = { reprPrec := Miestamo2005.instReprAsymmetrySource.repr }

structure Miestamo2005.MiestamoDatum : Type

A Miestamo-style negation profile extending the WALS classification.

• language : String
• morphemeType : Typology.Negation.NegMorphemeType

  WALS Ch 112: morpheme type

• symmetry : Typology.Negation.NegSymmetry

  WALS Ch 113: symmetric/asymmetric/both

• asymmetrySubtype : Typology.Negation.AsymmetrySubtype

  WALS Ch 114: asymmetry subtype

• asymmetryDimensions : List AsymmetryDimension

  Miestamo: which dimensions of asymmetry are present

• asymmetrySource : Option AsymmetrySource

  Miestamo: is the asymmetry derived or independent?

• negMarkers : List String

  Negation marker form(s), derived from Fragment where available

• asymmetryDescription : String

  Brief description of the asymmetry (if any)

@[implicit_reducible]

instance Miestamo2005.instReprMiestamoDatum : Repr MiestamoDatum

Equations

• Miestamo2005.instReprMiestamoDatum = { reprPrec := Miestamo2005.instReprMiestamoDatum.repr }

def Miestamo2005.instReprMiestamoDatum.repr : MiestamoDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Miestamo2005.instBEqMiestamoDatum : BEq MiestamoDatum

Equations

• Miestamo2005.instBEqMiestamoDatum = { beq := Miestamo2005.instBEqMiestamoDatum.beq }

def Miestamo2005.instBEqMiestamoDatum.beq : MiestamoDatum → MiestamoDatum → Bool

Equations

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

def Miestamo2005.finnish : MiestamoDatum

Finnish: constructional A/Fin, derived. Neg aux ei restructures clause. Form derived from Fragments.Finnish.Negation.negParadigm.

Equations

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

def Miestamo2005.german : MiestamoDatum

German: symmetric, no asymmetry. Particle nicht. Form derived from Fragments.German.Negation.nicht.form.

Equations

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

def Miestamo2005.japanese : MiestamoDatum

Japanese: constructional + paradigmatic, A/Fin+A/Cat. Suffix -nai changes verb to i-adjective (constructional) and shifts tense marking to the suffix (paradigmatic). Form derived from Fragments.Japanese.Negation.negSuffix.form.

Equations

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

def Miestamo2005.turkish : MiestamoDatum

Turkish: SymAsy with paradigmatic A/Cat (aorist only). Most constructions symmetric; aorist negative uses -z instead of -(I)r. Form derived from Fragments.Turkish.Negation.negSuffix.form.

Equations

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

def Miestamo2005.french : MiestamoDatum

French: symmetric. Bipartite ne...pas introduces no structural change. Forms derived from Fragments.French.Negation.

Equations

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

def Miestamo2005.burmese : MiestamoDatum

Burmese: constructional + paradigmatic A/Cat, independent. Circumfix ma-...-bu replaces TAM markers. Forms derived from Fragments.Burmese.Negation.

Equations

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

def Miestamo2005.italian : MiestamoDatum

Italian: symmetric. Particle non, no structural change. Form derived from Fragments.Italian.Negation.non.form.

Equations

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

def Miestamo2005.spanish : MiestamoDatum

Spanish: symmetric. Particle no, no structural change. Form derived from Fragments.Spanish.Negation.no.form.

Equations

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

def Miestamo2005.mandarin : MiestamoDatum

Mandarin Chinese: SymAsy with constructional A/Fin. Non-perfectives negated by bù (symmetric). Perfectives negated by méi(yǒu): the existential verb yǒu is introduced as the finite element (FE), the lexical verb loses finite status (A/Fin/Neg-FE). When méi occurs without yǒu, it functions as a negative existential verb (A/Fin/NegVerb). @cite{miestamo-2005} pp. 90–91, example 51. Forms derived from Fragments.Mandarin.Negation.

Equations

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

def Miestamo2005.english : MiestamoDatum

English: SymAsy with constructional A/Cat (do-support). With modals/be/have, negation is symmetric; with lexical verbs, do-support introduces a structural change (constructional asymmetry). Form derived from Fragments.English.Negation.not.form.

Equations

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

def Miestamo2005.russian : MiestamoDatum

Russian: symmetric. Particle не (ne), no structural change. Form derived from Fragments.Slavic.Russian.Negation.ne.form.

Equations

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

def Miestamo2005.czech : MiestamoDatum

Czech: symmetric. Prefix ne-, no structural change. Form derived from Fragments.Slavic.Czech.Negation.negPrefix.

Equations

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

def Miestamo2005.maori : MiestamoDatum

Maori: constructional A/Fin, source unclear. Kāhore functions as a quasi-auxiliary, changing the finiteness structure. WALS classifies morpheme type as wordUnclear. Form derived from Fragments.Maori.Negation.kahore.form.

Equations

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

def Miestamo2005.hixkaryana : MiestamoDatum

Hixkaryana: constructional A/Fin, independent. Suffix -hira deverbalizes the verb; a copula becomes the finite element. Form derived from Fragments.Hixkaryana.Negation.hira.form.

Equations

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

def Miestamo2005.imbaburaQuechua : MiestamoDatum

Imbabura Quechua: SymAsy with paradigmatic A/NonReal, independent. Particle mana; validator enclitic -chu obligatory in some negative constructions. -chu also appears in polar interrogatives — it is a general "validator" expressing assertion authority (@cite{miestamo-2005} p. 158). Some constructions symmetric, others require -chu. Form derived from Fragments.Quechua.Negation.mana.form.

Equations

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

def Miestamo2005.allData : List MiestamoDatum

Equations

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

theorem Miestamo2005.symmetric_no_dimensions : ((List.filter (fun (x : MiestamoDatum) => x.symmetry == Typology.Negation.NegSymmetry.symmetric) allData).all fun (d : MiestamoDatum) => d.asymmetryDimensions.isEmpty) = true

Symmetric languages have no asymmetry dimensions.

theorem Miestamo2005.symmetric_no_source : ((List.filter (fun (x : MiestamoDatum) => x.symmetry == Typology.Negation.NegSymmetry.symmetric) allData).all fun (d : MiestamoDatum) => d.asymmetrySource.isNone) = true

Symmetric languages have no asymmetry source.

theorem Miestamo2005.asymmetric_has_dimensions : ((List.filter (fun (x : MiestamoDatum) => x.symmetry == Typology.Negation.NegSymmetry.asymmetric) allData).all fun (d : MiestamoDatum) => !d.asymmetryDimensions.isEmpty) = true

Asymmetric languages have at least one asymmetry dimension.

theorem Miestamo2005.asymmetric_has_source : ((List.filter (fun (x : MiestamoDatum) => x.symmetry == Typology.Negation.NegSymmetry.asymmetric) allData).all fun (d : MiestamoDatum) => d.asymmetrySource.isSome) = true

Asymmetric languages have an asymmetry source.

theorem Miestamo2005.symasy_has_dimensions : ((List.filter (fun (x : MiestamoDatum) => x.symmetry == Typology.Negation.NegSymmetry.both) allData).all fun (d : MiestamoDatum) => !d.asymmetryDimensions.isEmpty) = true

SymAsy languages have at least one asymmetry dimension (for their asymmetric constructions).

theorem Miestamo2005.afin_verbal_implies_constructional : ((List.filter (fun (d : MiestamoDatum) => (d.asymmetrySubtype == Typology.Negation.AsymmetrySubtype.finiteness || d.asymmetrySubtype == Typology.Negation.AsymmetrySubtype.finAndCat || d.asymmetrySubtype == Typology.Negation.AsymmetrySubtype.finAndNonReal) && d.morphemeType == Typology.Negation.NegMorphemeType.auxVerb) allData).all fun (d : MiestamoDatum) => d.asymmetryDimensions.contains AsymmetryDimension.constructional) = true

A/Fin with a verbal negator implies constructional asymmetry: the negative verb takes over the finite verb slot, necessarily restructuring the clause.

theorem Miestamo2005.afin_always_constructional_in_sample : ((List.filter (fun (d : MiestamoDatum) => d.asymmetrySubtype == Typology.Negation.AsymmetrySubtype.finiteness || d.asymmetrySubtype == Typology.Negation.AsymmetrySubtype.finAndCat || d.asymmetrySubtype == Typology.Negation.AsymmetrySubtype.finAndNonReal) allData).all fun (d : MiestamoDatum) => d.asymmetryDimensions.contains AsymmetryDimension.constructional) = true

All A/Fin languages in our sample have constructional asymmetry, regardless of negation marker type. Even Mandarin's particle-type méi(yǒu) introduces structural changes (existential verb as FE).

theorem Miestamo2005.symmetric_implies_nonassignable : ((List.filter (fun (x : MiestamoDatum) => x.symmetry == Typology.Negation.NegSymmetry.symmetric) allData).all fun (d : MiestamoDatum) => d.asymmetrySubtype == Typology.Negation.AsymmetrySubtype.nonAssignable) = true

Symmetric-only (WALS) implies nonAssignable asymmetry subtype.

theorem Miestamo2005.finnish_morpheme_consistent : finnish.morphemeType = Fragments.Finnish.Negation.negationProfile.morphemeType

Morpheme types are consistent with WALS Typology profiles.

theorem Miestamo2005.german_morpheme_consistent : german.morphemeType = Fragments.German.Negation.negationProfile.morphemeType

theorem Miestamo2005.japanese_morpheme_consistent : japanese.morphemeType = Fragments.Japanese.Negation.negationProfile.morphemeType

theorem Miestamo2005.turkish_morpheme_consistent : turkish.morphemeType = Fragments.Turkish.Negation.negationProfile.morphemeType

theorem Miestamo2005.italian_morpheme_consistent : italian.morphemeType = Fragments.Italian.Negation.negationProfile.morphemeType

theorem Miestamo2005.burmese_morpheme_consistent : burmese.morphemeType = Fragments.Burmese.Negation.negationProfile.morphemeType

theorem Miestamo2005.french_morpheme_consistent : french.morphemeType = Fragments.French.Negation.negationProfile.morphemeType

theorem Miestamo2005.spanish_morpheme_consistent : spanish.morphemeType = Fragments.Spanish.Negation.negationProfile.morphemeType

theorem Miestamo2005.mandarin_morpheme_consistent : mandarin.morphemeType = Fragments.Mandarin.Negation.negationProfile.morphemeType

theorem Miestamo2005.english_morpheme_consistent : english.morphemeType = Fragments.English.Negation.negationProfile.morphemeType

theorem Miestamo2005.russian_morpheme_consistent : russian.morphemeType = Fragments.Slavic.Russian.Negation.negationProfile.morphemeType

theorem Miestamo2005.czech_morpheme_consistent : czech.morphemeType = Fragments.Slavic.Czech.Negation.negationProfile.morphemeType

theorem Miestamo2005.maori_morpheme_consistent : maori.morphemeType = Fragments.Maori.Negation.negationProfile.morphemeType

theorem Miestamo2005.hixkaryana_morpheme_consistent : hixkaryana.morphemeType = Fragments.Hixkaryana.Negation.negationProfile.morphemeType

theorem Miestamo2005.imbaburaQuechua_morpheme_consistent : imbaburaQuechua.morphemeType = Fragments.Quechua.Negation.negationProfile.morphemeType

theorem Miestamo2005.finnish_symmetry_consistent : finnish.symmetry = Fragments.Finnish.Negation.negationProfile.symmetry

Symmetry values are consistent with WALS Typology profiles.

theorem Miestamo2005.german_symmetry_consistent : german.symmetry = Fragments.German.Negation.negationProfile.symmetry

theorem Miestamo2005.japanese_symmetry_consistent : japanese.symmetry = Fragments.Japanese.Negation.negationProfile.symmetry

theorem Miestamo2005.turkish_symmetry_consistent : turkish.symmetry = Fragments.Turkish.Negation.negationProfile.symmetry

theorem Miestamo2005.italian_symmetry_consistent : italian.symmetry = Fragments.Italian.Negation.negationProfile.symmetry

theorem Miestamo2005.burmese_symmetry_consistent : burmese.symmetry = Fragments.Burmese.Negation.negationProfile.symmetry

theorem Miestamo2005.french_symmetry_consistent : french.symmetry = Fragments.French.Negation.negationProfile.symmetry

theorem Miestamo2005.spanish_symmetry_consistent : spanish.symmetry = Fragments.Spanish.Negation.negationProfile.symmetry

theorem Miestamo2005.mandarin_symmetry_consistent : mandarin.symmetry = Fragments.Mandarin.Negation.negationProfile.symmetry

theorem Miestamo2005.english_symmetry_consistent : english.symmetry = Fragments.English.Negation.negationProfile.symmetry

theorem Miestamo2005.russian_symmetry_consistent : russian.symmetry = Fragments.Slavic.Russian.Negation.negationProfile.symmetry

theorem Miestamo2005.czech_symmetry_consistent : czech.symmetry = Fragments.Slavic.Czech.Negation.negationProfile.symmetry

theorem Miestamo2005.maori_symmetry_consistent : maori.symmetry = Fragments.Maori.Negation.negationProfile.symmetry

theorem Miestamo2005.hixkaryana_symmetry_consistent : hixkaryana.symmetry = Fragments.Hixkaryana.Negation.negationProfile.symmetry

theorem Miestamo2005.imbaburaQuechua_symmetry_consistent : imbaburaQuechua.symmetry = Fragments.Quechua.Negation.negationProfile.symmetry

theorem Miestamo2005.finnish_subtype_consistent : finnish.asymmetrySubtype = Fragments.Finnish.Negation.negationProfile.asymmetrySubtype

Asymmetry subtypes are consistent with WALS Typology profiles.

theorem Miestamo2005.german_subtype_consistent : german.asymmetrySubtype = Fragments.German.Negation.negationProfile.asymmetrySubtype

theorem Miestamo2005.japanese_subtype_consistent : japanese.asymmetrySubtype = Fragments.Japanese.Negation.negationProfile.asymmetrySubtype

theorem Miestamo2005.turkish_subtype_consistent : turkish.asymmetrySubtype = Fragments.Turkish.Negation.negationProfile.asymmetrySubtype

theorem Miestamo2005.italian_subtype_consistent : italian.asymmetrySubtype = Fragments.Italian.Negation.negationProfile.asymmetrySubtype

theorem Miestamo2005.burmese_subtype_consistent : burmese.asymmetrySubtype = Fragments.Burmese.Negation.negationProfile.asymmetrySubtype

theorem Miestamo2005.french_subtype_consistent : french.asymmetrySubtype = Fragments.French.Negation.negationProfile.asymmetrySubtype

theorem Miestamo2005.spanish_subtype_consistent : spanish.asymmetrySubtype = Fragments.Spanish.Negation.negationProfile.asymmetrySubtype

theorem Miestamo2005.mandarin_subtype_consistent : mandarin.asymmetrySubtype = Fragments.Mandarin.Negation.negationProfile.asymmetrySubtype

theorem Miestamo2005.english_subtype_consistent : english.asymmetrySubtype = Fragments.English.Negation.negationProfile.asymmetrySubtype

theorem Miestamo2005.russian_subtype_consistent : russian.asymmetrySubtype = Fragments.Slavic.Russian.Negation.negationProfile.asymmetrySubtype

theorem Miestamo2005.czech_subtype_consistent : czech.asymmetrySubtype = Fragments.Slavic.Czech.Negation.negationProfile.asymmetrySubtype

theorem Miestamo2005.maori_subtype_consistent : maori.asymmetrySubtype = Fragments.Maori.Negation.negationProfile.asymmetrySubtype

theorem Miestamo2005.hixkaryana_subtype_consistent : hixkaryana.asymmetrySubtype = Fragments.Hixkaryana.Negation.negationProfile.asymmetrySubtype

theorem Miestamo2005.imbaburaQuechua_subtype_consistent : imbaburaQuechua.asymmetrySubtype = Fragments.Quechua.Negation.negationProfile.asymmetrySubtype

theorem Miestamo2005.finnish_markers_from_fragment : finnish.negMarkers = List.map (fun (x : Fragments.Finnish.Negation.NegForm) => x.form) Fragments.Finnish.Negation.negParadigm

Finnish negation markers derive from the Fragment paradigm.

theorem Miestamo2005.finnish_marker_count : finnish.negMarkers.length = 6

Finnish has 6 neg aux forms (3 persons x 2 numbers).

theorem Miestamo2005.german_marker_from_fragment : german.negMarkers = [Fragments.German.Negation.nicht.form]

German negation marker derives from Fragment.

theorem Miestamo2005.german_marker_is_nicht : german.negMarkers = ["nicht"]

German marker is nicht.

theorem Miestamo2005.japanese_marker_from_fragment : japanese.negMarkers = [Fragments.Japanese.Negation.negSuffix.form]

Japanese negation marker derives from Fragment.

theorem Miestamo2005.japanese_marker_is_nai : japanese.negMarkers = ["-nai"]

Japanese marker is -nai.

theorem Miestamo2005.turkish_marker_from_fragment : turkish.negMarkers = [Fragments.Turkish.Negation.negSuffix.form]

Turkish negation marker derives from Fragment.

theorem Miestamo2005.turkish_marker_is_mA : turkish.negMarkers = ["-mA-"]

Turkish marker is -mA-.

theorem Miestamo2005.french_markers_from_fragment : french.negMarkers = [Fragments.French.Negation.neClitic, Fragments.French.Negation.pasReinforcer]

French negation markers derive from Fragment.

theorem Miestamo2005.french_markers_are_ne_pas : french.negMarkers = ["ne", "pas"]

French markers are ne and pas.

theorem Miestamo2005.burmese_markers_from_fragment : burmese.negMarkers = [Fragments.Burmese.Negation.negPrefix, Fragments.Burmese.Negation.negSuffix]

Burmese negation markers derive from Fragment.

theorem Miestamo2005.burmese_markers_are_ma_bu : burmese.negMarkers = ["ma-", "-bu"]

Burmese markers are ma- and -bu.

theorem Miestamo2005.italian_marker_from_fragment : italian.negMarkers = [Fragments.Italian.Negation.non.form]

Italian negation marker derives from Fragment.

theorem Miestamo2005.italian_marker_is_non : italian.negMarkers = ["non"]

Italian marker is non.

theorem Miestamo2005.spanish_marker_from_fragment : spanish.negMarkers = [Fragments.Spanish.Negation.no.form]

Spanish negation marker derives from Fragment.

theorem Miestamo2005.spanish_marker_is_no : spanish.negMarkers = ["no"]

Spanish marker is no.

theorem Miestamo2005.mandarin_markers_from_fragment : mandarin.negMarkers = [Fragments.Mandarin.Negation.bu.form, Fragments.Mandarin.Negation.mei.form]

Mandarin negation markers derive from Fragment.

theorem Miestamo2005.mandarin_markers_are_bu_mei : mandarin.negMarkers = ["bù", "méi"]

Mandarin markers are bù and méi.

theorem Miestamo2005.english_marker_from_fragment : english.negMarkers = [Fragments.English.Negation.not.form]

English negation marker derives from Fragment.

theorem Miestamo2005.english_marker_is_not : english.negMarkers = ["not"]

English marker is not.

theorem Miestamo2005.russian_marker_from_fragment : russian.negMarkers = [Fragments.Slavic.Russian.Negation.ne.form]

Russian negation marker derives from Fragment.

theorem Miestamo2005.russian_marker_is_ne : russian.negMarkers = ["не"]

Russian marker is не.

theorem Miestamo2005.czech_marker_from_fragment : czech.negMarkers = [Fragments.Slavic.Czech.Negation.negPrefix]

Czech negation marker derives from Fragment.

theorem Miestamo2005.czech_marker_is_ne : czech.negMarkers = ["ne-"]

Czech marker is ne-.

theorem Miestamo2005.maori_marker_from_fragment : maori.negMarkers = [Fragments.Maori.Negation.kahore.form]

Maori negation word derives from Fragment.

theorem Miestamo2005.maori_marker_is_kahore : maori.negMarkers = ["kāhore"]

Maori marker is kāhore.

theorem Miestamo2005.hixkaryana_marker_from_fragment : hixkaryana.negMarkers = [Fragments.Hixkaryana.Negation.hira.form]

Hixkaryana negation suffix derives from Fragment.

theorem Miestamo2005.hixkaryana_marker_is_hira : hixkaryana.negMarkers = ["-hira"]

Hixkaryana marker is -hira.

theorem Miestamo2005.imbaburaQuechua_marker_from_fragment : imbaburaQuechua.negMarkers = [Fragments.Quechua.Negation.mana.form]

Imbabura Quechua negation particle derives from Fragment.

theorem Miestamo2005.imbaburaQuechua_marker_is_mana : imbaburaQuechua.negMarkers = ["mana"]

Imbabura Quechua marker is mana.

theorem Miestamo2005.neg_aux_implies_derived_constructional : ((List.filter (fun (x : MiestamoDatum) => x.morphemeType == Typology.Negation.NegMorphemeType.auxVerb) allData).all fun (d : MiestamoDatum) => decide ((d.asymmetrySource == some AsymmetrySource.derived) = true ∧ d.asymmetryDimensions.contains AsymmetryDimension.constructional = true)) = true

Derived asymmetry: negative auxiliary verbs always produce constructional A/Fin asymmetry. The asymmetry is derived because a verb-type negator structurally entails finiteness restructuring.

theorem Miestamo2005.symmetric_particles_no_dimensions : ((List.filter (fun (d : MiestamoDatum) => d.morphemeType == Typology.Negation.NegMorphemeType.particle && d.symmetry == Typology.Negation.NegSymmetry.symmetric) allData).all fun (d : MiestamoDatum) => d.asymmetryDimensions.isEmpty) = true

Particles that are symmetric-only have no asymmetry dimensions. Mandarin and English are SymAsy particles with constructional asymmetry (méi(yǒu) introduces A/Fin; do-support introduces A/Cat).

theorem Miestamo2005.affixes_variable : List.map (fun (x : MiestamoDatum) => x.symmetry) (List.filter (fun (x : MiestamoDatum) => x.morphemeType == Typology.Negation.NegMorphemeType.affix) allData) = [Typology.Negation.NegSymmetry.asymmetric, Typology.Negation.NegSymmetry.both, Typology.Negation.NegSymmetry.symmetric, Typology.Negation.NegSymmetry.asymmetric]

Affixes can produce symmetric, asymmetric, or SymAsy negation.

theorem Miestamo2005.finnish_no_paradigmatic_asymmetry : finnish.asymmetryDimensions = [AsymmetryDimension.constructional]

Constructional asymmetry (only) implies the paradigm is maintained: Finnish has A/Fin constructional asymmetry but no paradigmatic gaps.

theorem Miestamo2005.burmese_both_dimensions : burmese.asymmetryDimensions = [AsymmetryDimension.constructional, AsymmetryDimension.paradigmatic]

Burmese has both dimensions of asymmetry: the circumfix changes structure (constructional) and neutralizes TAM (paradigmatic).

theorem Miestamo2005.turkish_paradigmatic_only : turkish.asymmetryDimensions = [AsymmetryDimension.paradigmatic]

Turkish has paradigmatic-only asymmetry: the aorist marker changes but the clause structure does not.

theorem Miestamo2005.finnish_split_confirms_constructional : have dist := Fragments.Finnish.Negation.finnishNegDistribution; dist.onAux.length > 0 ∧ dist.onLex.length > 0 ∧ finnish.asymmetryDimensions.contains AsymmetryDimension.constructional = true

Finnish Fragment inflection distribution is consistent with constructional A/Fin: categories split across neg aux and main verb.

theorem Miestamo2005.japanese_distribution_confirms_asymmetry : have dist := Fragments.Japanese.Negation.japaneseNegDistribution; dist.affirmativeOnStem.contains Core.Morphology.MorphCategory.tense = true ∧ dist.negativeOnStem.contains Core.Morphology.MorphCategory.tense = false ∧ dist.negativeOnSuffix.contains Core.Morphology.MorphCategory.tense = true ∧ japanese.asymmetryDimensions.contains AsymmetryDimension.constructional = true ∧ japanese.asymmetryDimensions.contains AsymmetryDimension.paradigmatic = true

Japanese Fragment distribution confirms constructional + paradigmatic: tense moves from stem to suffix (both structural and paradigmatic change).

theorem Miestamo2005.turkish_fragment_confirms_symasy : (List.filter (fun (x : Fragments.Turkish.Negation.NegParadigmEntry) => x.symmetric) Fragments.Turkish.Negation.gelParadigm).length = 4 ∧ (List.filter (fun (e : Fragments.Turkish.Negation.NegParadigmEntry) => !e.symmetric) Fragments.Turkish.Negation.gelParadigm).length = 1 ∧ (turkish.symmetry == Typology.Negation.NegSymmetry.both) = true

Turkish Fragment confirms SymAsy: 4 of 5 constructions are symmetric, only the aorist is asymmetric.

theorem Miestamo2005.german_fragment_confirms_symmetric : Fragments.German.Negation.allExamples.length = 5 ∧ german.asymmetryDimensions.isEmpty = true

German Fragment confirms symmetric: all tenses available, negation is just adding nicht.

theorem Miestamo2005.burmese_fragment_confirms_paradigmatic : Fragments.Burmese.Negation.burmeseTAM.affirmativeTAM.length = 3 ∧ Fragments.Burmese.Negation.burmeseTAM.negativeTAM.length = 1 ∧ burmese.asymmetryDimensions.contains AsymmetryDimension.paradigmatic = true

Burmese Fragment confirms paradigmatic asymmetry: TAM neutralized (3 affirmative distinctions → 1 negative form).

theorem Miestamo2005.french_fragment_confirms_symmetric : Fragments.French.Negation.allExamples.length = 5 ∧ french.asymmetryDimensions.isEmpty = true

French Fragment confirms symmetric: all tenses available under negation.

theorem Miestamo2005.spanish_fragment_confirms_symmetric : Fragments.Spanish.Negation.allExamples.length = 5 ∧ spanish.asymmetryDimensions.isEmpty = true

Spanish Fragment confirms symmetric: all tenses available, no adds negation without structural change.

theorem Miestamo2005.mandarin_fragment_confirms_symasy : (List.filter (fun (x : Fragments.Mandarin.Negation.NegExample) => x.symmetric) Fragments.Mandarin.Negation.allExamples).length = 3 ∧ (List.filter (fun (e : Fragments.Mandarin.Negation.NegExample) => !e.symmetric) Fragments.Mandarin.Negation.allExamples).length = 2 ∧ (mandarin.symmetry == Typology.Negation.NegSymmetry.both) = true ∧ (mandarin.asymmetryDimensions == [AsymmetryDimension.constructional]) = true

Mandarin Fragment confirms SymAsy: 3 bù (symmetric) + 2 méi (asymmetric) constructions, matching the constructional A/Fin classification.

theorem Miestamo2005.mandarin_meiyou_cross_module : Fragments.Mandarin.AspectComparison.meiyou.hanzi = "没有" ∧ Fragments.Mandarin.AspectComparison.meiyou.pinyin = "méi-yǒu"

Mandarin méi-yǒu connects to AspectComparison: the same particle is formalized as a cross-domain negative perfective there.

theorem Miestamo2005.english_fragment_confirms_symasy : (List.filter (fun (x : Fragments.English.Negation.NegExample) => x.symmetric) Fragments.English.Negation.allExamples).length = 3 ∧ (List.filter (fun (e : Fragments.English.Negation.NegExample) => !e.symmetric) Fragments.English.Negation.allExamples).length = 2 ∧ (english.symmetry == Typology.Negation.NegSymmetry.both) = true

English Fragment confirms SymAsy: 3 symmetric (modal, copula, aux have)

• 2 asymmetric (lexical verb with do-support).

theorem Miestamo2005.english_dosupport_is_asymmetry : (Fragments.English.Negation.allExamples.all fun (e : Fragments.English.Negation.NegExample) => e.symmetric == !e.doSupport) = true

English do-support is exactly the asymmetric constructions.

theorem Miestamo2005.russian_fragment_confirms_symmetric : Fragments.Slavic.Russian.Negation.allExamples.length = 4 ∧ russian.asymmetryDimensions.isEmpty = true

Russian Fragment confirms symmetric: all constructions available, не adds negation without structural change.

theorem Miestamo2005.russian_concord_confirms_cooccur : (Fragments.Slavic.Russian.Negation.allConcordExamples.all fun (e : Fragments.Slavic.Russian.Negation.NegConcordExample) => decide ((e.sentence.splitOn "не").length > 1)) = true

Russian negative concord: all n-words co-occur with не.

theorem Miestamo2005.czech_fragment_confirms_symmetric : Fragments.Slavic.Czech.Negation.allExamples.length = 4 ∧ czech.asymmetryDimensions.isEmpty = true

Czech Fragment confirms symmetric: all constructions available, prefix ne- adds negation without structural change.

theorem Miestamo2005.czech_concord_confirms_cooccur : (Fragments.Slavic.Czech.Negation.allConcordExamples.all fun (e : Fragments.Slavic.Czech.Negation.NegConcordExample) => decide ((e.sentence.splitOn "ne").length > 1)) = true

Czech negative concord: all n-words co-occur with ne- prefix.

theorem Miestamo2005.maori_fragment_confirms_asymmetric : (Fragments.Maori.Negation.allExamples.all fun (e : Fragments.Maori.Negation.NegExample) => !e.symmetric) = true ∧ maori.asymmetryDimensions.contains AsymmetryDimension.constructional = true

Maori Fragment confirms asymmetric: all constructions are A/Fin.

theorem Miestamo2005.hixkaryana_fragment_confirms_asymmetric : (Fragments.Hixkaryana.Negation.allExamples.all fun (e : Fragments.Hixkaryana.Negation.NegExample) => !e.symmetric) = true ∧ (Fragments.Hixkaryana.Negation.allExamples.all fun (x : Fragments.Hixkaryana.Negation.NegExample) => x.copulaFinite) = true ∧ hixkaryana.asymmetryDimensions.contains AsymmetryDimension.constructional = true

Hixkaryana Fragment confirms asymmetric A/Fin with copula finite.

theorem Miestamo2005.imbaburaQuechua_fragment_confirms_symasy : (List.filter (fun (x : Fragments.Quechua.Negation.NegExample) => x.symmetric) Fragments.Quechua.Negation.allExamples).length = 1 ∧ (List.filter (fun (e : Fragments.Quechua.Negation.NegExample) => !e.symmetric) Fragments.Quechua.Negation.allExamples).length = 2 ∧ (imbaburaQuechua.symmetry == Typology.Negation.NegSymmetry.both) = true

Imbabura Quechua Fragment confirms SymAsy: 1 symmetric + 2 asymmetric constructions, with asymmetric = requiring -chu.

theorem Miestamo2005.imbaburaQuechua_chu_is_asymmetry : (Fragments.Quechua.Negation.allExamples.all fun (e : Fragments.Quechua.Negation.NegExample) => e.symmetric == !e.requiresChu) = true

Imbabura Quechua: -chu requirement is exactly the asymmetric constructions.

theorem Miestamo2005.sample_size : allData.length = 15

theorem Miestamo2005.symmetric_count : (List.filter (fun (x : MiestamoDatum) => x.symmetry == Typology.Negation.NegSymmetry.symmetric) allData).length = 6

theorem Miestamo2005.asymmetric_count : (List.filter (fun (x : MiestamoDatum) => x.symmetry == Typology.Negation.NegSymmetry.asymmetric) allData).length = 5

theorem Miestamo2005.symasy_count : (List.filter (fun (x : MiestamoDatum) => x.symmetry == Typology.Negation.NegSymmetry.both) allData).length = 4

theorem Miestamo2005.constructional_count : (List.filter (fun (d : MiestamoDatum) => d.asymmetryDimensions.contains AsymmetryDimension.constructional) allData).length = 7

theorem Miestamo2005.paradigmatic_count : (List.filter (fun (d : MiestamoDatum) => d.asymmetryDimensions.contains AsymmetryDimension.paradigmatic) allData).length = 4

theorem Miestamo2005.both_dimensions_count : (List.filter (fun (d : MiestamoDatum) => d.asymmetryDimensions.contains AsymmetryDimension.constructional && d.asymmetryDimensions.contains AsymmetryDimension.paradigmatic) allData).length = 2

theorem Miestamo2005.derived_count : (List.filter (fun (x : MiestamoDatum) => x.asymmetrySource == some AsymmetrySource.derived) allData).length = 2

theorem Miestamo2005.independent_count : (List.filter (fun (x : MiestamoDatum) => x.asymmetrySource == some AsymmetrySource.independent) allData).length = 7

structure Miestamo2005.SurveyDistribution : Type

Distribution from @cite{miestamo-2005}'s 179-language representative sample (RS). These are the headline empirical results of Ch 4's typological survey. Note: the WALS Ch 113 sample (also by Miestamo) covers 297 languages with different numbers; those are captured separately in Typology.lean via Data.WALS.F113A.

• totalLanguages : ℕ
• symmetricOnly : ℕ
• asymmetricOnly : ℕ
• symAsy : ℕ
• complete : self.symmetricOnly + self.asymmetricOnly + self.symAsy = self.totalLanguages

  Proportion check: parts sum to whole.

@[implicit_reducible]

instance Miestamo2005.instReprSurveyDistribution : Repr SurveyDistribution

Equations

• Miestamo2005.instReprSurveyDistribution = { reprPrec := Miestamo2005.instReprSurveyDistribution.repr }

def Miestamo2005.instReprSurveyDistribution.repr : SurveyDistribution → ℕ → Std.Format

Equations

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

def Miestamo2005.miestamo179 : SurveyDistribution

The 179-language RS distribution from @cite{miestamo-2005} Table 3 (p. 171). Sym = 72 (40%), SymAsy = 76 (42%), Asy = 31 (17%).

Equations

• Miestamo2005.miestamo179 = { totalLanguages := 179, symmetricOnly := 72, asymmetricOnly := 31, symAsy := 76, complete := Miestamo2005.miestamo179._proof_2 }

theorem Miestamo2005.symasy_plurality : miestamo179.symAsy > miestamo179.symmetricOnly ∧ miestamo179.symAsy > miestamo179.asymmetricOnly

SymAsy is the most common type in the RS (76 > 72 > 31). @cite{miestamo-2005} Table 3 (p. 171).

theorem Miestamo2005.asymmetric_minority : miestamo179.asymmetricOnly < miestamo179.symmetricOnly ∧ miestamo179.asymmetricOnly < miestamo179.symAsy

Purely asymmetric negation (type Asy) is the least common type. @cite{miestamo-2005} p. 171: "symmetric negation is more common in the world's languages than asymmetric negation."

theorem Miestamo2005.symmetric_constructions_common : miestamo179.symmetricOnly + miestamo179.symAsy > miestamo179.asymmetricOnly

Languages with any symmetric construction (S column in Table 3: Sym + SymAsy = 148, 83%) greatly outnumber purely asymmetric.

structure Miestamo2005.SubtypeDistribution : Type

Asymmetry subtype frequencies from @cite{miestamo-2005} Table 5 (p. 173). A/Cat is most common, A/Emph least common. Frequency order: A/Cat (59) > A/Fin (45) > A/NonReal (23) > A/Emph (4).

• aFin : ℕ
• aNonReal : ℕ
• aEmph : ℕ
• aCat : ℕ

@[implicit_reducible]

instance Miestamo2005.instReprSubtypeDistribution : Repr SubtypeDistribution

Equations

• Miestamo2005.instReprSubtypeDistribution = { reprPrec := Miestamo2005.instReprSubtypeDistribution.repr }

def Miestamo2005.instReprSubtypeDistribution.repr : SubtypeDistribution → ℕ → Std.Format

Equations

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

def Miestamo2005.subtypeDist : SubtypeDistribution

Table 5 totals (across SymAsy + Asy). Languages can show multiple subtypes, so these sum to more than 107.

Equations

• Miestamo2005.subtypeDist = { aFin := 45, aNonReal := 23, aEmph := 4, aCat := 59 }

theorem Miestamo2005.acat_most_common : subtypeDist.aCat > subtypeDist.aFin

theorem Miestamo2005.aemph_least_common : subtypeDist.aEmph < subtypeDist.aNonReal ∧ subtypeDist.aEmph < subtypeDist.aFin ∧ subtypeDist.aEmph < subtypeDist.aCat

theorem Miestamo2005.anonreal_implies_paradigmatic : ((List.filter (fun (d : MiestamoDatum) => d.asymmetrySubtype == Typology.Negation.AsymmetrySubtype.realityStatus || d.asymmetrySubtype == Typology.Negation.AsymmetrySubtype.finAndNonReal || d.asymmetrySubtype == Typology.Negation.AsymmetrySubtype.nonRealAndCat) allData).all fun (d : MiestamoDatum) => d.asymmetryDimensions.contains AsymmetryDimension.paradigmatic) = true

A/NonReal asymmetry is always paradigmatic, never constructional. The irrealis category is a paradigmatic distinction (a new cell in the paradigm), not a structural restructuring of the clause.

theorem Miestamo2005.anonreal_never_constructional : ((List.filter (fun (d : MiestamoDatum) => d.asymmetrySubtype == Typology.Negation.AsymmetrySubtype.realityStatus) allData).all fun (d : MiestamoDatum) => !d.asymmetryDimensions.contains AsymmetryDimension.constructional) = true

A/NonReal asymmetry in our sample is never constructional. Note: this is a sample limitation (we have only 1 A/NonReal language). @cite{miestamo-2005} (p. 96) reports that "both constructional and paradigmatic asymmetry is commonly found in type A/NonReal", with 8 of 23 A/NonReal languages showing constructional asymmetry (Table 5).

theorem Miestamo2005.symmetric_no_paradigmatic : ((List.filter (fun (x : MiestamoDatum) => x.symmetry == Typology.Negation.NegSymmetry.symmetric) allData).all fun (d : MiestamoDatum) => !d.asymmetryDimensions.contains AsymmetryDimension.paradigmatic) = true

Symmetric-only negation never has paradigmatic asymmetry. By definition: if the paradigm is unchanged, negation is symmetric.

theorem Miestamo2005.verbal_constructional_always_derived : ((List.filter (fun (d : MiestamoDatum) => d.morphemeType == Typology.Negation.NegMorphemeType.auxVerb && d.asymmetryDimensions.contains AsymmetryDimension.constructional) allData).all fun (d : MiestamoDatum) => d.asymmetrySource == some AsymmetrySource.derived) = true

Constructional asymmetry with a verbal negator is always derived: a verb-type negator structurally entails finiteness restructuring, so the asymmetry follows from the marker's properties.

theorem Miestamo2005.finnish_neg_aux_cross_module : (Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.finnish.strategy == Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.NegStrategy.negVerb) = true ∧ (finnish.morphemeType == Typology.Negation.NegMorphemeType.auxVerb) = true

Finnish is classified as negVerb in the auxiliary literature and as auxVerb in the negation typology. These refer to the same phenomenon: the negative element is an inflecting auxiliary verb.

theorem Miestamo2005.finnish_strategy_morpheme_consistent : Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.NegStrategy.negVerb.toNegMorphemeType = finnish.morphemeType

The NegStrategy→NegMorphemeType mapping is consistent with Finnish's classification in both modules.

theorem Miestamo2005.neg_verb_implies_avc_and_afin : Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.NegStrategy.negVerb.isVerbal = true ∧ finnish.asymmetryDimensions.contains AsymmetryDimension.constructional = true ∧ (finnish.asymmetrySource == some AsymmetrySource.derived) = true

Verbal negation strategy always implies constructional asymmetry in both the auxiliary literature (creates an AVC) and the negation typology (derived A/Fin).