Miestamo (2005): Standard Negation

[Mie05]

[Mie05] refines the WALS symmetric/asymmetric classification (Ch 113-114) with the orthogonal distinction between constructional and paradigmatic asymmetry:

• Constructional: the structure of the negative clause differs from the affirmative beyond adding the negation marker — added finite elements (Finnish neg aux + connegative, A/Fin) and marker replacement (Turkish aorist -(I)r → -z; replacement asymmetry is constructional A/Cat).

• Paradigmatic: the paradigm of available distinctions differs in the negative — neutralization (Burmese -bu collapses three TAM distinctions to one; English negatives lack the periphrastic emphatic, A/Emph/Neutr) or displacement (Imbabura Quechua negatives require the validator -chu, A/NonReal/Displc).

The dimensions are orthogonal: Finnish is constructional-only, Imbabura Quechua paradigmatic-only, Burmese both.

Derived vs independent asymmetry

When a language shows multiple asymmetries, one may be derived from another rather than being a direct consequence of negation: Maung's TAM neutralization follows from its obligatory irrealis-marking (A/NonReal), and Imbabura Quechua's ban on other validators follows from the A/NonReal validator -chu. Derivedness relates asymmetries to each other, not asymmetries to marker types; it is noted in datum docstrings where relevant rather than carried as a field (no sample language here has an independent multiple asymmetry).

WALS consistency

Datum codings follow the book's Appendix III analyses. They agree with the (later, same-author) WALS Ch 112A-114A codings for every sample language except English: the book analyses English SN as symmetric AUX+not with paradigmatic A/Emph/Neutr asymmetry, where WALS Ch 114A codes English A/Cat (english_subtype_diverges_from_wals). Czech is absent from the book's sample and from WALS Ch 113A-115A; its datum applies the book's criteria.

Quantitative data

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

Miestamo's asymmetry dimensions (beyond WALS)

inductive Miestamo2005.AsymmetryDimension : Type

[Mie05]'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 differs structurally from the affirmative beyond the negation marker: added finite elements (A/Fin) or marker replacement (replacement asymmetry is constructional A/Cat).

• paradigmatic : AsymmetryDimension

  The negative paradigm makes different formal distinctions than the affirmative: neutralization (Burmese TAM, English A/Emph) or displacement (Quechua validators).

@[instance_reducible]

instance Miestamo2005.instDecidableEqAsymmetryDimension : DecidableEq AsymmetryDimension

Equations

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

@[instance_reducible]

instance Miestamo2005.instBEqAsymmetryDimension : BEq AsymmetryDimension

Equations

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

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

Equations

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

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

Equations

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

@[instance_reducible]

instance Miestamo2005.instReprAsymmetryDimension : Repr AsymmetryDimension

Equations

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

Datum

structure Miestamo2005.MiestamoDatum : Type

A Miestamo-style negation datum: the WALS-chapter classification plus the book's constructional/paradigmatic dimension coding (Appendix III).

• language : String
• iso : String

  ISO 639-3 code; the key for the WALS-consistency checks.

• morphemeType : Syntax.Negation.NegMorphemeType

  WALS Ch 112: morpheme type

• symmetry : Syntax.Negation.NegSymmetry

  WALS Ch 113: symmetric/asymmetric/both

• asymmetrySubtype : Syntax.Negation.AsymmetrySubtype

  WALS Ch 114: asymmetry subtype

• asymmetryDimensions : List AsymmetryDimension

  Which dimensions of asymmetry are present (Appendix III C/P columns)

• negMarkers : List String

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

• asymmetryDescription : String

  Brief description of the asymmetry (if any)

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

Equations

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

@[instance_reducible]

instance Miestamo2005.instReprMiestamoDatum : Repr MiestamoDatum

Equations

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

@[instance_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

Per-language data (Fragment-derived where possible)

Codings follow the book's Appendix III rows; deviations from WALS or gaps in the book's sample are flagged in the datum docstrings.

def Miestamo2005.finnish : MiestamoDatum

Finnish: constructional A/Fin/NegVerb. The negative auxiliary is the finite element; the lexical verb appears as a nonfinite connegative. Forms derived from Finnish.Negation.negParadigm.

Equations

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

def Miestamo2005.german : MiestamoDatum

German: symmetric. Particle nicht. Form derived from German.Negation.nicht.form.

Equations

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

def Miestamo2005.japanese : MiestamoDatum

Japanese: constructional A/Fin + A/Cat. Plain -nai adjectivalizes the verb (A/Fin/Neg-LV); the polite nonpast replaces TAM material (A/Cat/TAM); the polite past adds a finite element. Appendix III codes all three constructions as constructional, with no paradigmatic row. Form derived from Japanese.Negation.negSuffix.form.

Equations

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

def Miestamo2005.turkish : MiestamoDatum

Turkish: SymAsy with constructional A/Cat/TAM in the aorist only. The aorist suffix changes to -z in the 2nd/3rd persons and is omitted in the 1st (Appendix II ex. 260); negation is symmetric elsewhere. Form derived from 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 French.Negation.

Equations

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

def Miestamo2005.burmese : MiestamoDatum

Burmese: constructional + paradigmatic A/Cat, in one construction (Appendix III type B): the circumfix replaces the TAM slot and neutralizes the actual/potential distinction (A/Cat/TAM/Neutr). Forms derived from 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 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 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 (A/Fin/Neg-FE); when méi occurs without yǒu, it functions as a negative existential verb (A/Fin/NegVerb). [Mie05] pp. 90-91, example (51). Forms derived from Mandarin.Negation.

Equations

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

def Miestamo2005.english : MiestamoDatum

English: SymAsy with paradigmatic A/Emph/Neutr. Appendix III codes AUX+not as symmetric (with do as the finite AUX host) and locates the asymmetry in the paradigm: the periphrastic emphatic (I DO eat) is unavailable in negatives. WALS Ch 114A instead codes English A/Cat; see english_subtype_diverges_from_wals. Form derived from 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 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. Not in the book's RS (nor the WALS Ch 113A-115A samples); coded here by applying the book's criteria to symmetric ne- prefixation. Form derived from Czech.Negation.negPrefix.

Equations

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

def Miestamo2005.maori : MiestamoDatum

Maori: constructional A/Fin/NegVerb. Kāhore is the finite element and the lexical clause is subordinated. WALS Ch 112A codes the morpheme type as wordUnclear. Form derived from 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/Neg-LV. Suffix -hɨra deverbalizes the verb; a copula becomes the finite element. Form derived from 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/Displc. Mana constructions are symmetric; negatives require the validator enclitic -chu, which also marks interrogatives. Since only one validator may occur per sentence, the further ban on other validators is an asymmetry the book classifies as derived from this one (p. 158). Form derived from 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.

WALS consistency

The book's codings against the (later, same-author) WALS chapter rows, read via the Syntax.Negation per-ISO accessors. Languages absent from a chapter's WALS sample (Czech throughout) pass vacuously.

theorem Miestamo2005.morphemeType_matches_wals : (allData.all fun (d : MiestamoDatum) => Option.all (fun (x : Syntax.Negation.NegMorphemeType) => x == d.morphemeType) (Syntax.Negation.morphemeTypeOfISO d.iso)) = true

Datum morpheme types agree with WALS Ch 112A wherever coded. (Scoped maxRecDepth: kernel evaluation recurses through the 1157-row Ch 112A table.)

theorem Miestamo2005.symmetry_matches_wals : (allData.all fun (d : MiestamoDatum) => Option.all (fun (x : Syntax.Negation.NegSymmetry) => x == d.symmetry) (Syntax.Negation.symmetryOfISO d.iso)) = true

Datum symmetry codings agree with WALS Ch 113A wherever coded.

theorem Miestamo2005.subtype_matches_wals_except_english : (allData.all fun (d : MiestamoDatum) => d.language == "English" || Option.all (fun (x : Syntax.Negation.AsymmetrySubtype) => x == d.asymmetrySubtype) (Syntax.Negation.asymmetrySubtypeOfISO d.iso)) = true

Datum subtype codings agree with WALS Ch 114A wherever coded — except English, where the book's A/Emph analysis diverges from WALS's A/Cat.

theorem Miestamo2005.english_subtype_diverges_from_wals : english.asymmetrySubtype = Syntax.Negation.AsymmetrySubtype.emphasis ∧ Syntax.Negation.asymmetrySubtypeOfISO english.iso = some Syntax.Negation.AsymmetrySubtype.otherCategories

The book vs WALS on English: Appendix III codes English SN as symmetric AUX+not with paradigmatic A/Emph/Neutr asymmetry; WALS Ch 114A codes English A/Cat.

Structural sanity of the coding

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

Symmetric languages have no asymmetry dimensions.

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

Asymmetric languages have at least one asymmetry dimension.

theorem Miestamo2005.symasy_has_dimensions : ((List.filter (fun (x : MiestamoDatum) => x.symmetry == Syntax.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.symmetric_implies_nonassignable : ((List.filter (fun (x : MiestamoDatum) => x.symmetry == Syntax.Negation.NegSymmetry.symmetric) allData).all fun (d : MiestamoDatum) => d.asymmetrySubtype == Syntax.Negation.AsymmetrySubtype.nonAssignable) = true

Symmetric-only (WALS) implies nonAssignable asymmetry subtype.

theorem Miestamo2005.afin_verbal_implies_constructional : ((List.filter (fun (d : MiestamoDatum) => (d.asymmetrySubtype == Syntax.Negation.AsymmetrySubtype.finiteness || d.asymmetrySubtype == Syntax.Negation.AsymmetrySubtype.finAndCat || d.asymmetrySubtype == Syntax.Negation.AsymmetrySubtype.finAndNonReal) && d.morphemeType == Syntax.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 == Syntax.Negation.AsymmetrySubtype.finiteness || d.asymmetrySubtype == Syntax.Negation.AsymmetrySubtype.finAndCat || d.asymmetrySubtype == Syntax.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 — matching Table 5, where A/Fin is constructional in 44 of 45 RS languages.

Theoretical predictions

theorem Miestamo2005.symmetric_particles_no_dimensions : ((List.filter (fun (d : MiestamoDatum) => d.morphemeType == Syntax.Negation.NegMorphemeType.particle && d.symmetry == Syntax.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 asymmetry elsewhere (méi(yǒu) introduces A/Fin; the emphatic paradigm is neutralized).

theorem Miestamo2005.affixes_variable : List.map (fun (x : MiestamoDatum) => x.symmetry) (List.filter (fun (x : MiestamoDatum) => x.morphemeType == Syntax.Negation.NegMorphemeType.affix) allData) = [Syntax.Negation.NegSymmetry.asymmetric, Syntax.Negation.NegSymmetry.both, Syntax.Negation.NegSymmetry.symmetric, Syntax.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_constructional_only : turkish.asymmetryDimensions = [AsymmetryDimension.constructional]

Turkish has constructional-only asymmetry: the aorist marker is replaced (or omitted), but no distinctions are neutralized.

theorem Miestamo2005.quechua_paradigmatic_only : imbaburaQuechua.asymmetryDimensions = [AsymmetryDimension.paradigmatic]

Imbabura Quechua has paradigmatic-only asymmetry: the validator requirement changes the paradigm, not the clause structure.

Fragment cross-validation

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

Japanese Fragment distribution shows the tense shift from stem to suffix that Appendix III codes as constructional replacement (A/Cat/TAM) alongside the A/Fin adjectivalization.

theorem Miestamo2005.turkish_fragment_confirms_symasy : List.map (fun (x : Turkish.Negation.NegParadigmEntry) => x.formLabel) (List.filter (fun (e : Turkish.Negation.NegParadigmEntry) => !e.symmetric) Turkish.Negation.gelParadigm) = ["aorist"] ∧ (turkish.symmetry == Syntax.Negation.NegSymmetry.both) = true

Turkish Fragment confirms SymAsy: the aorist is the only asymmetric construction in the gelmek paradigm.

theorem Miestamo2005.burmese_fragment_confirms_paradigmatic : Burmese.Negation.burmeseTAM.affirmativeTAM.length = 3 ∧ 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.mandarin_fragment_confirms_symasy : (Mandarin.Negation.allExamples.any fun (x : Mandarin.Negation.NegExample) => x.symmetric) = true ∧ (Mandarin.Negation.allExamples.any fun (e : Mandarin.Negation.NegExample) => !e.symmetric) = true ∧ (mandarin.symmetry == Syntax.Negation.NegSymmetry.both) = true

Mandarin Fragment confirms SymAsy: the example set contains both symmetric (bù) and asymmetric (méi) constructions.

theorem Miestamo2005.mandarin_meiyou_cross_module : Mandarin.AspectComparison.meiyou.hanzi = "没有" ∧ 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_dosupport_is_asymmetry : (English.Negation.allExamples.all fun (e : English.Negation.NegExample) => e.symmetric == !e.doSupport) = true

English do-support is exactly the asymmetric constructions in the Fragment's construction-level coding. The book instead treats AUX+not as symmetric and locates English asymmetry in the emphatic paradigm (see english); the fragment fact is stable under either construal.

theorem Miestamo2005.maori_fragment_confirms_asymmetric : (Maori.Negation.allExamples.all fun (e : 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 : (Hixkaryana.Negation.allExamples.all fun (e : Hixkaryana.Negation.NegExample) => !e.symmetric) = true ∧ (Hixkaryana.Negation.allExamples.all fun (x : Hixkaryana.Negation.NegExample) => x.copulaFinite) = true ∧ hixkaryana.asymmetryDimensions.contains AsymmetryDimension.constructional = true

Hixkaryana Fragment confirms asymmetric A/Fin with copula finite.

theorem Miestamo2005.imbaburaQuechua_chu_is_asymmetry : (Quechua.Negation.allExamples.any fun (x : Quechua.Negation.NegExample) => x.symmetric) = true ∧ (Quechua.Negation.allExamples.all fun (e : Quechua.Negation.NegExample) => e.symmetric == !e.requiresChu) = true ∧ (imbaburaQuechua.symmetry == Syntax.Negation.NegSymmetry.both) = true

Imbabura Quechua Fragment confirms SymAsy, with the -chu requirement marking exactly the asymmetric constructions.

Miestamo's 179-language survey distribution (Table 3)

structure Miestamo2005.SurveyDistribution : Type

Distribution from [Mie05]'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 via Data.WALS.F113A.

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

  Proportion check: parts sum to whole.

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

Equations

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

@[instance_reducible]

instance Miestamo2005.instReprSurveyDistribution : Repr SurveyDistribution

Equations

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

def Miestamo2005.miestamo179 : SurveyDistribution

The 179-language RS distribution from [Mie05] 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). [Mie05] 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. [Mie05] 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 [Mie05] 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 : ℕ

@[instance_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

Implicational universals

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

A/NonReal asymmetry in our sample is paradigmatic.

theorem Miestamo2005.anonreal_never_constructional : ((List.filter (fun (d : MiestamoDatum) => d.asymmetrySubtype == Syntax.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). [Mie05] (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 == Syntax.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.

Bridge to auxiliary verb literature

theorem Miestamo2005.finnish_strategy_morpheme_consistent : Syntax.Negation.NegStrategy.negVerb.toNegMorphemeType = finnish.morphemeType

The NegStrategy→NegMorphemeType mapping is consistent with Finnish's classification: the auxiliary literature's negVerb strategy and this study's auxVerb morpheme type refer to the same phenomenon — the negative element is an inflecting auxiliary verb.

theorem Miestamo2005.neg_verb_implies_avc_and_afin : Syntax.Negation.NegStrategy.negVerb.isVerbal = true ∧ finnish.asymmetryDimensions.contains AsymmetryDimension.constructional = true

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