Cross-Linguistic Typology of Coordination

Three complementary typological perspectives on coordination:

1. Structural Typology

Classifies coordination by overt form:

• Syndesis: asyndetic (A B), monosyndetic (A co-B), bisyndetic (co-A co-B)
• Coordinator position: prepositive (co-A) vs postpositive (A-co)
• Universal gap: the pattern co-A B is unattested (@cite{haspelmath-2007}; sample: @cite{stassen-2000}, n=260)
• Diachronic sources: comitative ("with") -> monosyndetic J; additive focus particle ("also") -> bisyndetic MU

2. Semantic Decomposition (@cite{mitrovic-sauerland-2014}, @cite{mitrovic-sauerland-2016})

Classifies by underlying semantic structure:

• J (set intersection) + MU (subset/additive) + type-shifter
• Languages vary in which pieces are overtly realized

3. WALS Typological Features (Chapters 56, 63, 64)

Three WALS features capture cross-linguistic variation in coordination:

Ch 56: Conjunctions and Universal Quantifiers (@cite{dryer-haspelmath-2013})

Whether a language's conjunction marker ("and") is formally similar to its universal quantifier ("all/every"). Three values:

• Formally different: "and" and "all" are unrelated forms (40/116)
• Formally similar, without interrogative: "and"/"all" are similar but the interrogative ("what/who") is different (33/116)
• Formally similar, with interrogative: "and"/"all"/"wh" are all formally similar (43/116)

Ch 63: Noun Phrase Conjunction (@cite{dryer-haspelmath-2013})

Whether a language's NP conjunction marker ("and") is the same as its comitative marker ("with"). Two values:

• 'And' different from 'with': distinct forms (131/234)
• 'And' identical to 'with': same form for both (103/234)

Ch 64: Nominal and Verbal Conjunction (@cite{dryer-haspelmath-2013})

Whether a language uses the same marker for NP conjunction ("A and B") and VP/clausal conjunction ("sang and danced"). Three values:

• Identity: same marker for both (161/301)
• Differentiation: different markers (125/301)
• Both expressed by juxtaposition: no overt marker for either (15/301)

Connection

Haspelmath's structural categories map onto M&S's semantic pieces:

• Monosyndetic medial (A co-B) = J-only (comitative source)
• Bisyndetic postpositive (A-co B-co) = MU-only (focus particle source)
• Bisyndetic mixed (co-A co-B, A-co co-B) = J-MU (both sources)

The MU particle in conjunction is typically the SAME morpheme as the language's additive/focus particle, confirming the diachronic link.

The WALS Ch 63 feature (and = with) connects directly to the diachronic comitative source: languages where "and" IS "with" are precisely those where the comitative-to-coordinator grammaticalization is still transparent.

inductive Phenomena.Coordination.Typology.Syndesis : Type

Syndesis: presence and number of overt coordinators (Haspelmath §1).

• asyndetic : Syndesis
• monosyndetic : Syndesis
• bisyndetic : Syndesis

instance Phenomena.Coordination.Typology.instDecidableEqSyndesis : DecidableEq Syndesis

Equations

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

def Phenomena.Coordination.Typology.instBEqSyndesis.beq : Syndesis → Syndesis → Bool

Equations

• Phenomena.Coordination.Typology.instBEqSyndesis.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Coordination.Typology.instBEqSyndesis : BEq Syndesis

Equations

• Phenomena.Coordination.Typology.instBEqSyndesis = { beq := Phenomena.Coordination.Typology.instBEqSyndesis.beq }

instance Phenomena.Coordination.Typology.instReprSyndesis : Repr Syndesis

Equations

• Phenomena.Coordination.Typology.instReprSyndesis = { reprPrec := Phenomena.Coordination.Typology.instReprSyndesis.repr }

def Phenomena.Coordination.Typology.instReprSyndesis.repr : Syndesis → ℕ → Std.Format

Equations

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

inductive Phenomena.Coordination.Typology.CoordinatorPosition : Type

Coordinator position relative to its coordinand (Haspelmath §1.2).

@cite{haspelmath-2007} notes that co-A B (prepositive on first coordinand only) is unattested (cf. @cite{stassen-2000}, n=260). This is the one logically possible monosyndetic pattern that never occurs.

• prepositive : CoordinatorPosition
• postpositive : CoordinatorPosition

instance Phenomena.Coordination.Typology.instDecidableEqCoordinatorPosition : DecidableEq CoordinatorPosition

Equations

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

def Phenomena.Coordination.Typology.instBEqCoordinatorPosition.beq : CoordinatorPosition → CoordinatorPosition → Bool

Equations

• Phenomena.Coordination.Typology.instBEqCoordinatorPosition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Coordination.Typology.instBEqCoordinatorPosition : BEq CoordinatorPosition

Equations

• Phenomena.Coordination.Typology.instBEqCoordinatorPosition = { beq := Phenomena.Coordination.Typology.instBEqCoordinatorPosition.beq }

instance Phenomena.Coordination.Typology.instReprCoordinatorPosition : Repr CoordinatorPosition

Equations

• Phenomena.Coordination.Typology.instReprCoordinatorPosition = { reprPrec := Phenomena.Coordination.Typology.instReprCoordinatorPosition.repr }

def Phenomena.Coordination.Typology.instReprCoordinatorPosition.repr : CoordinatorPosition → ℕ → Std.Format

Equations

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

inductive Phenomena.Coordination.Typology.CoordPattern : Type

Structural pattern for binary coordination (Haspelmath (17)).

Monosyndetic: 3 attested patterns (of 4 logically possible). A co-B (prepositive on 2nd: English "A and B") A-co B (postpositive on 1st: Tibetan "A-daŋ B") A B-co (postpositive on 2nd: Latin "A B-que")

co-A B — UNATTESTED (@cite{haspelmath-2007}; cf. @cite{stassen-2000}, n=260)

Bisyndetic: 4 attested patterns. co-A co-B (prepositive: Yoruba "àtí A àtí B") A-co B-co (postpositive: Martuthunira "A-thurti B-thurti") A-co co-B (mixed: Homeric Greek "A-te kaì B") co-A B-co (mixed: Latin "et A B-que")

• a_co_b : CoordPattern

  A co-B: medial prepositive (English "A and B", Lango "A kèdè B")

• a'co_b : CoordPattern

  A-co B: medial postpositive on 1st (Tibetan "A-daŋ B")

• a_b'co : CoordPattern

  A B-co: final postpositive (Latin "senatus populus-que")

• co'a_co'b : CoordPattern

  co-A co-B: prepositive bisyndetic (Yoruba "àtí A àtí B")

• a'co_b'co : CoordPattern

  A-co B-co: postpositive bisyndetic (Martuthunira "A-thurti B-thurti")

• a'co_co'b : CoordPattern

  A-co co-B: mixed bisyndetic (Homeric Greek "A-te kaì B")

• co'a_b'co : CoordPattern

  co-A B-co: mixed bisyndetic (Latin "et A B-que")

instance Phenomena.Coordination.Typology.instDecidableEqCoordPattern : DecidableEq CoordPattern

Equations

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

def Phenomena.Coordination.Typology.instBEqCoordPattern.beq : CoordPattern → CoordPattern → Bool

Equations

• Phenomena.Coordination.Typology.instBEqCoordPattern.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Coordination.Typology.instBEqCoordPattern : BEq CoordPattern

Equations

• Phenomena.Coordination.Typology.instBEqCoordPattern = { beq := Phenomena.Coordination.Typology.instBEqCoordPattern.beq }

def Phenomena.Coordination.Typology.instReprCoordPattern.repr : CoordPattern → ℕ → Std.Format

Equations

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

instance Phenomena.Coordination.Typology.instReprCoordPattern : Repr CoordPattern

Equations

• Phenomena.Coordination.Typology.instReprCoordPattern = { reprPrec := Phenomena.Coordination.Typology.instReprCoordPattern.repr }

def Phenomena.Coordination.Typology.CoordPattern.syndesis : CoordPattern → Syndesis

Classify a pattern's syndesis.

Equations

• Phenomena.Coordination.Typology.CoordPattern.a_co_b.syndesis = Phenomena.Coordination.Typology.Syndesis.monosyndetic
• Phenomena.Coordination.Typology.CoordPattern.a'co_b.syndesis = Phenomena.Coordination.Typology.Syndesis.monosyndetic
• Phenomena.Coordination.Typology.CoordPattern.a_b'co.syndesis = Phenomena.Coordination.Typology.Syndesis.monosyndetic
• Phenomena.Coordination.Typology.CoordPattern.co'a_co'b.syndesis = Phenomena.Coordination.Typology.Syndesis.bisyndetic
• Phenomena.Coordination.Typology.CoordPattern.a'co_b'co.syndesis = Phenomena.Coordination.Typology.Syndesis.bisyndetic
• Phenomena.Coordination.Typology.CoordPattern.a'co_co'b.syndesis = Phenomena.Coordination.Typology.Syndesis.bisyndetic
• Phenomena.Coordination.Typology.CoordPattern.co'a_b'co.syndesis = Phenomena.Coordination.Typology.Syndesis.bisyndetic

inductive Phenomena.Coordination.Typology.DiachronicSource : Type

Diachronic source of conjunction constructions (Haspelmath §5.1, p.10).

Two main pathways create conjunction markers:

1. Comitative "with" → monosyndetic coordinator (A with B → A and B)
2. Additive focus particle "also/too" → bisyndetic coordinator (A also B also)

• comitative : DiachronicSource
• focusParticle : DiachronicSource
• other : DiachronicSource

instance Phenomena.Coordination.Typology.instDecidableEqDiachronicSource : DecidableEq DiachronicSource

Equations

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

def Phenomena.Coordination.Typology.instBEqDiachronicSource.beq : DiachronicSource → DiachronicSource → Bool

Equations

• Phenomena.Coordination.Typology.instBEqDiachronicSource.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Coordination.Typology.instBEqDiachronicSource : BEq DiachronicSource

Equations

• Phenomena.Coordination.Typology.instBEqDiachronicSource = { beq := Phenomena.Coordination.Typology.instBEqDiachronicSource.beq }

def Phenomena.Coordination.Typology.instReprDiachronicSource.repr : DiachronicSource → ℕ → Std.Format

Equations

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

instance Phenomena.Coordination.Typology.instReprDiachronicSource : Repr DiachronicSource

Equations

• Phenomena.Coordination.Typology.instReprDiachronicSource = { reprPrec := Phenomena.Coordination.Typology.instReprDiachronicSource.repr }

def Phenomena.Coordination.Typology.DiachronicSource.expectedPattern : DiachronicSource → Syndesis

Haspelmath's key insight connecting diachronic source to structural pattern:

• Comitative source → monosyndetic (because "with" links two NPs)
• Focus particle source → bisyndetic (because "also" marks each NP)

This aligns with M&S: J ≈ comitative-derived, MU ≈ focus-particle-derived.

Equations

• Phenomena.Coordination.Typology.DiachronicSource.comitative.expectedPattern = Phenomena.Coordination.Typology.Syndesis.monosyndetic
• Phenomena.Coordination.Typology.DiachronicSource.focusParticle.expectedPattern = Phenomena.Coordination.Typology.Syndesis.bisyndetic
• Phenomena.Coordination.Typology.DiachronicSource.other.expectedPattern = Phenomena.Coordination.Typology.Syndesis.monosyndetic

inductive Phenomena.Coordination.Typology.Boundness : Type

Morphological boundness: whether a particle is a clitic/suffix or a free word. Relevant to acquisition (@cite{clark-2017}: free morphemes acquired more readily).

• free : Boundness
• bound : Boundness

instance Phenomena.Coordination.Typology.instDecidableEqBoundness : DecidableEq Boundness

Equations

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

def Phenomena.Coordination.Typology.instBEqBoundness.beq : Boundness → Boundness → Bool

Equations

• Phenomena.Coordination.Typology.instBEqBoundness.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Coordination.Typology.instBEqBoundness : BEq Boundness

Equations

• Phenomena.Coordination.Typology.instBEqBoundness = { beq := Phenomena.Coordination.Typology.instBEqBoundness.beq }

def Phenomena.Coordination.Typology.instReprBoundness.repr : Boundness → ℕ → Std.Format

Equations

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

instance Phenomena.Coordination.Typology.instReprBoundness : Repr Boundness

Equations

• Phenomena.Coordination.Typology.instReprBoundness = { reprPrec := Phenomena.Coordination.Typology.instReprBoundness.repr }

structure Phenomena.Coordination.Typology.ConjMorpheme : Type

A conjunction morpheme in a specific language.

• form : String
• role : String
• boundness : Boundness
• alsoAdditive : Bool

  Does this morpheme also serve as an additive/focus particle?

• source : Option DiachronicSource

  Likely diachronic source, if known

def Phenomena.Coordination.Typology.instReprConjMorpheme.repr : ConjMorpheme → ℕ → Std.Format

Equations

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

instance Phenomena.Coordination.Typology.instReprConjMorpheme : Repr ConjMorpheme

Equations

• Phenomena.Coordination.Typology.instReprConjMorpheme = { reprPrec := Phenomena.Coordination.Typology.instReprConjMorpheme.repr }

structure Phenomena.Coordination.Typology.ConjunctionSystem : Type

A language's conjunction system.

• language : String
• morphemes : List ConjMorpheme

  Available conjunction morphemes

• strategies : List Studies.BillEtAl2025.ConjunctionStrategy

  Which conjunction strategies are available (M&S classification)

• patterns : List CoordPattern

  Structural patterns attested (Haspelmath classification)

• iso : String

  ISO 639-3 code

def Phenomena.Coordination.Typology.instReprConjunctionSystem.repr : ConjunctionSystem → ℕ → Std.Format

Equations

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

instance Phenomena.Coordination.Typology.instReprConjunctionSystem : Repr ConjunctionSystem

Equations

• Phenomena.Coordination.Typology.instReprConjunctionSystem = { reprPrec := Phenomena.Coordination.Typology.instReprConjunctionSystem.repr }

def Phenomena.Coordination.Typology.english : ConjunctionSystem

English only has J ("and"). "Both...and" is sometimes analyzed as J-MU, but "both" is not productively used as an additive particle ("John both slept") and English lacks MU-only conjunction ("John both Mary both slept"). See FormMeaning.lean andBoth for the "both" ≈ precision-adding analysis.

Equations

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

def Phenomena.Coordination.Typology.japanese : ConjunctionSystem

Japanese conjunction uses "to" (J) and "mo" (MU). "to" derives from the comitative marker. "mo" is also the additive particle (see AdditiveParticles/Data.lean japaneseMo).

Equations

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

def Phenomena.Coordination.Typology.hungarian : ConjunctionSystem

Hungarian: "és" (J, free, prepositive), "is" (MU, free, postpositive). "is" is also the additive focus particle ("also"). One of two languages in our sample with all three strategies (J, MU, J-MU).

Equations

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

def Phenomena.Coordination.Typology.georgian : ConjunctionSystem

Georgian: "da" (J, free), "-c" (MU, bound clitic). "-c" is also the additive/focus particle. One of two languages in our sample with all three strategies.

Equations

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

def Phenomena.Coordination.Typology.latin : ConjunctionSystem

Latin: "et" (J, free, prepositive) and "-que" (MU, bound enclitic, postpositive). "-que" is the classic bound MU particle. Three structural patterns attested: A et B (monosyndetic), A B-que (monosyndetic), et A B-que (mixed bisyndetic).

Equations

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

def Phenomena.Coordination.Typology.korean : ConjunctionSystem

Korean: "-(i)rang" (J, bound, postpositive) and "-to" (MU, bound, also additive). Pattern: A-(i)rang B (monosyndetic postpositive), A-to B-to (bisyndetic postpositive).

Equations

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

def Phenomena.Coordination.Typology.slovenian : ConjunctionSystem

Slovenian: "in" (J, free, prepositive). Primarily J-only for standard conjunction.

Equations

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

def Phenomena.Coordination.Typology.lango : ConjunctionSystem

Lango (Nilotic, Uganda): "kèdè" is a comitative marker ("with") that also serves as coordinator ("and"). The classic AND-language: comitative source gives monosyndetic A co-B (@cite{noonan-1992}:163, @cite{haspelmath-2007}: (20)).

Equations

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

def Phenomena.Coordination.Typology.hausa : ConjunctionSystem

Hausa (Chadic, Nigeria): "da" means both "with" (comitative) and "and" (conjunction). Archetypal comitative → conjunction path (@cite{schwartz-1989}:32,36; @cite{haspelmath-2007}: (12)).

Equations

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

def Phenomena.Coordination.Typology.yoruba : ConjunctionSystem

Yoruba (Kwa, Nigeria): "àtí" in the pattern "àtí A àtí B" is the canonical example of prepositive bisyndetic coordination (@cite{rowlands-1969}:201ff, @cite{haspelmath-2007}: (25)).

Equations

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

def Phenomena.Coordination.Typology.kannada : ConjunctionSystem

Kannada (Dravidian, southern India): postpositive "-u" on each coordinand gives A-co B-co (@cite{sridhar-1990}:106, @cite{haspelmath-2007}: (5)). "-u" is also the additive/focus particle in Dravidian.

Equations

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

def Phenomena.Coordination.Typology.martuthunira : ConjunctionSystem

Martuthunira (Pama-Nyungan, W. Australia): "-thurti" on each coordinand gives A-co B-co (@cite{dench-1995}:98, @cite{haspelmath-2007}: (26)).

Equations

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

def Phenomena.Coordination.Typology.classicalTibetan : ConjunctionSystem

Classical Tibetan: "-daŋ" is postpositive on first coordinand, giving A-co B. Derives from comitative source (@cite{beyer-1992}:240, @cite{haspelmath-2007}: (21)).

Equations

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

def Phenomena.Coordination.Typology.hindiUrdu : ConjunctionSystem

Hindi-Urdu: "aur" (J, free, prepositive) and "bhii" (MU, free, additive). "bhii" is the additive particle "also/too" (see AdditiveParticles). Pattern: A aur B (monosyndetic), A bhii B bhii (bisyndetic postpositive).

Equations

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

def Phenomena.Coordination.Typology.turkish : ConjunctionSystem

Turkish: "ve" (J, free, prepositive) and "de/da" (MU, free, additive). "de/da" is the additive particle "also" (vowel harmony alternation). Pattern: A ve B (monosyndetic), A da B de (bisyndetic postpositive).

Equations

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

def Phenomena.Coordination.Typology.irish : ConjunctionSystem

Irish: "agus" (J, free, prepositive). No MU strategy attested. Pattern: A agus B (monosyndetic medial).

Equations

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

def Phenomena.Coordination.Typology.persian : ConjunctionSystem

Persian: "va" (J, free, prepositive) and "ham" (MU, free, additive). "ham" is the additive particle "also/too". Pattern: A va B (monosyndetic), A ham B ham (bisyndetic postpositive).

Equations

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

def Phenomena.Coordination.Typology.finnish : ConjunctionSystem

Finnish: "ja" (J, free, prepositive) and "-kin" (MU, bound, additive). "-kin" is the additive focus particle "also/too": koira-kin kissa-kin 'dog-too cat-too' = 'both the dog and the cat'. Standard conjunction: koira ja kissa 'dog and cat' (monosyndetic medial).

Equations

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

def Phenomena.Coordination.Typology.allLanguages : List ConjunctionSystem

Equations

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

def Phenomena.Coordination.Typology.ConjunctionSystem.hasStrategy (sys : ConjunctionSystem) (s : Studies.BillEtAl2025.ConjunctionStrategy) : Bool

Does a language have a given strategy?

Equations

• sys.hasStrategy s = sys.strategies.contains s

def Phenomena.Coordination.Typology.ConjunctionSystem.muIsAdditive (sys : ConjunctionSystem) : Bool

Does a language have a MU morpheme that also serves as additive?

Equations

• sys.muIsAdditive = sys.morphemes.any fun (m : Phenomena.Coordination.Typology.ConjMorpheme) => m.role == "MU" && m.alsoAdditive

theorem Phenomena.Coordination.Typology.mu_additive_generalization : have withMu := List.filter (fun (sys : ConjunctionSystem) => sys.morphemes.any fun (x : ConjMorpheme) => x.role == "MU") allLanguages; (withMu.all fun (x : ConjunctionSystem) => x.muIsAdditive) = true

Every language with a MU conjunction particle uses the same morpheme as its additive ("also/too") particle.

This is a core prediction of M&S / Mitrović (2021): MU is a single lexical item with subset semantics that appears in both conjunction and additive contexts.

NOTE: Restricted to languages in our sample that HAVE a MU morpheme.

def Phenomena.Coordination.Typology.hasAllThreeStrategies (sys : ConjunctionSystem) : Bool

All three strategies (J, MU, J-MU) attested only in Georgian and Hungarian in our sample. This is typologically rare.

Equations

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

theorem Phenomena.Coordination.Typology.all_three_is_rare : have count := (List.filter hasAllThreeStrategies allLanguages).length; (count == 2) = true

def Phenomena.Coordination.Typology.msLanguages : List ConjunctionSystem

Languages with full M&S strategy classification (from @cite{bill-etal-2025}).

Equations

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

theorem Phenomena.Coordination.Typology.j_is_universal : (msLanguages.all fun (x : ConjunctionSystem) => x.hasStrategy Studies.BillEtAl2025.ConjunctionStrategy.jOnly) = true

Every M&S-classified language in our sample has at least the J-only strategy.

def Phenomena.Coordination.Typology.ConjunctionSystem.muBoundness (sys : ConjunctionSystem) : Option Boundness

Get the boundness of a language's MU particle, if it has one.

Equations

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

theorem Phenomena.Coordination.Typology.mu_boundness_asymmetry : georgian.muBoundness = some Boundness.bound ∧ hungarian.muBoundness = some Boundness.free

Georgian MU is bound, Hungarian MU is free.

@cite{bill-etal-2025} @cite{mitrovic-2021} speculate this morphological difference may explain why Georgian children found MU-involving expressions harder than Hungarian children did: bound morphemes are harder to segment and acquire.

def Phenomena.Coordination.Typology.ConjunctionSystem.hasSource (sys : ConjunctionSystem) (s : DiachronicSource) : Bool

Does a language have a morpheme with a given diachronic source?

Equations

• sys.hasSource s = sys.morphemes.any fun (m : Phenomena.Coordination.Typology.ConjMorpheme) => m.source == some s

def Phenomena.Coordination.Typology.ConjunctionSystem.hasMonosyndetic (sys : ConjunctionSystem) : Bool

Does a language have at least one monosyndetic pattern?

Equations

• sys.hasMonosyndetic = sys.patterns.any fun (p : Phenomena.Coordination.Typology.CoordPattern) => p.syndesis == Phenomena.Coordination.Typology.Syndesis.monosyndetic

def Phenomena.Coordination.Typology.ConjunctionSystem.hasBisyndetic (sys : ConjunctionSystem) : Bool

Does a language have at least one bisyndetic pattern?

Equations

• sys.hasBisyndetic = sys.patterns.any fun (p : Phenomena.Coordination.Typology.CoordPattern) => p.syndesis == Phenomena.Coordination.Typology.Syndesis.bisyndetic

theorem Phenomena.Coordination.Typology.comitative_source_monosyndetic : have withComitative := List.filter (fun (x : ConjunctionSystem) => x.hasSource DiachronicSource.comitative) allLanguages; (withComitative.all fun (x : ConjunctionSystem) => x.hasMonosyndetic) = true

Haspelmath's diachronic generalization (§5.1): Every language with a known comitative-sourced morpheme has at least one monosyndetic structural pattern.

This confirms: comitative "with" → monosyndetic A co-B / A-co B. Languages: Lango ("kèdè"), Hausa ("da"), Japanese ("to"), Classical Tibetan ("-daŋ").

theorem Phenomena.Coordination.Typology.focus_particle_source_bisyndetic : have withFocusParticle := List.filter (fun (x : ConjunctionSystem) => x.hasSource DiachronicSource.focusParticle) allLanguages; (withFocusParticle.all fun (x : ConjunctionSystem) => x.hasBisyndetic) = true

Haspelmath's diachronic generalization (§5.1): Every language with a known focus-particle-sourced morpheme has at least one bisyndetic structural pattern.

This confirms: additive focus particle "also" → bisyndetic A-co B-co. Languages: Japanese ("mo"), Hungarian ("is"), Georgian ("-c"), Latin ("-que"), Korean ("-to"), Kannada ("-u").

Mitrović & Sauerland's Universal Structure

@cite{stassen-2000} @cite{haspelmath-2007} @cite{schwartz-1989}

@cite{mitrovic-sauerland-2016} claim that EVERY language has the same underlying structure for DP conjunction:

[JP [MuP [DP ☉] MU] [J' J [MuP [DP ☉] MU]]]

All three strategies (J, MU, J-MU) are underlyingly identical. What varies is which functional heads (J, MU₁, MU₂) are pronounced.

Semantic content (via Montague/Conjunction.lean)

• J = genConj at type ⟨⟨e,t⟩,⟨⟨e,t⟩,t⟩⟩ (Partee & Rooth set intersection)
• MU = inclFunc (INCL schema: subset check)
• ☉ = typeRaise (individual → generalized quantifier)

See BillEtAl2025.ms_decomposition_eq_coord for the proof that this roundtrip recovers standard coordEntities semantics.

theorem Phenomena.Coordination.Typology.ms_universality_challenged : hasAllThreeStrategies georgian = true ∧ Studies.BillEtAl2025.transparencyPredicts Studies.BillEtAl2025.ConjunctionStrategy.jMu Studies.BillEtAl2025.ConjunctionStrategy.jOnly = true ∧ Studies.BillEtAl2025.georgianChild_j_vs_jmu.significant = true ∧ Studies.BillEtAl2025.georgianChild_j_vs_jmu.estimate_thou < 0

Empirical challenge to M&S universality.

The M&S decomposition + Transparency Principle predicts J-MU (where all semantic pieces are overtly realized) should be EASIEST to acquire. But in Georgian, J-MU is significantly HARDER for children than either J-only or MU-only.

This theorem surfaces the contradiction at the typology level so that any module importing Typology.lean sees that the M&S categories are empirically contested, not established universals.

Conjunct 1: Georgian has all three M&S strategies (as M&S predicts). Conjunct 2: M&S + Transparency predicts J-MU is most transparent. Conjunct 3: Georgian children found J-MU significantly harder (more replays).

theorem Phenomena.Coordination.Typology.boundness_confound : georgian.muBoundness = some Boundness.bound ∧ hungarian.muBoundness = some Boundness.free ∧ Studies.BillEtAl2025.georgianChild_j_vs_jmu.significant = true ∧ ((List.filter (fun (x : Studies.BillEtAl2025.LRTResult) => x.effect == "sentence") Studies.BillEtAl2025.hungarianSentencePlayedLRT).all fun (x : Studies.BillEtAl2025.LRTResult) => x.significant == false) = true

The boundness confound.

Georgian MU (-c) is bound; Hungarian MU (is) is free. Hungarian children showed no significant sentence-type effect on either accuracy or replays. This raises the possibility that morphological boundness — not the M&S decomposition itself — drives the Georgian difficulty.

If boundness is the real factor, then M&S categories (J, MU, J-MU) are not the right level of analysis for acquisition predictions.

theorem Phenomena.Coordination.Typology.predict_acquisition_asymmetry (sys : ConjunctionSystem) (h_all : hasAllThreeStrategies sys = true) (h_bound : sys.muBoundness = some Boundness.bound) : True

Open problem: predict the @cite{bill-etal-2025} acquisition asymmetry.

No existing account predicts the full cross-linguistic pattern:

• @cite{mitrovic-sauerland-2016} + Transparency Principle → predicts J-MU easiest. Wrong for Georgian.
• @cite{szabolcsi-2015} → alternative quantifier-particle analysis. Doesn't predict it.
• @cite{haslinger-etal-2019} → plural/distributive analysis. Doesn't predict it.

A complete theory should derive: when MU is morphologically bound, J-MU incurs extra acquisition cost (segmentation difficulty outweighs transparency benefit). When MU is free, no such cost arises, yielding the Hungarian null.

TODO: This likely requires a processing/acquisition model where morphological complexity (boundness) and syntactic transparency (overt form-meaning mapping) are competing factors. The sorry marks this as the central open gap in the coordination typology — the M&S categories describe the space but don't yet predict which regions are hard to acquire.

inductive Phenomena.Coordination.Typology.ConjQuantRelation : Type

WALS Ch 56: Whether a language's conjunction marker is formally similar to its universal quantifier and/or interrogative pronoun.

This captures a deep typological pattern: in many languages, "and", "all/every", and "what/who" share morphological material, suggesting a common semantic core (set-theoretic operations over individuals).

• formallyDifferent : ConjQuantRelation

  Conjunction and universal quantifier are formally unrelated. Example: English "and" vs "every/all".

• similarNoInterrogative : ConjQuantRelation

  Conjunction and universal quantifier share formal material, but the interrogative pronoun is different. Example: English "every" "and" similarity is marginal; Hungarian "es" (and) "minden" (every) share no form but the quantifier and interrogative are linked.

• similarWithInterrogative : ConjQuantRelation

  Conjunction, universal quantifier, and interrogative pronoun all share formal material. Example: Japanese "mo" serves as conjunction particle ("A-mo B-mo"), universal quantifier ("dare-mo" = everyone), and is related to the interrogative "dare" (who).

instance Phenomena.Coordination.Typology.instDecidableEqConjQuantRelation : DecidableEq ConjQuantRelation

Equations

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

def Phenomena.Coordination.Typology.instBEqConjQuantRelation.beq : ConjQuantRelation → ConjQuantRelation → Bool

Equations

• Phenomena.Coordination.Typology.instBEqConjQuantRelation.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Coordination.Typology.instBEqConjQuantRelation : BEq ConjQuantRelation

Equations

• Phenomena.Coordination.Typology.instBEqConjQuantRelation = { beq := Phenomena.Coordination.Typology.instBEqConjQuantRelation.beq }

def Phenomena.Coordination.Typology.instReprConjQuantRelation.repr : ConjQuantRelation → ℕ → Std.Format

Equations

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

instance Phenomena.Coordination.Typology.instReprConjQuantRelation : Repr ConjQuantRelation

Equations

• Phenomena.Coordination.Typology.instReprConjQuantRelation = { reprPrec := Phenomena.Coordination.Typology.instReprConjQuantRelation.repr }

inductive Phenomena.Coordination.Typology.ConjComitativeRelation : Type

WALS Ch 63: Whether a language's NP coordinator ("and") is formally identical to its comitative adposition ("with").

This is directly relevant to the diachronic source of coordinators: languages where "and" = "with" are those where the comitative-to- coordinator grammaticalization pathway is still transparent.

• andDifferentFromWith : ConjComitativeRelation

  The conjunction marker and comitative marker are different forms. Example: English "and" (conjunction) vs "with" (comitative).

• andIdenticalToWith : ConjComitativeRelation

  The conjunction marker and comitative marker are the same form. Example: Japanese "to" serves as both comitative ("with") and conjunction ("and"); Swahili "na" means both "and" and "with".

instance Phenomena.Coordination.Typology.instDecidableEqConjComitativeRelation : DecidableEq ConjComitativeRelation

Equations

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

instance Phenomena.Coordination.Typology.instBEqConjComitativeRelation : BEq ConjComitativeRelation

Equations

• Phenomena.Coordination.Typology.instBEqConjComitativeRelation = { beq := Phenomena.Coordination.Typology.instBEqConjComitativeRelation.beq }

def Phenomena.Coordination.Typology.instBEqConjComitativeRelation.beq : ConjComitativeRelation → ConjComitativeRelation → Bool

Equations

• Phenomena.Coordination.Typology.instBEqConjComitativeRelation.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Coordination.Typology.instReprConjComitativeRelation : Repr ConjComitativeRelation

Equations

• Phenomena.Coordination.Typology.instReprConjComitativeRelation = { reprPrec := Phenomena.Coordination.Typology.instReprConjComitativeRelation.repr }

def Phenomena.Coordination.Typology.instReprConjComitativeRelation.repr : ConjComitativeRelation → ℕ → Std.Format

Equations

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

inductive Phenomena.Coordination.Typology.AndWithStatus : Type

@cite{stassen-2000} AND/WITH classification of languages. AND-languages have structurally distinct coordinate and comitative strategies. WITH-languages use comitative encoding as the only strategy for NP conjunction.

Derived from WALS Ch 63 conjunction/comitative relation: languages where "and" ≠ "with" have differentiated the two strategies (AND-status); languages where "and" = "with" retain comitative-based conjunction (WITH-status).

• andLang : AndWithStatus
• withLang : AndWithStatus

instance Phenomena.Coordination.Typology.instDecidableEqAndWithStatus : DecidableEq AndWithStatus

Equations

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

instance Phenomena.Coordination.Typology.instBEqAndWithStatus : BEq AndWithStatus

Equations

• Phenomena.Coordination.Typology.instBEqAndWithStatus = { beq := Phenomena.Coordination.Typology.instBEqAndWithStatus.beq }

def Phenomena.Coordination.Typology.instBEqAndWithStatus.beq : AndWithStatus → AndWithStatus → Bool

Equations

• Phenomena.Coordination.Typology.instBEqAndWithStatus.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Coordination.Typology.instReprAndWithStatus.repr : AndWithStatus → ℕ → Std.Format

Equations

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

instance Phenomena.Coordination.Typology.instReprAndWithStatus : Repr AndWithStatus

Equations

• Phenomena.Coordination.Typology.instReprAndWithStatus = { reprPrec := Phenomena.Coordination.Typology.instReprAndWithStatus.repr }

def Phenomena.Coordination.Typology.ConjComitativeRelation.toAndWithStatus : ConjComitativeRelation → AndWithStatus

Derive AND/WITH status from the conjunction-comitative relation. @cite{stassen-2000}: lexical identity of "and" and "with" is the diagnostic for WITH-language status.

Equations

• Phenomena.Coordination.Typology.ConjComitativeRelation.andDifferentFromWith.toAndWithStatus = Phenomena.Coordination.Typology.AndWithStatus.andLang
• Phenomena.Coordination.Typology.ConjComitativeRelation.andIdenticalToWith.toAndWithStatus = Phenomena.Coordination.Typology.AndWithStatus.withLang

inductive Phenomena.Coordination.Typology.NomVerbalConjRelation : Type

WALS Ch 64: Whether a language uses the same conjunction marker for NP coordination ("cats and dogs") and VP/clausal coordination ("sang and danced").

Languages that differentiate may use distinct markers, or may use overt coordination for one but juxtaposition for the other.

• identity : NomVerbalConjRelation

  Same conjunction marker for NP and VP coordination. Example: English "and" in both "cats and dogs" and "sang and danced".

• differentiation : NomVerbalConjRelation

  Different conjunction markers for NP and VP coordination. Example: Japanese "to" for NPs ("inu to neko") but different strategies for VP conjunction.

• bothJuxtaposition : NomVerbalConjRelation

  Both NP and VP coordination are expressed by juxtaposition (no overt marker for either). Example: some Australian and South American languages.

instance Phenomena.Coordination.Typology.instDecidableEqNomVerbalConjRelation : DecidableEq NomVerbalConjRelation

Equations

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

instance Phenomena.Coordination.Typology.instBEqNomVerbalConjRelation : BEq NomVerbalConjRelation

Equations

• Phenomena.Coordination.Typology.instBEqNomVerbalConjRelation = { beq := Phenomena.Coordination.Typology.instBEqNomVerbalConjRelation.beq }

def Phenomena.Coordination.Typology.instBEqNomVerbalConjRelation.beq : NomVerbalConjRelation → NomVerbalConjRelation → Bool

Equations

• Phenomena.Coordination.Typology.instBEqNomVerbalConjRelation.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Coordination.Typology.instReprNomVerbalConjRelation : Repr NomVerbalConjRelation

Equations

• Phenomena.Coordination.Typology.instReprNomVerbalConjRelation = { reprPrec := Phenomena.Coordination.Typology.instReprNomVerbalConjRelation.repr }

def Phenomena.Coordination.Typology.instReprNomVerbalConjRelation.repr : NomVerbalConjRelation → ℕ → Std.Format

Equations

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

structure Phenomena.Coordination.Typology.CoordinationProfile : Type

A language's coordination typology profile across WALS Chapters 56, 63, 64.

• language : String

  Language name.

• iso : String

  ISO 639-3 code.

• family : String

  Language family.

• conjQuant : Option ConjQuantRelation

  Ch 56: Relationship between conjunction and universal quantifier.

• conjComitative : Option ConjComitativeRelation

  Ch 63: Whether "and" = "with".

• nomVerbalConj : Option NomVerbalConjRelation

  Ch 64: Whether NP and VP conjunction use the same marker.

• walsNotes : String

  Notes on the coordination system.

instance Phenomena.Coordination.Typology.instReprCoordinationProfile : Repr CoordinationProfile

Equations

• Phenomena.Coordination.Typology.instReprCoordinationProfile = { reprPrec := Phenomena.Coordination.Typology.instReprCoordinationProfile.repr }

def Phenomena.Coordination.Typology.instReprCoordinationProfile.repr : CoordinationProfile → ℕ → Std.Format

Equations

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

def Phenomena.Coordination.Typology.CoordinationProfile.andWithStatus (p : CoordinationProfile) : Option AndWithStatus

Derive AND/WITH status for a coordination profile from its Ch 63 value. @cite{stassen-2000}: lexical identity of "and" and "with" is the diagnostic for WITH-language status.

Equations

• p.andWithStatus = Option.map (fun (x : Phenomena.Coordination.Typology.ConjComitativeRelation) => x.toAndWithStatus) p.conjComitative

def Phenomena.Coordination.Typology.englishWALS : CoordinationProfile

English (Indo-European, Germanic). Ch 56: "and" and "every/all" are formally similar without interrogative link. Ch 63: "and" is different from "with". Ch 64: Same "and" for NP and VP coordination (identity).

Equations

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

def Phenomena.Coordination.Typology.germanWALS : CoordinationProfile

German (Indo-European, Germanic). Ch 56: Not in WALS F56A sample. Ch 63: Not in WALS F63A sample. Ch 64: Same "und" for NP and VP coordination (identity).

Equations

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

def Phenomena.Coordination.Typology.frenchWALS : CoordinationProfile

French (Indo-European, Romance). Ch 56: "et" (and) and "tout/chaque" (all/every) are formally different. Ch 63: "et" (and) is different from "avec" (with). Ch 64: Same "et" for NP and VP coordination (identity).

Equations

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

def Phenomena.Coordination.Typology.spanishWALS : CoordinationProfile

Spanish (Indo-European, Romance). Ch 56: Not in WALS F56A sample. Ch 63: "y" (and) is different from "con" (with). Ch 64: Same "y" for NP and VP coordination (identity).

Equations

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

def Phenomena.Coordination.Typology.russianWALS : CoordinationProfile

Russian (Indo-European, Slavic). Ch 56: Not in WALS F56A sample. Ch 63: "i" (and) is different from "s" (with). Ch 64: Same "i" for NP and VP coordination (identity).

Equations

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

def Phenomena.Coordination.Typology.japaneseWALS : CoordinationProfile

Japanese (Japonic). Ch 56: Conjunction "mo", universal quantifier "mo" (dare-mo = everyone), and interrogative "dare" (who) are all formally similar. Ch 63: "to" (and) is identical to "to" (with/comitative). Ch 64: NP and VP conjunction use different strategies (differentiation). NP: "A to B" or "A mo B mo"; VP: different connective strategies.

Equations

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

def Phenomena.Coordination.Typology.mandarinWALS : CoordinationProfile

Mandarin Chinese (Sino-Tibetan). Ch 56: Conjunction, quantifier, and interrogative are formally similar. Ch 63: "he" or "gen" (and) is identical to comitative "gen/he" (with). Ch 64: NP and VP conjunction use different strategies (differentiation). NP: "A he B"; VP: different connective or serial verb.

Equations

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

def Phenomena.Coordination.Typology.koreanWALS : CoordinationProfile

Korean (Koreanic). Ch 56: Not in WALS F56A sample. Ch 63: Conjunction marker is different from comitative. Ch 64: NP and VP conjunction use different markers (differentiation).

Equations

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

def Phenomena.Coordination.Typology.turkishWALS : CoordinationProfile

Turkish (Turkic). Ch 56: "ve" (and) and "her" (every) are formally different. Ch 63: "ve" (and) is different from "ile" (with). Ch 64: Same conjunction for NP and VP coordination (identity).

Equations

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

def Phenomena.Coordination.Typology.finnishWALS : CoordinationProfile

Finnish (Uralic). Ch 56: Conjunction and universal quantifier formally similar with interrogative link. Ch 63: "ja" (and) is different from comitative case marker. Ch 64: Same "ja" for NP and VP coordination (identity).

Equations

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

def Phenomena.Coordination.Typology.hungarianWALS : CoordinationProfile

Hungarian (Uralic). Ch 56: Conjunction and universal quantifier formally similar without interrogative link. Ch 63: "es" (and) is different from comitative "-val, -vel" (with). Ch 64: Same "es" for NP and VP coordination (identity).

Equations

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

def Phenomena.Coordination.Typology.hindiWALS : CoordinationProfile

Hindi (Indo-European, Indo-Aryan). Ch 56: Conjunction, universal quantifier, and interrogative formally similar. Ch 63: "aur" (and) is different from "ke saath" (with). Ch 64: Same "aur" for NP and VP coordination (identity).

Equations

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

def Phenomena.Coordination.Typology.arabicWALS : CoordinationProfile

Arabic (Egyptian) (Afro-Asiatic, Semitic). Ch 56: Not in WALS F56A sample. Ch 63: "wa/wi" (and) is different from "ma'a" (with). Ch 64: Same conjunction for NP and VP coordination (identity).

Equations

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

def Phenomena.Coordination.Typology.swahiliWALS : CoordinationProfile

Swahili (Niger-Congo, Bantu). Ch 56: Not in WALS F56A sample. Ch 63: "na" serves as both conjunction ("and") and comitative ("with"). Ch 64: Not in WALS F64A sample.

Equations

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

def Phenomena.Coordination.Typology.tagalogWALS : CoordinationProfile

Tagalog (Austronesian). Ch 56: Conjunction, universal quantifier, and interrogative formally similar. Ch 63: "at" (and) is different from "kasama" (with). Ch 64: Same conjunction for NP and VP coordination (identity).

Equations

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

def Phenomena.Coordination.Typology.allWALSProfiles : List CoordinationProfile

All WALS coordination profiles in the sample.

Equations

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

theorem Phenomena.Coordination.Typology.english_f56a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F56A.ConjunctionsAndUniversalQuantifiers) => Phenomena.Coordination.Typology.fromWALS56A✝ x.value) (Core.WALS.F56A.lookup "eng") = englishWALS.conjQuant

theorem Phenomena.Coordination.Typology.french_f56a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F56A.ConjunctionsAndUniversalQuantifiers) => Phenomena.Coordination.Typology.fromWALS56A✝ x.value) (Core.WALS.F56A.lookup "fre") = frenchWALS.conjQuant

theorem Phenomena.Coordination.Typology.japanese_f56a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F56A.ConjunctionsAndUniversalQuantifiers) => Phenomena.Coordination.Typology.fromWALS56A✝ x.value) (Core.WALS.F56A.lookup "jpn") = japaneseWALS.conjQuant

theorem Phenomena.Coordination.Typology.mandarin_f56a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F56A.ConjunctionsAndUniversalQuantifiers) => Phenomena.Coordination.Typology.fromWALS56A✝ x.value) (Core.WALS.F56A.lookup "mnd") = mandarinWALS.conjQuant

theorem Phenomena.Coordination.Typology.turkish_f56a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F56A.ConjunctionsAndUniversalQuantifiers) => Phenomena.Coordination.Typology.fromWALS56A✝ x.value) (Core.WALS.F56A.lookup "tur") = turkishWALS.conjQuant

theorem Phenomena.Coordination.Typology.finnish_f56a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F56A.ConjunctionsAndUniversalQuantifiers) => Phenomena.Coordination.Typology.fromWALS56A✝ x.value) (Core.WALS.F56A.lookup "fin") = finnishWALS.conjQuant

theorem Phenomena.Coordination.Typology.hungarian_f56a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F56A.ConjunctionsAndUniversalQuantifiers) => Phenomena.Coordination.Typology.fromWALS56A✝ x.value) (Core.WALS.F56A.lookup "hun") = hungarianWALS.conjQuant

theorem Phenomena.Coordination.Typology.hindi_f56a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F56A.ConjunctionsAndUniversalQuantifiers) => Phenomena.Coordination.Typology.fromWALS56A✝ x.value) (Core.WALS.F56A.lookup "hin") = hindiWALS.conjQuant

theorem Phenomena.Coordination.Typology.tagalog_f56a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F56A.ConjunctionsAndUniversalQuantifiers) => Phenomena.Coordination.Typology.fromWALS56A✝ x.value) (Core.WALS.F56A.lookup "tag") = tagalogWALS.conjQuant

theorem Phenomena.Coordination.Typology.english_f63a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F63A.NounPhraseConjunction) => Phenomena.Coordination.Typology.fromWALS63A✝ x.value) (Core.WALS.F63A.lookup "eng") = englishWALS.conjComitative

theorem Phenomena.Coordination.Typology.french_f63a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F63A.NounPhraseConjunction) => Phenomena.Coordination.Typology.fromWALS63A✝ x.value) (Core.WALS.F63A.lookup "fre") = frenchWALS.conjComitative

theorem Phenomena.Coordination.Typology.spanish_f63a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F63A.NounPhraseConjunction) => Phenomena.Coordination.Typology.fromWALS63A✝ x.value) (Core.WALS.F63A.lookup "spa") = spanishWALS.conjComitative

theorem Phenomena.Coordination.Typology.russian_f63a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F63A.NounPhraseConjunction) => Phenomena.Coordination.Typology.fromWALS63A✝ x.value) (Core.WALS.F63A.lookup "rus") = russianWALS.conjComitative

theorem Phenomena.Coordination.Typology.japanese_f63a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F63A.NounPhraseConjunction) => Phenomena.Coordination.Typology.fromWALS63A✝ x.value) (Core.WALS.F63A.lookup "jpn") = japaneseWALS.conjComitative

theorem Phenomena.Coordination.Typology.mandarin_f63a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F63A.NounPhraseConjunction) => Phenomena.Coordination.Typology.fromWALS63A✝ x.value) (Core.WALS.F63A.lookup "mnd") = mandarinWALS.conjComitative

theorem Phenomena.Coordination.Typology.korean_f63a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F63A.NounPhraseConjunction) => Phenomena.Coordination.Typology.fromWALS63A✝ x.value) (Core.WALS.F63A.lookup "kor") = koreanWALS.conjComitative

theorem Phenomena.Coordination.Typology.turkish_f63a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F63A.NounPhraseConjunction) => Phenomena.Coordination.Typology.fromWALS63A✝ x.value) (Core.WALS.F63A.lookup "tur") = turkishWALS.conjComitative

theorem Phenomena.Coordination.Typology.finnish_f63a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F63A.NounPhraseConjunction) => Phenomena.Coordination.Typology.fromWALS63A✝ x.value) (Core.WALS.F63A.lookup "fin") = finnishWALS.conjComitative

theorem Phenomena.Coordination.Typology.hungarian_f63a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F63A.NounPhraseConjunction) => Phenomena.Coordination.Typology.fromWALS63A✝ x.value) (Core.WALS.F63A.lookup "hun") = hungarianWALS.conjComitative

theorem Phenomena.Coordination.Typology.hindi_f63a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F63A.NounPhraseConjunction) => Phenomena.Coordination.Typology.fromWALS63A✝ x.value) (Core.WALS.F63A.lookup "hin") = hindiWALS.conjComitative

theorem Phenomena.Coordination.Typology.arabic_f63a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F63A.NounPhraseConjunction) => Phenomena.Coordination.Typology.fromWALS63A✝ x.value) (Core.WALS.F63A.lookup "aeg") = arabicWALS.conjComitative

theorem Phenomena.Coordination.Typology.swahili_f63a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F63A.NounPhraseConjunction) => Phenomena.Coordination.Typology.fromWALS63A✝ x.value) (Core.WALS.F63A.lookup "swa") = swahiliWALS.conjComitative

theorem Phenomena.Coordination.Typology.tagalog_f63a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F63A.NounPhraseConjunction) => Phenomena.Coordination.Typology.fromWALS63A✝ x.value) (Core.WALS.F63A.lookup "tag") = tagalogWALS.conjComitative

theorem Phenomena.Coordination.Typology.english_f64a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F64A.NominalAndVerbalConjunction) => Phenomena.Coordination.Typology.fromWALS64A✝ x.value) (Core.WALS.F64A.lookup "eng") = englishWALS.nomVerbalConj

theorem Phenomena.Coordination.Typology.german_f64a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F64A.NominalAndVerbalConjunction) => Phenomena.Coordination.Typology.fromWALS64A✝ x.value) (Core.WALS.F64A.lookup "ger") = germanWALS.nomVerbalConj

theorem Phenomena.Coordination.Typology.french_f64a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F64A.NominalAndVerbalConjunction) => Phenomena.Coordination.Typology.fromWALS64A✝ x.value) (Core.WALS.F64A.lookup "fre") = frenchWALS.nomVerbalConj

theorem Phenomena.Coordination.Typology.spanish_f64a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F64A.NominalAndVerbalConjunction) => Phenomena.Coordination.Typology.fromWALS64A✝ x.value) (Core.WALS.F64A.lookup "spa") = spanishWALS.nomVerbalConj

theorem Phenomena.Coordination.Typology.russian_f64a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F64A.NominalAndVerbalConjunction) => Phenomena.Coordination.Typology.fromWALS64A✝ x.value) (Core.WALS.F64A.lookup "rus") = russianWALS.nomVerbalConj

theorem Phenomena.Coordination.Typology.japanese_f64a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F64A.NominalAndVerbalConjunction) => Phenomena.Coordination.Typology.fromWALS64A✝ x.value) (Core.WALS.F64A.lookup "jpn") = japaneseWALS.nomVerbalConj

theorem Phenomena.Coordination.Typology.mandarin_f64a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F64A.NominalAndVerbalConjunction) => Phenomena.Coordination.Typology.fromWALS64A✝ x.value) (Core.WALS.F64A.lookup "mnd") = mandarinWALS.nomVerbalConj

theorem Phenomena.Coordination.Typology.korean_f64a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F64A.NominalAndVerbalConjunction) => Phenomena.Coordination.Typology.fromWALS64A✝ x.value) (Core.WALS.F64A.lookup "kor") = koreanWALS.nomVerbalConj

theorem Phenomena.Coordination.Typology.turkish_f64a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F64A.NominalAndVerbalConjunction) => Phenomena.Coordination.Typology.fromWALS64A✝ x.value) (Core.WALS.F64A.lookup "tur") = turkishWALS.nomVerbalConj

theorem Phenomena.Coordination.Typology.finnish_f64a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F64A.NominalAndVerbalConjunction) => Phenomena.Coordination.Typology.fromWALS64A✝ x.value) (Core.WALS.F64A.lookup "fin") = finnishWALS.nomVerbalConj

theorem Phenomena.Coordination.Typology.hungarian_f64a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F64A.NominalAndVerbalConjunction) => Phenomena.Coordination.Typology.fromWALS64A✝ x.value) (Core.WALS.F64A.lookup "hun") = hungarianWALS.nomVerbalConj

theorem Phenomena.Coordination.Typology.hindi_f64a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F64A.NominalAndVerbalConjunction) => Phenomena.Coordination.Typology.fromWALS64A✝ x.value) (Core.WALS.F64A.lookup "hin") = hindiWALS.nomVerbalConj

theorem Phenomena.Coordination.Typology.arabic_f64a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F64A.NominalAndVerbalConjunction) => Phenomena.Coordination.Typology.fromWALS64A✝ x.value) (Core.WALS.F64A.lookup "aeg") = arabicWALS.nomVerbalConj

theorem Phenomena.Coordination.Typology.tagalog_f64a : Option.map (fun (x : Core.WALS.Datapoint Core.WALS.F64A.NominalAndVerbalConjunction) => Phenomena.Coordination.Typology.fromWALS64A✝ x.value) (Core.WALS.F64A.lookup "tag") = tagalogWALS.nomVerbalConj

theorem Phenomena.Coordination.Typology.wals_f56a_total : Phenomena.Coordination.Typology.ch56✝.length = 116

F56A total: 116 languages.

theorem Phenomena.Coordination.Typology.wals_f56a_formallyDifferent : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F56A.ConjunctionsAndUniversalQuantifiers) => x.value == Core.WALS.F56A.ConjunctionsAndUniversalQuantifiers.formallyDifferent) Phenomena.Coordination.Typology.ch56✝).length = 40

F56A distribution: conjunctions and universal quantifiers.

theorem Phenomena.Coordination.Typology.wals_f56a_similarNoInterrogative : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F56A.ConjunctionsAndUniversalQuantifiers) => x.value == Core.WALS.F56A.ConjunctionsAndUniversalQuantifiers.formallySimilarWithoutInterrogative) Phenomena.Coordination.Typology.ch56✝).length = 33

theorem Phenomena.Coordination.Typology.wals_f56a_similarWithInterrogative : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F56A.ConjunctionsAndUniversalQuantifiers) => x.value == Core.WALS.F56A.ConjunctionsAndUniversalQuantifiers.formallySimilarWithInterrogative) Phenomena.Coordination.Typology.ch56✝).length = 43

theorem Phenomena.Coordination.Typology.wals_f63a_total : Phenomena.Coordination.Typology.ch63✝.length = 234

F63A total: 234 languages.

theorem Phenomena.Coordination.Typology.wals_f63a_andDifferentFromWith : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F63A.NounPhraseConjunction) => x.value == Core.WALS.F63A.NounPhraseConjunction.andDifferentFromWith) Phenomena.Coordination.Typology.ch63✝).length = 131

F63A distribution: noun phrase conjunction.

theorem Phenomena.Coordination.Typology.wals_f63a_andIdenticalToWith : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F63A.NounPhraseConjunction) => x.value == Core.WALS.F63A.NounPhraseConjunction.andIdenticalToWith) Phenomena.Coordination.Typology.ch63✝).length = 103

theorem Phenomena.Coordination.Typology.wals_f64a_total : Phenomena.Coordination.Typology.ch64✝.length = 301

F64A total: 301 languages.

theorem Phenomena.Coordination.Typology.wals_f64a_identity : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F64A.NominalAndVerbalConjunction) => x.value == Core.WALS.F64A.NominalAndVerbalConjunction.identity) Phenomena.Coordination.Typology.ch64✝).length = 161

F64A distribution: nominal and verbal conjunction.

theorem Phenomena.Coordination.Typology.wals_f64a_differentiation : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F64A.NominalAndVerbalConjunction) => x.value == Core.WALS.F64A.NominalAndVerbalConjunction.differentiation) Phenomena.Coordination.Typology.ch64✝).length = 125

theorem Phenomena.Coordination.Typology.wals_f64a_juxtaposition : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F64A.NominalAndVerbalConjunction) => x.value == Core.WALS.F64A.NominalAndVerbalConjunction.bothExpressedByJuxtaposition) Phenomena.Coordination.Typology.ch64✝).length = 15

theorem Phenomena.Coordination.Typology.wals_profile_count : allWALSProfiles.length = 15

Number of WALS coordination profiles in our sample.

theorem Phenomena.Coordination.Typology.and_with_different_is_majority : 131 > 103

F63A: "and" being different from "with" is the majority pattern (131 > 103).

theorem Phenomena.Coordination.Typology.nom_verbal_identity_is_majority : 161 > 125 ∧ 161 > 15

F64A: Identity of NP and VP conjunction is the majority pattern (161/301).

theorem Phenomena.Coordination.Typology.conj_quant_similarity_majority : 33 + 43 > 40

F56A: Formal similarity between conjunction and universal quantifier (with or without interrogative) is the majority pattern: 33 + 43 = 76 > 40.

theorem Phenomena.Coordination.Typology.juxtaposition_rare : 15 * 20 < 301

F64A: Juxtaposition for both NP and VP conjunction is rare (15/301 = 5%).

theorem Phenomena.Coordination.Typology.comitative_source_substantial_minority : 103 * 2 < 234 ∧ 103 * 3 > 234

F63A connects to diachronic source: languages where "and" = "with" (103/234 = 44%) are those with transparent comitative-to-coordinator grammaticalization. This is a substantial minority but not the majority.

theorem Phenomena.Coordination.Typology.and_languages_majority : (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F63A.NounPhraseConjunction) => x.value == Core.WALS.F63A.NounPhraseConjunction.andDifferentFromWith) Phenomena.Coordination.Typology.ch63✝).length > (List.filter (fun (x : Core.WALS.Datapoint Core.WALS.F63A.NounPhraseConjunction) => x.value == Core.WALS.F63A.NounPhraseConjunction.andIdenticalToWith) Phenomena.Coordination.Typology.ch63✝¹).length

In the WALS F63A sample, AND-languages outnumber WITH-languages (131 > 103). @cite{stassen-2000}: this reflects the diachronic drift from WITH → AND.

theorem Phenomena.Coordination.Typology.english_is_andLang : englishWALS.andWithStatus = some AndWithStatus.andLang

Per-language AND/WITH classification.

theorem Phenomena.Coordination.Typology.french_is_andLang : frenchWALS.andWithStatus = some AndWithStatus.andLang

theorem Phenomena.Coordination.Typology.spanish_is_andLang : spanishWALS.andWithStatus = some AndWithStatus.andLang

theorem Phenomena.Coordination.Typology.russian_is_andLang : russianWALS.andWithStatus = some AndWithStatus.andLang

theorem Phenomena.Coordination.Typology.japanese_is_withLang : japaneseWALS.andWithStatus = some AndWithStatus.withLang

theorem Phenomena.Coordination.Typology.mandarin_is_withLang : mandarinWALS.andWithStatus = some AndWithStatus.withLang

theorem Phenomena.Coordination.Typology.korean_is_andLang : koreanWALS.andWithStatus = some AndWithStatus.andLang

theorem Phenomena.Coordination.Typology.turkish_is_andLang : turkishWALS.andWithStatus = some AndWithStatus.andLang

theorem Phenomena.Coordination.Typology.finnish_is_andLang : finnishWALS.andWithStatus = some AndWithStatus.andLang

theorem Phenomena.Coordination.Typology.hungarian_is_andLang : hungarianWALS.andWithStatus = some AndWithStatus.andLang

theorem Phenomena.Coordination.Typology.hindi_is_andLang : hindiWALS.andWithStatus = some AndWithStatus.andLang

theorem Phenomena.Coordination.Typology.arabic_is_andLang : arabicWALS.andWithStatus = some AndWithStatus.andLang

theorem Phenomena.Coordination.Typology.swahili_is_withLang : swahiliWALS.andWithStatus = some AndWithStatus.withLang

theorem Phenomena.Coordination.Typology.tagalog_is_andLang : tagalogWALS.andWithStatus = some AndWithStatus.andLang