Degano & Aloni 2025: 7-type team-semantic typology of indefinites

@cite{degano-aloni-2025} @cite{hodges-1997} @cite{vaananen-2007}

Degano & Aloni 2025's 7-type classification of indefinite pronouns, projected from the consensus Typology.Indefinite.IndefiniteEntry substrate (Haspelmath 1997 function-coverage data).

The team-semantic logic primitives D&A use (Hodges 1997 / Väänänen 2007: assignment teams, variation, constancy) are inlined here as a private namespace prelude — they currently have only one downstream linguistic consumer (this file + Bubnov 2026), so general placement in Core/Logic/ would be premature. When a second framework (branching quantifiers, IF-logic for definites, partial-information ellipsis) needs them, extract.

D&A's classification ↔ Haspelmath's map

D&A's typology operates on the SK/SU/NS triangle:

• SK = specific known: speaker has a particular referent in mind, hearer can identify
• SU = specific unknown: speaker has a referent in mind, hearer cannot
• NS = non-specific: no particular referent

These map 1:1 to Haspelmath 1997's first three slots:

• D&A SK ↔ Haspelmath specificKnown
• D&A SU ↔ Haspelmath specificUnknown
• D&A NS ↔ Haspelmath irrealis (D&A focus on irrealis-modal non-specific uses; Haspelmath's irrealis slot is broader but D&A treat it as the canonical NS-bearing region — see D&A 2025 §2)

The DAType.profile function below uses the Haspelmath identifiers because that's the substrate the projection consumes; the D&A column heading in the type table is for reference.

Schema

• DAType: the 7 types arising from Boolean combinations of var(y,x) and dep(y,x) with within-world (v) and across-all-worlds (∅) parameter choices.
• DAType.profile: each type's theoretical coverage on the Haspelmath SK/SU/irrealis triangle.
• IndefiniteEntry.surfaceDAType: classify an entry by exact match of its actual function-coverage to a D&A type's profile. Returns none when the entry covers a region D&A doesn't subdivide (e.g., free choice, polarity-sensitive forms) or when actual ⊊ profile.
• IndefiniteEntry.consistentWith: weaker relation — actual coverage is a subset of the theoretical profile. Used for entries where paradigmatic competition narrows the actual distribution (e.g., Russian kto-to ⊊ type-iv epistemic profile).

Type table (D&A's row labels; Haspelmath identifiers in profile)

Type	Requirement	D&A profile (SK/SU/NS)	Example
(i)	(none)	{SK, SU, NS}	English some-
(ii)	dep(v,x)	{SK, SU}	Yakut kim ere
(iii)	var(v,x)	{NS}	Russian -nibud'
(iv)	var(∅,x)	{SU, NS}	German irgend-
(v)	dep(∅,x)	{SK}	Russian koe-
(vi)	dep(∅,x)∧var(v,x)	{SK, NS}	unattested
(vii)	dep(v,x)∧var(∅,x)	{SU}	Kannada yāru-oo

@[reducible, inline]

abbrev Phenomena.Indefinites.Studies.DeganoAloni2025.DependenceLogic.AssignmentTeam (V E : Type) : Type

An assignment team: a list of variable-to-entity assignments. The setting for dependence logic (@cite{vaananen-2007}) and D&A's indefinite semantics.

Equations

• Phenomena.Indefinites.Studies.DeganoAloni2025.DependenceLogic.AssignmentTeam V E = List (V → E)

def Phenomena.Indefinites.Studies.DeganoAloni2025.DependenceLogic.variation {V E : Type} [DecidableEq V] [DecidableEq E] (t : AssignmentTeam V E) (y x : V) : Bool

Variation: variable x varies w.r.t. parameter y in team t. var(y, x) holds iff there exist two assignments in t that agree on y but disagree on x.

Equations

• Phenomena.Indefinites.Studies.DeganoAloni2025.DependenceLogic.variation t y x = List.any t fun (a₁ : V → E) => List.any t fun (a₂ : V → E) => a₁ y == a₂ y && a₁ x != a₂ x

def Phenomena.Indefinites.Studies.DeganoAloni2025.DependenceLogic.constancy {V E : Type} [DecidableEq V] [DecidableEq E] (t : AssignmentTeam V E) (y x : V) : Bool

Constancy (functional dependence): x depends on y in team t. dep(y, x) holds iff all assignments agreeing on y also agree on x.

Equations

• Phenomena.Indefinites.Studies.DeganoAloni2025.DependenceLogic.constancy t y x = List.all t fun (a₁ : V → E) => List.all t fun (a₂ : V → E) => a₁ y != a₂ y || a₁ x == a₂ x

theorem Phenomena.Indefinites.Studies.DeganoAloni2025.DependenceLogic.constancy_excludes_variation_witness : have t := [fun (v : Fin 2) => if v = 0 then 0 else 0, fun (v : Fin 2) => if v = 0 then 0 else 1]; variation t 0 1 = true ∧ constancy t 0 1 = false

Concrete witness: a 2-assignment team where var(y,x) holds and dep(y,x) fails.

theorem Phenomena.Indefinites.Studies.DeganoAloni2025.DependenceLogic.constancy_excludes_variation {V E : Type} [DecidableEq V] [DecidableEq E] (t : AssignmentTeam V E) (y x : V) (hdep : constancy t y x = true) (hvar : variation t y x = true) : False

Constancy and variation are jointly unsatisfiable.

theorem Phenomena.Indefinites.Studies.DeganoAloni2025.DependenceLogic.variation_monotone {V E : Type} [DecidableEq V] [DecidableEq E] (t : AssignmentTeam V E) (v y x : V) (hvar : variation t v x = true) (h_agree : ∀ (a₁ a₂ : V → E), a₁ v = a₂ v → a₁ y = a₂ y) : variation t y x = true

Variation lifts to a coarser parameter: if v-agreement implies y-agreement, then var(v, x) → var(y, x). Grounds D&A's diachronic prediction var(v, x) → var(∅, x) (see @cite{bubnov-2026} §6).

inductive Phenomena.Indefinites.Studies.DeganoAloni2025.DAType : Type

@cite{degano-aloni-2025}'s seven-type team-semantic typology.

• unmarked : DAType

  (i) No restriction. Profile: SK ∪ SU ∪ NS.

• specific : DAType

  (ii) dep(v,x): constancy within each epistemic world. Profile: SK + SU.

• nonSpecific : DAType

  (iii) var(v,x): variation within some epistemic world. Profile: NS only.

• epistemic : DAType

  (iv) var(∅,x): variation across all epistemic worlds. Profile: SU + NS.

• specificKnown : DAType

  (v) dep(∅,x): constancy across all epistemic worlds. Profile: SK only.

• skPlusNS : DAType

  (vi) dep(∅,x) ∧ var(v,x): jointly forbidden by team-semantic logic AND empirically unattested in D&A's surveyed languages. The two failure modes are independent: even if some non-team-semantic account licensed it, the {SK, NS} profile would still need a witness.

• specificUnknown : DAType

  (vii) dep(v,x) ∧ var(∅,x): rare conjunctive type; profile SU only.

@[implicit_reducible]

instance Phenomena.Indefinites.Studies.DeganoAloni2025.instDecidableEqDAType : DecidableEq DAType

Equations

• Phenomena.Indefinites.Studies.DeganoAloni2025.instDecidableEqDAType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Indefinites.Studies.DeganoAloni2025.instReprDAType.repr : DAType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Indefinites.Studies.DeganoAloni2025.instReprDAType : Repr DAType

Equations

• Phenomena.Indefinites.Studies.DeganoAloni2025.instReprDAType = { reprPrec := Phenomena.Indefinites.Studies.DeganoAloni2025.instReprDAType.repr }

@[implicit_reducible]

instance Phenomena.Indefinites.Studies.DeganoAloni2025.instBEqDAType : BEq DAType

Equations

• Phenomena.Indefinites.Studies.DeganoAloni2025.instBEqDAType = { beq := Phenomena.Indefinites.Studies.DeganoAloni2025.instBEqDAType.beq }

def Phenomena.Indefinites.Studies.DeganoAloni2025.instBEqDAType.beq : DAType → DAType → Bool

Equations

• Phenomena.Indefinites.Studies.DeganoAloni2025.instBEqDAType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Indefinites.Studies.DeganoAloni2025.DAType.profile : DAType → Finset Typology.Indefinite.HaspelmathFunction

D&A theoretical profile: the SK/SU/NS subset of Haspelmath functions a type's semantics PERMITS. Actual paradigm distribution may be narrower due to competition with more-specific forms.

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Indefinites.Studies.DeganoAloni2025.DAType.specific.profile = {Typology.Indefinite.HaspelmathFunction.specificKnown, Typology.Indefinite.HaspelmathFunction.specificUnknown}
• Phenomena.Indefinites.Studies.DeganoAloni2025.DAType.nonSpecific.profile = {Typology.Indefinite.HaspelmathFunction.irrealis}
• Phenomena.Indefinites.Studies.DeganoAloni2025.DAType.epistemic.profile = {Typology.Indefinite.HaspelmathFunction.specificUnknown, Typology.Indefinite.HaspelmathFunction.irrealis}
• Phenomena.Indefinites.Studies.DeganoAloni2025.DAType.specificKnown.profile = {Typology.Indefinite.HaspelmathFunction.specificKnown}
• Phenomena.Indefinites.Studies.DeganoAloni2025.DAType.skPlusNS.profile = {Typology.Indefinite.HaspelmathFunction.specificKnown, Typology.Indefinite.HaspelmathFunction.irrealis}
• Phenomena.Indefinites.Studies.DeganoAloni2025.DAType.specificUnknown.profile = {Typology.Indefinite.HaspelmathFunction.specificUnknown}

def Phenomena.Indefinites.Studies.DeganoAloni2025.DAType.IsAttested (t : DAType) : Prop

Type (vi) skPlusNS is jointly forbidden by team-semantic logic AND empirically unattested. The team-semantic argument: dep(∅,x) forbids cross-world variation while var(v,x) requires intra-world variation. The empirical argument is independent: D&A find no surveyed language with a form whose distribution exactly matches the {SK, NS} profile. Both arguments must hold; the predicate marks attestation, not logical consistency.

Equations

• t.IsAttested = (t ≠ Phenomena.Indefinites.Studies.DeganoAloni2025.DAType.skPlusNS)

@[implicit_reducible]

instance Phenomena.Indefinites.Studies.DeganoAloni2025.instDecidablePredDATypeIsAttested : DecidablePred DAType.IsAttested

Equations

• Phenomena.Indefinites.Studies.DeganoAloni2025.instDecidablePredDATypeIsAttested x✝ = Phenomena.Indefinites.Studies.DeganoAloni2025.instDecidablePredDATypeIsAttested._aux_1 x✝

theorem Phenomena.Indefinites.Studies.DeganoAloni2025.skPlusNS_unattested : ¬DAType.skPlusNS.IsAttested

def Phenomena.Indefinites.Studies.DeganoAloni2025.specificityRegion : Finset Typology.Indefinite.HaspelmathFunction

The Haspelmath functions that D&A's profile projection ranges over: the specificity triangle (specificKnown, specificUnknown, irrealis). D&A's typology is built around the SK/SU/NS dimension; D&A's irrealis slot identifies with Haspelmath's irrealis (see the module docstring's "D&A ↔ Haspelmath" section).

Equations

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

theorem Phenomena.Indefinites.Studies.DeganoAloni2025.DAType.profile_subset_specificityRegion (t : DAType) : t.profile ⊆ specificityRegion

Projection range, not framework scope. Every D&A type's profile is a subset of specificityRegion. This is a structural fact about the projection function DAType.profile, not a claim about the empirical reach of D&A 2025's framework: D&A's account empirically covers polarity-sensitive uses of indefinites (e.g., German irgendein under modals) through composition mechanisms that are not captured by the direct profile projection. The theorem says only that the range of profile lies in the specificity region; what each type predicts in composition is a separate question.

See the audit notes in 0.230.529's CHANGELOG entry on why the symmetric Chierchia-side scope theorem fails: Chierchia's PSIProfile.predictedFunctions for plain indefinites (obligatoryDomainAlts := false) ranges over {SK, SU, irrealis} too, so the would-be "disjoint scope" picture collapses. The structural pattern only survives on the D&A side.

def Typology.Indefinite.IndefiniteEntry.surfaceDAType (e : IndefiniteEntry) : Option Phenomena.Indefinites.Studies.DeganoAloni2025.DAType

Surface-classifier: project an entry to the D&A type whose theoretical profile exactly matches the entry's actual function-coverage.

Returns none when the entry covers a region D&A doesn't subdivide (free choice, polarity-sensitive uses, or any function outside SK/SU/NS) or when actual coverage is a proper subset of any type's profile (a paradigmatic-competition case — see consistentWith).

Equations

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

def Typology.Indefinite.IndefiniteEntry.consistentWith (e : IndefiniteEntry) (t : Phenomena.Indefinites.Studies.DeganoAloni2025.DAType) : Bool

Consistency relation: an entry's actual coverage is contained in t's theoretical profile. Allows actual ⊊ profile, capturing paradigmatic-competition cases such as Russian kto-to (type-iv epistemic profile permits SU + NS, but -to covers only SU because -nibud' blocks it from NS — see @cite{bubnov-2026} §7).

Equations

• e.consistentWith t = decide (e.functions ⊆ t.profile)