Nominal Ellipsis Licensing

@cite{merchant-2001} @cite{saab-2026} @cite{lobeck-1995}

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).

Nominal Argument Domain

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

structure Minimalist.Ellipsis.Nominal.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 : Cat

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

@[implicit_reducible]

instance Minimalist.Ellipsis.Nominal.instReprNominalEllipsisLicense : Repr NominalEllipsisLicense

Equations

• Minimalist.Ellipsis.Nominal.instReprNominalEllipsisLicense = { reprPrec := Minimalist.Ellipsis.Nominal.instReprNominalEllipsisLicense.repr }

def Minimalist.Ellipsis.Nominal.instReprNominalEllipsisLicense.repr : NominalEllipsisLicense → ℕ → Std.Format

Equations

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

def Minimalist.Ellipsis.Nominal.instDecidableEqNominalEllipsisLicense.decEq (x✝ x✝¹ : NominalEllipsisLicense) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Minimalist.Ellipsis.Nominal.instDecidableEqNominalEllipsisLicense : DecidableEq NominalEllipsisLicense

Equations

• Minimalist.Ellipsis.Nominal.instDecidableEqNominalEllipsisLicense = Minimalist.Ellipsis.Nominal.instDecidableEqNominalEllipsisLicense.decEq

def Minimalist.Ellipsis.Nominal.NominalEllipsisLicense.isLicensed (nel : NominalEllipsisLicense) : Bool

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

Equations

• nel.isLicensed = nel.numHasE

theorem Minimalist.Ellipsis.Nominal.n_lexical_in_nominal_argdomain : isInArgumentDomain Cat.N Cat.D = true

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

theorem Minimalist.Ellipsis.Nominal.n_functional_in_nominal_argdomain : isInArgumentDomain Cat.n Cat.D = true

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

theorem Minimalist.Ellipsis.Nominal.num_not_in_nominal_argdomain : isInArgumentDomain Cat.Num Cat.D = false

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

theorem Minimalist.Ellipsis.Nominal.q_not_in_nominal_argdomain : isInArgumentDomain Cat.Q Cat.D = false

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

theorem Minimalist.Ellipsis.Nominal.d_not_in_nominal_argdomain : isInArgumentDomain Cat.D Cat.D = false

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

theorem Minimalist.Ellipsis.Nominal.pseudopartitive_licenses_npe : { numHasE := true }.isLicensed = true

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

theorem Minimalist.Ellipsis.Nominal.qualitative_blocks_npe : { numHasE := false }.isLicensed = false

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