Dalrymple & Kaplan 2000: Feature Indeterminacy and Feature Resolution

[DK00]

Set-valued syntactic features, against atomic-value-plus-equality. Two phenomena, one representational move (§4, eq. 25: "Sets encode indeterminate feature possibilities"):

• Indeterminacy (distributive features: case, noun class, vform): a syncretic form bears a set of atomic values — German was {NOM, ACC} — and contextual requirements are membership assertions (ACC ∈ (↑ OBJ CASE)), not equalities. The paper refutes the two obvious alternatives: disjunctive specification DNF-collapses into a homophone listing (§3.1), and underspecification both derives NOM = ACC by transitivity of equality and overgenerates dative contexts (§3.2).
• Resolution (nondistributive features: person, gender): a coordinate phrase's person/gender is the union of its conjuncts' marker sets (§6, §7) — person values are subsets of {S, H} ({S} 1exc, {S,H} 1inc, {H} 2nd, {} 3rd), and the union analysis predicts the full Fula paradigm (87–88), the collapsed English/Spanish/Slovak system (91–92), and the gender tables of Hindi (112), Icelandic (120), and Slovene with the conjunction contributing F (126–127).

The deliberate sharp line (§8): resolving features are never indeterminate — Hindi wah is masc-or-fem by wide-scope disjunction (ambiguity), not by a set value, which is why *wah arrived.MASC and arrived.FEM fails (128).

This is the flagship counterexample to treating the flat information order (Morphology/Unification.lean) as linguistically definitional: indeterminate agreement is an annotation-level phenomenon demanding non-flat (set-valued) slots. toIndet below certifies the relationship — the flat order embeds into the (superset-ordered) indeterminacy lattice as the determinate fragment, with none (no information) mapping to the universal set.

Formal highlights replicated as theorems: the German/Polish contrast set ((17)/(28) vs (32); (40) vs (41)), the §3 refutations, verb-side indeterminacy (Xhosa (56), Chicheŵa (59), German kaufen (62)), the resolution tables, the minimal-model derivation of José y tu (96–97), the Sag-et-al intersection refutation (§6.5, (100)–(101) vs Fula), and the De Morgan duality (102–103) — which is mathlib's Finset.compl_union. The person-marker sets also project onto the binary person decomposition of Features/Person.lean, with the inclusive/exclusive collapse made explicit.

§4: indeterminate values are sets; checking is membership

@[reducible, inline]

abbrev DalrympleKaplan2000.IndetVal (α : Type u_1) : Type u_1

An indeterminate feature value: the set of atomic values the form can realize (eq. 25). Singleton = determinate.

Equations

• DalrympleKaplan2000.IndetVal α = Finset α

@[reducible, inline]

abbrev DalrympleKaplan2000.requires {α : Type u_1} [DecidableEq α] (c : α) (v : IndetVal α) : Prop

Contextual requirement (eq. 27): the required atom is a member of the value set.

Equations

• DalrympleKaplan2000.requires c v = (c ∈ v)

def DalrympleKaplan2000.wer : IndetVal Case

German relative pronouns (26): wer nominative, was syncretic, wem dative.

Equations

• DalrympleKaplan2000.wer = {Case.nom}

def DalrympleKaplan2000.was : IndetVal Case

Equations

• DalrympleKaplan2000.was = {Case.nom, Case.acc}

def DalrympleKaplan2000.wem : IndetVal Case

Equations

• DalrympleKaplan2000.wem = {Case.dat}

theorem DalrympleKaplan2000.was_satisfies_both : requires Case.acc was ∧ requires Case.nom was

(17)/(28): Ich habe gegessen was übrig war — was satisfies the matrix verb's accusative requirement and the relative clause's nominative requirement at once.

theorem DalrympleKaplan2000.wem_fails_matrix : requires Case.dat wem ∧ ¬requires Case.nom wem

(32): *Wem du vertraust muss klug sein — wem {DAT} satisfies vertraut but not the matrix NOM ∈ requirement.

def DalrympleKaplan2000.kogo : IndetVal Case

Polish (40)/(41): kogo {ACC, GEN} survives coordination of an ACC-taking and a GEN-taking verb; co {NOM, ACC} does not.

Equations

• DalrympleKaplan2000.kogo = {Case.acc, Case.gen}

def DalrympleKaplan2000.co : IndetVal Case

Equations

• DalrympleKaplan2000.co = {Case.nom, Case.acc}

theorem DalrympleKaplan2000.kogo_grammatical : requires Case.acc kogo ∧ requires Case.gen kogo

theorem DalrympleKaplan2000.co_ungrammatical : requires Case.acc co ∧ ¬requires Case.gen co

§3: why the rival accounts fail

def DalrympleKaplan2000.atomicSatisfies (x : Case) (reqs : List Case) : Prop

An atomic-value account: one case value checked by equality against every requirement.

Equations

• DalrympleKaplan2000.atomicSatisfies x reqs = ∀ r ∈ reqs, x = r

theorem DalrympleKaplan2000.underspecification_fails : ¬∃ (x : Case), atomicSatisfies x [Case.acc, Case.nom]

§3.2 (eq. 24): no single atomic value satisfies both verbs of (17) — transitivity of equality would force NOM = ACC.

theorem DalrympleKaplan2000.disjunction_collapses (x : Case) : x ∈ was → ¬atomicSatisfies x [Case.acc, Case.nom]

§3.1 (18)–(21): disjunctive specification means choosing one disjunct per utterance — and every choice from {NOM, ACC} fails one of the two requirements. The set-based account (was_satisfies_both) succeeds where every disjunctive resolution fails: that contrast is the paper's argument.

§4.4: indeterminate requirements (verb-side sets)

theorem DalrympleKaplan2000.xhosa_zibomvu : 7 ∈ {7, 9} ∧ 9 ∈ {7, 9}

Xhosa (54)–(56): zibomvu requires its subject's noun class to be in {7/8, 9/10} (classes as their singular-class numbers), so class-7/8 izandla and class-9/10 neendlebe conjuncts each satisfy it.

def DalrympleKaplan2000.kaufenReq : IndetVal UD.Person

German (60)–(63): kaufen imposes (↑ SUBJ PERSON) ∈ {1, 3}; right-node raising over a 1-person and a 3-person subject satisfies the requirement in each conjunct.

Equations

• DalrympleKaplan2000.kaufenReq = {UD.Person.first, UD.Person.third}

theorem DalrympleKaplan2000.kaufen_rnr : requires UD.Person.first kaufenReq ∧ requires UD.Person.third kaufenReq ∧ ¬requires UD.Person.second kaufenReq

The refinement certificate: the flat order is the determinate fragment

Morphology/Unification.lean's flat slot order embeds into the indeterminacy lattice: a determinate commitment some x is the singleton {x}, and no information is the universal set (any realization possible). Information increases as sets shrink, so the embedding is order-reversing into ⊆ — i.e. an embedding into the superset order. Set-valued slots are a refinement of the flat layer, not a rival to it.

def DalrympleKaplan2000.toIndet (a : Option Case) : IndetVal Case

A flat slot as an indeterminate value: none = no commitment = anything goes.

Equations

• DalrympleKaplan2000.toIndet none = Finset.univ
• DalrympleKaplan2000.toIndet (some x) = {x}

theorem DalrympleKaplan2000.toIndet_injective : Function.Injective toIndet

theorem DalrympleKaplan2000.flatLE_iff_toIndet_superset (a b : Option Case) : a.FlatLE b ↔ toIndet b ⊆ toIndet a

The embedding certificate: flat subsumption is superset inclusion of realization sets. More committed = smaller set; none sits below everything because univ contains everything.

§§5–6: feature resolution — person as marker sets, resolution as union

inductive DalrympleKaplan2000.Marker : Type

The person markers (§6): S speaker, H hearer. §6.3 argues no third marker is attested (Sierra Popoluca's "limited inclusive" is an inclusive dual, per Noyer).

• S : Marker
• H : Marker

@[implicit_reducible]

instance DalrympleKaplan2000.instDecidableEqMarker : DecidableEq Marker

Equations

• DalrympleKaplan2000.instDecidableEqMarker x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def DalrympleKaplan2000.instReprMarker.repr : Marker → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance DalrympleKaplan2000.instReprMarker : Repr Marker

Equations

• DalrympleKaplan2000.instReprMarker = { reprPrec := DalrympleKaplan2000.instReprMarker.repr }

@[implicit_reducible]

instance DalrympleKaplan2000.instFintypeMarker : Fintype Marker

Equations

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

@[reducible, inline]

abbrev DalrympleKaplan2000.PersonSet : Type

Equations

• DalrympleKaplan2000.PersonSet = Finset DalrympleKaplan2000.Marker

def DalrympleKaplan2000.fula1exc : PersonSet

Fula's four-way system (87): full use of the marker inventory.

Equations

• DalrympleKaplan2000.fula1exc = {DalrympleKaplan2000.Marker.S}

def DalrympleKaplan2000.fula1inc : PersonSet

Equations

• DalrympleKaplan2000.fula1inc = {DalrympleKaplan2000.Marker.S, DalrympleKaplan2000.Marker.H}

def DalrympleKaplan2000.fula2 : PersonSet

Equations

• DalrympleKaplan2000.fula2 = {DalrympleKaplan2000.Marker.H}

def DalrympleKaplan2000.fula3 : PersonSet

Equations

• DalrympleKaplan2000.fula3 = ∅

def DalrympleKaplan2000.resolve (p q : PersonSet) : PersonSet

Resolution is union (77, 93): "the person feature of a coordinate structure is resolved to be the UNION of the person features of the conjuncts".

Equations

• DalrympleKaplan2000.resolve p q = p ∪ q

theorem DalrympleKaplan2000.fula_table : resolve fula1exc fula2 = fula1inc ∧ resolve (resolve fula1exc fula2) fula3 = fula1inc ∧ resolve fula1exc fula3 = fula1exc ∧ resolve fula2 fula3 = fula2 ∧ resolve fula3 fula3 = fula3

The Fula resolution table (78)/(88), in full.

def DalrympleKaplan2000.eng1 : PersonSet

English/Spanish/Slovak collapse the inclusive/exclusive distinction (§6.2): all first person is {S, H} — preserving only attested syntactic distinctions at the cost of the referential correlation (Aronoff's impersonal you, French on).

Equations

• DalrympleKaplan2000.eng1 = {DalrympleKaplan2000.Marker.S, DalrympleKaplan2000.Marker.H}

def DalrympleKaplan2000.eng2 : PersonSet

Equations

• DalrympleKaplan2000.eng2 = {DalrympleKaplan2000.Marker.H}

def DalrympleKaplan2000.eng3 : PersonSet

Equations

• DalrympleKaplan2000.eng3 = ∅

theorem DalrympleKaplan2000.english_table : resolve eng1 eng2 = eng1 ∧ resolve eng1 eng3 = eng1 ∧ resolve eng2 eng3 = eng2 ∧ resolve eng3 eng3 = eng3

The collapsed-system resolution table (91)/(92).

theorem DalrympleKaplan2000.jose_y_tu : resolve eng3 eng2 = eng2 ∧ resolve eng3 eng2 ≠ eng1

José y tu habláis (95)–(99): the resolved person of 3 ∪ 2 is {H} — the minimal model — so the 2PL verb's constraining equation =c {H} succeeds and the 1PL verb's =c {S,H} fails.

The substrate bridge: Person.resolve is marker-set union

def DalrympleKaplan2000.markerSetOf : Person → Option PersonSet

The marker sets of the canonical quadripartition values — the Fula encoding (87). Plain first underdetermines clusivity (their §6.2 English collapse picks {S, H} by stipulation), and zero is outside the system, so both map to none.

Equations

• DalrympleKaplan2000.markerSetOf Person.firstExclusive = some DalrympleKaplan2000.fula1exc
• DalrympleKaplan2000.markerSetOf Person.firstInclusive = some DalrympleKaplan2000.fula1inc
• DalrympleKaplan2000.markerSetOf Person.second = some DalrympleKaplan2000.fula2
• DalrympleKaplan2000.markerSetOf Person.third = some DalrympleKaplan2000.fula3
• DalrympleKaplan2000.markerSetOf x✝ = none

theorem DalrympleKaplan2000.person_resolve_is_union (p q : Person) (sp sq : PersonSet) : markerSetOf p = some sp → markerSetOf q = some sq → markerSetOf (p.resolve q) = some (resolve sp sq)

The substrate's canonical resolution is the paper's union (77)/(93): on the quadripartition, Person.resolve commutes with the marker encoding — the same grounding Person.resolve_profile states intrinsically, here in the paper's own vocabulary.

theorem DalrympleKaplan2000.two_markers_four_persons : Fintype.card PersonSet = 4

Two markers bound the system (§6.3): at most four person values are expressible, matching the maximally differentiated (Fula-type) inventory.

§6.5: union vs intersection — Sag et al. refuted, De Morgan vindicated

def DalrympleKaplan2000.sag1 : PersonSet

Sag et al. 1985's marker sets (100): first = {}, second = {XSP}, third = {XSP, THP}, resolution by intersection. Reusing our two markers for their two.

Equations

• DalrympleKaplan2000.sag1 = ∅

def DalrympleKaplan2000.sag2 : PersonSet

Equations

• DalrympleKaplan2000.sag2 = {DalrympleKaplan2000.Marker.S}

def DalrympleKaplan2000.sag3 : PersonSet

Equations

• DalrympleKaplan2000.sag3 = {DalrympleKaplan2000.Marker.S, DalrympleKaplan2000.Marker.H}

theorem DalrympleKaplan2000.sag_intersection_fails : sag1 ∩ sag2 = sag1 ∩ sag3 ∧ resolve fula1exc fula2 ≠ resolve fula1exc fula3

The refutation (§6.5): with first person as ∅, intersection makes you and I and Bill and I indistinguishable — "it is in principle impossible to distinguish different kinds of coordination involving a first person pronoun", so Fula's inclusive/exclusive contrast is underivable. Union keeps them apart.

theorem DalrympleKaplan2000.union_intersection_duality (p q : PersonSet) : (p ∪ q)ᶜ = pᶜ ∩ qᶜ

The De Morgan duality (102)–(103): any union analysis transforms into an equivalent intersection analysis over complement sets (markers reread as absences). The paper's observation is mathlib's Finset.compl_union.

§7: gender resolution by the same mechanism

inductive DalrympleKaplan2000.GMark : Type

Gender markers; per-language assignments below reuse one inventory.

• M : GMark
• F : GMark
• N : GMark

@[implicit_reducible]

instance DalrympleKaplan2000.instDecidableEqGMark : DecidableEq GMark

Equations

• DalrympleKaplan2000.instDecidableEqGMark x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def DalrympleKaplan2000.instReprGMark.repr : GMark → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance DalrympleKaplan2000.instReprGMark : Repr GMark

Equations

• DalrympleKaplan2000.instReprGMark = { reprPrec := DalrympleKaplan2000.instReprGMark.repr }

@[implicit_reducible]

instance DalrympleKaplan2000.instFintypeGMark : Fintype GMark

Equations

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

@[reducible, inline]

abbrev DalrympleKaplan2000.GenderSet : Type

Equations

• DalrympleKaplan2000.GenderSet = Finset DalrympleKaplan2000.GMark

theorem DalrympleKaplan2000.hindi_table : {GMark.M} ∪ {GMark.M} = {GMark.M} ∧ {GMark.M} ∪ ∅ = {GMark.M} ∧ ∅ ∪ ∅ = ∅

Hindi (111): two genders, masculine {M}, feminine {} — mixed coordination resolves masculine (112).

theorem DalrympleKaplan2000.icelandic_mixed_is_neuter : {GMark.M} ∪ {GMark.F} = {GMark.M, GMark.F} ∧ {GMark.M} ∪ {GMark.M, GMark.F} = {GMark.M, GMark.F} ∧ {GMark.F} ∪ {GMark.M, GMark.F} = {GMark.M, GMark.F}

Icelandic (119): masc {M}, fem {F}, neut {M, F} — like genders preserved, any mixture resolves neuter (118/120).

def DalrympleKaplan2000.slovResolve (p q : GenderSet) : GenderSet

Slovene (122)/(126)–(127): masc {F, N}, fem {F}, neut {N}, and the conjunction itself contributes F ∈ (↑ GENDER) — deriving the surprising NEUT & NEUT = MASC (123)–(124).

Equations

• DalrympleKaplan2000.slovResolve p q = p ∪ q ∪ {DalrympleKaplan2000.GMark.F}

theorem DalrympleKaplan2000.slovene_neut_neut_is_masc : slovResolve {GMark.N} {GMark.N} = {GMark.F, GMark.N} ∧ slovResolve {GMark.F} {GMark.F} = {GMark.F}

Bridge: marker sets project onto the binary person decomposition

Features/Person.lean's two-boolean decomposition (hasAuthor, hasParticipant) is the image of the marker-set representation: S ∈ p is authorship, membership of either marker is participanthood. The map collapses exactly the inclusive/exclusive distinction — Fula's {S} and {S, H} land on the same binary value — which is the formal content of §6.2's "fewer pronominal distinctions".

def DalrympleKaplan2000.toBinary (p : PersonSet) : Person.Features

Project a marker set onto the binary decomposition.

Equations

• DalrympleKaplan2000.toBinary p = { hasParticipant := decide (DalrympleKaplan2000.Marker.S ∈ p ∨ DalrympleKaplan2000.Marker.H ∈ p), hasAuthor := decide (DalrympleKaplan2000.Marker.S ∈ p) }

theorem DalrympleKaplan2000.toBinary_values : toBinary fula1exc = Person.firstF ∧ toBinary fula1inc = Person.firstF ∧ toBinary fula2 = Person.secondF ∧ toBinary fula3 = Person.thirdF

theorem DalrympleKaplan2000.binary_collapses_clusivity : toBinary fula1exc = toBinary fula1inc ∧ fula1exc ≠ fula1inc

The inclusive/exclusive collapse, explicitly: the binary decomposition cannot separate Fula's two first persons.

BundleLike with Finset slots: the generic substrate accommodates indeterminacy

A multi-feature indeterminacy bundle is just a Pi type with Finset slots, ordered superset-first (more determinate = smaller set). BundleLike's slot type family S : F → Type* (parameter S carrying its own order) covers this case without any new generic machinery: S t := (Finset (V t))ᵒᵈ. The BundleLike.Subsumes order then reads, per slot, b₁ t ≤ b₂ t in the order dual — i.e. (b₂ t).1 ⊆ (b₁ t).1 — which is exactly the §4 (eq. 25) information-as-set-of-possibilities convention.

This is the structural payoff: a feature-space tweak (Finset slots instead of Flat slots), not a re-development of the lattice theory.

@[reducible, inline]

abbrev DalrympleKaplan2000.IndetBundle (F : Type u_1) (V : F → Type u_2) : Type (max u_1 u_2)

An indeterminacy bundle: each slot holds a Finset of possible atomic values, ordered superset-first via Finset's order dual.

Equations

• DalrympleKaplan2000.IndetBundle F V = ((t : F) → (Finset (V t))ᵒᵈ)

@[implicit_reducible]

instance DalrympleKaplan2000.IndetBundle.instBundleLikeOrderDualFinset {F : Type u_1} {V : F → Type u_2} : BundleLike (IndetBundle F V) F fun (t : F) => (Finset (V t))ᵒᵈ

Equations

• DalrympleKaplan2000.IndetBundle.instBundleLikeOrderDualFinset = { val := fun (b : DalrympleKaplan2000.IndetBundle F V) => b }

instance DalrympleKaplan2000.IndetBundle.instLawfulBundleLikeOrderDualFinset {F : Type u_1} {V : F → Type u_2} : LawfulBundleLike (IndetBundle F V)

Concrete witness: a 1-feature Case-indeterminacy bundle. We exhibit two bundles — was {NOM, ACC} and wer {NOM} — and confirm that wer subsumes (is more determinate than) was, via the generic BundleLike.Subsumes.

@[reducible, inline]

abbrev DalrympleKaplan2000.CaseBundle : Type

A single-feature Case bundle.

Equations

• DalrympleKaplan2000.CaseBundle = DalrympleKaplan2000.IndetBundle Unit fun (x : Unit) => Case

def DalrympleKaplan2000.wasBundle : CaseBundle

Equations

• DalrympleKaplan2000.wasBundle x✝ = OrderDual.toDual DalrympleKaplan2000.was

def DalrympleKaplan2000.werBundle : CaseBundle

Equations

• DalrympleKaplan2000.werBundle x✝ = OrderDual.toDual DalrympleKaplan2000.wer

theorem DalrympleKaplan2000.wer_subsumes_was : BundleLike.Subsumes wasBundle werBundle

wer {NOM} is more determinate than was {NOM, ACC}: their subsumption in the generic BundleLike order matches set-superset on the slot.