structure Minimalism.Sluicing.ArgumentDomain : Type

The argument domain of an extended projection (@cite{anand-mccloskey-2025}, Def 4).

The argument domain is the most inclusive projection in the EP that denotes type ⟨e,t⟩ (a property). This is the domain relevant for syntactic identity in sluicing.

For full clauses (CP/TP): the argument domain = vP

• vP still denotes ⟨e,t⟩ (property of events)
• Everything above vP (T, C) is outside the argument domain

For small clauses: the argument domain = the SC itself

• No functional layers above the lexical head

• ep : ExtendedProjection

  The EP this argument domain belongs to

• boundary : SyntacticObject

  The syntactic object at the argument domain boundary

• boundaryCat : Cat

  The category at the boundary

• denotesProperty : epSemanticType self.boundaryCat = EPSemanticType.property ∨ epSemanticType self.boundaryCat = EPSemanticType.intermediate

  The boundary denotes a property or is intermediate

def Minimalism.Sluicing.argumentDomainSpine (topCat : Cat) : List Cat → List Cat

The categories within the argument domain for a given top category. Filters the full EP spine to just those at or below the AD boundary.

Equations

• Minimalism.Sluicing.argumentDomainSpine topCat = List.filter fun (c : Minimalism.Cat) => Minimalism.isInArgumentDomain c topCat

structure Minimalism.Sluicing.HeadPair : Type

A head pair: a head and its complement category within the argument domain. Head pairs encode the local syntactic structure that must match between antecedent and ellipsis site.

@cite{anand-mccloskey-2025} Definition 5: Two heads are lexically identical iff they have the same category AND complement category. Case is included because it is assigned within the argument domain: a V that assigns dative is structurally distinct from one that assigns accusative (@cite{merchant-2001}, @cite{anand-hardt-mccloskey-2021} §5.5).

• head : Cat

  The category of the head

• complement : Cat

  The category of its complement

• headId : ℕ

  Lexical identity token (from LIToken.id) for identity tracking

• assignedCase : Option UD.Case

  Case assigned by the head to its complement, when relevant. none for head pairs where case is not assigned (e.g., v–V).

• voiceFlavor : Option VoiceFlavor

  Voice flavor of the head (agentive, nonThematic, etc.), when relevant. Distinguishes active v[agentive] from passive v[nonThematic] within the argument domain.

def Minimalism.Sluicing.instReprHeadPair.repr : HeadPair → ℕ → Std.Format

Equations

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

instance Minimalism.Sluicing.instReprHeadPair : Repr HeadPair

Equations

• Minimalism.Sluicing.instReprHeadPair = { reprPrec := Minimalism.Sluicing.instReprHeadPair.repr }

instance Minimalism.Sluicing.instDecidableEqHeadPair : DecidableEq HeadPair

Equations

• Minimalism.Sluicing.instDecidableEqHeadPair = Minimalism.Sluicing.instDecidableEqHeadPair.decEq

def Minimalism.Sluicing.instDecidableEqHeadPair.decEq (x✝ x✝¹ : HeadPair) : Decidable (x✝ = x✝¹)

Equations

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

instance Minimalism.Sluicing.instBEqHeadPair : BEq HeadPair

Equations

• Minimalism.Sluicing.instBEqHeadPair = { beq := Minimalism.Sluicing.instBEqHeadPair.beq }

def Minimalism.Sluicing.instBEqHeadPair.beq : HeadPair → HeadPair → Bool

Equations

• One or more equations did not get rendered due to their size.
• Minimalism.Sluicing.instBEqHeadPair.beq x✝¹ x✝ = false

partial def Minimalism.Sluicing.extractHeadPairs (so : SyntacticObject) (topCat : Cat) : List HeadPair

Extract head pairs from a syntactic object, restricted to heads whose F-value falls within the argument domain of the given top category.

Each node ⟨head, complement⟩ where the head selects the complement produces a head pair recording their categories.

def Minimalism.Sluicing.lexicallyIdentical (hp1 hp2 : HeadPair) : Bool

Lexical identity of head pairs (@cite{anand-mccloskey-2025}, Def 5): Two head pairs are lexically identical iff they have the same head category, complement category, and assigned case (when both specify case).

Case matching follows from the SIC because case is assigned within the argument domain: if the head assigns different case, the head-complement relationship is structurally distinct.

Note: headId is ignored — lexical identity is about structural properties, not token identity. When either side has assignedCase = none, case is not checked (the head pair does not involve case assignment, e.g., v selecting VP).

Equations

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

def Minimalism.Sluicing.removeFirst {α : Type} (p : α → Bool) : List α → Option (List α)

Remove the first element matching a predicate from a list. Returns none if no match found, some remaining otherwise.

Equations

• Minimalism.Sluicing.removeFirst p [] = none
• Minimalism.Sluicing.removeFirst p (x_1 :: xs) = if p x_1 = true then some xs else Option.map (fun (x : List α) => x_1 :: x) (Minimalism.Sluicing.removeFirst p xs)

def Minimalism.Sluicing.matchHeadPairs : List HeadPair → List HeadPair → Bool

Check if every head pair in pairs1 has a lexically identical match in pairs2, consuming matches (1-1 correspondence).

Equations

• One or more equations did not get rendered due to their size.
• Minimalism.Sluicing.matchHeadPairs [] x✝ = true

def Minimalism.Sluicing.structurallyIdentical (pairs1 pairs2 : List HeadPair) : Bool

Structural identity (@cite{anand-mccloskey-2025}, Def 6): Two sets of head pairs are structurally identical iff they can be put in 1-1 correspondence where each pair is lexically identical.

This requires same cardinality AND a bijective matching.

Equations

• Minimalism.Sluicing.structurallyIdentical pairs1 pairs2 = (pairs1.length == pairs2.length && Minimalism.Sluicing.matchHeadPairs pairs1 pairs2)

structure Minimalism.Sluicing.SluicingLicense : Type

Sluicing license: the Syntactic Isomorphism Condition (SIC).

Sluicing of a CP is licensed iff the argument domain of the ellipsis site has structurally identical head pairs to the argument domain of the antecedent.

• antecedentPairs : List HeadPair

  Head pairs from the antecedent's argument domain

• ellipsisPairs : List HeadPair

  Head pairs from the ellipsis site's argument domain

• antecedentTop : Cat

  Top category of the antecedent clause

• ellipsisTop : Cat

  Top category of the ellipsis clause

def Minimalism.Sluicing.SluicingLicense.isLicensed (sl : SluicingLicense) : Bool

Is sluicing licensed? Checks structural identity of head pairs.

Equations

• sl.isLicensed = Minimalism.Sluicing.structurallyIdentical sl.antecedentPairs sl.ellipsisPairs

def Minimalism.Sluicing.mkSluicingLicense (antecedent ellipsis : SyntacticObject) (antTop ellTop : Cat) : SluicingLicense

Build a sluicing license from two syntactic objects.

Equations

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

theorem Minimalism.Sluicing.voice_flavor_in_argdomain : isInArgumentDomain Cat.Voice Cat.C = true

Voice is within the argument domain (F1, same level as v). @cite{anand-hardt-mccloskey-2021}: voice mismatches ARE blocked by the SIC because v[agentive] ≠ v[nonThematic] within the argument domain.

theorem Minimalism.Sluicing.t_outside_argdomain : isInArgumentDomain Cat.T Cat.C = false

T is not within the argument domain of a CP.

theorem Minimalism.Sluicing.c_outside_argdomain : isInArgumentDomain Cat.C Cat.C = false

C is not within the argument domain.

def Minimalism.Sluicing.activeVP : List HeadPair

Head pairs for an active (agentive) transitive vP. v[agentive] selects VP, V selects DP.

Equations

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

def Minimalism.Sluicing.passiveVP : List HeadPair

Head pairs for a passive (non-thematic) transitive vP. v[nonThematic] selects VP, V selects DP.

Equations

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

theorem Minimalism.Sluicing.voice_mismatch_blocks_sluicing : structurallyIdentical activeVP passiveVP = false

Voice mismatch blocks sluicing: active v[agentive] ≠ passive v[nonThematic] within the argument domain.

theorem Minimalism.Sluicing.voice_match_licenses_sluicing : structurallyIdentical activeVP activeVP = true

Same voice licenses sluicing: active→active is structurally identical.

theorem Minimalism.Sluicing.v_lexical_in_argdomain : isInArgumentDomain Cat.V Cat.C = true

V is within the argument domain of a CP (F0 ≤ F1).

theorem Minimalism.Sluicing.v_functional_in_argdomain : isInArgumentDomain Cat.v Cat.C = true

v is within the argument domain of a CP (F1 ≤ F1).

theorem Minimalism.Sluicing.small_clause_argdomain_is_self : argumentDomainCat Cat.V = Cat.V

For a small clause (top = V), the argument domain is V itself. Only F0 heads are in the argument domain.

theorem Minimalism.Sluicing.small_clause_excludes_v : isInArgumentDomain Cat.v Cat.V = false

In a small clause, v is NOT in the argument domain (since the top is V at F0, and v is F1).

theorem Minimalism.Sluicing.small_clause_smaller_argdomain : (argumentDomainSpine Cat.V fullVerbalEP).length < (argumentDomainSpine Cat.C fullVerbalEP).length

Small clause argument domains are smaller (fewer head pairs to match). This predicts more permissive matching for SC sluicing, because fewer structural correspondences are required.

theorem Minimalism.Sluicing.cat_beq_refl (c : Cat) : (c == c) = true

BEq on Cat is reflexive.

theorem Minimalism.Sluicing.lexicallyIdentical_refl (hp : HeadPair) : lexicallyIdentical hp hp = true

Lexical identity is reflexive for any head pair.

theorem Minimalism.Sluicing.empty_domains_identical : structurallyIdentical [] [] = true

Empty argument domains are trivially structurally identical.

theorem Minimalism.Sluicing.single_pair_matches (hp : HeadPair) : structurallyIdentical [hp] [hp] = true

A single head pair matches itself.

theorem Minimalism.Sluicing.case_mismatch_not_identical : lexicallyIdentical { head := Cat.V, complement := Cat.D, assignedCase := some UD.Case.Dat } { head := Cat.V, complement := Cat.D, assignedCase := some UD.Case.Acc } = false

Case mismatch blocks lexical identity: a V–D pair assigning dative is not lexically identical to one assigning accusative.

theorem Minimalism.Sluicing.case_match_identical : lexicallyIdentical { head := Cat.V, complement := Cat.D, assignedCase := some UD.Case.Dat } { head := Cat.V, complement := Cat.D, assignedCase := some UD.Case.Dat } = true

Case match preserves lexical identity.

theorem Minimalism.Sluicing.no_case_identity : lexicallyIdentical { head := Cat.v, complement := Cat.V } { head := Cat.v, complement := Cat.V } = true

When no case is specified (e.g., v–V), identity depends only on categories.

theorem Minimalism.Sluicing.case_mismatch_blocks_sluicing : structurallyIdentical [{ head := Cat.v, complement := Cat.V }, { head := Cat.V, complement := Cat.D, assignedCase := some UD.Case.Dat }] [{ head := Cat.v, complement := Cat.V }, { head := Cat.V, complement := Cat.D, assignedCase := some UD.Case.Acc }] = false

Case mismatch blocks structural identity even when all other head pairs match. This is the formal basis of the German case-matching data: "wem" (dat) matches "jemandem" (dat), but "wen" (acc) does not.

theorem Minimalism.Sluicing.case_match_licenses_sluicing : structurallyIdentical [{ head := Cat.v, complement := Cat.V }, { head := Cat.V, complement := Cat.D, assignedCase := some UD.Case.Dat }] [{ head := Cat.v, complement := Cat.V }, { head := Cat.V, complement := Cat.D, assignedCase := some UD.Case.Dat }] = true

Same case → structural identity holds → sluicing licensed.

structure Minimalism.Sluicing.EGivenness (Prop' : Type) : Type

e-GIVENness: the semantic identity condition for ellipsis. The antecedent entails the F-closure of the ellipsis site and vice versa. F-closure existentially binds all F-marked (focused) material.

• antecedent : Prop'

  The antecedent proposition

• ellipsisSite : Prop'

  The ellipsis site proposition

• fClosure : Prop' → Prop'

  F-closure: existentially bind all F-marked material

• entails : Prop' → Prop' → Prop

  Entailment relation

• forward : self.entails self.antecedent (self.fClosure self.ellipsisSite)

  Forward: antecedent entails F-closure of ellipsis site

• backward : self.entails self.ellipsisSite (self.fClosure self.antecedent)

  Backward: ellipsis site entails F-closure of antecedent

structure Minimalism.Sluicing.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).

def Minimalism.Sluicing.instReprNominalEllipsisLicense.repr : NominalEllipsisLicense → ℕ → Std.Format

Equations

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

instance Minimalism.Sluicing.instReprNominalEllipsisLicense : Repr NominalEllipsisLicense

Equations

• Minimalism.Sluicing.instReprNominalEllipsisLicense = { reprPrec := Minimalism.Sluicing.instReprNominalEllipsisLicense.repr }

instance Minimalism.Sluicing.instDecidableEqNominalEllipsisLicense : DecidableEq NominalEllipsisLicense

Equations

• Minimalism.Sluicing.instDecidableEqNominalEllipsisLicense = Minimalism.Sluicing.instDecidableEqNominalEllipsisLicense.decEq

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

Equations

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

def Minimalism.Sluicing.instBEqNominalEllipsisLicense.beq : NominalEllipsisLicense → NominalEllipsisLicense → Bool

Equations

• Minimalism.Sluicing.instBEqNominalEllipsisLicense.beq { numHasE := a, argDomainBoundary := a_1 } { numHasE := b, argDomainBoundary := b_1 } = (a == b && a_1 == b_1)
• Minimalism.Sluicing.instBEqNominalEllipsisLicense.beq x✝¹ x✝ = false

instance Minimalism.Sluicing.instBEqNominalEllipsisLicense : BEq NominalEllipsisLicense

Equations

• Minimalism.Sluicing.instBEqNominalEllipsisLicense = { beq := Minimalism.Sluicing.instBEqNominalEllipsisLicense.beq }

def Minimalism.Sluicing.NominalEllipsisLicense.isLicensed (nel : NominalEllipsisLicense) : Bool

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

Equations

• nel.isLicensed = nel.numHasE

structure Minimalism.Sluicing.EllipsisLicense (Prop' : Type) : Type

Full ellipsis license: semantic identity (e-GIVENness) + optional SIC

• optional Num[E].

• VP ellipsis: e-GIVENness only
• Sluicing: e-GIVENness + SIC
• NP-ellipsis: e-GIVENness + Num[E]

• semantic : EGivenness Prop'

  Semantic identity: e-GIVENness (required for all ellipsis)

• syntactic : Option SluicingLicense

  Syntactic identity: SIC (required for sluicing, not for VPE)

• nominal : Option NominalEllipsisLicense

  Nominal licensing: Num[E] (required for NP-ellipsis)

theorem Minimalism.Sluicing.n_lexical_in_nominal_argdomain : isInArgumentDomain Cat.N Cat.D = true

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

theorem Minimalism.Sluicing.n_functional_in_nominal_argdomain : isInArgumentDomain Cat.n Cat.D = true

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

theorem Minimalism.Sluicing.num_not_in_nominal_argdomain : isInArgumentDomain Cat.Num Cat.D = false

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

theorem Minimalism.Sluicing.q_not_in_nominal_argdomain : isInArgumentDomain Cat.Q Cat.D = false

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

theorem Minimalism.Sluicing.d_not_in_nominal_argdomain : isInArgumentDomain Cat.D Cat.D = false

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

theorem Minimalism.Sluicing.pseudopartitive_licenses_npe : { numHasE := true }.isLicensed = true

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

theorem Minimalism.Sluicing.qualitative_blocks_npe : { numHasE := false }.isLicensed = false

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