Dryer (2013): WALS chapters on negation morpheme + word-order (112A, 143A, 144A)

@cite{dryer-2013-wals} @cite{wals-2013}

WALS chapters by Matthew S. Dryer covering negation typology:

• Ch 112A: Negative Morphemes
• Ch 143A: Order of Negative Morpheme and Verb
• Ch 144A: Position of Negative Word with Respect to Subject, Object, Verb

Per the project's "WALS goes to Linglib/Typology/" rule, the WALS aggregate distributions live in the substrate (Linglib/Typology/Negation.lean). This study file holds cross-linguistic generalisations that consume the Fragment-side negationProfile data with non-trivial semantic content (bipartite_implies_asymmetric, aux_verb_implies_afin, etc.).

Per-language Fragment-vs-WALS data-equality theorems are deliberately absent: Fragments.{Lang}.Negation.negationProfile already encodes the typed value at definition site, and verifying it equals Data.WALS.lookup "iso" is "encoding conclusions as definitions" — the two would have to diverge for the theorem to fail, and the substrate's NegationSystem.ofISO already populates from the same WALS source.

Ch 113-115 (Miestamo's symmetric/asymmetric chapters) are grounded in Studies/Miestamo2005.lean.

def Phenomena.Negation.Studies.Dryer2013.allLanguages : List Typology.Negation.NegationProfile

The 15-language sample drawn from per-language Fragment Negation files. Sample shrunk from the dissolved file's 19 (dropped Izi, KolymaYukaghir, Rama, Nelemwa — none of which had Fragment files in the project).

Equations

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

theorem Phenomena.Negation.Studies.Dryer2013.sample_size : allLanguages.length = 15

Sample size.

theorem Phenomena.Negation.Studies.Dryer2013.sample_affix_count : Typology.Negation.countByMorphemeType allLanguages Typology.Negation.NegMorphemeType.affix = 4

Morpheme type distribution in the sample.

theorem Phenomena.Negation.Studies.Dryer2013.sample_particle_count : Typology.Negation.countByMorphemeType allLanguages Typology.Negation.NegMorphemeType.particle = 8

theorem Phenomena.Negation.Studies.Dryer2013.sample_auxverb_count : Typology.Negation.countByMorphemeType allLanguages Typology.Negation.NegMorphemeType.auxVerb = 1

theorem Phenomena.Negation.Studies.Dryer2013.sample_double_count : Typology.Negation.countByMorphemeType allLanguages Typology.Negation.NegMorphemeType.doubleNeg = 1

theorem Phenomena.Negation.Studies.Dryer2013.sample_unclear_count : Typology.Negation.countByMorphemeType allLanguages Typology.Negation.NegMorphemeType.wordUnclear = 1

theorem Phenomena.Negation.Studies.Dryer2013.sample_variation_count : Typology.Negation.countByMorphemeType allLanguages Typology.Negation.NegMorphemeType.variation = 0

theorem Phenomena.Negation.Studies.Dryer2013.sample_symmetry_counts : Typology.Negation.countBySymmetry allLanguages Typology.Negation.NegSymmetry.symmetric = 6 ∧ Typology.Negation.countBySymmetry allLanguages Typology.Negation.NegSymmetry.asymmetric = 5 ∧ Typology.Negation.countBySymmetry allLanguages Typology.Negation.NegSymmetry.both = 4

Symmetry distribution in the sample.

theorem Phenomena.Negation.Studies.Dryer2013.bipartite_implies_asymmetric : have bipartite := List.filter (fun (x : Typology.Negation.NegationProfile) => x.hasMorphemeType Typology.Negation.NegMorphemeType.doubleNeg) allLanguages; (bipartite.all fun (x : Typology.Negation.NegationProfile) => x.hasAsymmetric) = true

In the sample, every language with bipartite ("double") negation morphemes has asymmetric negation. If negation requires two markers whose placement changes the clause structure, the negative clause structurally differs from the affirmative.

theorem Phenomena.Negation.Studies.Dryer2013.symmetric_implies_nonassignable : have symmetric := List.filter (fun (x : Typology.Negation.NegationProfile) => x.symmetry == Typology.Negation.NegSymmetry.symmetric) allLanguages; (symmetric.all fun (x : Typology.Negation.NegationProfile) => x.asymmetrySubtype == Typology.Negation.AsymmetrySubtype.nonAssignable) = true

In the sample, every language classified as symmetric-only (Ch 113) has a non-assignable asymmetry subtype (Ch 114).

theorem Phenomena.Negation.Studies.Dryer2013.asymmetric_implies_assignable : have asymmetric := List.filter (fun (x : Typology.Negation.NegationProfile) => x.hasAsymmetric) allLanguages; (asymmetric.all fun (x : Typology.Negation.NegationProfile) => x.asymmetrySubtype != Typology.Negation.AsymmetrySubtype.nonAssignable) = true

In the sample, no language classified as asymmetric or both has a non-assignable subtype.

theorem Phenomena.Negation.Studies.Dryer2013.aux_verb_implies_afin : have auxLangs := List.filter (fun (x : Typology.Negation.NegationProfile) => x.hasMorphemeType Typology.Negation.NegMorphemeType.auxVerb) allLanguages; (auxLangs.all fun (x : Typology.Negation.NegationProfile) => x.asymmetrySubtype == Typology.Negation.AsymmetrySubtype.finiteness) = true

Negative auxiliary verbs (Ch 112) are always associated with asymmetric negation of subtype A/Fin: the auxiliary becomes the finite element, and the lexical verb is deficitized. Finnish illustrates this perfectly.

theorem Phenomena.Negation.Studies.Dryer2013.slavic_neg_concord : Fragments.Slavic.Russian.Negation.negationProfile.hasNegConcord = true ∧ Fragments.Slavic.Czech.Negation.negationProfile.hasNegConcord = true

All Slavic languages in the sample (Russian, Czech) show negative concord.