Minimalist Nominal Spine → NP-Ellipsis [Saa26]

[Lob95] [Rit91]

Connects the Minimalist nominal extended projection (N → n → Q → Num → D) to the NP-ellipsis data in Spanish binominals.

Key Results

1. The nominal argument domain (nP = {N, n}) parallels the verbal argument domain (vP = {V, v}) at the same F-level cutoff.
2. NP-ellipsis targets exactly the nominal argument domain: everything at or below n (F1) is deleted when Num carries [E].
3. Pseudo-partitive and quantificational binominals have Num[E]; qualitative binominals lack it due to their EquP structure.
4. The genitive source ([Pes13] primeval vs. equative) and the verbal-agreement number track the same split, and the typed example rows (Data.Examples.Saab2026) conform to all predictions.

Nominal ellipsis licensing (relocated from Minimalist/Ellipsis/Nominal.lean)

[Mer01] [Saa26] [Lob95]

NP-ellipsis is licensed when the Num head carries an [E] feature, which permits PF-deletion of the nominal argument domain (complement of Num — everything at or below nP).

The nominal argument domain is {N, n} (F0–F1), parallel to the verbal argument domain {V, v}. Num (F2) and above are outside.

structure Saab2026.NominalEllipsisLicense : Type

Nominal ellipsis license: Num[E] feature. NP-ellipsis is licensed when the Num head carries an [E] feature, which permits PF-deletion of the nominal argument domain (complement of Num — everything at or below nP).

• numHasE : Bool

  Does Num carry [E]?

• argDomainBoundary : Minimalist.Cat

  The nominal argument domain boundary (n for full DPs).

def Saab2026.instReprNominalEllipsisLicense.repr : NominalEllipsisLicense → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Saab2026.instReprNominalEllipsisLicense : Repr NominalEllipsisLicense

Equations

• Saab2026.instReprNominalEllipsisLicense = { reprPrec := Saab2026.instReprNominalEllipsisLicense.repr }

@[implicit_reducible]

instance Saab2026.instDecidableEqNominalEllipsisLicense : DecidableEq NominalEllipsisLicense

Equations

• Saab2026.instDecidableEqNominalEllipsisLicense = Saab2026.instDecidableEqNominalEllipsisLicense.decEq

def Saab2026.instDecidableEqNominalEllipsisLicense.decEq (x✝ x✝¹ : NominalEllipsisLicense) : Decidable (x✝ = x✝¹)

Equations

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

def Saab2026.NominalEllipsisLicense.isLicensed (nel : NominalEllipsisLicense) : Bool

Is NP-ellipsis licensed? Requires Num[E].

Equations

• nel.isLicensed = nel.numHasE

theorem Saab2026.n_lexical_in_nominal_argdomain : Minimalist.isInArgumentDomain Minimalist.Cat.N Minimalist.Cat.D

N is within the nominal argument domain (F0 ≤ F1 = n).

theorem Saab2026.n_functional_in_nominal_argdomain : Minimalist.isInArgumentDomain Minimalist.Cat.n Minimalist.Cat.D

n is within the nominal argument domain (F1 ≤ F1).

theorem Saab2026.num_not_in_nominal_argdomain : ¬Minimalist.isInArgumentDomain Minimalist.Cat.Num Minimalist.Cat.D

Num is NOT in the nominal argument domain (F2 > F1 = n).

theorem Saab2026.q_not_in_nominal_argdomain : ¬Minimalist.isInArgumentDomain Minimalist.Cat.Q Minimalist.Cat.D

Q is NOT in the nominal argument domain (F3 > F1 = n).

theorem Saab2026.d_not_in_nominal_argdomain : ¬Minimalist.isInArgumentDomain Minimalist.Cat.D Minimalist.Cat.D

D is NOT in the nominal argument domain (F4 > F1 = n).

theorem Saab2026.pseudopartitive_licenses_npe : { numHasE := true }.isLicensed = true

NP-ellipsis with Num[E]: pseudo-partitive/quantificational binominals license deletion of the nominal argument domain.

theorem Saab2026.qualitative_blocks_npe : { numHasE := false }.isLicensed = false

NP-ellipsis without Num[E]: qualitative binominals (with EquP + indexical empty noun) block NP-ellipsis.

theorem Saab2026.nominal_ep_wellformed : Minimalist.allCategoryConsistent Minimalist.fullNominalEP = true ∧ Minimalist.allFMonotone Minimalist.fullNominalEP = true

The full nominal EP [N, n, Q, Num, D] is well-formed: category-consistent and F-monotone.

theorem Saab2026.nominal_verbal_spine_parallel : Minimalist.fValue Minimalist.Cat.N = Minimalist.fValue Minimalist.Cat.V ∧ Minimalist.fValue Minimalist.Cat.n = Minimalist.fValue Minimalist.Cat.v ∧ Minimalist.fValue Minimalist.Cat.Q = Minimalist.fValue Minimalist.Cat.T ∧ Minimalist.fValue Minimalist.Cat.Num = Minimalist.fValue Minimalist.Cat.Fin

The nominal spine is structurally parallel to the verbal spine at all F-levels: lexical (F0) → categorizer (F1) → specification (F2) → inner edge (F3) → discourse (F4+).

At F2–F3, the parallel is structural (same EP zone) rather than functional: T specifies temporally while Q specifies via individuation; Fin types the clause while Num types the nominal.

theorem Saab2026.argdomain_boundary_parallel : Minimalist.fValue (Minimalist.argumentDomainCat Minimalist.Cat.C) = Minimalist.fValue (Minimalist.argumentDomainCat Minimalist.Cat.D)

The verbal and nominal argument domains use the same F-level boundary (F1): v for clauses, n for noun phrases.

theorem Saab2026.verbal_nominal_argdomain_symmetric : Minimalist.isInArgumentDomain Minimalist.Cat.V Minimalist.Cat.C ∧ Minimalist.isInArgumentDomain Minimalist.Cat.v Minimalist.Cat.C ∧ ¬Minimalist.isInArgumentDomain Minimalist.Cat.T Minimalist.Cat.C ∧ Minimalist.isInArgumentDomain Minimalist.Cat.N Minimalist.Cat.D ∧ Minimalist.isInArgumentDomain Minimalist.Cat.n Minimalist.Cat.D ∧ ¬Minimalist.isInArgumentDomain Minimalist.Cat.Q Minimalist.Cat.D

The verbal argument domain is {V, v} (F0–F1). The nominal argument domain is {N, n} (F0–F1). Both exclude inflectional heads (T/Num at F2).

def Saab2026.mkNominalLicense (b : Quantification.Binominal.BinominalType) : NominalEllipsisLicense

Build a NominalEllipsisLicense from a BinominalType.

Equations

• Saab2026.mkNominalLicense b = { numHasE := b.hasNumE }

theorem Saab2026.pseudopartitive_license : (mkNominalLicense Quantification.Binominal.BinominalType.pseudoPartitive).isLicensed = true

Pseudo-partitive Num[E] licenses NP-ellipsis.

theorem Saab2026.quantificational_license : (mkNominalLicense Quantification.Binominal.BinominalType.quantificational).isLicensed = true

Quantificational Num[E] licenses NP-ellipsis.

theorem Saab2026.qualitative_no_license : (mkNominalLicense Quantification.Binominal.BinominalType.qualitative).isLicensed = false

Qualitative lacks Num[E], blocking NP-ellipsis.

theorem Saab2026.licensing_matches_data (b : Quantification.Binominal.BinominalType) : (mkNominalLicense b).isLicensed = b.licensesNPE

The licensing prediction matches the empirical data for every binominal type.

inductive Saab2026.GenitiveSource : Type

The structural source of the genitive de in a binominal.

• primeval : GenitiveSource

  [Pes13]'s primeval genitive: default case assigned when D blocks structural case.

• equative : GenitiveSource

  [dD06]-style EquP predication, not a true genitive.

@[implicit_reducible]

instance Saab2026.instDecidableEqGenitiveSource : DecidableEq GenitiveSource

Equations

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

@[implicit_reducible]

instance Saab2026.instReprGenitiveSource : Repr GenitiveSource

Equations

• Saab2026.instReprGenitiveSource = { reprPrec := Saab2026.instReprGenitiveSource.repr }

def Saab2026.instReprGenitiveSource.repr : GenitiveSource → ℕ → Std.Format

Equations

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

def Saab2026.genitiveSource : Quantification.Binominal.BinominalType → GenitiveSource

Map a binominal type to its genitive source. Pseudo-partitive and quantificational binominals have the primeval genitive; qualitative binominals have the equative structure, whose indexical empty noun (contextually referential, like a pronoun) is unrecoverable at the ellipsis site.

Equations

• Saab2026.genitiveSource Quantification.Binominal.BinominalType.pseudoPartitive = Saab2026.GenitiveSource.primeval
• Saab2026.genitiveSource Quantification.Binominal.BinominalType.quantificational = Saab2026.GenitiveSource.primeval
• Saab2026.genitiveSource Quantification.Binominal.BinominalType.qualitative = Saab2026.GenitiveSource.equative

theorem Saab2026.primeval_iff_npe (b : Quantification.Binominal.BinominalType) : (genitiveSource b == GenitiveSource.primeval) = b.licensesNPE

Primeval genitive ↔ NP-ellipsis licensed: the genitive source and Num[E]-driven licensing are coextensive across binominal types.

def Saab2026.verbAgreement : Quantification.Binominal.BinominalType → Number

The number on the verb for each binominal type: Num inherits plural from the complement NP in pseudo-partitives and quantificationals, but gets singular from the expressive noun in qualitatives.

Equations

• Saab2026.verbAgreement Quantification.Binominal.BinominalType.pseudoPartitive = Number.plural
• Saab2026.verbAgreement Quantification.Binominal.BinominalType.quantificational = Number.plural
• Saab2026.verbAgreement Quantification.Binominal.BinominalType.qualitative = Number.singular

def Saab2026.binominalOfFeature : String → Option Quantification.Binominal.BinominalType

Parse a binominal_type paper-feature value.

Equations

• Saab2026.binominalOfFeature "pseudo_partitive" = some Quantification.Binominal.BinominalType.pseudoPartitive
• Saab2026.binominalOfFeature "quantificational" = some Quantification.Binominal.BinominalType.quantificational
• Saab2026.binominalOfFeature "qualitative" = some Quantification.Binominal.BinominalType.qualitative
• Saab2026.binominalOfFeature x✝ = none

def Saab2026.numberOfFeature : String → Option Number

Parse a verb_agreement paper-feature value.

Equations

• Saab2026.numberOfFeature "singular" = some Number.singular
• Saab2026.numberOfFeature "plural" = some Number.plural
• Saab2026.numberOfFeature x✝ = none

theorem Saab2026.examples_conform : (Examples.all.all fun (e : Data.Examples.LinguisticExample) => match (List.lookup "binominal_type" e.paperFeatures).bind binominalOfFeature with | some b => List.lookup "npe_grammatical" e.paperFeatures == some (if b.licensesNPE = true then "true" else "false") && (List.lookup "verb_agreement" e.paperFeatures).bind numberOfFeature == some (verbAgreement b) | none => false) = true

Every example row's npe_grammatical and verb_agreement features match the predictions (licensesNPE, verbAgreement) for its binominal_type.

theorem Saab2026.nominal_spine_ep_internal : Minimalist.isEPInternal Minimalist.Cat.N Minimalist.Cat.n = true ∧ Minimalist.isEPInternal Minimalist.Cat.n Minimalist.Cat.Q = true ∧ Minimalist.isEPInternal Minimalist.Cat.Q Minimalist.Cat.Num = true ∧ Minimalist.isEPInternal Minimalist.Cat.Num Minimalist.Cat.D = true

Each nominal functional head is EP-internal to the next higher head — complement selection proceeds up the nominal spine: N(F0) → n(F1) → Q(F2) → Num(F3) → D(F4).

theorem Saab2026.nominal_external_to_verbal : Minimalist.isEPExternal Minimalist.Cat.D Minimalist.Cat.v = true ∧ Minimalist.isEPExternal Minimalist.Cat.Q Minimalist.Cat.T = true ∧ Minimalist.isEPExternal Minimalist.Cat.n Minimalist.Cat.v = true

Nominal heads are EP-external to verbal projections: a DP in Spec,vP is always EP-external (nominal ≠ verbal).