Copula and Predication Typology (WALS Chapters 117--120)

@cite{hengeveld-1992} @cite{pustet-2003} @cite{stassen-2013} @cite{haspelmath-2001}

Cross-linguistic data on predication strategies and copulas from four WALS chapters, all authored by Leon @cite{stassen-2013}. These chapters address a cluster of related questions: how languages express predication when the predicate is an adjective, a noun phrase, or a locative, and whether a copular element is needed in each case.

The key insight from Stassen's typological work is that predication is not uniform across predicate types. Many languages use fundamentally different strategies for adjectival predication ("The book is red"), nominal predication ("She is a doctor"), and locational predication ("The cat is on the mat"). The copula, where it exists, is best understood not as a single phenomenon but as a family of strategies that languages deploy differently across predicate types.

Ch 117: Predicative Possession (N = 240)

How languages express predicative possession ("I have a book"). Five values:

• Locational (48/240): possession expressed as location ("a book is at me").
• Genitive (22/240): possession expressed with genitive ("my book exists").
• Topic (48/240): possession expressed as topic construction.
• Conjunctional (59/240): possession expressed with conjunctional strategy.
• 'Have' (63/240): a dedicated 'have' verb is used.

Ch 118: Predicative Adjectives (N = 386)

How languages express adjectival predication. Three values:

• Verbal encoding: adjectives behave like verbs (take verbal morphology, no copula). This is the most common strategy worldwide (151/386 = 39.1%).
• Nonverbal encoding: adjectives require a copula or other non-verbal strategy (132/386 = 34.2%).
• Mixed: some adjectives are verbal, others require a copula (103/386 = 26.7%).

Ch 119: Nominal and Locational Predication (N = 386)

Whether a language uses the same or different strategy for nominal predication ("is a doctor") and locational predication ("is in the room"). Two values:

• Different: different copulas or strategies for NOM vs LOC (269/386 = 69.7%).
• Identical: same copula/strategy for both (117/386 = 30.3%).

The majority pattern is to differentiate: even English, which uses "be" for both, is cross-linguistically unusual in using a single copula.

Ch 120: Zero Copula for Predicate Nominals (N = 386)

Whether the copula can be absent in nominal predication. Two values:

• Impossible: copula is always required (211/386 = 54.7%).
• Possible: zero copula is allowed in some or all contexts (175/386 = 45.3%).

inductive Phenomena.Copulas.Typology.PredAdjStrategy : Type

WALS Ch 117: How a language expresses adjectival predication ("The book is red").

The three-way distinction reflects the categorial status of adjectives in the language. In "verbal" languages, adjectives inflect like verbs and need no copula. In "non-verbal" languages, adjectives are a distinct category requiring a copula. "Mixed" languages have adjectives that split between verbal and non-verbal behavior.

• verbal : PredAdjStrategy

  Adjectives behave like verbs: they take verbal morphology (tense, aspect, negation) and occur as predicates without a copula. Example: Mandarin shu hong 'book red' = 'The book is red', where hong can take aspect markers directly.

• mixed : PredAdjStrategy

  Some adjectives are verbal (typically core/frequent ones), others require a copula (typically peripheral/borrowed ones). Example: Japanese has verbal adjectives (i-adjectives: takai 'is expensive') and non-verbal adjectives (na-adjectives: shizuka-da 'quiet-COP').

• nonVerbal : PredAdjStrategy

  Adjectives are categorially distinct from verbs and require a copula or other linking element for predication. Example: English The book is red requires the copula is.

instance Phenomena.Copulas.Typology.instDecidableEqPredAdjStrategy : DecidableEq PredAdjStrategy

Equations

• Phenomena.Copulas.Typology.instDecidableEqPredAdjStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Copulas.Typology.instBEqPredAdjStrategy.beq : PredAdjStrategy → PredAdjStrategy → Bool

Equations

• Phenomena.Copulas.Typology.instBEqPredAdjStrategy.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Copulas.Typology.instBEqPredAdjStrategy : BEq PredAdjStrategy

Equations

• Phenomena.Copulas.Typology.instBEqPredAdjStrategy = { beq := Phenomena.Copulas.Typology.instBEqPredAdjStrategy.beq }

instance Phenomena.Copulas.Typology.instReprPredAdjStrategy : Repr PredAdjStrategy

Equations

• Phenomena.Copulas.Typology.instReprPredAdjStrategy = { reprPrec := Phenomena.Copulas.Typology.instReprPredAdjStrategy.repr }

def Phenomena.Copulas.Typology.instReprPredAdjStrategy.repr : PredAdjStrategy → Nat → Std.Format

Equations

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

inductive Phenomena.Copulas.Typology.PredNounStrategy : Type

WALS Ch 118: How a language expresses nominal predication ("She is a doctor").

The binary distinction captures whether the language uses a verbal copula (a word that inflects like a verb and carries tense/agreement) or a non-verbal strategy (juxtaposition, pronominal copula, or invariant particle).

• verbal : PredNounStrategy

  Nominal predication uses a verbal copula that inflects for tense, agreement, etc. Example: English She is a doctor, where is is a fully inflecting verb (am/is/are/was/were).

• nonVerbal : PredNounStrategy

  Nominal predication uses juxtaposition or a non-verbal element (particle, pronoun, etc.), not a copula verb. Example: Russian present tense Ona vrach 'She doctor' = 'She is a doctor' (no copula in present tense).

instance Phenomena.Copulas.Typology.instDecidableEqPredNounStrategy : DecidableEq PredNounStrategy

Equations

• Phenomena.Copulas.Typology.instDecidableEqPredNounStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Copulas.Typology.instBEqPredNounStrategy : BEq PredNounStrategy

Equations

• Phenomena.Copulas.Typology.instBEqPredNounStrategy = { beq := Phenomena.Copulas.Typology.instBEqPredNounStrategy.beq }

def Phenomena.Copulas.Typology.instBEqPredNounStrategy.beq : PredNounStrategy → PredNounStrategy → Bool

Equations

• Phenomena.Copulas.Typology.instBEqPredNounStrategy.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Copulas.Typology.instReprPredNounStrategy : Repr PredNounStrategy

Equations

• Phenomena.Copulas.Typology.instReprPredNounStrategy = { reprPrec := Phenomena.Copulas.Typology.instReprPredNounStrategy.repr }

def Phenomena.Copulas.Typology.instReprPredNounStrategy.repr : PredNounStrategy → Nat → Std.Format

Equations

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

inductive Phenomena.Copulas.Typology.NomLocStrategy : Type

WALS Ch 119: Whether a language uses the same or different strategy for nominal predication ("She is a doctor") and locational predication ("The cat is on the mat").

Many languages use different verbs: e.g., Spanish ser (nominal) vs estar (locational), or have a copula for one but not the other. The "different" value is the majority pattern cross-linguistically.

• identical : NomLocStrategy

  The same copula or strategy is used for both nominal and locational predication. Example: English She is a doctor / The cat is on the mat -- both use be.

• different : NomLocStrategy

  Different copulas or strategies are used for nominal vs locational predication. Example: Spanish ser (nominal: Es doctora) vs estar (locational: Esta en la casa).

instance Phenomena.Copulas.Typology.instDecidableEqNomLocStrategy : DecidableEq NomLocStrategy

Equations

• Phenomena.Copulas.Typology.instDecidableEqNomLocStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Copulas.Typology.instBEqNomLocStrategy.beq : NomLocStrategy → NomLocStrategy → Bool

Equations

• Phenomena.Copulas.Typology.instBEqNomLocStrategy.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Copulas.Typology.instBEqNomLocStrategy : BEq NomLocStrategy

Equations

• Phenomena.Copulas.Typology.instBEqNomLocStrategy = { beq := Phenomena.Copulas.Typology.instBEqNomLocStrategy.beq }

instance Phenomena.Copulas.Typology.instReprNomLocStrategy : Repr NomLocStrategy

Equations

• Phenomena.Copulas.Typology.instReprNomLocStrategy = { reprPrec := Phenomena.Copulas.Typology.instReprNomLocStrategy.repr }

def Phenomena.Copulas.Typology.instReprNomLocStrategy.repr : NomLocStrategy → Nat → Std.Format

Equations

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

inductive Phenomena.Copulas.Typology.ZeroCopulaStatus : Type

WALS Ch 120: Whether the copula can be absent in nominal predication.

Zero copula is typically conditioned by tense (present only) or person (3rd person only). "Widespread" means zero copula is the default, unrestricted strategy.

• impossible : ZeroCopulaStatus

  Zero copula is impossible: the copula is always required in nominal predication, regardless of tense, person, or other factors. Example: English *She doctor is ungrammatical.

• restricted : ZeroCopulaStatus

  Zero copula is possible in restricted contexts: typically present tense, or 3rd person, or in certain clause types. The copula appears in other environments. Example: Russian allows zero copula in present tense (Ona vrach 'She doctor') but requires it in past tense (Ona byla vrach 'She was doctor').

• widespread : ZeroCopulaStatus

  Zero copula is the normal, widespread, or default strategy. The copula is absent in most environments. Example: Tagalog Doktor siya 'Doctor she' = 'She is a doctor'.

instance Phenomena.Copulas.Typology.instDecidableEqZeroCopulaStatus : DecidableEq ZeroCopulaStatus

Equations

• Phenomena.Copulas.Typology.instDecidableEqZeroCopulaStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Copulas.Typology.instBEqZeroCopulaStatus : BEq ZeroCopulaStatus

Equations

• Phenomena.Copulas.Typology.instBEqZeroCopulaStatus = { beq := Phenomena.Copulas.Typology.instBEqZeroCopulaStatus.beq }

def Phenomena.Copulas.Typology.instBEqZeroCopulaStatus.beq : ZeroCopulaStatus → ZeroCopulaStatus → Bool

Equations

• Phenomena.Copulas.Typology.instBEqZeroCopulaStatus.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Copulas.Typology.instReprZeroCopulaStatus : Repr ZeroCopulaStatus

Equations

• Phenomena.Copulas.Typology.instReprZeroCopulaStatus = { reprPrec := Phenomena.Copulas.Typology.instReprZeroCopulaStatus.repr }

def Phenomena.Copulas.Typology.instReprZeroCopulaStatus.repr : ZeroCopulaStatus → Nat → Std.Format

Equations

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

inductive Phenomena.Copulas.Typology.CopulaType : Type

Morphosyntactic type of copula, when present.

This supplements the WALS classification with a finer-grained typology of copular elements, following @cite{pustet-2003} and @cite{hengeveld-1992}.

• verbalCopula : CopulaType

  Fully inflecting verbal copula: takes tense, agreement, negation like other verbs. Example: English be (am/is/are/was/were).

• pronominalCopula : CopulaType

  Pronominal copula: a pronoun-like element that agrees with the subject. Example: Hebrew hu/hi/hem/hen (he/she/they.m/they.f) used as a copula in present tense.

• particle : CopulaType

  Invariant particle: a non-inflecting element linking subject and predicate. Example: Swahili ni (affirmative copula, invariant).

• zero : CopulaType

  No copula: predication by juxtaposition.

instance Phenomena.Copulas.Typology.instDecidableEqCopulaType : DecidableEq CopulaType

Equations

• Phenomena.Copulas.Typology.instDecidableEqCopulaType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Copulas.Typology.instBEqCopulaType : BEq CopulaType

Equations

• Phenomena.Copulas.Typology.instBEqCopulaType = { beq := Phenomena.Copulas.Typology.instBEqCopulaType.beq }

def Phenomena.Copulas.Typology.instBEqCopulaType.beq : CopulaType → CopulaType → Bool

Equations

• Phenomena.Copulas.Typology.instBEqCopulaType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Copulas.Typology.instReprCopulaType.repr : CopulaType → Nat → Std.Format

Equations

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

instance Phenomena.Copulas.Typology.instReprCopulaType : Repr CopulaType

Equations

• Phenomena.Copulas.Typology.instReprCopulaType = { reprPrec := Phenomena.Copulas.Typology.instReprCopulaType.repr }

structure Phenomena.Copulas.Typology.WALSCount : Type

A single row in a WALS frequency table: a category label and its count.

• label : String
• count : Nat

instance Phenomena.Copulas.Typology.instReprWALSCount : Repr WALSCount

Equations

• Phenomena.Copulas.Typology.instReprWALSCount = { reprPrec := Phenomena.Copulas.Typology.instReprWALSCount.repr }

def Phenomena.Copulas.Typology.instReprWALSCount.repr : WALSCount → Nat → Std.Format

Equations

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

instance Phenomena.Copulas.Typology.instDecidableEqWALSCount : DecidableEq WALSCount

Equations

• Phenomena.Copulas.Typology.instDecidableEqWALSCount = Phenomena.Copulas.Typology.instDecidableEqWALSCount.decEq

def Phenomena.Copulas.Typology.instDecidableEqWALSCount.decEq (x✝ x✝¹ : WALSCount) : Decidable (x✝ = x✝¹)

Equations

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

def Phenomena.Copulas.Typology.instBEqWALSCount.beq : WALSCount → WALSCount → Bool

Equations

• Phenomena.Copulas.Typology.instBEqWALSCount.beq { label := a, count := a_1 } { label := b, count := b_1 } = (a == b && a_1 == b_1)
• Phenomena.Copulas.Typology.instBEqWALSCount.beq x✝¹ x✝ = false

instance Phenomena.Copulas.Typology.instBEqWALSCount : BEq WALSCount

Equations

• Phenomena.Copulas.Typology.instBEqWALSCount = { beq := Phenomena.Copulas.Typology.instBEqWALSCount.beq }

def Phenomena.Copulas.Typology.WALSCount.totalOf (cs : List WALSCount) : Nat

Sum of counts in a WALS table.

Equations

• Phenomena.Copulas.Typology.WALSCount.totalOf cs = List.foldl (fun (acc : Nat) (c : Phenomena.Copulas.Typology.WALSCount) => acc + c.count) 0 cs

def Phenomena.Copulas.Typology.ch117Counts : List WALSCount

Chapter 117 distribution: predicative possession (N = 240).

Equations

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

def Phenomena.Copulas.Typology.ch118Counts : List WALSCount

Chapter 118 distribution: predicative adjectives (N = 386).

Equations

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

def Phenomena.Copulas.Typology.ch119Counts : List WALSCount

Chapter 119 distribution: nominal and locational predication (N = 386).

Equations

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

def Phenomena.Copulas.Typology.ch120Counts : List WALSCount

Chapter 120 distribution: zero copula for predicate nominals (N = 386).

Equations

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

theorem Phenomena.Copulas.Typology.ch117_total : WALSCount.totalOf ch117Counts = 240

Ch 117 total: 240 languages.

theorem Phenomena.Copulas.Typology.ch118_total : WALSCount.totalOf ch118Counts = 386

Ch 118 total: 386 languages.

theorem Phenomena.Copulas.Typology.ch119_total : WALSCount.totalOf ch119Counts = 386

Ch 119 total: 386 languages.

theorem Phenomena.Copulas.Typology.ch120_total : WALSCount.totalOf ch120Counts = 386

Ch 120 total: 386 languages.

theorem Phenomena.Copulas.Typology.ch118_119_120_same_sample : WALSCount.totalOf ch118Counts = WALSCount.totalOf ch119Counts ∧ WALSCount.totalOf ch119Counts = WALSCount.totalOf ch120Counts

Chapters 118, 119, 120 use the same 386-language sample. Chapter 117 uses a smaller 240-language sample.

structure Phenomena.Copulas.Typology.CopulaProfile : Type

A language's copula and predication profile across WALS Chapters 117--120.

• language : String

  Language name.

• iso : String

  ISO 639-3 code.

• family : String

  Language family.

• predAdj : PredAdjStrategy

  Ch 117: How adjectival predication is expressed.

• predNoun : PredNounStrategy

  Ch 118: How nominal predication is expressed.

• nomLoc : NomLocStrategy

  Ch 119: Whether nominal and locational predication use the same or different strategy.

• zeroCopula : ZeroCopulaStatus

  Ch 120: Whether zero copula is possible in nominal predication.

• copulaType : CopulaType

  Primary copula type in the language (supplementary).

• copulaForms : List String

  Illustrative copula form(s).

• notes : String

  Notes on the predication system.

instance Phenomena.Copulas.Typology.instReprCopulaProfile : Repr CopulaProfile

Equations

• Phenomena.Copulas.Typology.instReprCopulaProfile = { reprPrec := Phenomena.Copulas.Typology.instReprCopulaProfile.repr }

def Phenomena.Copulas.Typology.instReprCopulaProfile.repr : CopulaProfile → Nat → Std.Format

Equations

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

def Phenomena.Copulas.Typology.english : CopulaProfile

English (Indo-European, Germanic). Adjectives are non-verbal: require copula be ("The book is red"). Nominal predication uses the verbal copula be ("She is a doctor"). Same copula be for both nominal and locational predication. Zero copula is impossible: *She doctor, *Book red.

Equations

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

def Phenomena.Copulas.Typology.french : CopulaProfile

French (Indo-European, Romance). Adjectives are non-verbal: Le livre est rouge ('The book is red'). Nominal predication uses verbal copula etre: Elle est medecin. Same copula etre for nominal and locational predication. Zero copula is impossible.

Equations

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

def Phenomena.Copulas.Typology.german : CopulaProfile

German (Indo-European, Germanic). Adjectives are non-verbal: Das Buch ist rot ('The book is red'). Nominal predication uses verbal copula sein: Sie ist Arztin. Same copula for nominal and locational predication. Zero copula is impossible.

Equations

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

def Phenomena.Copulas.Typology.spanish : CopulaProfile

Spanish (Indo-European, Romance). Adjectives are non-verbal: El libro es rojo ('The book is red'). Nominal predication uses verbal copula ser: Ella es doctora. DIFFERENT copulas for nominal vs locational: ser (permanent/nominal) vs estar (temporary/locational). Zero copula is impossible.

Equations

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

def Phenomena.Copulas.Typology.russian : CopulaProfile

Russian (Indo-European, Slavic). Adjectives are non-verbal in present tense (zero copula: Kniga krasnaja 'Book red'), verbal copula byt' in past (Kniga byla krasnaja). Nominal predication uses zero copula in present: Ona vrach ('She doctor'). Same strategy for nominal and locational (both use zero copula in present). Zero copula is RESTRICTED to present tense: past and future require byt'.

Equations

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

def Phenomena.Copulas.Typology.arabic : CopulaProfile

Arabic (Standard) (Afro-Asiatic, Semitic). Adjectives are non-verbal: al-kitab ahmar 'the-book red'. Nominal predication is non-verbal in present: hiya tabiba 'she doctor'. Different strategies for nominal vs locational (locational uses fi 'in' with possible copula). Zero copula is RESTRICTED: present tense allows zero, past requires kaana.

Equations

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

def Phenomena.Copulas.Typology.hebrew : CopulaProfile

Hebrew (Afro-Asiatic, Semitic). Adjectives are non-verbal: ha-sefer adom 'the-book red'. Nominal predication uses a pronominal copula in present: hi rofaa or hi hi rofaa (she COP.3F doctor). Past/future use haya. Different strategies for nominal vs locational. Zero copula is RESTRICTED: present allows zero/pronominal, past requires haya.

Equations

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

def Phenomena.Copulas.Typology.hungarian : CopulaProfile

Hungarian (Uralic). Adjectives are non-verbal: A konyv piros 'The book red'. Nominal predication: zero copula in 3rd person present (O orvos 'She doctor'), verbal copula van in other persons/tenses. Same strategy for nominal and locational. Zero copula is RESTRICTED to 3rd person present tense.

Equations

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

def Phenomena.Copulas.Typology.japanese : CopulaProfile

Japanese (Japonic). Adjectives are MIXED: i-adjectives are verbal (takai 'is.expensive', takes tense: takakatta 'was.expensive'), but na-adjectives require copula da (shizuka-da 'quiet-COP'). Nominal predication uses copula da/desu: Kanojo wa isha da 'She TOP doctor COP'. Different strategies for nominal and locational (locational uses ni iru/aru). Zero copula is impossible in standard forms (copula always required for nominals).

Equations

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

def Phenomena.Copulas.Typology.korean : CopulaProfile

Korean (Koreanic). Adjectives are verbal: chaek-i ppalgah-da 'book-NOM red-DECL' with verbal inflection on the adjective. No copula needed. Nominal predication uses copula -i-da: geunyeo-neun uisa-i-da 'she-TOP doctor-COP-DECL'. Different strategies for nominal vs locational (locational uses iss-da 'exist-DECL'). Zero copula is impossible for nominals.

Equations

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

def Phenomena.Copulas.Typology.mandarin : CopulaProfile

Mandarin Chinese (Sino-Tibetan). Adjectives are verbal: shu hong 'book red' = 'The book is red'. Adjectives can take aspect markers (le, guo) and negation (bu) directly. Nominal predication uses copula shi: ta shi yisheng 'she COP doctor'. Different strategies for nominal vs locational (locational uses zai 'at'). Zero copula is impossible for nominal predication (shi is required).

Equations

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

def Phenomena.Copulas.Typology.turkish : CopulaProfile

Turkish (Turkic). Adjectives are verbal: Kitap kirmizi 'Book red' = 'The book is red'. Adjective takes verbal suffixes for tense. Nominal predication uses a copular suffix: O doktor-dur 'S/he doctor-COP'. Different strategies for nominal vs locational (locational uses postposition + var/yok). Zero copula is RESTRICTED: 3rd person present often has zero copula (O doktor 'S/he doctor'), but past requires -di/-ydi.

Equations

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

def Phenomena.Copulas.Typology.swahili : CopulaProfile

Swahili (Niger-Congo, Bantu). Adjectives are verbal: -zuri 'good' takes verbal agreement prefixes (m-zuri 'good (cl.1)'). Predication: Kitabu ni kizuri uses ni. Nominal predication uses particle ni: Yeye ni daktari 'S/he COP doctor'. Different strategies for nominal vs locational (locational uses -ko locative suffixes and different verbal forms). Zero copula is WIDESPREAD in some constructions: Yeye daktari is acceptable in many contexts.

Equations

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

def Phenomena.Copulas.Typology.hindiUrdu : CopulaProfile

Hindi-Urdu (Indo-European, Indo-Aryan). Adjectives are non-verbal: kitab lal hai 'book red COP.PRS'. Nominal predication uses copula hona: vo daktar hai 'she doctor COP.PRS'. Same copula hona for nominal and locational predication. Zero copula is impossible in standard Hindi-Urdu.

Equations

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

def Phenomena.Copulas.Typology.tagalog : CopulaProfile

Tagalog (Austronesian). Adjectives are verbal: maganda ang babae 'beautiful ANG woman'. Nominal predication is non-verbal: doktor siya 'doctor she'. Same strategy for nominal and locational. Zero copula is WIDESPREAD: doktor siya with no overt copula is the normal strategy.

Equations

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

def Phenomena.Copulas.Typology.irish : CopulaProfile

Irish (Indo-European, Celtic). Adjectives are non-verbal: Ta an leabhar dearg 'COP the book red'. Nominal predication uses copula is: Is dochtúir í 'COP doctor she'. DIFFERENT copulas: is (classificatory/identificational) vs ta (attributive/locational). Zero copula is impossible.

Equations

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

def Phenomena.Copulas.Typology.finnish : CopulaProfile

Finnish (Uralic). Adjectives are non-verbal: Kirja on punainen 'Book COP red'. Nominal predication uses verbal copula olla: Han on laakari 'S/he COP doctor'. Same copula olla for nominal and locational predication. Zero copula is impossible.

Equations

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

def Phenomena.Copulas.Typology.quechua : CopulaProfile

Quechua (Quechuan). Adjectives are non-verbal: Wasi hatun-mi 'House big-EVID' with copular suffix. Nominal predication uses copular suffixes: Pay yachachiq-mi 'S/he teacher-EVID' (copula as suffix -mi/-n). Same strategy for nominal and locational predication. Zero copula is RESTRICTED: 3rd person present often has zero or reduced copula, but other persons/tenses require overt copula ka-.

Equations

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

def Phenomena.Copulas.Typology.yoruba : CopulaProfile

Yoruba (Niger-Congo, Atlantic-Congo). Adjectives are verbal: Iwe na tobi 'book the big' (adjective inflects verbally). Nominal predication uses non-verbal strategy (juxtaposition or pronoun): O je dokita 'She be doctor' or O dokita ni 'She doctor COP'. Different strategies for nominal vs locational. Zero copula is WIDESPREAD for nominal predication.

Equations

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

def Phenomena.Copulas.Typology.thai : CopulaProfile

Thai (Tai-Kadai). Adjectives are verbal: Nangsue daeng 'Book red' = 'The book is red', where the adjective takes verbal markers directly. Nominal predication uses verbal copula pen: Khao pen mor 'S/he COP doctor'. Different strategies for nominal vs locational (locational uses yuu 'be.at'). Zero copula is impossible for nominal predication.

Equations

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

def Phenomena.Copulas.Typology.allLanguages : List CopulaProfile

All language profiles in the sample.

Equations

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

def Phenomena.Copulas.Typology.CopulaProfile.hasVerbalAdj (p : CopulaProfile) : Bool

Does a language have verbal adjectives?

Equations

• p.hasVerbalAdj = (p.predAdj == Phenomena.Copulas.Typology.PredAdjStrategy.verbal)

def Phenomena.Copulas.Typology.CopulaProfile.hasVerbalNounCopula (p : CopulaProfile) : Bool

Does a language have a verbal copula for nominal predication?

Equations

• p.hasVerbalNounCopula = (p.predNoun == Phenomena.Copulas.Typology.PredNounStrategy.verbal)

def Phenomena.Copulas.Typology.CopulaProfile.allowsZeroCopula (p : CopulaProfile) : Bool

Does a language allow zero copula (restricted or widespread)?

Equations

• p.allowsZeroCopula = (p.zeroCopula == Phenomena.Copulas.Typology.ZeroCopulaStatus.restricted || p.zeroCopula == Phenomena.Copulas.Typology.ZeroCopulaStatus.widespread)

def Phenomena.Copulas.Typology.CopulaProfile.hasNomLocSplit (p : CopulaProfile) : Bool

Does a language split nominal and locational predication?

Equations

• p.hasNomLocSplit = (p.nomLoc == Phenomena.Copulas.Typology.NomLocStrategy.different)

def Phenomena.Copulas.Typology.CopulaProfile.alwaysRequiresCopula (p : CopulaProfile) : Bool

Does a language require a copula in all contexts?

Equations

• p.alwaysRequiresCopula = (p.zeroCopula == Phenomena.Copulas.Typology.ZeroCopulaStatus.impossible)

def Phenomena.Copulas.Typology.countBy (langs : List CopulaProfile) (pred : CopulaProfile → Bool) : Nat

Count of languages in a list matching a predicate.

Equations

• Phenomena.Copulas.Typology.countBy langs pred = (List.filter pred langs).length

theorem Phenomena.Copulas.Typology.english_adj_nonverbal : (english.predAdj == PredAdjStrategy.nonVerbal) = true

theorem Phenomena.Copulas.Typology.japanese_adj_mixed : (japanese.predAdj == PredAdjStrategy.mixed) = true

theorem Phenomena.Copulas.Typology.korean_adj_verbal : (korean.predAdj == PredAdjStrategy.verbal) = true

theorem Phenomena.Copulas.Typology.mandarin_adj_verbal : (mandarin.predAdj == PredAdjStrategy.verbal) = true

theorem Phenomena.Copulas.Typology.turkish_adj_verbal : (turkish.predAdj == PredAdjStrategy.verbal) = true

theorem Phenomena.Copulas.Typology.russian_adj_nonverbal : (russian.predAdj == PredAdjStrategy.nonVerbal) = true

theorem Phenomena.Copulas.Typology.english_noun_verbal : (english.predNoun == PredNounStrategy.verbal) = true

theorem Phenomena.Copulas.Typology.russian_noun_nonverbal : (russian.predNoun == PredNounStrategy.nonVerbal) = true

theorem Phenomena.Copulas.Typology.mandarin_noun_verbal : (mandarin.predNoun == PredNounStrategy.verbal) = true

theorem Phenomena.Copulas.Typology.tagalog_noun_nonverbal : (tagalog.predNoun == PredNounStrategy.nonVerbal) = true

theorem Phenomena.Copulas.Typology.swahili_noun_nonverbal : (swahili.predNoun == PredNounStrategy.nonVerbal) = true

theorem Phenomena.Copulas.Typology.english_nomLoc_identical : (english.nomLoc == NomLocStrategy.identical) = true

theorem Phenomena.Copulas.Typology.spanish_nomLoc_different : (spanish.nomLoc == NomLocStrategy.different) = true

theorem Phenomena.Copulas.Typology.irish_nomLoc_different : (irish.nomLoc == NomLocStrategy.different) = true

theorem Phenomena.Copulas.Typology.mandarin_nomLoc_different : (mandarin.nomLoc == NomLocStrategy.different) = true

theorem Phenomena.Copulas.Typology.english_no_zero : (english.zeroCopula == ZeroCopulaStatus.impossible) = true

theorem Phenomena.Copulas.Typology.russian_zero_restricted : (russian.zeroCopula == ZeroCopulaStatus.restricted) = true

theorem Phenomena.Copulas.Typology.hungarian_zero_restricted : (hungarian.zeroCopula == ZeroCopulaStatus.restricted) = true

theorem Phenomena.Copulas.Typology.tagalog_zero_widespread : (tagalog.zeroCopula == ZeroCopulaStatus.widespread) = true

theorem Phenomena.Copulas.Typology.arabic_zero_restricted : (arabic.zeroCopula == ZeroCopulaStatus.restricted) = true

theorem Phenomena.Copulas.Typology.sample_size : allLanguages.length = 20

Number of languages in our sample.

theorem Phenomena.Copulas.Typology.sample_verbal_adj_count : (countBy allLanguages fun (x : CopulaProfile) => x.hasVerbalAdj) = 7

Ch 117 distribution in our sample.

theorem Phenomena.Copulas.Typology.sample_mixed_adj_count : (countBy allLanguages fun (x : CopulaProfile) => x.predAdj == PredAdjStrategy.mixed) = 1

theorem Phenomena.Copulas.Typology.sample_nonverbal_adj_count : (countBy allLanguages fun (x : CopulaProfile) => x.predAdj == PredAdjStrategy.nonVerbal) = 12

theorem Phenomena.Copulas.Typology.sample_verbal_noun_count : (countBy allLanguages fun (x : CopulaProfile) => x.hasVerbalNounCopula) = 11

Ch 118 distribution in our sample.

theorem Phenomena.Copulas.Typology.sample_nonverbal_noun_count : (countBy allLanguages fun (x : CopulaProfile) => x.predNoun == PredNounStrategy.nonVerbal) = 9

theorem Phenomena.Copulas.Typology.sample_nomloc_different_count : (countBy allLanguages fun (x : CopulaProfile) => x.hasNomLocSplit) = 11

Ch 119 distribution in our sample.

theorem Phenomena.Copulas.Typology.sample_nomloc_identical_count : (countBy allLanguages fun (x : CopulaProfile) => x.nomLoc == NomLocStrategy.identical) = 9

theorem Phenomena.Copulas.Typology.sample_zero_impossible_count : (countBy allLanguages fun (x : CopulaProfile) => x.alwaysRequiresCopula) = 11

Ch 120 distribution in our sample.

theorem Phenomena.Copulas.Typology.sample_zero_restricted_count : (countBy allLanguages fun (x : CopulaProfile) => x.zeroCopula == ZeroCopulaStatus.restricted) = 6

theorem Phenomena.Copulas.Typology.sample_zero_widespread_count : (countBy allLanguages fun (x : CopulaProfile) => x.zeroCopula == ZeroCopulaStatus.widespread) = 3

theorem Phenomena.Copulas.Typology.verbal_adj_most_common : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F118A.PredicativeAdjectiveType) => x.value == Core.WALS.F118A.PredicativeAdjectiveType.verbalEncoding) Phenomena.Copulas.Typology.ch118✝).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F118A.PredicativeAdjectiveType) => x.value == Core.WALS.F118A.PredicativeAdjectiveType.nonverbalEncoding) Phenomena.Copulas.Typology.ch118✝¹).length ∧ (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F118A.PredicativeAdjectiveType) => x.value == Core.WALS.F118A.PredicativeAdjectiveType.verbalEncoding) Phenomena.Copulas.Typology.ch118✝²).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F118A.PredicativeAdjectiveType) => x.value == Core.WALS.F118A.PredicativeAdjectiveType.mixed) Phenomena.Copulas.Typology.ch118✝³).length

Ch 118: Verbal encoding is the most common strategy for predicative adjectives, exceeding both mixed and nonverbal encoding.

theorem Phenomena.Copulas.Typology.verbal_adj_plurality : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F118A.PredicativeAdjectiveType) => x.value == Core.WALS.F118A.PredicativeAdjectiveType.verbalEncoding) Phenomena.Copulas.Typology.ch118✝).length * 3 > Phenomena.Copulas.Typology.ch118✝¹.length

Ch 118: Verbal adjectives account for roughly 39% of the sample (151/386).

theorem Phenomena.Copulas.Typology.nonverbal_adj_vs_verbal : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F118A.PredicativeAdjectiveType) => x.value == Core.WALS.F118A.PredicativeAdjectiveType.verbalEncoding) Phenomena.Copulas.Typology.ch118✝).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F118A.PredicativeAdjectiveType) => x.value == Core.WALS.F118A.PredicativeAdjectiveType.nonverbalEncoding) Phenomena.Copulas.Typology.ch118✝¹).length

Ch 118: Nonverbal encoding (132) is less common than verbal encoding (151) for predicative adjectives, but the three values are fairly balanced across the 386-language sample.

theorem Phenomena.Copulas.Typology.no_adj_strategy_majority : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F118A.PredicativeAdjectiveType) => x.value == Core.WALS.F118A.PredicativeAdjectiveType.verbalEncoding) Phenomena.Copulas.Typology.ch118✝).length * 2 < Phenomena.Copulas.Typology.ch118✝¹.length

Ch 118: No single predicative adjective strategy is a strict majority.

theorem Phenomena.Copulas.Typology.nomloc_split_majority : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F119A.NominalLocationalPredication) => x.value == Core.WALS.F119A.NominalLocationalPredication.different) Phenomena.Copulas.Typology.ch119✝).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F119A.NominalLocationalPredication) => x.value == Core.WALS.F119A.NominalLocationalPredication.identical) Phenomena.Copulas.Typology.ch119✝¹).length

Ch 119: Using different strategies for nominal and locational predication is more common than using the same strategy. This means that languages typically distinguish "is a doctor" from "is in the room" with different grammatical means.

theorem Phenomena.Copulas.Typology.nomloc_split_supermajority : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F119A.NominalLocationalPredication) => x.value == Core.WALS.F119A.NominalLocationalPredication.different) Phenomena.Copulas.Typology.ch119✝).length > Phenomena.Copulas.Typology.ch119✝¹.length / 2

Ch 119: The split pattern accounts for a clear majority.

theorem Phenomena.Copulas.Typology.impossible_is_majority : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F120A.ZeroCopulaType) => x.value == Core.WALS.F120A.ZeroCopulaType.impossible) Phenomena.Copulas.Typology.ch120✝).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F120A.ZeroCopulaType) => x.value == Core.WALS.F120A.ZeroCopulaType.possible) Phenomena.Copulas.Typology.ch120✝¹).length

Ch 120: "Impossible" (copula always required) is the majority value.

theorem Phenomena.Copulas.Typology.impossible_over_half : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F120A.ZeroCopulaType) => x.value == Core.WALS.F120A.ZeroCopulaType.impossible) Phenomena.Copulas.Typology.ch120✝).length > Phenomena.Copulas.Typology.ch120✝¹.length / 2

Ch 120: "Impossible" accounts for more than half the sample.

theorem Phenomena.Copulas.Typology.verbal_adj_nonverbal_noun : have verbalAdjNonverbalNoun := List.filter (fun (p : CopulaProfile) => p.predAdj == PredAdjStrategy.verbal && p.predNoun == PredNounStrategy.nonVerbal) allLanguages; verbalAdjNonverbalNoun.length ≥ 3

In our sample, languages with verbal adjectives (Ch 117) tend NOT to also have verbal copulas for nouns -- they often use a different strategy for nominal predication. This is because the verbal adjective strategy eliminates the need for a copula with adjectives but does not necessarily provide a copula for nouns.

Count of languages with verbal adjectives AND non-verbal noun predication.

theorem Phenomena.Copulas.Typology.restricted_zero_has_copula_forms : have restricted := List.filter (fun (x : CopulaProfile) => x.zeroCopula == ZeroCopulaStatus.restricted) allLanguages; (restricted.all fun (x : CopulaProfile) => decide (x.copulaForms.length > 0)) = true

In our sample, languages with restricted zero copula (Ch 120) allow zero copula in present tense but require an overt copula in past tense. Russian, Arabic, Hungarian, and Turkish all exhibit this pattern: present tense allows copula dropping but past requires an overt form.

All restricted-zero-copula languages in our sample have overt past-tense copula forms.

theorem Phenomena.Copulas.Typology.nonverbal_noun_implies_zero_copula : have nonverbalNoun := List.filter (fun (x : CopulaProfile) => x.predNoun == PredNounStrategy.nonVerbal) allLanguages; (nonverbalNoun.all fun (x : CopulaProfile) => x.allowsZeroCopula) = true

Languages that use non-verbal noun predication (Ch 118) tend to allow zero copula (Ch 120). In our sample, every language with non-verbal noun predication allows zero copula (restricted or widespread).

theorem Phenomena.Copulas.Typology.verbal_adj_tends_nomloc_split : have verbalAdj := List.filter (fun (x : CopulaProfile) => x.hasVerbalAdj) allLanguages; have splitNomLoc := List.filter (fun (x : CopulaProfile) => x.hasNomLocSplit) verbalAdj; splitNomLoc.length > verbalAdj.length / 2

Languages with verbal adjectives tend to split nominal and locational predication (Ch 119 = different). In our sample, the majority of verbal-adjective languages have different nom-loc strategies.

theorem Phenomena.Copulas.Typology.copula_required_tends_identical : have required := List.filter (fun (x : CopulaProfile) => x.alwaysRequiresCopula) allLanguages; have identical := List.filter (fun (x : CopulaProfile) => x.nomLoc == NomLocStrategy.identical) required; identical.length ≥ required.length / 2

Languages where the copula is always required (Ch 120 = impossible) are more likely to use the SAME copula for nominal and locational predication (Ch 119 = identical) than languages that allow zero copula.

Among copula-requiring languages in our sample, at least half use the same strategy for both predication types.

def Phenomena.Copulas.Typology.westernEuropean : List CopulaProfile

Western European languages (English, French, German) share a common copula profile: non-verbal adjectives, verbal nominal copula, and no zero copula. This is the "Standard Average European" pattern.

Equations

• Phenomena.Copulas.Typology.westernEuropean = [Phenomena.Copulas.Typology.english, Phenomena.Copulas.Typology.french, Phenomena.Copulas.Typology.german]

theorem Phenomena.Copulas.Typology.western_european_nonverbal_adj : (westernEuropean.all fun (x : CopulaProfile) => x.predAdj == PredAdjStrategy.nonVerbal) = true

theorem Phenomena.Copulas.Typology.western_european_verbal_noun : (westernEuropean.all fun (x : CopulaProfile) => x.predNoun == PredNounStrategy.verbal) = true

theorem Phenomena.Copulas.Typology.western_european_no_zero : (westernEuropean.all fun (x : CopulaProfile) => x.alwaysRequiresCopula) = true

theorem Phenomena.Copulas.Typology.verbal_both_count : have verbalBoth := List.filter (fun (p : CopulaProfile) => p.predAdj == PredAdjStrategy.verbal && p.predNoun == PredNounStrategy.verbal) allLanguages; verbalBoth.length ≥ 3

Cross-chapter interaction: languages with verbal adjectives (Ch 117) and verbal noun predication (Ch 118) are the only languages in our sample that can have verbal predication for BOTH adjectives and nouns with different copula forms.

theorem Phenomena.Copulas.Typology.mixed_adj_implies_verbal_noun : have mixedAdj := List.filter (fun (x : CopulaProfile) => x.predAdj == PredAdjStrategy.mixed) allLanguages; (mixedAdj.all fun (x : CopulaProfile) => x.predNoun == PredNounStrategy.verbal) = true

In our sample, no language has mixed adjectives (Ch 117) AND non-verbal noun predication (Ch 118). Mixed adjective languages tend to have verbal copulas for nouns.

theorem Phenomena.Copulas.Typology.widespread_zero_implies_nonverbal_noun : have widespread := List.filter (fun (x : CopulaProfile) => x.zeroCopula == ZeroCopulaStatus.widespread) allLanguages; (widespread.all fun (x : CopulaProfile) => x.predNoun == PredNounStrategy.nonVerbal) = true

Languages with widespread zero copula (Ch 120) always allow non-verbal nominal predication (Ch 118). This is logically expected: if zero copula is the norm, nominal predication IS non-verbal.

theorem Phenomena.Copulas.Typology.stassen_implication_noun_zero : (allLanguages.all fun (p : CopulaProfile) => if (p.predNoun == PredNounStrategy.nonVerbal) = true then p.allowsZeroCopula else true) = true

Stassen's Implicational Universal: if a language has non-verbal encoding for nouns (Ch 118), it allows some form of zero copula (Ch 120 = restricted or widespread). In our sample this holds without exception.

theorem Phenomena.Copulas.Typology.no_zero_implies_verbal_noun : (allLanguages.all fun (p : CopulaProfile) => if (p.zeroCopula == ZeroCopulaStatus.impossible) = true then p.predNoun == PredNounStrategy.verbal else true) = true

Converse of Stassen's implication: if a language has zero copula impossible (Ch 120), then it uses verbal nominal predication (Ch 118). This is the contrapositive of the above.

def Phenomena.Copulas.Typology.CopulaProfile.hasSplitPredication (p : CopulaProfile) : Bool

A split predication language uses different strategies for at least two of: adjectival, nominal, and locational predication.

Equations

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

theorem Phenomena.Copulas.Typology.split_predication_common : (countBy allLanguages fun (x : CopulaProfile) => x.hasSplitPredication) ≥ 12

Count of languages in our sample with some form of split predication.

theorem Phenomena.Copulas.Typology.spanish_irish_clear_split : spanish.hasNomLocSplit = true ∧ irish.hasNomLocSplit = true

Spanish and Irish exemplify the clearest nom-loc splits: both have two distinct copulas that partition predicate types.

theorem Phenomena.Copulas.Typology.mandarin_three_way_split : (mandarin.predAdj == PredAdjStrategy.verbal) = true ∧ (mandarin.predNoun == PredNounStrategy.verbal) = true ∧ (mandarin.nomLoc == NomLocStrategy.different) = true

Mandarin exemplifies a three-way split: adjectives are verbal (no copula), nouns require shi, locations use zai. Three different strategies for three predicate types.

theorem Phenomena.Copulas.Typology.nomloc_split_languages_have_distinct_forms : have splitLangs := List.filter (fun (x : CopulaProfile) => x.hasNomLocSplit) allLanguages; (splitLangs.all fun (x : CopulaProfile) => decide (x.copulaForms.length ≥ 1)) = true

Languages that split nominal and locational predication (Ch 119) often use existential verbs for locational predication. In our sample, several nom-loc-split languages have distinct existential/locational forms in their copula inventory.

def Phenomena.Copulas.Typology.eastAsian : List CopulaProfile

East and Southeast Asian languages (Japanese, Korean, Mandarin, Thai) all have verbal adjectives. This is an areal feature of the region.

Equations

• Phenomena.Copulas.Typology.eastAsian = [Phenomena.Copulas.Typology.japanese, Phenomena.Copulas.Typology.korean, Phenomena.Copulas.Typology.mandarin, Phenomena.Copulas.Typology.thai]

theorem Phenomena.Copulas.Typology.east_asian_verbal_or_mixed_adj : (eastAsian.all fun (p : CopulaProfile) => p.predAdj == PredAdjStrategy.verbal || p.predAdj == PredAdjStrategy.mixed) = true

def Phenomena.Copulas.Typology.semitic : List CopulaProfile

Semitic languages (Arabic, Hebrew) share a copula profile: non-verbal adjectives, non-verbal nominal predication, and restricted zero copula (present tense only).

Equations

• Phenomena.Copulas.Typology.semitic = [Phenomena.Copulas.Typology.arabic, Phenomena.Copulas.Typology.hebrew]

theorem Phenomena.Copulas.Typology.semitic_nonverbal_adj : (semitic.all fun (x : CopulaProfile) => x.predAdj == PredAdjStrategy.nonVerbal) = true

theorem Phenomena.Copulas.Typology.semitic_nonverbal_noun : (semitic.all fun (x : CopulaProfile) => x.predNoun == PredNounStrategy.nonVerbal) = true

theorem Phenomena.Copulas.Typology.semitic_restricted_zero : (semitic.all fun (x : CopulaProfile) => x.zeroCopula == ZeroCopulaStatus.restricted) = true

theorem Phenomena.Copulas.Typology.east_asian_nomloc_split : (eastAsian.all fun (x : CopulaProfile) => x.hasNomLocSplit) = true

East Asian languages all split nominal and locational predication.

theorem Phenomena.Copulas.Typology.sample_verbal_copula_count : (countBy allLanguages fun (x : CopulaProfile) => x.copulaType == CopulaType.verbalCopula) = 11

Distribution of copula types in our sample.

theorem Phenomena.Copulas.Typology.sample_zero_copula_type_count : (countBy allLanguages fun (x : CopulaProfile) => x.copulaType == CopulaType.zero) = 4

theorem Phenomena.Copulas.Typology.sample_particle_copula_count : (countBy allLanguages fun (x : CopulaProfile) => x.copulaType == CopulaType.particle) = 4

theorem Phenomena.Copulas.Typology.sample_pronominal_copula_count : (countBy allLanguages fun (x : CopulaProfile) => x.copulaType == CopulaType.pronominalCopula) = 1

theorem Phenomena.Copulas.Typology.verbal_copula_most_common : ((countBy allLanguages fun (x : CopulaProfile) => x.copulaType == CopulaType.verbalCopula) > countBy allLanguages fun (x : CopulaProfile) => x.copulaType == CopulaType.particle) ∧ ((countBy allLanguages fun (x : CopulaProfile) => x.copulaType == CopulaType.verbalCopula) > countBy allLanguages fun (x : CopulaProfile) => x.copulaType == CopulaType.zero) ∧ (countBy allLanguages fun (x : CopulaProfile) => x.copulaType == CopulaType.verbalCopula) > countBy allLanguages fun (x : CopulaProfile) => x.copulaType == CopulaType.pronominalCopula

Verbal copulas are the most common copula type in our sample.

theorem Phenomena.Copulas.Typology.wals_f117a_total : Phenomena.Copulas.Typology.ch117✝.length = 240

F117A: 240 languages (predicative possession).

theorem Phenomena.Copulas.Typology.wals_f118a_total : Phenomena.Copulas.Typology.ch118✝.length = 386

F118A: 386 languages (predicative adjectives).

theorem Phenomena.Copulas.Typology.wals_f119a_total : Phenomena.Copulas.Typology.ch119✝.length = 386

F119A: 386 languages (nominal and locational predication).

theorem Phenomena.Copulas.Typology.wals_f120a_total : Phenomena.Copulas.Typology.ch120✝.length = 386

F120A: 386 languages (zero copula for predicate nominals).

theorem Phenomena.Copulas.Typology.wals_f118_f119_f120_same_sample : Phenomena.Copulas.Typology.ch118✝.length = Phenomena.Copulas.Typology.ch119✝.length ∧ Phenomena.Copulas.Typology.ch119✝¹.length = Phenomena.Copulas.Typology.ch120✝.length

F118A, F119A, F120A all use the same 386-language sample.

theorem Phenomena.Copulas.Typology.wals_f118a_verbal_count : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F118A.PredicativeAdjectiveType) => x.value == Core.WALS.F118A.PredicativeAdjectiveType.verbalEncoding) Phenomena.Copulas.Typology.ch118✝).length = 151

F118A distribution: predicative adjectives.

theorem Phenomena.Copulas.Typology.wals_f118a_nonverbal_count : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F118A.PredicativeAdjectiveType) => x.value == Core.WALS.F118A.PredicativeAdjectiveType.nonverbalEncoding) Phenomena.Copulas.Typology.ch118✝).length = 132

theorem Phenomena.Copulas.Typology.wals_f118a_mixed_count : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F118A.PredicativeAdjectiveType) => x.value == Core.WALS.F118A.PredicativeAdjectiveType.mixed) Phenomena.Copulas.Typology.ch118✝).length = 103

theorem Phenomena.Copulas.Typology.wals_f119a_different_count : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F119A.NominalLocationalPredication) => x.value == Core.WALS.F119A.NominalLocationalPredication.different) Phenomena.Copulas.Typology.ch119✝).length = 269

F119A distribution: nominal and locational predication.

theorem Phenomena.Copulas.Typology.wals_f119a_identical_count : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F119A.NominalLocationalPredication) => x.value == Core.WALS.F119A.NominalLocationalPredication.identical) Phenomena.Copulas.Typology.ch119✝).length = 117

theorem Phenomena.Copulas.Typology.wals_f120a_impossible_count : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F120A.ZeroCopulaType) => x.value == Core.WALS.F120A.ZeroCopulaType.impossible) Phenomena.Copulas.Typology.ch120✝).length = 211

F120A distribution: zero copula for predicate nominals.

theorem Phenomena.Copulas.Typology.wals_f120a_possible_count : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F120A.ZeroCopulaType) => x.value == Core.WALS.F120A.ZeroCopulaType.possible) Phenomena.Copulas.Typology.ch120✝).length = 175

theorem Phenomena.Copulas.Typology.wals_f117a_locational_count : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F117A.PredicativePossession) => x.value == Core.WALS.F117A.PredicativePossession.locational) Phenomena.Copulas.Typology.ch117✝).length = 48

F117A distribution: predicative possession.

theorem Phenomena.Copulas.Typology.wals_f117a_genitive_count : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F117A.PredicativePossession) => x.value == Core.WALS.F117A.PredicativePossession.genitive) Phenomena.Copulas.Typology.ch117✝).length = 22

theorem Phenomena.Copulas.Typology.wals_f117a_topic_count : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F117A.PredicativePossession) => x.value == Core.WALS.F117A.PredicativePossession.topic) Phenomena.Copulas.Typology.ch117✝).length = 48

theorem Phenomena.Copulas.Typology.wals_f117a_conjunctional_count : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F117A.PredicativePossession) => x.value == Core.WALS.F117A.PredicativePossession.conjunctional) Phenomena.Copulas.Typology.ch117✝).length = 59

theorem Phenomena.Copulas.Typology.wals_f117a_have_count : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F117A.PredicativePossession) => x.value == Core.WALS.F117A.PredicativePossession.have) Phenomena.Copulas.Typology.ch117✝).length = 63

theorem Phenomena.Copulas.Typology.english_f118a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F118A.PredicativeAdjectiveType) => Phenomena.Copulas.Typology.fromWALS118A✝ x.value) (Core.WALS.F118A.lookup "eng") = some english.predAdj

theorem Phenomena.Copulas.Typology.french_f118a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F118A.PredicativeAdjectiveType) => Phenomena.Copulas.Typology.fromWALS118A✝ x.value) (Core.WALS.F118A.lookup "fre") = some french.predAdj

theorem Phenomena.Copulas.Typology.spanish_f118a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F118A.PredicativeAdjectiveType) => Phenomena.Copulas.Typology.fromWALS118A✝ x.value) (Core.WALS.F118A.lookup "spa") = some spanish.predAdj

theorem Phenomena.Copulas.Typology.russian_f118a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F118A.PredicativeAdjectiveType) => Phenomena.Copulas.Typology.fromWALS118A✝ x.value) (Core.WALS.F118A.lookup "rus") = some russian.predAdj

theorem Phenomena.Copulas.Typology.finnish_f118a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F118A.PredicativeAdjectiveType) => Phenomena.Copulas.Typology.fromWALS118A✝ x.value) (Core.WALS.F118A.lookup "fin") = some finnish.predAdj

theorem Phenomena.Copulas.Typology.japanese_f118a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F118A.PredicativeAdjectiveType) => Phenomena.Copulas.Typology.fromWALS118A✝ x.value) (Core.WALS.F118A.lookup "jpn") = some japanese.predAdj

theorem Phenomena.Copulas.Typology.mandarin_f118a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F118A.PredicativeAdjectiveType) => Phenomena.Copulas.Typology.fromWALS118A✝ x.value) (Core.WALS.F118A.lookup "mnd") = some mandarin.predAdj

theorem Phenomena.Copulas.Typology.hindi_f118a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F118A.PredicativeAdjectiveType) => Phenomena.Copulas.Typology.fromWALS118A✝ x.value) (Core.WALS.F118A.lookup "hin") = some hindiUrdu.predAdj

theorem Phenomena.Copulas.Typology.tagalog_f118a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F118A.PredicativeAdjectiveType) => Phenomena.Copulas.Typology.fromWALS118A✝ x.value) (Core.WALS.F118A.lookup "tag") = some tagalog.predAdj

theorem Phenomena.Copulas.Typology.irish_f118a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F118A.PredicativeAdjectiveType) => Phenomena.Copulas.Typology.fromWALS118A✝ x.value) (Core.WALS.F118A.lookup "iri") = some irish.predAdj

theorem Phenomena.Copulas.Typology.hungarian_f118a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F118A.PredicativeAdjectiveType) => Phenomena.Copulas.Typology.fromWALS118A✝ x.value) (Core.WALS.F118A.lookup "hun") = some hungarian.predAdj

theorem Phenomena.Copulas.Typology.thai_f118a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F118A.PredicativeAdjectiveType) => Phenomena.Copulas.Typology.fromWALS118A✝ x.value) (Core.WALS.F118A.lookup "tha") = some thai.predAdj

theorem Phenomena.Copulas.Typology.yoruba_f118a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F118A.PredicativeAdjectiveType) => Phenomena.Copulas.Typology.fromWALS118A✝ x.value) (Core.WALS.F118A.lookup "yor") = some yoruba.predAdj

theorem Phenomena.Copulas.Typology.hebrew_f118a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F118A.PredicativeAdjectiveType) => Phenomena.Copulas.Typology.fromWALS118A✝ x.value) (Core.WALS.F118A.lookup "heb") = some hebrew.predAdj

theorem Phenomena.Copulas.Typology.arabic_f118a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F118A.PredicativeAdjectiveType) => Phenomena.Copulas.Typology.fromWALS118A✝ x.value) (Core.WALS.F118A.lookup "aeg") = some arabic.predAdj

theorem Phenomena.Copulas.Typology.quechua_f118a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F118A.PredicativeAdjectiveType) => Phenomena.Copulas.Typology.fromWALS118A✝ x.value) (Core.WALS.F118A.lookup "qcu") = some quechua.predAdj

theorem Phenomena.Copulas.Typology.english_f119a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F119A.NominalLocationalPredication) => Phenomena.Copulas.Typology.fromWALS119A✝ x.value) (Core.WALS.F119A.lookup "eng") = some english.nomLoc

theorem Phenomena.Copulas.Typology.french_f119a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F119A.NominalLocationalPredication) => Phenomena.Copulas.Typology.fromWALS119A✝ x.value) (Core.WALS.F119A.lookup "fre") = some french.nomLoc

theorem Phenomena.Copulas.Typology.spanish_f119a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F119A.NominalLocationalPredication) => Phenomena.Copulas.Typology.fromWALS119A✝ x.value) (Core.WALS.F119A.lookup "spa") = some spanish.nomLoc

theorem Phenomena.Copulas.Typology.russian_f119a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F119A.NominalLocationalPredication) => Phenomena.Copulas.Typology.fromWALS119A✝ x.value) (Core.WALS.F119A.lookup "rus") = some russian.nomLoc

theorem Phenomena.Copulas.Typology.finnish_f119a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F119A.NominalLocationalPredication) => Phenomena.Copulas.Typology.fromWALS119A✝ x.value) (Core.WALS.F119A.lookup "fin") = some finnish.nomLoc

theorem Phenomena.Copulas.Typology.japanese_f119a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F119A.NominalLocationalPredication) => Phenomena.Copulas.Typology.fromWALS119A✝ x.value) (Core.WALS.F119A.lookup "jpn") = some japanese.nomLoc

theorem Phenomena.Copulas.Typology.mandarin_f119a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F119A.NominalLocationalPredication) => Phenomena.Copulas.Typology.fromWALS119A✝ x.value) (Core.WALS.F119A.lookup "mnd") = some mandarin.nomLoc

theorem Phenomena.Copulas.Typology.korean_f119a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F119A.NominalLocationalPredication) => Phenomena.Copulas.Typology.fromWALS119A✝ x.value) (Core.WALS.F119A.lookup "kor") = some korean.nomLoc

theorem Phenomena.Copulas.Typology.hindi_f119a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F119A.NominalLocationalPredication) => Phenomena.Copulas.Typology.fromWALS119A✝ x.value) (Core.WALS.F119A.lookup "hin") = some hindiUrdu.nomLoc

theorem Phenomena.Copulas.Typology.irish_f119a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F119A.NominalLocationalPredication) => Phenomena.Copulas.Typology.fromWALS119A✝ x.value) (Core.WALS.F119A.lookup "iri") = some irish.nomLoc

theorem Phenomena.Copulas.Typology.hungarian_f119a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F119A.NominalLocationalPredication) => Phenomena.Copulas.Typology.fromWALS119A✝ x.value) (Core.WALS.F119A.lookup "hun") = some hungarian.nomLoc

theorem Phenomena.Copulas.Typology.thai_f119a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F119A.NominalLocationalPredication) => Phenomena.Copulas.Typology.fromWALS119A✝ x.value) (Core.WALS.F119A.lookup "tha") = some thai.nomLoc

theorem Phenomena.Copulas.Typology.yoruba_f119a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F119A.NominalLocationalPredication) => Phenomena.Copulas.Typology.fromWALS119A✝ x.value) (Core.WALS.F119A.lookup "yor") = some yoruba.nomLoc

theorem Phenomena.Copulas.Typology.quechua_f119a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F119A.NominalLocationalPredication) => Phenomena.Copulas.Typology.fromWALS119A✝ x.value) (Core.WALS.F119A.lookup "qcu") = some quechua.nomLoc

theorem Phenomena.Copulas.Typology.english_f120a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F120A.ZeroCopulaType) => Phenomena.Copulas.Typology.fromWALS120A✝ x.value) (Core.WALS.F120A.lookup "eng") = some (some english.zeroCopula)

theorem Phenomena.Copulas.Typology.french_f120a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F120A.ZeroCopulaType) => Phenomena.Copulas.Typology.fromWALS120A✝ x.value) (Core.WALS.F120A.lookup "fre") = some (some french.zeroCopula)

theorem Phenomena.Copulas.Typology.spanish_f120a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F120A.ZeroCopulaType) => Phenomena.Copulas.Typology.fromWALS120A✝ x.value) (Core.WALS.F120A.lookup "spa") = some (some spanish.zeroCopula)

theorem Phenomena.Copulas.Typology.finnish_f120a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F120A.ZeroCopulaType) => Phenomena.Copulas.Typology.fromWALS120A✝ x.value) (Core.WALS.F120A.lookup "fin") = some (some finnish.zeroCopula)

theorem Phenomena.Copulas.Typology.japanese_f120a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F120A.ZeroCopulaType) => Phenomena.Copulas.Typology.fromWALS120A✝ x.value) (Core.WALS.F120A.lookup "jpn") = some (some japanese.zeroCopula)

theorem Phenomena.Copulas.Typology.korean_f120a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F120A.ZeroCopulaType) => Phenomena.Copulas.Typology.fromWALS120A✝ x.value) (Core.WALS.F120A.lookup "kor") = some (some korean.zeroCopula)

theorem Phenomena.Copulas.Typology.mandarin_f120a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F120A.ZeroCopulaType) => Phenomena.Copulas.Typology.fromWALS120A✝ x.value) (Core.WALS.F120A.lookup "mnd") = some (some mandarin.zeroCopula)

theorem Phenomena.Copulas.Typology.irish_f120a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F120A.ZeroCopulaType) => Phenomena.Copulas.Typology.fromWALS120A✝ x.value) (Core.WALS.F120A.lookup "iri") = some (some irish.zeroCopula)

theorem Phenomena.Copulas.Typology.hindi_f120a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F120A.ZeroCopulaType) => Phenomena.Copulas.Typology.fromWALS120A✝ x.value) (Core.WALS.F120A.lookup "hin") = some (some hindiUrdu.zeroCopula)

theorem Phenomena.Copulas.Typology.russian_f120a_consistent : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F120A.ZeroCopulaType) => Phenomena.Copulas.Typology.wals120A_allowsZero✝ x.value) (Core.WALS.F120A.lookup "rus") = some russian.allowsZeroCopula

theorem Phenomena.Copulas.Typology.hungarian_f120a_consistent : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F120A.ZeroCopulaType) => Phenomena.Copulas.Typology.wals120A_allowsZero✝ x.value) (Core.WALS.F120A.lookup "hun") = some hungarian.allowsZeroCopula

theorem Phenomena.Copulas.Typology.arabic_f120a_consistent : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F120A.ZeroCopulaType) => Phenomena.Copulas.Typology.wals120A_allowsZero✝ x.value) (Core.WALS.F120A.lookup "aeg") = some arabic.allowsZeroCopula

theorem Phenomena.Copulas.Typology.hebrew_f120a_consistent : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F120A.ZeroCopulaType) => Phenomena.Copulas.Typology.wals120A_allowsZero✝ x.value) (Core.WALS.F120A.lookup "heb") = some hebrew.allowsZeroCopula

theorem Phenomena.Copulas.Typology.quechua_f120a_consistent : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F120A.ZeroCopulaType) => Phenomena.Copulas.Typology.wals120A_allowsZero✝ x.value) (Core.WALS.F120A.lookup "qcu") = some quechua.allowsZeroCopula

theorem Phenomena.Copulas.Typology.english_f117a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F117A.PredicativePossession) => x.value) (Core.WALS.F117A.lookup "eng") = some Core.WALS.F117A.PredicativePossession.have

theorem Phenomena.Copulas.Typology.spanish_f117a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F117A.PredicativePossession) => x.value) (Core.WALS.F117A.lookup "spa") = some Core.WALS.F117A.PredicativePossession.have

theorem Phenomena.Copulas.Typology.finnish_f117a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F117A.PredicativePossession) => x.value) (Core.WALS.F117A.lookup "fin") = some Core.WALS.F117A.PredicativePossession.locational

theorem Phenomena.Copulas.Typology.russian_f117a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F117A.PredicativePossession) => x.value) (Core.WALS.F117A.lookup "rus") = some Core.WALS.F117A.PredicativePossession.locational

theorem Phenomena.Copulas.Typology.japanese_f117a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F117A.PredicativePossession) => x.value) (Core.WALS.F117A.lookup "jpn") = some Core.WALS.F117A.PredicativePossession.locational

theorem Phenomena.Copulas.Typology.korean_f117a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F117A.PredicativePossession) => x.value) (Core.WALS.F117A.lookup "kor") = some Core.WALS.F117A.PredicativePossession.locational

theorem Phenomena.Copulas.Typology.mandarin_f117a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F117A.PredicativePossession) => x.value) (Core.WALS.F117A.lookup "mnd") = some Core.WALS.F117A.PredicativePossession.topic

theorem Phenomena.Copulas.Typology.turkish_f117a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F117A.PredicativePossession) => x.value) (Core.WALS.F117A.lookup "tur") = some Core.WALS.F117A.PredicativePossession.genitive

theorem Phenomena.Copulas.Typology.hindi_f117a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F117A.PredicativePossession) => x.value) (Core.WALS.F117A.lookup "hin") = some Core.WALS.F117A.PredicativePossession.locational

theorem Phenomena.Copulas.Typology.hungarian_f117a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F117A.PredicativePossession) => x.value) (Core.WALS.F117A.lookup "hun") = some Core.WALS.F117A.PredicativePossession.locational

theorem Phenomena.Copulas.Typology.hebrew_f117a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F117A.PredicativePossession) => x.value) (Core.WALS.F117A.lookup "heb") = some Core.WALS.F117A.PredicativePossession.locational

theorem Phenomena.Copulas.Typology.irish_f117a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F117A.PredicativePossession) => x.value) (Core.WALS.F117A.lookup "iri") = some Core.WALS.F117A.PredicativePossession.locational

theorem Phenomena.Copulas.Typology.swahili_f117a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F117A.PredicativePossession) => x.value) (Core.WALS.F117A.lookup "swa") = some Core.WALS.F117A.PredicativePossession.conjunctional

theorem Phenomena.Copulas.Typology.tagalog_f117a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F117A.PredicativePossession) => x.value) (Core.WALS.F117A.lookup "tag") = some Core.WALS.F117A.PredicativePossession.topic

theorem Phenomena.Copulas.Typology.thai_f117a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F117A.PredicativePossession) => x.value) (Core.WALS.F117A.lookup "tha") = some Core.WALS.F117A.PredicativePossession.topic

theorem Phenomena.Copulas.Typology.yoruba_f117a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F117A.PredicativePossession) => x.value) (Core.WALS.F117A.lookup "yor") = some Core.WALS.F117A.PredicativePossession.have

theorem Phenomena.Copulas.Typology.arabic_f117a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F117A.PredicativePossession) => x.value) (Core.WALS.F117A.lookup "aeg") = some Core.WALS.F117A.PredicativePossession.locational