@cite{stassen-2000} — AND-languages and WITH-languages

Linguistic Typology 4(1), 1-54.

Core Contribution

A binary typological parameter classifying languages by how they encode NP conjunction:

• AND-languages: have a structurally distinct coordinate strategy (balanced, symmetric, plural agreement) alongside a separate comitative ("with") construction.
• WITH-languages: use comitative encoding as the only strategy for NP conjunction — the "and" marker is lexically identical to "with".

Key Claims

1. The AND/WITH parameter is diagnosed by lexical identity: if "and" = "with", the language is WITH; if "and" ≠ "with", it is AND.

2. WITH→AND drift: diachronically, WITH-languages tend to grammaticalize toward AND-status (comitative markers become balanced coordinators). The reverse drift (AND→WITH) does not occur.

3. Correlational parameters: AND-status correlates with "casedness" (bound case morphology) and "tensedness" (obligatory bound tense marking). These are statistical tendencies, not absolute universals.

Integration

The AND/WITH parameter is derived from WALS Ch 63 (ConjComitativeRelation) via AndWithStatus in Typology.lean, following the "derive, don't duplicate" principle. This file adds:

• Stassen's strategy feature diagnostics (coordinate vs comitative encoding)
• Fragment↔Typology bridge theorems for Georgian, Hungarian, Latin, Irish
• The WITH→AND drift linked to DiachronicSource.comitative
• Correlational parameter types (sorry-marked: statistical tendencies)

2026 Consensus

The AND/WITH distinction is well-established and encoded in WALS Ch 63A (authored by @cite{haspelmath-2007}, building on Stassen's framework). The diachronic WITH→AND drift is broadly accepted. The correlational parameters (casedness, tensedness) are the least settled — recognized as tendencies but with many counterexamples.

inductive Phenomena.Coordination.Studies.Stassen2000.ConjunctionEncoding : Type

@cite{stassen-2000}'s two encoding strategies for NP conjunction.

Coordinate encoding: balanced, symmetric structure where both conjuncts have equal syntactic rank. Diagnostics: constituent status, plural agreement, dedicated coordinator morpheme distinct from comitative.

Comitative encoding: asymmetric structure where one NP is the "companion" of another, modeled on "A with B". Diagnostics: comitative case marking, no obligatory plural agreement, "and" = "with" lexically.

• coordinate : ConjunctionEncoding
• comitative : ConjunctionEncoding

instance Phenomena.Coordination.Studies.Stassen2000.instDecidableEqConjunctionEncoding : DecidableEq ConjunctionEncoding

Equations

• Phenomena.Coordination.Studies.Stassen2000.instDecidableEqConjunctionEncoding x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Coordination.Studies.Stassen2000.instBEqConjunctionEncoding.beq : ConjunctionEncoding → ConjunctionEncoding → Bool

Equations

• Phenomena.Coordination.Studies.Stassen2000.instBEqConjunctionEncoding.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Coordination.Studies.Stassen2000.instBEqConjunctionEncoding : BEq ConjunctionEncoding

Equations

• Phenomena.Coordination.Studies.Stassen2000.instBEqConjunctionEncoding = { beq := Phenomena.Coordination.Studies.Stassen2000.instBEqConjunctionEncoding.beq }

def Phenomena.Coordination.Studies.Stassen2000.instReprConjunctionEncoding.repr : ConjunctionEncoding → ℕ → Std.Format

Equations

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

instance Phenomena.Coordination.Studies.Stassen2000.instReprConjunctionEncoding : Repr ConjunctionEncoding

Equations

• Phenomena.Coordination.Studies.Stassen2000.instReprConjunctionEncoding = { reprPrec := Phenomena.Coordination.Studies.Stassen2000.instReprConjunctionEncoding.repr }

structure Phenomena.Coordination.Studies.Stassen2000.StrategyFeatures : Type

Diagnostic features for distinguishing coordinate from comitative encoding. Based on @cite{stassen-2000}'s structural diagnostics for balanced vs dependent encoding.

• equalRank : Bool

  Both conjuncts have equal syntactic rank (neither is embedded).

• constituency : Bool

  The conjoined phrase forms a syntactic constituent.

• pluralAgreement : Bool

  The conjoined subject triggers plural agreement on the verb.

• uniqueMarker : Bool

  The coordination marker is a dedicated form, not identical to "with".

instance Phenomena.Coordination.Studies.Stassen2000.instDecidableEqStrategyFeatures : DecidableEq StrategyFeatures

Equations

• Phenomena.Coordination.Studies.Stassen2000.instDecidableEqStrategyFeatures = Phenomena.Coordination.Studies.Stassen2000.instDecidableEqStrategyFeatures.decEq

def Phenomena.Coordination.Studies.Stassen2000.instDecidableEqStrategyFeatures.decEq (x✝ x✝¹ : StrategyFeatures) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.Coordination.Studies.Stassen2000.instBEqStrategyFeatures : BEq StrategyFeatures

Equations

• Phenomena.Coordination.Studies.Stassen2000.instBEqStrategyFeatures = { beq := Phenomena.Coordination.Studies.Stassen2000.instBEqStrategyFeatures.beq }

def Phenomena.Coordination.Studies.Stassen2000.instBEqStrategyFeatures.beq : StrategyFeatures → StrategyFeatures → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Coordination.Studies.Stassen2000.instBEqStrategyFeatures.beq x✝¹ x✝ = false

def Phenomena.Coordination.Studies.Stassen2000.instReprStrategyFeatures.repr : StrategyFeatures → ℕ → Std.Format

Equations

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

instance Phenomena.Coordination.Studies.Stassen2000.instReprStrategyFeatures : Repr StrategyFeatures

Equations

• Phenomena.Coordination.Studies.Stassen2000.instReprStrategyFeatures = { reprPrec := Phenomena.Coordination.Studies.Stassen2000.instReprStrategyFeatures.repr }

def Phenomena.Coordination.Studies.Stassen2000.coordinateFeatures : StrategyFeatures

Coordinate strategies have all four diagnostic properties.

Equations

• Phenomena.Coordination.Studies.Stassen2000.coordinateFeatures = { equalRank := true, constituency := true, pluralAgreement := true, uniqueMarker := true }

def Phenomena.Coordination.Studies.Stassen2000.comitativeFeatures : StrategyFeatures

Comitative strategies lack all four (prototypically).

Equations

• Phenomena.Coordination.Studies.Stassen2000.comitativeFeatures = { equalRank := false, constituency := false, pluralAgreement := false, uniqueMarker := false }

def Phenomena.Coordination.Studies.Stassen2000.StrategyFeatures.isCoordinate (f : StrategyFeatures) : Bool

A strategy counts as coordinate iff all four features are positive.

Equations

• f.isCoordinate = (f.equalRank && f.constituency && f.pluralAgreement && f.uniqueMarker)

theorem Phenomena.Coordination.Studies.Stassen2000.coordinateFeatures_is_coordinate : coordinateFeatures.isCoordinate = true

theorem Phenomena.Coordination.Studies.Stassen2000.comitativeFeatures_is_not_coordinate : comitativeFeatures.isCoordinate = false

inductive Phenomena.Coordination.Studies.Stassen2000.DriftDirection : Type

@cite{stassen-2000}: diachronic drift is unidirectional — WITH → AND. Comitative markers grammaticalize into balanced coordinators over time, but the reverse does not occur. This is the same process captured by DiachronicSource.comitative in the Haspelmath typology: a "with" marker becomes a conjunction marker, moving the language from WITH-status to AND-status.

• withToAnd : DriftDirection
• andToWith : DriftDirection

instance Phenomena.Coordination.Studies.Stassen2000.instDecidableEqDriftDirection : DecidableEq DriftDirection

Equations

• Phenomena.Coordination.Studies.Stassen2000.instDecidableEqDriftDirection x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Coordination.Studies.Stassen2000.instBEqDriftDirection : BEq DriftDirection

Equations

• Phenomena.Coordination.Studies.Stassen2000.instBEqDriftDirection = { beq := Phenomena.Coordination.Studies.Stassen2000.instBEqDriftDirection.beq }

def Phenomena.Coordination.Studies.Stassen2000.instBEqDriftDirection.beq : DriftDirection → DriftDirection → Bool

Equations

• Phenomena.Coordination.Studies.Stassen2000.instBEqDriftDirection.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Coordination.Studies.Stassen2000.instReprDriftDirection : Repr DriftDirection

Equations

• Phenomena.Coordination.Studies.Stassen2000.instReprDriftDirection = { reprPrec := Phenomena.Coordination.Studies.Stassen2000.instReprDriftDirection.repr }

def Phenomena.Coordination.Studies.Stassen2000.instReprDriftDirection.repr : DriftDirection → ℕ → Std.Format

Equations

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

def Phenomena.Coordination.Studies.Stassen2000.attestedDrift : DriftDirection

The only attested drift direction is WITH → AND.

Equations

• Phenomena.Coordination.Studies.Stassen2000.attestedDrift = Phenomena.Coordination.Studies.Stassen2000.DriftDirection.withToAnd

def Phenomena.Coordination.Studies.Stassen2000.DriftDirection.toDiachronicSource : DriftDirection → Option Typology.DiachronicSource

@cite{stassen-2000}'s WITH→AND drift corresponds to @cite{haspelmath-2007}'s comitative diachronic source: a comitative marker grammaticalizing into a coordinator is exactly the mechanism by which a WITH-language becomes an AND-language.

Equations

• Phenomena.Coordination.Studies.Stassen2000.DriftDirection.withToAnd.toDiachronicSource = some Phenomena.Coordination.Typology.DiachronicSource.comitative
• Phenomena.Coordination.Studies.Stassen2000.DriftDirection.andToWith.toDiachronicSource = none

theorem Phenomena.Coordination.Studies.Stassen2000.attested_drift_is_comitative : DriftDirection.withToAnd.toDiachronicSource = some Typology.DiachronicSource.comitative

The attested drift direction (WITH→AND) corresponds to comitative source.

theorem Phenomena.Coordination.Studies.Stassen2000.drift_yields_monosyndetic : Typology.DiachronicSource.comitative.expectedPattern = Typology.Syndesis.monosyndetic

Comitative-sourced coordinators yield monosyndetic patterns, connecting Stassen's diachronic drift to Haspelmath's structural typology: WITH→AND drift → comitative source → monosyndetic pattern.

inductive Phenomena.Coordination.Studies.Stassen2000.Casedness : Type

@cite{stassen-2000}: "Casedness" — whether a language has bound case morphology on core argument NPs. Correlates statistically with AND-status.

• cased : Casedness
• uncased : Casedness

instance Phenomena.Coordination.Studies.Stassen2000.instDecidableEqCasedness : DecidableEq Casedness

Equations

• Phenomena.Coordination.Studies.Stassen2000.instDecidableEqCasedness x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Coordination.Studies.Stassen2000.instBEqCasedness : BEq Casedness

Equations

• Phenomena.Coordination.Studies.Stassen2000.instBEqCasedness = { beq := Phenomena.Coordination.Studies.Stassen2000.instBEqCasedness.beq }

def Phenomena.Coordination.Studies.Stassen2000.instBEqCasedness.beq : Casedness → Casedness → Bool

Equations

• Phenomena.Coordination.Studies.Stassen2000.instBEqCasedness.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Coordination.Studies.Stassen2000.instReprCasedness.repr : Casedness → ℕ → Std.Format

Equations

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

instance Phenomena.Coordination.Studies.Stassen2000.instReprCasedness : Repr Casedness

Equations

• Phenomena.Coordination.Studies.Stassen2000.instReprCasedness = { reprPrec := Phenomena.Coordination.Studies.Stassen2000.instReprCasedness.repr }

inductive Phenomena.Coordination.Studies.Stassen2000.Tensedness : Type

@cite{stassen-2000}: "Tensedness" — whether a language has obligatory bound past/non-past marking on verbs. Correlates statistically with AND-status.

• tensed : Tensedness
• untensed : Tensedness

instance Phenomena.Coordination.Studies.Stassen2000.instDecidableEqTensedness : DecidableEq Tensedness

Equations

• Phenomena.Coordination.Studies.Stassen2000.instDecidableEqTensedness x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Coordination.Studies.Stassen2000.instBEqTensedness : BEq Tensedness

Equations

• Phenomena.Coordination.Studies.Stassen2000.instBEqTensedness = { beq := Phenomena.Coordination.Studies.Stassen2000.instBEqTensedness.beq }

def Phenomena.Coordination.Studies.Stassen2000.instBEqTensedness.beq : Tensedness → Tensedness → Bool

Equations

• Phenomena.Coordination.Studies.Stassen2000.instBEqTensedness.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Coordination.Studies.Stassen2000.instReprTensedness : Repr Tensedness

Equations

• Phenomena.Coordination.Studies.Stassen2000.instReprTensedness = { reprPrec := Phenomena.Coordination.Studies.Stassen2000.instReprTensedness.repr }

def Phenomena.Coordination.Studies.Stassen2000.instReprTensedness.repr : Tensedness → ℕ → Std.Format

Equations

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

theorem Phenomena.Coordination.Studies.Stassen2000.casedness_skews_andWith : ∃ (casedAND : ℕ) (casedWITH : ℕ) (uncasedAND : ℕ) (uncasedWITH : ℕ), casedAND + casedWITH + uncasedAND + uncasedWITH = 260 ∧ casedAND * (uncasedAND + uncasedWITH) > uncasedAND * (casedAND + casedWITH)

@cite{stassen-2000}: among cased languages, AND-status is more frequent than WITH-status; among uncased languages, the reverse holds. Stated as: there exists a partition of the 260-language sample into four cells (cased×AND, cased×WITH, uncased×AND, uncased×WITH) such that the proportion of AND among cased exceeds the proportion among uncased. Cross-multiplied to avoid rationals. [sorry: requires the cross-tabulation from the paper]

theorem Phenomena.Coordination.Studies.Stassen2000.tensedness_skews_andWith : ∃ (tensedAND : ℕ) (tensedWITH : ℕ) (untensedAND : ℕ) (untensedWITH : ℕ), tensedAND + tensedWITH + untensedAND + untensedWITH = 260 ∧ tensedAND * (untensedAND + untensedWITH) > untensedAND * (tensedAND + tensedWITH)

@cite{stassen-2000}: among tensed languages, AND-status is more frequent than WITH-status; among untensed languages, the reverse holds. Same cross-multiplication encoding as casedness_skews_andWith. [sorry: requires the cross-tabulation from the paper]

Fragment Bridges

These theorems verify that morpheme data in independently-defined Fragment entries is consistent with the corresponding Typology ConjunctionSystem entries. Since the Fragment types (CoordRole, Boundness, CoordEntry) are defined independently per language, we compare via string-valued fields (.form). This means a change to either side breaks the relevant theorem.

theorem Phenomena.Coordination.Studies.Stassen2000.georgian_j_bridge : ((List.filter (fun (x : Typology.ConjMorpheme) => x.role == "J") Typology.georgian.morphemes).any fun (x : Typology.ConjMorpheme) => x.form == "da") = true ∧ Fragments.Georgian.Coordination.da.form = "da"

Georgian Fragment's J morpheme "da" matches Typology's Georgian "da".

theorem Phenomena.Coordination.Studies.Stassen2000.georgian_mu_bridge : ((List.filter (fun (x : Typology.ConjMorpheme) => x.role == "MU") Typology.georgian.morphemes).any fun (x : Typology.ConjMorpheme) => x.form == "-c") = true ∧ Fragments.Georgian.Coordination.c_.form = "-c"

Georgian Fragment's MU morpheme "-c" matches Typology's Georgian "-c".

theorem Phenomena.Coordination.Studies.Stassen2000.georgian_mu_bound_bridge : ((List.filter (fun (x : Typology.ConjMorpheme) => x.role == "MU") Typology.georgian.morphemes).all fun (x : Typology.ConjMorpheme) => x.boundness == Typology.Boundness.bound) = true ∧ (Fragments.Georgian.Coordination.c_.boundness == Fragments.Georgian.Coordination.Boundness.bound) = true

Georgian MU is bound in both Fragment and Typology.

theorem Phenomena.Coordination.Studies.Stassen2000.georgian_mu_additive_bridge : ((List.filter (fun (x : Typology.ConjMorpheme) => x.role == "MU") Typology.georgian.morphemes).all fun (x : Typology.ConjMorpheme) => x.alsoAdditive) = true ∧ Fragments.Georgian.Coordination.c_.alsoAdditive = true

Georgian MU is additive in both Fragment and Typology.

theorem Phenomena.Coordination.Studies.Stassen2000.hungarian_j_bridge : ((List.filter (fun (x : Typology.ConjMorpheme) => x.role == "J") Typology.hungarian.morphemes).any fun (x : Typology.ConjMorpheme) => x.form == "és") = true ∧ Fragments.Hungarian.Coordination.es.form = "és"

Hungarian Fragment's J morpheme "és" matches Typology's Hungarian "és".

theorem Phenomena.Coordination.Studies.Stassen2000.hungarian_mu_bridge : ((List.filter (fun (x : Typology.ConjMorpheme) => x.role == "MU") Typology.hungarian.morphemes).any fun (x : Typology.ConjMorpheme) => x.form == "is") = true ∧ Fragments.Hungarian.Coordination.is_.form = "is"

Hungarian Fragment's MU morpheme "is" matches Typology's Hungarian "is".

theorem Phenomena.Coordination.Studies.Stassen2000.hungarian_mu_free_bridge : ((List.filter (fun (x : Typology.ConjMorpheme) => x.role == "MU") Typology.hungarian.morphemes).all fun (x : Typology.ConjMorpheme) => x.boundness == Typology.Boundness.free) = true ∧ (Fragments.Hungarian.Coordination.is_.boundness == Fragments.Hungarian.Coordination.Boundness.free) = true

Hungarian MU is free in both Fragment and Typology.

theorem Phenomena.Coordination.Studies.Stassen2000.hungarian_mu_additive_bridge : ((List.filter (fun (x : Typology.ConjMorpheme) => x.role == "MU") Typology.hungarian.morphemes).all fun (x : Typology.ConjMorpheme) => x.alsoAdditive) = true ∧ Fragments.Hungarian.Coordination.is_.alsoAdditive = true

Hungarian MU is additive in both Fragment and Typology.

theorem Phenomena.Coordination.Studies.Stassen2000.latin_j_bridge : ((List.filter (fun (x : Typology.ConjMorpheme) => x.role == "J") Typology.latin.morphemes).any fun (x : Typology.ConjMorpheme) => x.form == "et") = true ∧ Fragments.Latin.Coordination.et.form = "et"

Latin Fragment's J morpheme "et" matches Typology's Latin "et".

theorem Phenomena.Coordination.Studies.Stassen2000.latin_mu_bridge : ((List.filter (fun (x : Typology.ConjMorpheme) => x.role == "MU") Typology.latin.morphemes).any fun (x : Typology.ConjMorpheme) => x.form == "-que") = true ∧ Fragments.Latin.Coordination.que.form = "-que"

Latin Fragment's MU morpheme "-que" matches Typology's Latin "-que".

theorem Phenomena.Coordination.Studies.Stassen2000.latin_mu_bound_bridge : ((List.filter (fun (x : Typology.ConjMorpheme) => x.role == "MU") Typology.latin.morphemes).all fun (x : Typology.ConjMorpheme) => x.boundness == Typology.Boundness.bound) = true ∧ (Fragments.Latin.Coordination.que.boundness == Fragments.Latin.Coordination.Boundness.bound) = true

Latin MU is bound in both Fragment and Typology.

theorem Phenomena.Coordination.Studies.Stassen2000.irish_j_bridge : ((List.filter (fun (x : Typology.ConjMorpheme) => x.role == "J") Typology.irish.morphemes).any fun (x : Typology.ConjMorpheme) => x.form == "agus") = true ∧ Fragments.Irish.Coordination.agus.form = "agus"

Irish Fragment's J morpheme "agus" matches Typology's Irish "agus".

theorem Phenomena.Coordination.Studies.Stassen2000.irish_j_only_bridge : (List.filter (fun (x : Typology.ConjMorpheme) => x.role == "MU") Typology.irish.morphemes).length = 0 ∧ (List.filter (fun (x : Fragments.Irish.Coordination.CoordEntry) => x.role == Fragments.Irish.Coordination.CoordRole.j) Fragments.Irish.Coordination.allEntries).length = 1

Irish has no MU morpheme — J-only in both Fragment and Typology.

theorem Phenomena.Coordination.Studies.Stassen2000.boundness_asymmetry_bridge : Typology.georgian.muBoundness = some Typology.Boundness.bound ∧ Typology.hungarian.muBoundness = some Typology.Boundness.free ∧ (Fragments.Georgian.Coordination.c_.boundness == Fragments.Georgian.Coordination.Boundness.bound) = true ∧ (Fragments.Hungarian.Coordination.is_.boundness == Fragments.Hungarian.Coordination.Boundness.free) = true

The Fragment-level boundness asymmetry between Georgian MU (bound) and Hungarian MU (free) is consistent with the Typology-level asymmetry. This connects @cite{bill-etal-2025}'s acquisition data (Georgian children found J-MU harder) to the morphological difference.