Spanish Noun Gender

[BBMR19] [Kra15] [Kra20] [Har91]

Spanish has two genders, masculine and feminine ([BBMR19] §1.1). Per [BBMR19] §1.2, Group A: nouns referring to humans + a few well-known animals get natural gender; per §1.3, Group B (lifeless things, plants, other animals) get arbitrary gender. Per §1.2.11, a small set of common-gender nouns (e.g. persona, víctima, ángel) take fixed gender regardless of referent.

Theory-neutral data layer

The Fragment carries two empirical fields per entry:

• attestedGender : Gender — the agreement-trigger fact (verified against [BBMR19] §1.2-1.3).
• isNaturalGender : Bool — whether the gender is semantically motivated by the referent's biological sex. False for inanimates, for non-natural-gender animals (cf. §1.3.1), and for the §1.2.11 fixed-gender common-gender exceptions (persona, ángel).

These two fields suffice to project every entry's structural analysis under [Kra15] Ch. 6's Set-1 DM categorizer (the projection lives in Studies/Kramer2020.lean); they also support [Har91]'s lexical-rule analysis directly (Harris's [FEMALE] and [HUMAN] features map onto attestedGender and the natural-gender inference).

Per-entry verification

Entries explicitly named in [Kra15]: hombre, mujer, niño, niña, mesa, cama, persona, libro, soldado, estudiante, artista. Other entries (rey/reina/gato/gata, silla/casa/puerta/ventana, zapato/coche/árbol/cielo/vaso, ángel) are extrapolations from Kramer's framework, anchored on the textbook-consensus genders documented in [BBMR19].

structure Spanish.Gender.SpanishNoun : Type

A Spanish noun. No commitment to any specific theoretical framework — Kramer's DM categorizing head, Harris's lexical rule, etc. are projections that live in Studies/.

• form : String
• gloss : String
• attestedGender : Gender

  Empirical agreement-trigger fact ([BBMR19]).

• isNaturalGender : Bool

  True iff the gender is semantically motivated by the referent's biological sex. False for inanimates, for non-natural-gender animals, and for the [BBMR19] §1.2.11 common-gender fixed-assignment exceptions (persona feminine for any sex; ángel masculine for any sex).

@[implicit_reducible]

instance Spanish.Gender.instDecidableEqSpanishNoun : DecidableEq SpanishNoun

Equations

• Spanish.Gender.instDecidableEqSpanishNoun = Spanish.Gender.instDecidableEqSpanishNoun.decEq

def Spanish.Gender.instDecidableEqSpanishNoun.decEq (x✝ x✝¹ : SpanishNoun) : Decidable (x✝ = x✝¹)

Equations

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

def Spanish.Gender.instReprSpanishNoun.repr : SpanishNoun → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Spanish.Gender.instReprSpanishNoun : Repr SpanishNoun

Equations

• Spanish.Gender.instReprSpanishNoun = { reprPrec := Spanish.Gender.instReprSpanishNoun.repr }

@[reducible, inline]

abbrev Spanish.Gender.SpanishNoun.gender (n : SpanishNoun) : Gender

Surface gender alias for ergonomic consumer access.

Equations

• n.gender = n.attestedGender

def Spanish.Gender.hombre : SpanishNoun

Equations

• Spanish.Gender.hombre = { form := "hombre", gloss := "man", attestedGender := Gender.masculine, isNaturalGender := true }

def Spanish.Gender.mujer : SpanishNoun

Equations

• Spanish.Gender.mujer = { form := "mujer", gloss := "woman", attestedGender := Gender.feminine, isNaturalGender := true }

def Spanish.Gender.niño : SpanishNoun

Equations

• Spanish.Gender.niño = { form := "niño", gloss := "boy", attestedGender := Gender.masculine, isNaturalGender := true }

def Spanish.Gender.niña : SpanishNoun

Equations

• Spanish.Gender.niña = { form := "niña", gloss := "girl", attestedGender := Gender.feminine, isNaturalGender := true }

def Spanish.Gender.rey : SpanishNoun

Equations

• Spanish.Gender.rey = { form := "rey", gloss := "king", attestedGender := Gender.masculine, isNaturalGender := true }

def Spanish.Gender.reina : SpanishNoun

Equations

• Spanish.Gender.reina = { form := "reina", gloss := "queen", attestedGender := Gender.feminine, isNaturalGender := true }

def Spanish.Gender.gato : SpanishNoun

Equations

• Spanish.Gender.gato = { form := "gato", gloss := "cat.M", attestedGender := Gender.masculine, isNaturalGender := true }

def Spanish.Gender.gata : SpanishNoun

Equations

• Spanish.Gender.gata = { form := "gata", gloss := "cat.F", attestedGender := Gender.feminine, isNaturalGender := true }

def Spanish.Gender.mesa : SpanishNoun

Equations

• Spanish.Gender.mesa = { form := "mesa", gloss := "table", attestedGender := Gender.feminine, isNaturalGender := false }

def Spanish.Gender.silla : SpanishNoun

Equations

• Spanish.Gender.silla = { form := "silla", gloss := "chair", attestedGender := Gender.feminine, isNaturalGender := false }

def Spanish.Gender.casa : SpanishNoun

Equations

• Spanish.Gender.casa = { form := "casa", gloss := "house", attestedGender := Gender.feminine, isNaturalGender := false }

def Spanish.Gender.puerta : SpanishNoun

Equations

• Spanish.Gender.puerta = { form := "puerta", gloss := "door", attestedGender := Gender.feminine, isNaturalGender := false }

def Spanish.Gender.ventana : SpanishNoun

Equations

• Spanish.Gender.ventana = { form := "ventana", gloss := "window", attestedGender := Gender.feminine, isNaturalGender := false }

def Spanish.Gender.cama : SpanishNoun

Equations

• Spanish.Gender.cama = { form := "cama", gloss := "bed", attestedGender := Gender.feminine, isNaturalGender := false }

def Spanish.Gender.persona : SpanishNoun

persona 'person': common-gender noun ([BBMR19] §1.2.11) — feminine regardless of referent's sex. The famous [Kra15] §6.2 exception: human-denoting noun with structurally arbitrary feminine gender. isNaturalGender = false captures that the gender does NOT come from biological sex (even though referent is human).

Equations

• Spanish.Gender.persona = { form := "persona", gloss := "person", attestedGender := Gender.feminine, isNaturalGender := false }

def Spanish.Gender.libro : SpanishNoun

Equations

• Spanish.Gender.libro = { form := "libro", gloss := "book", attestedGender := Gender.masculine, isNaturalGender := false }

def Spanish.Gender.zapato : SpanishNoun

Equations

• Spanish.Gender.zapato = { form := "zapato", gloss := "shoe", attestedGender := Gender.masculine, isNaturalGender := false }

def Spanish.Gender.coche : SpanishNoun

Equations

• Spanish.Gender.coche = { form := "coche", gloss := "car", attestedGender := Gender.masculine, isNaturalGender := false }

def Spanish.Gender.árbol : SpanishNoun

Equations

• Spanish.Gender.árbol = { form := "árbol", gloss := "tree", attestedGender := Gender.masculine, isNaturalGender := false }

def Spanish.Gender.cielo : SpanishNoun

Equations

• Spanish.Gender.cielo = { form := "cielo", gloss := "sky", attestedGender := Gender.masculine, isNaturalGender := false }

def Spanish.Gender.vaso : SpanishNoun

Equations

• Spanish.Gender.vaso = { form := "vaso", gloss := "glass", attestedGender := Gender.masculine, isNaturalGender := false }

def Spanish.Gender.ángel : SpanishNoun

ángel 'angel': common-gender noun ([BBMR19] §1.2.11) — masculine for any sex. Companion to persona: the masculine fixed-gender exception. isNaturalGender = false.

Equations

• Spanish.Gender.ángel = { form := "ángel", gloss := "angel", attestedGender := Gender.masculine, isNaturalGender := false }

structure Spanish.Gender.SameRootEntry : Type

Same-root nominals: a single root that surfaces as either masculine or feminine depending on the referent's sex. Empirically polymorphic in gender (one form, two genders), distinct from the atomic SpanishNoun schema. The DM analysis (combination with i[+FEM] vs i[−FEM]) lives in Studies/Kramer2020.lean.

• form : String
• gloss : String

@[implicit_reducible]

instance Spanish.Gender.instDecidableEqSameRootEntry : DecidableEq SameRootEntry

Equations

• Spanish.Gender.instDecidableEqSameRootEntry = Spanish.Gender.instDecidableEqSameRootEntry.decEq

def Spanish.Gender.instDecidableEqSameRootEntry.decEq (x✝ x✝¹ : SameRootEntry) : Decidable (x✝ = x✝¹)

Equations

• Spanish.Gender.instDecidableEqSameRootEntry.decEq { form := a, gloss := a_1 } { form := b, gloss := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance Spanish.Gender.instReprSameRootEntry : Repr SameRootEntry

Equations

• Spanish.Gender.instReprSameRootEntry = { reprPrec := Spanish.Gender.instReprSameRootEntry.repr }

def Spanish.Gender.instReprSameRootEntry.repr : SameRootEntry → ℕ → Std.Format

Equations

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

def Spanish.Gender.soldado : SameRootEntry

Equations

• Spanish.Gender.soldado = { form := "soldado", gloss := "soldier" }

def Spanish.Gender.estudiante : SameRootEntry

Equations

• Spanish.Gender.estudiante = { form := "estudiante", gloss := "student" }

def Spanish.Gender.artista : SameRootEntry

Equations

• Spanish.Gender.artista = { form := "artista", gloss := "artist" }

def Spanish.Gender.naturalFemNouns : List SpanishNoun

Equations

• Spanish.Gender.naturalFemNouns = [Spanish.Gender.mujer, Spanish.Gender.niña, Spanish.Gender.reina, Spanish.Gender.gata]

def Spanish.Gender.naturalMascNouns : List SpanishNoun

Equations

• Spanish.Gender.naturalMascNouns = [Spanish.Gender.hombre, Spanish.Gender.niño, Spanish.Gender.rey, Spanish.Gender.gato]

def Spanish.Gender.arbitraryFemNouns : List SpanishNoun

Equations

• Spanish.Gender.arbitraryFemNouns = [Spanish.Gender.mesa, Spanish.Gender.silla, Spanish.Gender.casa, Spanish.Gender.puerta, Spanish.Gender.ventana, Spanish.Gender.cama, Spanish.Gender.persona]

def Spanish.Gender.defaultMascNouns : List SpanishNoun

Equations

• Spanish.Gender.defaultMascNouns = [Spanish.Gender.libro, Spanish.Gender.zapato, Spanish.Gender.coche, Spanish.Gender.árbol, Spanish.Gender.cielo, Spanish.Gender.vaso, Spanish.Gender.ángel]

def Spanish.Gender.allNouns : List SpanishNoun

Equations

• Spanish.Gender.allNouns = Spanish.Gender.naturalFemNouns ++ Spanish.Gender.naturalMascNouns ++ Spanish.Gender.arbitraryFemNouns ++ Spanish.Gender.defaultMascNouns

def Spanish.Gender.sameRootNouns : List SameRootEntry

Equations

• Spanish.Gender.sameRootNouns = [Spanish.Gender.soldado, Spanish.Gender.estudiante, Spanish.Gender.artista]

inductive Spanish.Gender.Value : Type

Spanish's two controller genders — the carrier of its Gender.System ([Cor91]; [Kra15]).

• masc : Value
• fem : Value

@[implicit_reducible]

instance Spanish.Gender.instDecidableEqValue : DecidableEq Value

Equations

• Spanish.Gender.instDecidableEqValue x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Spanish.Gender.instReprValue : Repr Value

Equations

• Spanish.Gender.instReprValue = { reprPrec := Spanish.Gender.instReprValue.repr }

def Spanish.Gender.instReprValue.repr : Value → ℕ → Std.Format

Equations

• Spanish.Gender.instReprValue.repr Spanish.Gender.Value.masc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Spanish.Gender.Value.masc")).group prec✝
• Spanish.Gender.instReprValue.repr Spanish.Gender.Value.fem prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Spanish.Gender.Value.fem")).group prec✝

@[implicit_reducible]

instance Spanish.Gender.instFintypeValue : Fintype Value

Equations

• Spanish.Gender.instFintypeValue = { elems := { val := ↑Spanish.Gender.Value.enumList, nodup := Spanish.Gender.Value.enumList_nodup }, complete := Spanish.Gender.instFintypeValue._proof_1 }

inductive Spanish.Gender.Concord : Type

Adjectival concord exponents: the -o vs -a desinence contrast ([BBMR19]). Evidence type for Gender.Faithful.

• o : Concord
• a : Concord

@[implicit_reducible]

instance Spanish.Gender.instDecidableEqConcord : DecidableEq Concord

Equations

• Spanish.Gender.instDecidableEqConcord x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Spanish.Gender.instReprConcord.repr : Concord → ℕ → Std.Format

Equations

• Spanish.Gender.instReprConcord.repr Spanish.Gender.Concord.o prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Spanish.Gender.Concord.o")).group prec✝
• Spanish.Gender.instReprConcord.repr Spanish.Gender.Concord.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Spanish.Gender.Concord.a")).group prec✝

@[implicit_reducible]

instance Spanish.Gender.instReprConcord : Repr Concord

Equations

• Spanish.Gender.instReprConcord = { reprPrec := Spanish.Gender.instReprConcord.repr }

def Spanish.Gender.Value.concord : Value → Concord

Per-gender adjectival concord.

Equations

• Spanish.Gender.Value.masc.concord = Spanish.Gender.Concord.o
• Spanish.Gender.Value.fem.concord = Spanish.Gender.Concord.a

def Spanish.Gender.system : Gender.System Value

The Spanish gender system over its own carrier: full comparative labelling; masculine is the morphosyntactic default (plain-n roots surface masculine — [Kra15]'s Set-1 derivation, exercised at Kramer2020.set1_plain_n_masculine).

Equations

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

def Spanish.Gender.Value.ofLabel : Gender → Value

Comparative label → controller gender (ingestion).

Equations

• Spanish.Gender.Value.ofLabel Gender.feminine = Spanish.Gender.Value.fem
• Spanish.Gender.Value.ofLabel x✝ = Spanish.Gender.Value.masc

def Spanish.Gender.SpanishNoun.controllerGender (n : SpanishNoun) : Value

Controller gender of a noun, from the attested agreement fact.

Equations

• n.controllerGender = Spanish.Gender.Value.ofLabel n.attestedGender

def Spanish.Gender.assigned : Gender.System.Assigned SpanishNoun Value

The assigned system: every noun gets its controller gender.

Equations

• Spanish.Gender.assigned = { toSystem := Spanish.Gender.system, assign := Spanish.Gender.SpanishNoun.controllerGender }

theorem Spanish.Gender.faithful_concord : Gender.Faithful fun (g : Value) (x : Unit) => g.concord

The carrier is faithful to the adjectival concord evidence: -o vs -a distinguishes the two genders. [Cor91]'s genders-are-agreement-classes criterion, discharged via Gender.Faithful.

theorem Spanish.Gender.system_label_assign (n : SpanishNoun) : n ∈ allNouns → system.label n.controllerGender = some n.attestedGender

Label ∘ assign recovers the attested gender across the inventory: the system view and the per-noun data agree.

theorem Spanish.Gender.assigned_semanticCore : assigned.SemanticCore {n : SpanishNoun | n.isNaturalGender = true} fun (x : SpanishNoun) => x.attestedGender

[Kra15]'s (7ii) / [Dah00]'s generalization instantiated: on the natural-gender core (Group A), assignment factors through the attested gender — which on that core is the referent-sex classification (that is what isNaturalGender asserts). persona and ángel are outside the core (isNaturalGender = false), so the fixed-gender exceptions do not disturb the factoring.