Stassen (2000): AND-languages and WITH-languages

@cite{stassen-2000} @cite{haspelmath-2007} @cite{dryer-haspelmath-2013}

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.toAndWithStatus in Linglib/Typology/Coordination.lean. This file adds:

• The 15-language WALS coordination sample (CoordinationProfile).
• Stassen's strategy feature diagnostics (coordinate vs comitative).
• The WITH→AND drift linked to DiachronicSource.comitative.
• Correlational parameter types (sorry-marked: statistical tendencies).
• Cross-module bridge: Japanese MU = additive = universal quantifier.

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 recognised as tendencies but with many counterexamples.

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

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

Coordinate: balanced, symmetric structure where both conjuncts have equal syntactic rank. Comitative: asymmetric structure modeled on "A with B".

• coordinate : ConjunctionEncoding
• comitative : ConjunctionEncoding

@[implicit_reducible]

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)

@[implicit_reducible]

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.

@[implicit_reducible]

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.

• equalRank : Bool

  Both conjuncts have equal syntactic rank.

• 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".

@[implicit_reducible]

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.

@[implicit_reducible]

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.

@[implicit_reducible]

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

Equations

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

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

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

def Phenomena.Coordination.Studies.Stassen2000.englishWALS : Typology.Coordination.CoordinationProfile

Equations

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

def Phenomena.Coordination.Studies.Stassen2000.germanWALS : Typology.Coordination.CoordinationProfile

Equations

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

def Phenomena.Coordination.Studies.Stassen2000.frenchWALS : Typology.Coordination.CoordinationProfile

Equations

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

def Phenomena.Coordination.Studies.Stassen2000.spanishWALS : Typology.Coordination.CoordinationProfile

Equations

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

def Phenomena.Coordination.Studies.Stassen2000.russianWALS : Typology.Coordination.CoordinationProfile

Equations

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

def Phenomena.Coordination.Studies.Stassen2000.japaneseWALS : Typology.Coordination.CoordinationProfile

Equations

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

def Phenomena.Coordination.Studies.Stassen2000.mandarinWALS : Typology.Coordination.CoordinationProfile

Equations

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

def Phenomena.Coordination.Studies.Stassen2000.koreanWALS : Typology.Coordination.CoordinationProfile

Equations

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

def Phenomena.Coordination.Studies.Stassen2000.turkishWALS : Typology.Coordination.CoordinationProfile

Equations

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

def Phenomena.Coordination.Studies.Stassen2000.finnishWALS : Typology.Coordination.CoordinationProfile

Equations

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

def Phenomena.Coordination.Studies.Stassen2000.hungarianWALS : Typology.Coordination.CoordinationProfile

Equations

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

def Phenomena.Coordination.Studies.Stassen2000.hindiWALS : Typology.Coordination.CoordinationProfile

Equations

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

def Phenomena.Coordination.Studies.Stassen2000.arabicWALS : Typology.Coordination.CoordinationProfile

Equations

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

def Phenomena.Coordination.Studies.Stassen2000.swahiliWALS : Typology.Coordination.CoordinationProfile

Equations

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

def Phenomena.Coordination.Studies.Stassen2000.tagalogWALS : Typology.Coordination.CoordinationProfile

Equations

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

def Phenomena.Coordination.Studies.Stassen2000.allWALSProfiles : List Typology.Coordination.CoordinationProfile

Equations

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

theorem Phenomena.Coordination.Studies.Stassen2000.wals_profile_count : allWALSProfiles.length = 15

def Phenomena.Coordination.Studies.Stassen2000.andCount : ℕ

Count of AND-languages in the sample.

Equations

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

def Phenomena.Coordination.Studies.Stassen2000.withCount : ℕ

Count of WITH-languages in the sample.

Equations

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

theorem Phenomena.Coordination.Studies.Stassen2000.and_outnumbers_with_in_sample : andCount > withCount

theorem Phenomena.Coordination.Studies.Stassen2000.with_languages_count : withCount = 3

Two WITH-languages in the sample (Japanese, Mandarin, Swahili — and = with).

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

@cite{stassen-2000}: diachronic drift is unidirectional — WITH → AND. Comitative markers grammaticalise into balanced coordinators over time; the reverse does not occur.

• withToAnd : DriftDirection
• andToWith : DriftDirection

@[implicit_reducible]

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 ⋯

@[implicit_reducible]

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)

@[implicit_reducible]

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.Coordination.DiachronicSource

@cite{stassen-2000}'s WITH→AND drift corresponds to @cite{haspelmath-2007}'s comitative diachronic source.

Equations

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

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

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

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

Comitative-sourced coordinators yield monosyndetic patterns: 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

@[implicit_reducible]

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 ⋯

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

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

Equations

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

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

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

• tensed : Tensedness
• untensed : Tensedness

@[implicit_reducible]

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 ⋯

@[implicit_reducible]

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)

@[implicit_reducible]

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. Cross-multiplied existential. [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.

theorem Phenomena.Coordination.Studies.Stassen2000.japanese_mu_quantifier_bridge : Fragments.Japanese.Coordination.mo.alsoQuantifier = true ∧ Fragments.Japanese.Coordination.mo.alsoAdditive = true ∧ Fragments.Japanese.Determiners.dare_mo.particle = some "mo"

Japanese MU "mo" also serves as a quantifier particle — the Fragment records this via alsoQuantifier, and the Determiners fragment independently records "mo" as the particle in dare-mo (universal). Triple identity: MU = additive = ∀.