NP-Ellipsis in Spanish Binominals @cite{saab-2026}

@cite{lobeck-1995} @cite{pesetsky-2013}

Theory-neutral data on NP-ellipsis patterns across three types of Spanish binominal constructions that are superficially syncretic (all use de) but differ in ellipsis licensing and agreement.

The Three Binominal Types

1. Pseudo-partitive: un grupo de estudiantes 'a group of students'

   • NP-ellipsis OK: un grupo ✓
   • Verb agrees with plural (students)

2. Quantificational: un montón de estudiantes 'a lot of students'

   • NP-ellipsis OK: un montón ✓
   • Verb agrees with plural (students)

3. Qualitative: una mierda de departamento 'a shit of apartment'

   • NP-ellipsis BLOCKED: *una mierda ✗ (with intended referent reading)
   • Verb agrees with singular (mierda)

Key Diagnostic

NP-ellipsis distinguishes pseudo-partitive/quantificational (which share a primeval genitive structure with Num[E]) from qualitative (which have an equative structure lacking Num[E]).

BinominalType and its core structural properties (licensesNPE, hasNumE) are defined in Core.Lexical.Binominal. This file adds ellipsis-specific data (genitive sources, agreement, concrete examples).

inductive Phenomena.Ellipsis.NPEllipsis.GenitiveSource : Type

The structural source of the genitive de (@cite{saab-2026} §4).

• primeval : GenitiveSource
• equative : GenitiveSource

instance Phenomena.Ellipsis.NPEllipsis.instDecidableEqGenitiveSource : DecidableEq GenitiveSource

Equations

• Phenomena.Ellipsis.NPEllipsis.instDecidableEqGenitiveSource x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Ellipsis.NPEllipsis.instBEqGenitiveSource.beq : GenitiveSource → GenitiveSource → Bool

Equations

• Phenomena.Ellipsis.NPEllipsis.instBEqGenitiveSource.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Ellipsis.NPEllipsis.instBEqGenitiveSource : BEq GenitiveSource

Equations

• Phenomena.Ellipsis.NPEllipsis.instBEqGenitiveSource = { beq := Phenomena.Ellipsis.NPEllipsis.instBEqGenitiveSource.beq }

instance Phenomena.Ellipsis.NPEllipsis.instReprGenitiveSource : Repr GenitiveSource

Equations

• Phenomena.Ellipsis.NPEllipsis.instReprGenitiveSource = { reprPrec := Phenomena.Ellipsis.NPEllipsis.instReprGenitiveSource.repr }

def Phenomena.Ellipsis.NPEllipsis.instReprGenitiveSource.repr : GenitiveSource → Nat → Std.Format

Equations

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

def Phenomena.Ellipsis.NPEllipsis.genitiveSource : Core.Lexical.Binominal.BinominalType → GenitiveSource

Map binominal type to its genitive source.

Equations

• Phenomena.Ellipsis.NPEllipsis.genitiveSource Core.Lexical.Binominal.BinominalType.pseudoPartitive = Phenomena.Ellipsis.NPEllipsis.GenitiveSource.primeval
• Phenomena.Ellipsis.NPEllipsis.genitiveSource Core.Lexical.Binominal.BinominalType.quantificational = Phenomena.Ellipsis.NPEllipsis.GenitiveSource.primeval
• Phenomena.Ellipsis.NPEllipsis.genitiveSource Core.Lexical.Binominal.BinominalType.qualitative = Phenomena.Ellipsis.NPEllipsis.GenitiveSource.equative

inductive Phenomena.Ellipsis.NPEllipsis.AgreementNumber : Type

Agreement number on the verb in binominal constructions. @cite{saab-2026} §2: the controller is always Num, not QP in Spec,DP.

• singular : AgreementNumber
• plural : AgreementNumber

instance Phenomena.Ellipsis.NPEllipsis.instDecidableEqAgreementNumber : DecidableEq AgreementNumber

Equations

• Phenomena.Ellipsis.NPEllipsis.instDecidableEqAgreementNumber x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Ellipsis.NPEllipsis.instBEqAgreementNumber.beq : AgreementNumber → AgreementNumber → Bool

Equations

• Phenomena.Ellipsis.NPEllipsis.instBEqAgreementNumber.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Ellipsis.NPEllipsis.instBEqAgreementNumber : BEq AgreementNumber

Equations

• Phenomena.Ellipsis.NPEllipsis.instBEqAgreementNumber = { beq := Phenomena.Ellipsis.NPEllipsis.instBEqAgreementNumber.beq }

def Phenomena.Ellipsis.NPEllipsis.instReprAgreementNumber.repr : AgreementNumber → Nat → Std.Format

Equations

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

instance Phenomena.Ellipsis.NPEllipsis.instReprAgreementNumber : Repr AgreementNumber

Equations

• Phenomena.Ellipsis.NPEllipsis.instReprAgreementNumber = { reprPrec := Phenomena.Ellipsis.NPEllipsis.instReprAgreementNumber.repr }

inductive Phenomena.Ellipsis.NPEllipsis.AgreementController : Type

Which element controls verbal agreement? @cite{saab-2026}: Num in all three types, never QP in Spec,DP.

• num : AgreementController
• specDP : AgreementController

instance Phenomena.Ellipsis.NPEllipsis.instDecidableEqAgreementController : DecidableEq AgreementController

Equations

• Phenomena.Ellipsis.NPEllipsis.instDecidableEqAgreementController x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Ellipsis.NPEllipsis.instBEqAgreementController.beq : AgreementController → AgreementController → Bool

Equations

• Phenomena.Ellipsis.NPEllipsis.instBEqAgreementController.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Ellipsis.NPEllipsis.instBEqAgreementController : BEq AgreementController

Equations

• Phenomena.Ellipsis.NPEllipsis.instBEqAgreementController = { beq := Phenomena.Ellipsis.NPEllipsis.instBEqAgreementController.beq }

def Phenomena.Ellipsis.NPEllipsis.instReprAgreementController.repr : AgreementController → Nat → Std.Format

Equations

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

instance Phenomena.Ellipsis.NPEllipsis.instReprAgreementController : Repr AgreementController

Equations

• Phenomena.Ellipsis.NPEllipsis.instReprAgreementController = { reprPrec := Phenomena.Ellipsis.NPEllipsis.instReprAgreementController.repr }

def Phenomena.Ellipsis.NPEllipsis.agreementController : Core.Lexical.Binominal.BinominalType → AgreementController

In all three types, Num controls agreement.

Equations

• Phenomena.Ellipsis.NPEllipsis.agreementController Core.Lexical.Binominal.BinominalType.pseudoPartitive = Phenomena.Ellipsis.NPEllipsis.AgreementController.num
• Phenomena.Ellipsis.NPEllipsis.agreementController Core.Lexical.Binominal.BinominalType.quantificational = Phenomena.Ellipsis.NPEllipsis.AgreementController.num
• Phenomena.Ellipsis.NPEllipsis.agreementController Core.Lexical.Binominal.BinominalType.qualitative = Phenomena.Ellipsis.NPEllipsis.AgreementController.num

def Phenomena.Ellipsis.NPEllipsis.verbAgreement : Core.Lexical.Binominal.BinominalType → AgreementNumber

The agreement number on the verb for each type. Pseudo-partitive/quantificational: Num inherits plural from complement NP. Qualitative: Num gets singular from the expressive noun.

Equations

• Phenomena.Ellipsis.NPEllipsis.verbAgreement Core.Lexical.Binominal.BinominalType.pseudoPartitive = Phenomena.Ellipsis.NPEllipsis.AgreementNumber.plural
• Phenomena.Ellipsis.NPEllipsis.verbAgreement Core.Lexical.Binominal.BinominalType.quantificational = Phenomena.Ellipsis.NPEllipsis.AgreementNumber.plural
• Phenomena.Ellipsis.NPEllipsis.verbAgreement Core.Lexical.Binominal.BinominalType.qualitative = Phenomena.Ellipsis.NPEllipsis.AgreementNumber.singular

theorem Phenomena.Ellipsis.NPEllipsis.agreement_from_num (b : Core.Lexical.Binominal.BinominalType) : agreementController b = AgreementController.num

Agreement controller is uniformly Num across all three types.

structure Phenomena.Ellipsis.NPEllipsis.NPEDatum : Type

An NP-ellipsis datum: a Spanish binominal sentence with its ellipsis and agreement properties.

• sentence : String

  The full sentence

• ellipsisForm : String

  The attempted ellipsis form

• npeGrammatical : Bool

  Is NP-ellipsis grammatical?

• binominalType : Core.Lexical.Binominal.BinominalType

  Binominal type

• agreement : AgreementNumber

  Agreement number on the verb

• source : String

  Source

instance Phenomena.Ellipsis.NPEllipsis.instReprNPEDatum : Repr NPEDatum

Equations

• Phenomena.Ellipsis.NPEllipsis.instReprNPEDatum = { reprPrec := Phenomena.Ellipsis.NPEllipsis.instReprNPEDatum.repr }

def Phenomena.Ellipsis.NPEllipsis.instReprNPEDatum.repr : NPEDatum → Nat → Std.Format

Equations

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

def Phenomena.Ellipsis.NPEllipsis.grupoDeEstudiantes : NPEDatum

Equations

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

def Phenomena.Ellipsis.NPEllipsis.conjuntoDeProblemas : NPEDatum

Equations

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

def Phenomena.Ellipsis.NPEllipsis.montonDeEstudiantes : NPEDatum

Equations

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

def Phenomena.Ellipsis.NPEllipsis.pilaDeLibros : NPEDatum

Equations

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

def Phenomena.Ellipsis.NPEllipsis.mierdaDeDepartamento : NPEDatum

Equations

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

def Phenomena.Ellipsis.NPEllipsis.maravillaDeMujer : NPEDatum

Equations

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

def Phenomena.Ellipsis.NPEllipsis.allExamples : List NPEDatum

All NP-ellipsis data.

Equations

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

theorem Phenomena.Ellipsis.NPEllipsis.grupo_npe_ok : grupoDeEstudiantes.npeGrammatical = grupoDeEstudiantes.binominalType.licensesNPE

Per-datum verification: each example's grammaticality matches its binominal type's NPE licensing prediction.

theorem Phenomena.Ellipsis.NPEllipsis.monton_npe_ok : montonDeEstudiantes.npeGrammatical = montonDeEstudiantes.binominalType.licensesNPE

theorem Phenomena.Ellipsis.NPEllipsis.mierda_npe_blocked : mierdaDeDepartamento.npeGrammatical = mierdaDeDepartamento.binominalType.licensesNPE

theorem Phenomena.Ellipsis.NPEllipsis.maravilla_npe_blocked : maravillaDeMujer.npeGrammatical = maravillaDeMujer.binominalType.licensesNPE

def Phenomena.Ellipsis.NPEllipsis.hasIndexicalEmptyNoun : Core.Lexical.Binominal.BinominalType → Bool

Qualitative binominals contain an indexical empty noun whose reference is contextually determined (like a pronoun). This is why NP-ellipsis fails: the empty noun cannot be recovered from the antecedent.

Equations

• Phenomena.Ellipsis.NPEllipsis.hasIndexicalEmptyNoun Core.Lexical.Binominal.BinominalType.pseudoPartitive = false
• Phenomena.Ellipsis.NPEllipsis.hasIndexicalEmptyNoun Core.Lexical.Binominal.BinominalType.quantificational = false
• Phenomena.Ellipsis.NPEllipsis.hasIndexicalEmptyNoun Core.Lexical.Binominal.BinominalType.qualitative = true

def Phenomena.Ellipsis.NPEllipsis.hasEquP : Core.Lexical.Binominal.BinominalType → Bool

Qualitative binominals contain an equative phrase (EquP) establishing a predication relation between the expressive noun and the referent.

Equations

• Phenomena.Ellipsis.NPEllipsis.hasEquP Core.Lexical.Binominal.BinominalType.pseudoPartitive = false
• Phenomena.Ellipsis.NPEllipsis.hasEquP Core.Lexical.Binominal.BinominalType.quantificational = false
• Phenomena.Ellipsis.NPEllipsis.hasEquP Core.Lexical.Binominal.BinominalType.qualitative = true

theorem Phenomena.Ellipsis.NPEllipsis.indexical_blocks_numE (b : Core.Lexical.Binominal.BinominalType) : hasIndexicalEmptyNoun b = true → b.hasNumE = false

The presence of an indexical empty noun entails no Num[E]: if the ellipsis site would include an unrecoverable element, NP-ellipsis is blocked.

theorem Phenomena.Ellipsis.NPEllipsis.primeval_iff_npe (b : Core.Lexical.Binominal.BinominalType) : (genitiveSource b == GenitiveSource.primeval) = b.licensesNPE

Primeval genitive ↔ Num[E] ↔ NP-ellipsis licensed. The three properties are coextensive across binominal types.