Documentation

Linglib.Typology.Negation

Typology.Negation #

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

Per-language typological substrate for the standard sentential negation marker of a language: form, morphological status, position, symmetric/ asymmetric status, asymmetry subtype, and negative-indefinite strategy.

Mirrors the Linglib/Typology/Possession.lean (Possession), Question.lean (Question), and Case.lean (Case) substrate-extension pattern: the substrate carries (a) per-paradigm-entry schema (NegMarkerEntry, NegationSystem), (b) the WALS-bundled per-language NegationProfile, (c) WALS converters and aggregate-distribution helpers / theorems.

What lives here #

NegMorphemeType — direct projection from WALS Ch 112A's 6-way classification (negativeAffix, negativeParticle, negativeAuxiliaryVerb, negativeWordUnclearIfVerbOrParticle, variationBetweenNegativeWordAndAffix, doubleNegation). This is Dryer's WALS Ch 112 morpheme typology, NOT @cite{miestamo-2005}'s construction-level typology — Miestamo classifies constructions, not morphemes. The substrate carries Dryer's classification for cross-linguistic indexing; Miestamo's framework lives in Studies/Miestamo2005.lean.
NegMarkerPosition — coarsening of WALS Ch 144A.
NegMarkerEntry — one language's standard sentential negation marker.
NegationSystem — bundles markers + WALS Ch 112A/143A/144A datapoints. The Fragment-side joint: every Fragments/{Lang}/Negation.lean exposes def negationSystem : NegationSystem.
NegSymmetry, AsymmetrySubtype, NegIndefiniteStrategy, NegVerbPosition, NegMorphemePosition — WALS Ch 113-115/143A feature enums.
NegationProfile — sibling per-language schema bundling Ch 112-115 + Greco's negIsHead + JinKoenig's enAttested. Each Fragment exposes def negationProfile : NegationProfile alongside def negationSystem. Sibling pattern (mirrors Typology/Possession.lean::PossessionProfile): the marker-side joint is independent from the typology-feature joint.
fromWALS112A/113A/114A/115A/143A converters.
WALS aggregate distribution theorems for Ch 112-115/143A/144A core.

Theory-laden caveats #

NegSymmetry and AsymmetrySubtype are WALS Ch 113/114 values (@cite{dryer-haspelmath-2013}). @cite{miestamo-2005}'s richer two-dimension framework (constructional vs paradigmatic asymmetry, derived vs independent source) lives in Studies/Miestamo2005.lean because it goes beyond what WALS encodes.

Out of scope #

Polarity-sensitive items (n-words, NPIs, FCIs) are NOT marker-side data; they live in Typology/PolarityItem.lean and in each language's Fragments/{Lang}/PolarityItems.lean. Cross-linguistic theorems consuming Fragment per-language data live in Phenomena/Negation/Studies/Dryer2013.lean (Ch 112/143A/144A grounding) and Studies/Miestamo2005.lean (Ch 113-115 grounding).

inductive Typology.Negation.NegMorphemeType :

Type of the standard negation morpheme @cite{dryer-2013-wals}.

Six categories anchored on WALS Ch 112A (negative morpheme classification). Direct projection from Data.WALS.F112A.NegativeMorphemeType via ofWALS112A; the substrate enum exists for ergonomic pattern-matching in Fragment files.

affix : NegMorphemeType
Negative affix on the verb (e.g., Kolyma Yukaghir el-jaqa-te-je 'NEG-achieve-FUT-1SG').
particle : NegMorphemeType
Free negative particle, no verbal inflection (e.g., English not, Italian non).
auxVerb : NegMorphemeType
Negative auxiliary verb inflecting for verbal categories (e.g., Finnish e-n 'NEG-1SG').
wordUnclear : NegMorphemeType
Negative word whose status as verb or particle is unclear, typically in isolating languages (e.g., Maori kaahore).
variation : NegMorphemeType
Language uses both negative word and negative affix in different constructions (e.g., Rama).
doubleNeg : NegMorphemeType
Bipartite negation: two co-occurring morphemes flanking the verb (e.g., French ne...pas, Izi to-...-du).

Instances For

@[implicit_reducible]

instance Typology.Negation.instDecidableEqNegMorphemeType :

DecidableEq NegMorphemeType

Equations

Typology.Negation.instDecidableEqNegMorphemeType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Typology.Negation.instBEqNegMorphemeType.beq :

NegMorphemeType → NegMorphemeType → Bool

Equations

Typology.Negation.instBEqNegMorphemeType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

@[implicit_reducible]

instance Typology.Negation.instBEqNegMorphemeType :

BEq NegMorphemeType

Equations

Typology.Negation.instBEqNegMorphemeType = { beq := Typology.Negation.instBEqNegMorphemeType.beq }

@[implicit_reducible]

instance Typology.Negation.instReprNegMorphemeType :

Repr NegMorphemeType

Equations

Typology.Negation.instReprNegMorphemeType = { reprPrec := Typology.Negation.instReprNegMorphemeType.repr }

def Typology.Negation.instReprNegMorphemeType.repr :

NegMorphemeType → Nat → Std.Format

Equations

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

Instances For

inductive Typology.Negation.NegMarkerPosition :

Position of the negation morpheme relative to the verb.

One-way coarsening of WALS Ch 144A's full S/O/V grid. The wals144A field on NegationSystem preserves the precise WALS classification for callers that need decoarsening.

preverbal : NegMarkerPosition
postverbal : NegMarkerPosition
discontinuous : NegMarkerPosition
morphological : NegMarkerPosition
other : NegMarkerPosition

Instances For

@[implicit_reducible]

instance Typology.Negation.instDecidableEqNegMarkerPosition :

DecidableEq NegMarkerPosition

Equations

Typology.Negation.instDecidableEqNegMarkerPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Typology.Negation.instBEqNegMarkerPosition :

BEq NegMarkerPosition

Equations

Typology.Negation.instBEqNegMarkerPosition = { beq := Typology.Negation.instBEqNegMarkerPosition.beq }

def Typology.Negation.instBEqNegMarkerPosition.beq :

NegMarkerPosition → NegMarkerPosition → Bool

Equations

Typology.Negation.instBEqNegMarkerPosition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

@[implicit_reducible]

instance Typology.Negation.instReprNegMarkerPosition :

Repr NegMarkerPosition

Equations

Typology.Negation.instReprNegMarkerPosition = { reprPrec := Typology.Negation.instReprNegMarkerPosition.repr }

def Typology.Negation.instReprNegMarkerPosition.repr :

NegMarkerPosition → Nat → Std.Format

Equations

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

Instances For

inductive Typology.Negation.NegSymmetry :

WALS Ch 113A: whether negation changes clause structure beyond adding the negative marker. Symmetric: no structural change. Asymmetric: changes in finiteness, verb paradigm, or TAM marking.

symmetric : NegSymmetry
asymmetric : NegSymmetry
both : NegSymmetry
Both symmetric and asymmetric (Type SymAsy): some constructions symmetric, others asymmetric.

Instances For

@[implicit_reducible]

instance Typology.Negation.instDecidableEqNegSymmetry :

DecidableEq NegSymmetry

Equations

Typology.Negation.instDecidableEqNegSymmetry x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Typology.Negation.instBEqNegSymmetry.beq :

NegSymmetry → NegSymmetry → Bool

Equations

Typology.Negation.instBEqNegSymmetry.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

@[implicit_reducible]

instance Typology.Negation.instBEqNegSymmetry :

BEq NegSymmetry

Equations

Typology.Negation.instBEqNegSymmetry = { beq := Typology.Negation.instBEqNegSymmetry.beq }

def Typology.Negation.instReprNegSymmetry.repr :

NegSymmetry → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Typology.Negation.instReprNegSymmetry :

Repr NegSymmetry

Equations

Typology.Negation.instReprNegSymmetry = { reprPrec := Typology.Negation.instReprNegSymmetry.repr }

inductive Typology.Negation.AsymmetrySubtype :

WALS Ch 114A: which grammatical domain is affected by asymmetric negation. The four primary subtypes correspond to @cite{miestamo-2005}'s A/Fin (finiteness), A/NonReal (reality status), A/Emph (emphasis), A/Cat (other categories) plus combined codings.

Note: WALS Ch 114 does not encode A/Emph as a separate value (@cite{miestamo-2005} Table 2 distinguishes it; WALS collapses it).

finiteness : AsymmetrySubtype
realityStatus : AsymmetrySubtype
emphasis : AsymmetrySubtype
otherCategories : AsymmetrySubtype
finAndNonReal : AsymmetrySubtype
finAndEmph : AsymmetrySubtype
finAndCat : AsymmetrySubtype
nonRealAndCat : AsymmetrySubtype
emphAndCat : AsymmetrySubtype
nonAssignable : AsymmetrySubtype
Non-assignable: language has only symmetric negation.

Instances For

@[implicit_reducible]

instance Typology.Negation.instDecidableEqAsymmetrySubtype :

DecidableEq AsymmetrySubtype

Equations

Typology.Negation.instDecidableEqAsymmetrySubtype x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Typology.Negation.instBEqAsymmetrySubtype :

BEq AsymmetrySubtype

Equations

Typology.Negation.instBEqAsymmetrySubtype = { beq := Typology.Negation.instBEqAsymmetrySubtype.beq }

def Typology.Negation.instBEqAsymmetrySubtype.beq :

AsymmetrySubtype → AsymmetrySubtype → Bool

Equations

Typology.Negation.instBEqAsymmetrySubtype.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

def Typology.Negation.instReprAsymmetrySubtype.repr :

AsymmetrySubtype → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Typology.Negation.instReprAsymmetrySubtype :

Repr AsymmetrySubtype

Equations

Typology.Negation.instReprAsymmetrySubtype = { reprPrec := Typology.Negation.instReprAsymmetrySubtype.repr }

inductive Typology.Negation.NegIndefiniteStrategy :

WALS Ch 115A: how negative indefinites interact with predicate negation.

cooccur : NegIndefiniteStrategy
Negative indefinites co-occur with predicate negation (negative concord). Dominant pattern worldwide.
preclude : NegIndefiniteStrategy
Negative indefinites preclude predicate negation.
mixed : NegIndefiniteStrategy
Mixed (position-dependent or different indefinite series).
negExistential : NegIndefiniteStrategy
Negative existential construction.

Instances For

@[implicit_reducible]

instance Typology.Negation.instDecidableEqNegIndefiniteStrategy :

DecidableEq NegIndefiniteStrategy

Equations

Typology.Negation.instDecidableEqNegIndefiniteStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Typology.Negation.instBEqNegIndefiniteStrategy.beq :

NegIndefiniteStrategy → NegIndefiniteStrategy → Bool

Equations

Typology.Negation.instBEqNegIndefiniteStrategy.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

@[implicit_reducible]

instance Typology.Negation.instBEqNegIndefiniteStrategy :

BEq NegIndefiniteStrategy

Equations

Typology.Negation.instBEqNegIndefiniteStrategy = { beq := Typology.Negation.instBEqNegIndefiniteStrategy.beq }

def Typology.Negation.instReprNegIndefiniteStrategy.repr :

NegIndefiniteStrategy → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Typology.Negation.instReprNegIndefiniteStrategy :

Repr NegIndefiniteStrategy

Equations

Typology.Negation.instReprNegIndefiniteStrategy = { reprPrec := Typology.Negation.instReprNegIndefiniteStrategy.repr }

inductive Typology.Negation.NegVerbPosition :

WALS Ch 143A: position of negative morpheme relative to verb. Single-negation types (NegV/VNeg/[Neg-V]/[V-Neg]) plus multi-negation types (obligatory/optional double, optional triple).

preverbalParticle : NegVerbPosition
Preverbal negative particle: NegV.
postverbalParticle : NegVerbPosition
Postverbal negative particle: VNeg.
preverbalAffix : NegVerbPosition
Preverbal negative affix: [Neg-V].
postverbalAffix : NegVerbPosition
Postverbal negative affix: [V-Neg].
negativeTone : NegVerbPosition
mixedSingle : NegVerbPosition
obligDoublNeg : NegVerbPosition
optDoubleNeg : NegVerbPosition
tripleNeg : NegVerbPosition
optSingleNeg : NegVerbPosition

Instances For

@[implicit_reducible]

instance Typology.Negation.instDecidableEqNegVerbPosition :

DecidableEq NegVerbPosition

Equations

Typology.Negation.instDecidableEqNegVerbPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Typology.Negation.instBEqNegVerbPosition.beq :

NegVerbPosition → NegVerbPosition → Bool

Equations

Typology.Negation.instBEqNegVerbPosition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

@[implicit_reducible]

instance Typology.Negation.instBEqNegVerbPosition :

BEq NegVerbPosition

Equations

Typology.Negation.instBEqNegVerbPosition = { beq := Typology.Negation.instBEqNegVerbPosition.beq }

@[implicit_reducible]

instance Typology.Negation.instReprNegVerbPosition :

Repr NegVerbPosition

Equations

Typology.Negation.instReprNegVerbPosition = { reprPrec := Typology.Negation.instReprNegVerbPosition.repr }

def Typology.Negation.instReprNegVerbPosition.repr :

NegVerbPosition → Nat → Std.Format

Equations

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

Instances For

inductive Typology.Negation.NegMorphemePosition :

WALS Ch 143E/F: whether a language has preverbal and/or postverbal negative morphemes.

preverbalOnly : NegMorphemePosition
postverbalOnly : NegMorphemePosition
preverbalAffixOnly : NegMorphemePosition
postverbalAffixOnly : NegMorphemePosition
both : NegMorphemePosition
none : NegMorphemePosition

Instances For

@[implicit_reducible]

instance Typology.Negation.instDecidableEqNegMorphemePosition :

DecidableEq NegMorphemePosition

Equations

Typology.Negation.instDecidableEqNegMorphemePosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Typology.Negation.instBEqNegMorphemePosition.beq :

NegMorphemePosition → NegMorphemePosition → Bool

Equations

Typology.Negation.instBEqNegMorphemePosition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

@[implicit_reducible]

instance Typology.Negation.instBEqNegMorphemePosition :

BEq NegMorphemePosition

Equations

Typology.Negation.instBEqNegMorphemePosition = { beq := Typology.Negation.instBEqNegMorphemePosition.beq }

def Typology.Negation.instReprNegMorphemePosition.repr :

NegMorphemePosition → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Typology.Negation.instReprNegMorphemePosition :

Repr NegMorphemePosition

Equations

Typology.Negation.instReprNegMorphemePosition = { reprPrec := Typology.Negation.instReprNegMorphemePosition.repr }

structure Typology.Negation.NegMarkerEntry :

One language's standard sentential negation marker.

form : String
Surface form. For affixal negation this is an abstract citation form (e.g., Turkish -mE- for the harmony-conditioned -ma- / -me- alternants). For tonal/morphological negation use position := .morphological and document the realization in the def docstring.
gloss : String
Standard interlinear gloss. Defaults to the WALS-style "NEG".
morphemeType : NegMorphemeType
Morphological status: affix, free particle, auxiliary, etc.
position : NegMarkerPosition
Coarse position relative to the verb.

Instances For

@[implicit_reducible]

instance Typology.Negation.instReprNegMarkerEntry :

Repr NegMarkerEntry

Equations

Typology.Negation.instReprNegMarkerEntry = { reprPrec := Typology.Negation.instReprNegMarkerEntry.repr }

def Typology.Negation.instReprNegMarkerEntry.repr :

NegMarkerEntry → Nat → Std.Format

Equations

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

Instances For

structure Typology.Negation.NegationSystem :

A language's standard negation system.

The Fragment-side joint: every Fragments/{Lang}/Negation.lean exposes def negationSystem : NegationSystem. Multiple markers handle languages with mood/aspect/lexical-class alternation (Greek, Mandarin, Korean). Length-1 for most languages.

WALS datapoints are bundled at the system level — in WALS coding, F112A/F143A/F144A take one value per language regardless of how many markers the language has.

markers : List NegMarkerEntry
Standard negation marker(s). Order is editorial; Fragment files should put the unmarked / default-context marker first.
wals112A : Option Data.WALS.F112A.NegativeMorphemeType
WALS Ch 112A: morpheme classification. Should not be hand-encoded in Fragment files — use NegationSystem.ofISO to populate from the Data.WALS data, which is the single source of truth.
wals143A : Option Data.WALS.F143A.NegVerbOrder
WALS Ch 143A: NegV / VNeg / double-negation pattern. Populated by NegationSystem.ofISO.
wals144A : Option Data.WALS.F144A.PositionOfNegativeWordWithRespectToSubjectObjectAndVerb
WALS Ch 144A: full S/O/V positional classification. Populated by NegationSystem.ofISO.

Instances For

def Typology.Negation.instReprNegationSystem.repr :

NegationSystem → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Typology.Negation.instReprNegationSystem :

Repr NegationSystem

Equations

Typology.Negation.instReprNegationSystem = { reprPrec := Typology.Negation.instReprNegationSystem.repr }

structure Typology.Negation.NegationProfile :

A language's negation profile across WALS Chapters 112-115, plus fields from @cite{greco-2020} (negIsHead) and @cite{jin-koenig-2021} (enAttested).

Sibling Fragment-side joint to NegationSystem: every Fragments/{Lang}/Negation.lean exposes def negationProfile : NegationProfile. The two joints are independent because the data partition is real: negationSystem.markers is consumed by lexical code; negationProfile is consumed by typology studies. Mirrors Typology/Possession.lean::PossessionProfile.

language : String
Language name.
iso : String
ISO 639-3 code.
morphemeType : NegMorphemeType
Ch 112: how standard negation is expressed.
symmetry : NegSymmetry
Ch 113: symmetric, asymmetric, or both.
asymmetrySubtype : AsymmetrySubtype
Ch 114: asymmetry subtype (nonAssignable if symmetric only).
negIndefinite : Option NegIndefiniteStrategy
Ch 115: strategy for negative indefinites, if attested.
negMarkers : List String
Illustrative negative marker form(s).
negIsHead : Option Bool
Is the negation marker a syntactic head (X°) rather than a phrase (XP)? Relevant for @cite{greco-2020}: only head-status markers can merge in CP to produce surprise negation.
enAttested : Option Bool
Is expletive negation attested in this language? @cite{jin-koenig-2021} (722-language survey: EN in 74 languages) and @cite{rett-2026}.

Instances For

@[implicit_reducible]

instance Typology.Negation.instReprNegationProfile :

Repr NegationProfile

Equations

Typology.Negation.instReprNegationProfile = { reprPrec := Typology.Negation.instReprNegationProfile.repr }

def Typology.Negation.instReprNegationProfile.repr :

NegationProfile → Nat → Std.Format

Equations

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

Instances For

def Typology.Negation.ofWALS112A :

Data.WALS.F112A.NegativeMorphemeType → NegMorphemeType

WALS Ch 112A → NegMorphemeType.

Equations

Instances For

def Typology.Negation.fromWALS113A :

Data.WALS.F113A.NegationSymmetry → NegSymmetry

WALS Ch 113A → NegSymmetry.

Equations

Instances For

def Typology.Negation.fromWALS114A :

Data.WALS.F114A.AsymmetricNegationSubtype → AsymmetrySubtype

WALS Ch 114A → AsymmetrySubtype.

Equations

Instances For

def Typology.Negation.fromWALS115A :

Data.WALS.F115A.NegativeIndefiniteType → NegIndefiniteStrategy

WALS Ch 115A → NegIndefiniteStrategy.

Equations

Instances For

def Typology.Negation.fromWALS143A :

Data.WALS.F143A.NegVerbOrder → NegVerbPosition

WALS Ch 143A → NegVerbPosition.

Equations

Instances For

def Typology.Negation.NegationSystem.ofISO (iso : String) (markers : List NegMarkerEntry) :

Build a NegationSystem for a language identified by ISO 639-3 code, pulling F112A / F143A / F144A values from the Data.WALS data.

Equations

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

Instances For

def Typology.Negation.NegationProfile.hasMorphemeType (p : NegationProfile) (t : NegMorphemeType) :

Bool

Does a language use a given morpheme type?

Equations

p.hasMorphemeType t = (p.morphemeType == t)

Instances For

def Typology.Negation.NegationProfile.hasSymmetric (p : NegationProfile) :

Bool

Does a language have symmetric negation (either symmetric only or both)?

Equations

p.hasSymmetric = (p.symmetry == Typology.Negation.NegSymmetry.symmetric || p.symmetry == Typology.Negation.NegSymmetry.both)

Instances For

def Typology.Negation.NegationProfile.hasAsymmetric (p : NegationProfile) :

Bool

Does a language have asymmetric negation (either asymmetric only or both)?

Equations

p.hasAsymmetric = (p.symmetry == Typology.Negation.NegSymmetry.asymmetric || p.symmetry == Typology.Negation.NegSymmetry.both)

Instances For

def Typology.Negation.NegationProfile.hasNegConcord (p : NegationProfile) :

Bool

Does a language show negative concord?

Equations

p.hasNegConcord = (p.negIndefinite == some Typology.Negation.NegIndefiniteStrategy.cooccur)

Instances For

def Typology.Negation.countByMorphemeType (langs : List NegationProfile) (t : NegMorphemeType) :

Nat

Count of languages in a sample with a given morpheme type.

Equations

Typology.Negation.countByMorphemeType langs t = (List.filter (fun (x : Typology.Negation.NegationProfile) => x.hasMorphemeType t) langs).length

Instances For

def Typology.Negation.countBySymmetry (langs : List NegationProfile) (s : NegSymmetry) :

Nat

Count of languages in a sample with a given symmetry type.

Equations

Typology.Negation.countBySymmetry langs s = (List.filter (fun (x : Typology.Negation.NegationProfile) => x.symmetry == s) langs).length

Instances For

theorem Typology.Negation.particles_most_common :

(List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F112A.NegativeMorphemeType) => x.value == Data.WALS.F112A.NegativeMorphemeType.negativeParticle) Typology.Negation.ch112✝).length > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F112A.NegativeMorphemeType) => x.value == Data.WALS.F112A.NegativeMorphemeType.negativeAffix) Typology.Negation.ch112✝).length

Ch 112: negative particles outnumber negative affixes.

theorem Typology.Negation.aux_verbs_rare :

(List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F112A.NegativeMorphemeType) => x.value == Data.WALS.F112A.NegativeMorphemeType.negativeAuxiliaryVerb) Typology.Negation.ch112✝).length * 20 < Typology.Negation.ch112✝.length

Ch 112: negative auxiliary verbs are rare (< 5% of sample).

theorem Typology.Negation.symasy_most_common :

have sym := (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F113A.NegationSymmetry) => x.value == Data.WALS.F113A.NegationSymmetry.symmetric) Typology.Negation.ch113✝).length; have asy := (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F113A.NegationSymmetry) => x.value == Data.WALS.F113A.NegationSymmetry.asymmetric) Typology.Negation.ch113✝).length; have both := (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F113A.NegationSymmetry) => x.value == Data.WALS.F113A.NegationSymmetry.both) Typology.Negation.ch113✝).length; both > sym ∧ sym > asy

Ch 113: SymAsy (both) is the most common type, followed by Sym, then Asy.

theorem Typology.Negation.acat_most_common_subtype :

have aCat := (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F114A.AsymmetricNegationSubtype) => x.value == Data.WALS.F114A.AsymmetricNegationSubtype.aCat) Typology.Negation.ch114✝).length; have aFin := (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F114A.AsymmetricNegationSubtype) => x.value == Data.WALS.F114A.AsymmetricNegationSubtype.aFin) Typology.Negation.ch114✝).length; have aNon := (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F114A.AsymmetricNegationSubtype) => x.value == Data.WALS.F114A.AsymmetricNegationSubtype.aNonreal) Typology.Negation.ch114✝).length; aCat > aFin ∧ aFin > aNon

Ch 114: A/Cat is the most common single asymmetry subtype, then A/Fin, then A/NonReal.

theorem Typology.Negation.neg_concord_dominant :

have cooccur := (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F115A.NegativeIndefiniteType) => x.value == Data.WALS.F115A.NegativeIndefiniteType.predicateNegationAlsoPresent) Typology.Negation.ch115✝).length; have preclude := (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F115A.NegativeIndefiniteType) => x.value == Data.WALS.F115A.NegativeIndefiniteType.noPredicateNegation) Typology.Negation.ch115✝).length; cooccur > preclude * 15

Ch 115: negative concord (co-occurrence) outnumbers preclusion by 15×.

theorem Typology.Negation.preclusion_rarest :

have preclude := (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F115A.NegativeIndefiniteType) => x.value == Data.WALS.F115A.NegativeIndefiniteType.noPredicateNegation) Typology.Negation.ch115✝).length; have mixed := (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F115A.NegativeIndefiniteType) => x.value == Data.WALS.F115A.NegativeIndefiniteType.mixedBehaviour) Typology.Negation.ch115✝).length; have negEx := (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F115A.NegativeIndefiniteType) => x.value == Data.WALS.F115A.NegativeIndefiniteType.negativeExistentialConstruction) Typology.Negation.ch115✝).length; preclude ≤ mixed ∧ preclude ≤ negEx

Ch 115: preclusion of predicate negation is the rarest strategy.

theorem Typology.Negation.ch143A_preverbal_dominates :

have preParticle := (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F143A.NegVerbOrder) => x.value == Data.WALS.F143A.NegVerbOrder.negv) Typology.Negation.ch143A✝).length; have preAffix := (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F143A.NegVerbOrder) => x.value == Data.WALS.F143A.NegVerbOrder.negV) Typology.Negation.ch143A✝).length; have postParticle := (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F143A.NegVerbOrder) => x.value == Data.WALS.F143A.NegVerbOrder.vneg) Typology.Negation.ch143A✝).length; have postAffix := (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F143A.NegVerbOrder) => x.value == Data.WALS.F143A.NegVerbOrder.vNeg) Typology.Negation.ch143A✝).length; preParticle + preAffix > postParticle + postAffix

Ch 143A: preverbal negation (particle or affix) dominates postverbal.

theorem Typology.Negation.ch144B_immed_preverbal_dominant :

(List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F144B.PositionOfNegativeWordsRelativeToBeginningAndEndOfClauseAndWithRespectToAdjacencyToVerb) => x.value == Data.WALS.F144B.PositionOfNegativeWordsRelativeToBeginningAndEndOfClauseAndWithRespectToAdjacencyToVerb.immedPreverbal) Typology.Negation.ch144B✝).length > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F144B.PositionOfNegativeWordsRelativeToBeginningAndEndOfClauseAndWithRespectToAdjacencyToVerb) => x.value == Data.WALS.F144B.PositionOfNegativeWordsRelativeToBeginningAndEndOfClauseAndWithRespectToAdjacencyToVerb.immedPostverbal) Typology.Negation.ch144B✝).length + (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F144B.PositionOfNegativeWordsRelativeToBeginningAndEndOfClauseAndWithRespectToAdjacencyToVerb) => x.value == Data.WALS.F144B.PositionOfNegativeWordsRelativeToBeginningAndEndOfClauseAndWithRespectToAdjacencyToVerb.endNotImmedPostverbal) Typology.Negation.ch144B✝).length

Ch 144B: immediately preverbal is the most common position for negative words.