Adamson & Anagnostopoulou 2025 [AA25]

Gender Features and Coordination Resolution in Greek and Other Three-Gendered Languages: Implications for the Crosslinguistic Representation of Gender. Linguistic Inquiry (Early Access).

Core result

Cross-linguistic variation in coordination resolution (Table 2) is derived from three interacting components, without stipulated defaults:

1. Feature geometry: language-specific hierarchies of privative gender features. In Greek, FEM is a dependent of MASC (= animate), so a feminine nominal also bears MASC. In Icelandic, MASC (= male) and FEM are independent under CLASS — neither entails the other.

2. Dual-feature system: interpretable features (iFs → LF) vs uninterpretable features (uFs → PF), linked by a redundancy rule that copies iFs to empty uF slots at Transfer.

3. Percolation + conversion: universal coordination resolution. iFs percolate from conjuncts to &P; shared iFs survive intersection (conversion); the Subset Principle selects the inflectional exponent.

Table 2 — resolution patterns derived from geometry:

Language	Humans	Inanimates
Greek	MASC	NEUT
Icelandic	NEUT	NEUT
BCS	MASC	MASC

Y-model architecture

The derivation follows the Minimalist Y-model:

• Narrow syntax: nominals bear both iFs and uFs; percolation collects features at &P.
• Transfer: conversion intersects iFs; redundancy rule copies resolved iFs to empty uF slots.
• PF: Vocabulary Insertion (Subset Principle) maps uF sets to inflectional exponents.
• LF: Lexical Complementarity restricts feature interpretation (e.g., iMASC restricted to ⟦MASC⟧ − ⟦FEM⟧).

Formalization

Resolution uses resolve — the single compositional endpoint — instantiated with GenderNode as the feature type. Each prediction is a verified theorem.

[AA25]'s gender-resolution mechanism: i(nterpretable) features percolate from each conjunct to the coordination; the shared i-features (the intersection) form its gender, an empty intersection being a language-specific default. Parameterized over the feature type, so it applies across language families. (Formerly Syntax/Minimalist/Agreement/GenderResolution.lean — relocated here as paper-specific apparatus; MCB's core models Merge, not φ-agreement.)

structure AdamsonAnagnostopoulou2025.AnnotatedFeature (F : Type) : Type

A gender feature annotated with interpretability ([Kra15]: gender on a categorizing head n is interpretable (natural) or uninterpretable (arbitrary); only i-features enter the resolution calculus).

• value : F
• interp : Minimalist.Interpretability

def AdamsonAnagnostopoulou2025.instDecidableEqAnnotatedFeature.decEq {F✝ : Type} [DecidableEq F✝] (x✝ x✝¹ : AnnotatedFeature F✝) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance AdamsonAnagnostopoulou2025.instDecidableEqAnnotatedFeature {F✝ : Type} [DecidableEq F✝] : DecidableEq (AnnotatedFeature F✝)

Equations

• AdamsonAnagnostopoulou2025.instDecidableEqAnnotatedFeature = AdamsonAnagnostopoulou2025.instDecidableEqAnnotatedFeature.decEq

@[implicit_reducible]

instance AdamsonAnagnostopoulou2025.instReprAnnotatedFeature {F✝ : Type} [Repr F✝] : Repr (AnnotatedFeature F✝)

Equations

• AdamsonAnagnostopoulou2025.instReprAnnotatedFeature = { reprPrec := AdamsonAnagnostopoulou2025.instReprAnnotatedFeature.repr }

def AdamsonAnagnostopoulou2025.instReprAnnotatedFeature.repr {F✝ : Type} [Repr F✝] : AnnotatedFeature F✝ → ℕ → Std.Format

Equations

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

@[reducible, inline]

abbrev AdamsonAnagnostopoulou2025.AnnotatedFeatures (F : Type) : Type

A conjunct's annotated feature list, ordered outermost (highest nP) to innermost.

Equations

• AdamsonAnagnostopoulou2025.AnnotatedFeatures F = List (AdamsonAnagnostopoulou2025.AnnotatedFeature F)

def AdamsonAnagnostopoulou2025.percolateI {F : Type} (fs : AnnotatedFeatures F) : List F

Percolation: extract the interpretable feature values; u-features are excluded.

Equations

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

def AdamsonAnagnostopoulou2025.intersectFeatures {F : Type} [BEq F] (xs ys : List F) : List F

Intersection of two percolated feature lists (order from the first).

Equations

• AdamsonAnagnostopoulou2025.intersectFeatures xs ys = List.filter (fun (x : F) => ys.contains x) xs

def AdamsonAnagnostopoulou2025.resolve {F : Type} [BEq F] (fs1 fs2 : AnnotatedFeatures F) : Option (List F)

Resolve gender for two conjoined DPs: percolate, intersect, some if the intersection is non-empty (matching agreement) else none (language-specific default). The compositional endpoint; language-specific resolutions project from it.

Equations

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

inductive AdamsonAnagnostopoulou2025.SelectionGrammar : Type

When multiple i-features survive (stacked nPs), the language selects which one determines the agreement class ([Car26] §5.1).

• highestWins : SelectionGrammar

  The outermost (highest) nP layer wins — the first surviving feature.

• bestSemanticMatch : SelectionGrammar

  The most specific semantic match wins.

@[implicit_reducible]

instance AdamsonAnagnostopoulou2025.instDecidableEqSelectionGrammar : DecidableEq SelectionGrammar

Equations

• AdamsonAnagnostopoulou2025.instDecidableEqSelectionGrammar x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance AdamsonAnagnostopoulou2025.instReprSelectionGrammar : Repr SelectionGrammar

Equations

• AdamsonAnagnostopoulou2025.instReprSelectionGrammar = { reprPrec := AdamsonAnagnostopoulou2025.instReprSelectionGrammar.repr }

def AdamsonAnagnostopoulou2025.instReprSelectionGrammar.repr : SelectionGrammar → ℕ → Std.Format

Equations

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

def AdamsonAnagnostopoulou2025.selectFeature {F : Type} (grammar : SelectionGrammar) (specificity : F → ℕ) (features : List F) : Option F

Select the determining feature from a non-empty intersection; specificity ranks features (higher = more specific).

Equations

• One or more equations did not get rendered due to their size.
• AdamsonAnagnostopoulou2025.selectFeature AdamsonAnagnostopoulou2025.SelectionGrammar.highestWins specificity features = features.head?

def AdamsonAnagnostopoulou2025.resolveN {F : Type} [BEq F] (bundles : List (AnnotatedFeatures F)) : Option (List F)

N-ary resolution: iterated intersection over all conjuncts' percolated features.

Equations

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

theorem AdamsonAnagnostopoulou2025.resolveN_binary {F : Type} [BEq F] (fs1 fs2 : AnnotatedFeatures F) : resolveN [fs1, fs2] = resolve fs1 fs2

N-ary resolution subsumes binary.

def AdamsonAnagnostopoulou2025.satisfiesMRH {F : Type} [BEq F] (bundles : List (AnnotatedFeatures F)) : Bool

A set of bundles satisfies MRH (Mismatch Resolution Hypothesis) if resolution succeeds for every pair — no empty intersection, no default insertion needed ([AA25]: Greek satisfies MRH; Bantu does not).

Equations

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

structure AdamsonAnagnostopoulou2025.FeatureOrder (F : Type) [BEq F] : Type

A feature geometry: the nodes and, per node, its full i-feature bundle (itself plus everything it entails). Cross-linguistic variation in resolution follows from differences in geometry ([AA25]).

• nodes : List F
• bundle : F → AnnotatedFeatures F

def AdamsonAnagnostopoulou2025.FeatureOrder.entails {F : Type} [BEq F] (order : FeatureOrder F) (f₁ f₂ : F) : Bool

f₁ entails f₂ iff every i-feature in f₂'s bundle is in f₁'s.

Equations

• order.entails f₁ f₂ = (AdamsonAnagnostopoulou2025.percolateI (order.bundle f₂)).all fun (x : F) => (AdamsonAnagnostopoulou2025.percolateI (order.bundle f₁)).contains x

def AdamsonAnagnostopoulou2025.FeatureOrder.satisfiesMRH' {F : Type} [BEq F] (order : FeatureOrder F) : Bool

A feature order satisfies MRH if all its bundles produce non-empty intersections.

Equations

• order.satisfiesMRH' = AdamsonAnagnostopoulou2025.satisfiesMRH (List.map order.bundle order.nodes)

inductive AdamsonAnagnostopoulou2025.GenderNode : Type

Privative feature nodes in the gender geometry (§2.2).

[AA25] modifies [HR02]: features are organized in language-specific hierarchies where more specific features entail broader features. The same labels appear across languages, but their geometric arrangement — and hence their semantic content — varies.

Language-specific geometries:

• Greek (17): CLASS > MASC > FEM (linear chain)
• Icelandic (63): CLASS > {MASC, FEM} (independent siblings)
• BCS (74): CLASS > INDIV > {GRP, MASC > ANIM > FEM}

• cls : GenderNode
• masc : GenderNode
• fem : GenderNode
• indiv : GenderNode
• grp : GenderNode
• anim : GenderNode

@[implicit_reducible]

instance AdamsonAnagnostopoulou2025.instDecidableEqGenderNode : DecidableEq GenderNode

Equations

• AdamsonAnagnostopoulou2025.instDecidableEqGenderNode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def AdamsonAnagnostopoulou2025.instReprGenderNode.repr : GenderNode → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance AdamsonAnagnostopoulou2025.instReprGenderNode : Repr GenderNode

Equations

• AdamsonAnagnostopoulou2025.instReprGenderNode = { reprPrec := AdamsonAnagnostopoulou2025.instReprGenderNode.repr }

def AdamsonAnagnostopoulou2025.GenderNode.toGenderDimension : GenderNode → Option Morphology.DM.GenderDimension

Partial bridge from privative geometry nodes to DM gender dimensions. .cls, .indiv, and .grp are structural organizing nodes with no counterpart in the DM GenderDimension type (which tracks only semantic gender dimensions).

Equations

• AdamsonAnagnostopoulou2025.GenderNode.masc.toGenderDimension = some Morphology.DM.GenderDimension.masc
• AdamsonAnagnostopoulou2025.GenderNode.fem.toGenderDimension = some Morphology.DM.GenderDimension.fem
• AdamsonAnagnostopoulou2025.GenderNode.anim.toGenderDimension = some Morphology.DM.GenderDimension.anim
• x✝.toGenderDimension = none

inductive AdamsonAnagnostopoulou2025.Infl : Type

Inflection class for three-gendered languages.

• fem : Infl
• masc : Infl
• neut : Infl

@[implicit_reducible]

instance AdamsonAnagnostopoulou2025.instDecidableEqInfl : DecidableEq Infl

Equations

• AdamsonAnagnostopoulou2025.instDecidableEqInfl x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def AdamsonAnagnostopoulou2025.instReprInfl.repr : Infl → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance AdamsonAnagnostopoulou2025.instReprInfl : Repr Infl

Equations

• AdamsonAnagnostopoulou2025.instReprInfl = { reprPrec := AdamsonAnagnostopoulou2025.instReprInfl.repr }

def AdamsonAnagnostopoulou2025.Infl.toGender : Infl → Gender

Bridge from VI inflection class to cross-linguistic surface gender.

Equations

• AdamsonAnagnostopoulou2025.Infl.fem.toGender = Gender.feminine
• AdamsonAnagnostopoulou2025.Infl.masc.toGender = Gender.masculine
• AdamsonAnagnostopoulou2025.Infl.neut.toGender = Gender.neuter

def AdamsonAnagnostopoulou2025.greekVI (fs : List GenderNode) : Infl

Greek vocabulary item schema (21).

uF specification	Exponent
{FEM, MASC}	"feminine inflection"
{MASC}	"masculine inflection"
∅	"neuter inflection"

The Subset Principle selects the most specific matching item.

Equations

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

@[reducible, inline]

abbrev AdamsonAnagnostopoulou2025.icelandicVI (fs : List GenderNode) : Infl

Icelandic vocabulary schema — identical to Greek. The geometry difference, not the vocabulary, drives the divergent resolution patterns.

Equations

• AdamsonAnagnostopoulou2025.icelandicVI = AdamsonAnagnostopoulou2025.greekVI

def AdamsonAnagnostopoulou2025.bcsVI (fs : List GenderNode) : Infl

BCS vocabulary item schema (75).

uF specification	Exponent
{FEM, ANIM, MASC, INDIV}	"F inflection"
{ANIM, MASC, INDIV}	"M animate inflection"
{INDIV}	"M inanimate inflection"
∅	"N inflection"

Simplified: FEM ∧ ANIM → F; INDIV present → M; else → N.

Equations

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

Greek feature geometry (17)

CLASS > MASC > FEM (linear chain).
Feature interpretations (18):
- CLASS: λx. x is an entity
- MASC: λx. x is animate
- FEM: λx. x is a woman

Having FEM entails MASC; having MASC entails CLASS.
Lexical Complementarity (19) restricts: iMASC picks out ⟦MASC⟧ − ⟦FEM⟧
(animate non-women); iFEM picks out women; iCLASS picks out entities. 

theorem AdamsonAnagnostopoulou2025.gk_uniform_fem : resolve AdamsonAnagnostopoulou2025.gkHF✝ AdamsonAnagnostopoulou2025.gkHF✝ = some [GenderNode.cls, GenderNode.masc, GenderNode.fem]

(25) Uniform humans resolve to their shared gender.

theorem AdamsonAnagnostopoulou2025.gk_uniform_masc : resolve AdamsonAnagnostopoulou2025.gkHM✝ AdamsonAnagnostopoulou2025.gkHM✝ = some [GenderNode.cls, GenderNode.masc]

theorem AdamsonAnagnostopoulou2025.gk_human_mismatch : resolve AdamsonAnagnostopoulou2025.gkHF✝ AdamsonAnagnostopoulou2025.gkHM✝ = some [GenderNode.cls, GenderNode.masc]

(22a) Mismatched humans → {CLASS, MASC} → masculine plural. Intersection: {CLASS,MASC,FEM} ∩ {CLASS,MASC} = {CLASS,MASC}. FEM is eliminated because only one conjunct bears it.

theorem AdamsonAnagnostopoulou2025.gk_human_mismatch_vi : greekVI [GenderNode.cls, GenderNode.masc] = Infl.masc

theorem AdamsonAnagnostopoulou2025.gk_inanim_MF : resolve AdamsonAnagnostopoulou2025.gkIM✝ AdamsonAnagnostopoulou2025.gkIF✝ = some [GenderNode.cls]

(22b, 40a-c) All inanimate mismatch combinations → {CLASS} → neuter. Percolation extracts only iCLASS from each conjunct (uFs excluded). This is NOT default insertion — it is the result of intersecting the iF sets, which contain only iCLASS for all inanimates.

theorem AdamsonAnagnostopoulou2025.gk_inanim_NF : resolve AdamsonAnagnostopoulou2025.gkIN✝ AdamsonAnagnostopoulou2025.gkIF✝ = some [GenderNode.cls]

theorem AdamsonAnagnostopoulou2025.gk_inanim_NM : resolve AdamsonAnagnostopoulou2025.gkIN✝ AdamsonAnagnostopoulou2025.gkIM✝ = some [GenderNode.cls]

theorem AdamsonAnagnostopoulou2025.gk_inanim_mismatch_vi : greekVI [GenderNode.cls] = Infl.neut

theorem AdamsonAnagnostopoulou2025.gk_no_default_human : (resolve AdamsonAnagnostopoulou2025.gkHF✝ AdamsonAnagnostopoulou2025.gkHM✝).isSome = true

Mismatch Resolution Hypothesis (24): no default feature insertion. All resolution outcomes have non-empty intersection (matching).

theorem AdamsonAnagnostopoulou2025.gk_no_default_inanim : (resolve AdamsonAnagnostopoulou2025.gkIM✝ AdamsonAnagnostopoulou2025.gkIF✝).isSome = true

Fixed-gender human nominals (§3.2)

*megalofiia* 'genius' is **grammatically** feminine (uFs) but its
**conceptual** gender (iFs) tracks the referent. Resolution operates
on iFs — crucial evidence for the Mismatch Resolution Hypothesis.

*thima* 'victim' is grammatically neuter (uF = {CLASS}) but
conceptually masculine/feminine depending on referent. 

theorem AdamsonAnagnostopoulou2025.gk_fixed_genius_sister : resolve AdamsonAnagnostopoulou2025.gkFixedFemMale✝ AdamsonAnagnostopoulou2025.gkHF✝ = some [GenderNode.cls, GenderNode.masc]

(36) megalofiia (male referent) + sister → masculine (M♂ + F♀ = M). Despite both being grammatically feminine, iF resolution yields {CLASS,MASC} ∩ {CLASS,MASC,FEM} = {CLASS,MASC} → MASC.

theorem AdamsonAnagnostopoulou2025.gk_fixed_genius_sister_vi : Option.map greekVI (resolve AdamsonAnagnostopoulou2025.gkFixedFemMale✝ AdamsonAnagnostopoulou2025.gkHF✝) = some Infl.masc

theorem AdamsonAnagnostopoulou2025.gk_fixed_victim_mother : resolve AdamsonAnagnostopoulou2025.gkFixedNeutFemale✝ AdamsonAnagnostopoulou2025.gkHF✝ = some [GenderNode.cls, GenderNode.masc, GenderNode.fem]

(37) thima (female referent) + her mother → feminine (N♀ + F♀ = F). Neuter noun's iFs are feminine (referent is female): {CLASS,MASC,FEM} ∩ {CLASS,MASC,FEM} = {CLASS,MASC,FEM} → FEM.

theorem AdamsonAnagnostopoulou2025.gk_fixed_victim_mother_vi : Option.map greekVI (resolve AdamsonAnagnostopoulou2025.gkFixedNeutFemale✝ AdamsonAnagnostopoulou2025.gkHF✝) = some Infl.fem

Humans + Inanimates (§3.5)

When a human (percolating iFs) and an inanimate (percolating uFs)
are coordinated, PF realization succeeds only if the features map
to the same inflection class. Otherwise: PF crash → ineffability.

Y-model significance: the crash happens at **PF**, not in narrow
syntax. [H + I] coordination is syntactically well-formed; the
problem is exponence of the resolved features. 

def AdamsonAnagnostopoulou2025.gkHIConverges (humanIFs inanimUFs : List GenderNode) : Bool

PF convergence test for [H + I] coordination. The human's iFs (→ uFs via redundancy rule at Transfer) must map to the same inflection as the inanimate's uFs.

Equations

• AdamsonAnagnostopoulou2025.gkHIConverges humanIFs inanimUFs = (AdamsonAnagnostopoulou2025.greekVI humanIFs == AdamsonAnagnostopoulou2025.greekVI inanimUFs)

theorem AdamsonAnagnostopoulou2025.gk_hi_matched_masc : gkHIConverges [GenderNode.cls, GenderNode.masc] [GenderNode.cls, GenderNode.masc] = true

(54a) M♂ + M■ → grammatical: both map to MASC. kleftis 'thief' (M) + pinakas 'painting' (M).

theorem AdamsonAnagnostopoulou2025.gk_hi_matched_fem : gkHIConverges [GenderNode.cls, GenderNode.masc, GenderNode.fem] [GenderNode.cls, GenderNode.masc, GenderNode.fem] = true

(54b) F♀ + F■ → grammatical: both map to FEM. gineka 'woman' (F) + ombrela 'umbrella' (F).

theorem AdamsonAnagnostopoulou2025.gk_hi_crash : gkHIConverges [GenderNode.cls, GenderNode.masc] [GenderNode.cls] = false

(47) M♂ + N■ → ineffable: MASC ≠ NEUT → PF crash. kleftis 'thief' (M♂) + daxtilidi 'ring' (N■). Human iFs → MASC; inanimate uFs → NEUT. No single exponent.

theorem AdamsonAnagnostopoulou2025.gk_hi_fixed_converge : gkHIConverges [GenderNode.cls, GenderNode.masc] [GenderNode.cls, GenderNode.masc] = true

(56) Fixed-gender F♂ + M■ → grammatical: iFs match. megalofiia 'genius' (iF = M♂) + pinakas 'painting' (uF = M■). Human's iFs = {CLASS,MASC} → MASC; inanimate's uFs = {CLASS,MASC} → MASC. PF converges despite different grammatical genders.

Fixed-gender humans + inanimates (§3.5)

The paper's strongest evidence for the iF-based analysis. When a
**fixed-gender human** is coordinated with an inanimate, the PF
convergence depends on the human's **iFs** (conceptual gender),
not their **uFs** (grammatical gender). 

theorem AdamsonAnagnostopoulou2025.gk_hi_fixed_victim_male : gkHIConverges [GenderNode.cls, GenderNode.masc] [GenderNode.cls, GenderNode.masc] = true

(57a) thima (N♀ victim, male referent) + pinakas (M■) → MASC. iFs of victim (male) = {CLASS, MASC}; uFs of painting = {CLASS, MASC}. VI match: MASC = MASC → PF converges.

theorem AdamsonAnagnostopoulou2025.gk_hi_fixed_victim_female : gkHIConverges [GenderNode.cls, GenderNode.masc, GenderNode.fem] [GenderNode.cls, GenderNode.masc, GenderNode.fem] = true

(57b) thima (N♀ victim, female referent) + fotografia (F■) → FEM. iFs of victim (female) = {CLASS, MASC, FEM}; uFs of picture = {CLASS, MASC, FEM}. VI match: FEM = FEM → PF converges.

theorem AdamsonAnagnostopoulou2025.gk_hi_fixed_victim_male_fem_crash : gkHIConverges [GenderNode.cls, GenderNode.masc] [GenderNode.cls, GenderNode.masc, GenderNode.fem] = false

(57a corollary) thima (N♀, male ref) + fotografia (F■) → PF crash. iFs of victim (male) = {CLASS, MASC} → VI → MASC. uFs of picture = {CLASS, MASC, FEM} → VI → FEM. MASC ≠ FEM → crash.

Uniform inanimate coordination (38a-c)

When two inanimates share the same grammatical gender, resolved
agreement matches that gender. Under the paper's analysis, this
obtains when inanimates percolate **uFs** (the alternative
derivation in (39)): the &P has a singleton uF set, and PF
realization succeeds with the shared exponent. 

theorem AdamsonAnagnostopoulou2025.gk_uniform_inanim_fem : greekVI [GenderNode.cls, GenderNode.masc, GenderNode.fem] = Infl.fem

(38a) F■ + F■ = F: fusta 'skirt' + bluza 'T-shirt'.

theorem AdamsonAnagnostopoulou2025.gk_uniform_inanim_masc : greekVI [GenderNode.cls, GenderNode.masc] = Infl.masc

(38b) M■ + M■ = M: anaptiras 'lighter' + fakos 'torch'.

theorem AdamsonAnagnostopoulou2025.gk_uniform_inanim_neut : greekVI [GenderNode.cls] = Infl.neut

(38c) N■ + N■ = N: piruni 'fork' + kutali 'spoon'.

theorem AdamsonAnagnostopoulou2025.gk_clausal_default : greekVI [] = Infl.neut

(2a, 58) Clausal subjects lack gender features entirely. No features to percolate → no vocabulary item matches → neuter (the elsewhere exponent, least specified).

Icelandic feature geometry (63)

```
(i/u)CLASS
   / \
MASC   FEM    ← independent (no entailment)
```

Unlike Greek, FEM is NOT a dependent of MASC. The crucial difference:
MASC means 'male' (not 'animate'), so gender-mixed groups are excluded
from both MASC (not all male) and FEM (not all female).
Lexical Complementarity: no restriction between MASC and FEM
(neither is a subset of the other). 

theorem AdamsonAnagnostopoulou2025.is_human_mismatch : resolve AdamsonAnagnostopoulou2025.isHM✝ AdamsonAnagnostopoulou2025.isHF✝ = some [GenderNode.cls]

(60) Mismatched humans → {CLASS} → neuter. {CLASS,MASC} ∩ {CLASS,FEM} = {CLASS}. Because MASC and FEM are independent siblings, only CLASS survives intersection.

theorem AdamsonAnagnostopoulou2025.is_human_mismatch_vi : icelandicVI [GenderNode.cls] = Infl.neut

theorem AdamsonAnagnostopoulou2025.is_inanim_mismatch : resolve AdamsonAnagnostopoulou2025.isIF✝ AdamsonAnagnostopoulou2025.isIM✝ = some [GenderNode.cls]

(59) Mismatched inanimates → {CLASS} → neuter. frægð 'fame' (F) + frami 'success' (M) → neuter plural. All Icelandic inanimates share iFs = {iCLASS} regardless of grammatical gender — uFs (uFEM, uMASC) are excluded from resolution.

theorem AdamsonAnagnostopoulou2025.geometry_drives_variation : resolve AdamsonAnagnostopoulou2025.gkHF✝ AdamsonAnagnostopoulou2025.gkHM✝ ≠ resolve AdamsonAnagnostopoulou2025.isHF✝ AdamsonAnagnostopoulou2025.isHM✝

The geometry contrast: same labels, different geometry, different outcome. Greek {CLASS,MASC,FEM} ∩ {CLASS,MASC} = some {CLASS,MASC}. Icelandic {CLASS,FEM} ∩ {CLASS,MASC} = some {CLASS}. Same mechanism, different input → different result.

BCS feature geometry (74)

```
CLASS
  |
INDIV
 / \
GRP  MASC
      |
    ANIM
      |
    FEM
```

Key differences from Greek and Icelandic:
1. MASC is under INDIV (not directly under CLASS)
2. Neuter ≈ mass (no INDIV) → can't be counted or coordinated as count
3. All coordinatable nominals have INDIV → resolved features include
   at least {INDIV} → vocabulary maps to masculine

Vocabulary consequence: masculine is the "default" for coordination
not by stipulation but because INDIV (required for plural) maps to
masculine via the Subset Principle. 

theorem AdamsonAnagnostopoulou2025.bcs_human_mismatch : resolve AdamsonAnagnostopoulou2025.bcsHF✝ AdamsonAnagnostopoulou2025.bcsHM✝ = some [GenderNode.cls, GenderNode.indiv, GenderNode.masc, GenderNode.anim]

(68) Mismatched humans → {CLASS, INDIV, MASC, ANIM} → masculine. {CLASS,INDIV,MASC,ANIM,FEM} ∩ {CLASS,INDIV,MASC,ANIM} = {CLASS,INDIV,MASC,ANIM}.

theorem AdamsonAnagnostopoulou2025.bcs_human_mismatch_vi : bcsVI [GenderNode.cls, GenderNode.indiv, GenderNode.masc, GenderNode.anim] = Infl.masc

theorem AdamsonAnagnostopoulou2025.bcs_inanim_MF : resolve AdamsonAnagnostopoulou2025.bcsIM✝ AdamsonAnagnostopoulou2025.bcsIF✝ = some [GenderNode.cls, GenderNode.indiv, GenderNode.masc]

Mismatched M + F inanimates → {CLASS, INDIV, MASC} → masculine. Both conjuncts share {CLASS, INDIV, MASC} as iFs; ANIM + FEM on the feminine noun are uFs, excluded from resolution.

theorem AdamsonAnagnostopoulou2025.bcs_inanim_NF_resolved : resolve AdamsonAnagnostopoulou2025.bcsN✝ AdamsonAnagnostopoulou2025.bcsIF✝ = some [GenderNode.cls]

(69) Mismatched N + F inanimates → masculine. znanje 'knowledge' (N) + intuicija 'intuition' (F). Neuter is mass (iFs = {CLASS}); feminine inanimate has iFs = {CLASS, INDIV, MASC}. Intersection = {CLASS}. But coordination introduces GRP (entailing INDIV), so the &P bears {CLASS, INDIV} at minimum → Subset Principle yields masculine.

NB: The formalization models this by checking that the gender resolution itself yields {CLASS}, and the coordinate structure's INDIV (from GRP/plural) independently ensures masculine VI.

theorem AdamsonAnagnostopoulou2025.bcs_inanim_NF_vi : bcsVI [GenderNode.cls, GenderNode.indiv] = Infl.masc

After coordination introduces INDIV, the combined features ({CLASS} from resolution + {INDIV} from GRP) map to masculine.

theorem AdamsonAnagnostopoulou2025.bcs_inanim_mismatch_vi : bcsVI [GenderNode.cls, GenderNode.indiv, GenderNode.masc] = Infl.masc

theorem AdamsonAnagnostopoulou2025.bcs_neut_resolved : resolve AdamsonAnagnostopoulou2025.bcsN✝ AdamsonAnagnostopoulou2025.bcsN✝ = some [GenderNode.cls]

(70) Even matched neuters → masculine when coordinated. selo 'village' (N) + brdo 'hill' (N). Individual neuter DPs are mass (iFs = {CLASS}). Resolution: {CLASS} ∩ {CLASS} = {CLASS}. But coordination introduces GRP (entailing INDIV). The combined {CLASS, INDIV} at &P maps to masculine via VI — INDIV is present → masculine.

theorem AdamsonAnagnostopoulou2025.bcs_neut_coord_masc : bcsVI [GenderNode.cls, GenderNode.indiv] = Infl.masc

theorem AdamsonAnagnostopoulou2025.table2_greek_humans : Option.map greekVI (resolve AdamsonAnagnostopoulou2025.gkHF✝ AdamsonAnagnostopoulou2025.gkHM✝) = some Infl.masc

Table 2 verified: all six cells derived from geometry + intersection.

theorem AdamsonAnagnostopoulou2025.table2_greek_inanimates : Option.map greekVI (resolve AdamsonAnagnostopoulou2025.gkIM✝ AdamsonAnagnostopoulou2025.gkIF✝) = some Infl.neut

theorem AdamsonAnagnostopoulou2025.table2_icelandic_humans : Option.map icelandicVI (resolve AdamsonAnagnostopoulou2025.isHM✝ AdamsonAnagnostopoulou2025.isHF✝) = some Infl.neut

theorem AdamsonAnagnostopoulou2025.table2_icelandic_inanimates : Option.map icelandicVI (resolve AdamsonAnagnostopoulou2025.isIF✝ AdamsonAnagnostopoulou2025.isIM✝) = some Infl.neut

theorem AdamsonAnagnostopoulou2025.table2_bcs_humans : Option.map bcsVI (resolve AdamsonAnagnostopoulou2025.bcsHF✝ AdamsonAnagnostopoulou2025.bcsHM✝) = some Infl.masc

theorem AdamsonAnagnostopoulou2025.table2_bcs_inanimates : Option.map bcsVI (resolve AdamsonAnagnostopoulou2025.bcsIM✝ AdamsonAnagnostopoulou2025.bcsIF✝) = some Infl.masc

def AdamsonAnagnostopoulou2025.redundancyRule (iFs uFs : List GenderNode) : List GenderNode

Redundancy rule (13): copy iF values to empty uF slots at Transfer. If uFs are already filled (arbitrary gender), the rule does not apply.

Y-model: this operation occurs at Transfer, the boundary between narrow syntax and the PF/LF interfaces.

Equations

• AdamsonAnagnostopoulou2025.redundancyRule iFs uFs = if uFs.isEmpty = true then iFs else uFs

theorem AdamsonAnagnostopoulou2025.redundancy_human : redundancyRule [GenderNode.cls, GenderNode.masc, GenderNode.fem] [] = [GenderNode.cls, GenderNode.masc, GenderNode.fem]

Human feminine: uFs empty → redundancy fills from iFs.

theorem AdamsonAnagnostopoulou2025.redundancy_arbitrary : redundancyRule [GenderNode.cls] [GenderNode.cls, GenderNode.masc, GenderNode.fem] = [GenderNode.cls, GenderNode.masc, GenderNode.fem]

Arbitrary feminine: uFs already filled → preserved.

The implicational feature hierarchy (CLASS > MASC > FEM) predicts the absence of ABA syncretism patterns (fn. 19). Neuter and feminine can never be syncretic to the exclusion of masculine — since the masculine feature set {MASC} is a proper subset of feminine {FEM,MASC} and a proper superset of neuter ∅, any syncretism of N and F would also include M.

theorem AdamsonAnagnostopoulou2025.no_aba_syncretism : ¬(greekVI [] = greekVI [GenderNode.cls, GenderNode.masc, GenderNode.fem] ∧ greekVI [] ≠ greekVI [GenderNode.cls, GenderNode.masc])

Greek inflection: M is always "between" N and F in feature specificity. This rules out N = F ≠ M syncretism patterns.

Geometry → outcome

The paper's central thesis: cross-linguistic variation in resolution
follows from differences in feature geometry, not from different
resolution mechanisms or stipulated defaults. Same labels, same
mechanism, different geometry → different outcome.

We formalize each language's geometry as a function from a base
gender node to the full set of entailed iFs, then prove that
resolution outcomes follow from geometry alone. 

def AdamsonAnagnostopoulou2025.greekGeometry : GenderNode → AnnotatedFeatures GenderNode

Greek geometry (17): CLASS > MASC > FEM (linear chain). FEM entails MASC entails CLASS.

Equations

• One or more equations did not get rendered due to their size.
• AdamsonAnagnostopoulou2025.greekGeometry AdamsonAnagnostopoulou2025.GenderNode.cls = [{ value := AdamsonAnagnostopoulou2025.GenderNode.cls, interp := Minimalist.Interpretability.interpretable }]
• AdamsonAnagnostopoulou2025.greekGeometry x✝ = []

def AdamsonAnagnostopoulou2025.icelandicGeometry : GenderNode → AnnotatedFeatures GenderNode

Icelandic geometry (63): CLASS > {MASC, FEM} (independent siblings). Neither FEM nor MASC entails the other.

Equations

• One or more equations did not get rendered due to their size.
• AdamsonAnagnostopoulou2025.icelandicGeometry x✝ = []

theorem AdamsonAnagnostopoulou2025.greek_geometry_human_mismatch : resolve (greekGeometry GenderNode.fem) (greekGeometry GenderNode.masc) = some [GenderNode.cls, GenderNode.masc]

The linear chain geometry guarantees that mismatched human resolution retains MASC — because both conjuncts bear iMASC (FEM entails MASC).

theorem AdamsonAnagnostopoulou2025.icelandic_geometry_human_mismatch : resolve (icelandicGeometry GenderNode.fem) (icelandicGeometry GenderNode.masc) = some [GenderNode.cls]

The independent geometry means human mismatch loses both MASC and FEM — only CLASS survives intersection.

theorem AdamsonAnagnostopoulou2025.geometry_determines_resolution : Option.map greekVI (resolve (greekGeometry GenderNode.fem) (greekGeometry GenderNode.masc)) = some Infl.masc ∧ Option.map icelandicVI (resolve (icelandicGeometry GenderNode.fem) (icelandicGeometry GenderNode.masc)) = some Infl.neut

Geometry determines resolution outcome: same mechanism + same feature labels → different VI output, entirely from geometry.

theorem AdamsonAnagnostopoulou2025.greek_geometry_faithful_fem : greekGeometry GenderNode.fem = AdamsonAnagnostopoulou2025.gkHF✝

The geometry functions reconstruct the noun data: Greek nouns are exactly the geometry applied to their most specific iF.

theorem AdamsonAnagnostopoulou2025.greek_geometry_faithful_masc : greekGeometry GenderNode.masc = AdamsonAnagnostopoulou2025.gkHM✝

theorem AdamsonAnagnostopoulou2025.icelandic_geometry_faithful_fem : icelandicGeometry GenderNode.fem = AdamsonAnagnostopoulou2025.isHF✝

theorem AdamsonAnagnostopoulou2025.icelandic_geometry_faithful_masc : icelandicGeometry GenderNode.masc = AdamsonAnagnostopoulou2025.isHM✝

theorem AdamsonAnagnostopoulou2025.greek_fem_entails_masc : ((percolateI (greekGeometry GenderNode.masc)).all fun (x : GenderNode) => (percolateI (greekGeometry GenderNode.fem)).contains x) = true

Entailment asymmetry: in the linear chain (Greek), FEM's iFs are a superset of MASC's iFs. In the independent geometry (Icelandic), neither is a superset of the other. This is WHY the intersection outcomes differ.

theorem AdamsonAnagnostopoulou2025.icelandic_fem_not_entails_masc : ((percolateI (icelandicGeometry GenderNode.masc)).all fun (x : GenderNode) => (percolateI (icelandicGeometry GenderNode.fem)).contains x) = false

Vocabulary as FeatureVI items

The ad-hoc `greekVI` function above implements the Subset Principle
procedurally. Here we define the same vocabulary as `FeatureVI` items
([halle-marantz-1993]) and prove that `subsetPrinciple` selects
the same exponents. This connects the gender resolution mechanism to
the formal DM vocabulary insertion framework. 

def AdamsonAnagnostopoulou2025.greekVocabItems : List (Morphology.DM.VI.FeatureVI GenderNode Infl)

Greek vocabulary items as FeatureVI entries (schema 21). Most specific first: {FEM,MASC} → F, {MASC} → M, {} → N.

Equations

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

def AdamsonAnagnostopoulou2025.bcsVocabItems : List (Morphology.DM.VI.FeatureVI GenderNode Infl)

BCS vocabulary items as FeatureVI entries (schema 75). {FEM,ANIM} → F, {INDIV} → M, {} → N.

Equations

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

theorem AdamsonAnagnostopoulou2025.sp_greek_human_mismatch : Morphology.DM.VI.subsetPrinciple greekVocabItems [GenderNode.cls, GenderNode.masc] = some Infl.masc

Subset Principle agrees with ad-hoc greekVI for human mismatch.

theorem AdamsonAnagnostopoulou2025.sp_greek_inanim_mismatch : Morphology.DM.VI.subsetPrinciple greekVocabItems [GenderNode.cls] = some Infl.neut

Subset Principle agrees with greekVI for inanimate mismatch.

theorem AdamsonAnagnostopoulou2025.sp_greek_uniform_fem : Morphology.DM.VI.subsetPrinciple greekVocabItems [GenderNode.cls, GenderNode.masc, GenderNode.fem] = some Infl.fem

Subset Principle agrees with greekVI for uniform feminine.

theorem AdamsonAnagnostopoulou2025.sp_bcs_human_mismatch : Morphology.DM.VI.subsetPrinciple bcsVocabItems [GenderNode.cls, GenderNode.indiv, GenderNode.masc, GenderNode.anim] = some Infl.masc

Subset Principle agrees with bcsVI for human mismatch.

theorem AdamsonAnagnostopoulou2025.sp_same_vocab_different_geometry : Morphology.DM.VI.subsetPrinciple greekVocabItems [GenderNode.cls, GenderNode.masc] = some Infl.masc ∧ Morphology.DM.VI.subsetPrinciple greekVocabItems [GenderNode.cls] = some Infl.neut

Same vocabulary + different geometry → different outcome. Greek and Icelandic share the vocabulary (both use greekVocabItems), but the Subset Principle yields different results because the geometry produces different intersections.

FeatureOrder instances

The `FeatureOrder` structure packages a feature geometry — its nodes
and the bundle function that maps each node to its full set of
entailed features. This formalizes the paper's central insight that
cross-linguistic variation is geometry variation. 

def AdamsonAnagnostopoulou2025.greekOrder : FeatureOrder GenderNode

Greek feature order: CLASS > MASC > FEM (linear chain).

Equations

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

def AdamsonAnagnostopoulou2025.icelandicOrder : FeatureOrder GenderNode

Icelandic feature order: CLASS > {MASC, FEM} (independent siblings).

Equations

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

theorem AdamsonAnagnostopoulou2025.greek_order_fem_entails_masc : greekOrder.entails GenderNode.fem GenderNode.masc = true

Greek entailment: FEM entails MASC (FEM's bundle ⊇ MASC's bundle).

theorem AdamsonAnagnostopoulou2025.icelandic_order_fem_not_entails_masc : icelandicOrder.entails GenderNode.fem GenderNode.masc = false

Icelandic: FEM does NOT entail MASC (independent siblings).

theorem AdamsonAnagnostopoulou2025.greek_order_masc_entails_cls : greekOrder.entails GenderNode.masc GenderNode.cls = true

Greek: MASC entails CLASS.

theorem AdamsonAnagnostopoulou2025.greek_order_cls_not_entails_masc : greekOrder.entails GenderNode.cls GenderNode.masc = false

Greek: CLASS does NOT entail MASC (entailment is asymmetric).

MRH as a property of geometries

[adamson-anagnostopoulou-2025]'s Mismatch Resolution Hypothesis:
Greek satisfies MRH because ALL pairwise resolution outcomes produce
non-empty intersections — no default insertion is ever needed.

We verify this via the `satisfiesMRH` predicate from
the §0 resolution mechanism, instantiated with the geometry-derived bundles. 

theorem AdamsonAnagnostopoulou2025.greek_satisfies_mrh : greekOrder.satisfiesMRH' = true

Greek satisfies MRH: all pairwise resolutions succeed.

theorem AdamsonAnagnostopoulou2025.icelandic_satisfies_mrh : icelandicOrder.satisfiesMRH' = true

Icelandic satisfies MRH: all pairwise resolutions succeed. Despite different outcomes (neuter for humans instead of masculine), no resolution yields an empty intersection.

theorem AdamsonAnagnostopoulou2025.both_satisfy_mrh : greekOrder.satisfiesMRH' = true ∧ icelandicOrder.satisfiesMRH' = true

Both satisfy MRH — this is the paper's "no default insertion" claim: the difference between Greek and Icelandic is the content of the intersection, not whether it exists.

Three or more conjuncts

`resolveN` extends binary resolution to n-ary coordination via
iterated intersection. The predictions are the same: gender-matching
agreement emerges iff all conjuncts share a feature (after percolation). 

theorem AdamsonAnagnostopoulou2025.gk_ternary_uniform_fem : resolveN [AdamsonAnagnostopoulou2025.gkHF✝, AdamsonAnagnostopoulou2025.gkHF✝, AdamsonAnagnostopoulou2025.gkHF✝] = some [GenderNode.cls, GenderNode.masc, GenderNode.fem]

Greek: three human feminines → {CLASS,MASC,FEM}.

theorem AdamsonAnagnostopoulou2025.gk_ternary_human_mismatch : resolveN [AdamsonAnagnostopoulou2025.gkHF✝, AdamsonAnagnostopoulou2025.gkHM✝, AdamsonAnagnostopoulou2025.gkHF✝] = some [GenderNode.cls, GenderNode.masc]

Greek: three mismatched humans → {CLASS,MASC} (FEM eliminated). FEM + MASC + FEM: FEM present in first and third but not second.

theorem AdamsonAnagnostopoulou2025.gk_ternary_inanim : resolveN [AdamsonAnagnostopoulou2025.gkIF✝, AdamsonAnagnostopoulou2025.gkIM✝, AdamsonAnagnostopoulou2025.gkIN✝] = some [GenderNode.cls]

Greek: three inanimates → {CLASS} → neuter.

theorem AdamsonAnagnostopoulou2025.is_ternary_human_mismatch : resolveN [AdamsonAnagnostopoulou2025.isHF✝, AdamsonAnagnostopoulou2025.isHM✝, AdamsonAnagnostopoulou2025.isHF✝] = some [GenderNode.cls]

Icelandic: three mismatched humans → {CLASS} → neuter. Because MASC and FEM are independent, any mismatch loses both.

theorem AdamsonAnagnostopoulou2025.bcs_ternary_human_mismatch : resolveN [AdamsonAnagnostopoulou2025.bcsHF✝, AdamsonAnagnostopoulou2025.bcsHM✝, AdamsonAnagnostopoulou2025.bcsHF✝] = some [GenderNode.cls, GenderNode.indiv, GenderNode.masc, GenderNode.anim]

BCS: three mismatched humans → {CLASS,INDIV,MASC,ANIM} → masculine. INDIV guarantees masculine even with mismatched FEM.

theorem AdamsonAnagnostopoulou2025.nary_subsumes_binary_greek : resolveN [AdamsonAnagnostopoulou2025.gkHF✝, AdamsonAnagnostopoulou2025.gkHM✝] = resolve AdamsonAnagnostopoulou2025.gkHF✝ AdamsonAnagnostopoulou2025.gkHM✝

N-ary subsumes binary: resolveN [fs1, fs2] = resolve fs1 fs2.