@cite{anand-hardt-mccloskey-2025} — The Domain of Formal Matching in Sluicing

@cite{anand-hardt-mccloskey-2025}

Anand, Hardt & McCloskey (2025) extend @cite{rudin-2019}'s proposal that syntactic isomorphism in sluicing applies only to the argument domain (the most inclusive ⟨e,t⟩ projection in the EP), not the entire elided clause.

Core Contributions

1. Small clause antecedents (§2): perception verbs, causatives (have), adjectival SCs, absolute with — the antecedent can be just a small clause.
2. Revised argument domain definition (Def 4): cross-categorial — covers verbal vP, nominal nP, adjectival A, and adpositional P uniformly.
3. Revised Syntactic Isomorphism Condition (Def 6): isomorphism required only over heads within the argument domain, via head pair correspondence.
4. Stranded prepositions (§4): nonargument PPs are outside the argument domain → Chung's Generalization follows without stipulation.
5. Copular pseudosluices (§5): nominal antecedents with implicit copular elided clauses — predicted, not anomalous.

Key Theoretical Claims

• The argument domain is the most inclusive projection denoting ⟨e,t⟩ in the extended projection (Def 4). For full clauses this is vP; for small clauses it is the SC itself.
• The SIC requires structural identity only within argument domains (Def 6). Material outside the argument domain (T, Mod, C, nonargument PPs) may differ freely between antecedent and ellipsis site.
• This resolves the paradox of strict argument structure matching coexisting with rampant tense/modality/polarity mismatches.

inductive AnandHardtMcCloskey2025.SCAntecedentType : Type

Antecedent types that license small clause sluicing.

@cite{anand-hardt-mccloskey-2025} §2: the antecedent need not be a full clause — a small clause suffices. The embedding predicate (perception verb, causative, with) and its external argument are NOT part of the argument domain.

• perceptionVerb : SCAntecedentType
• causativeHave : SCAntecedentType
• causativeMake : SCAntecedentType
• adjectivalConsider : SCAntecedentType
• absoluteWith : SCAntecedentType

@[implicit_reducible]

instance AnandHardtMcCloskey2025.instDecidableEqSCAntecedentType : DecidableEq SCAntecedentType

Equations

• AnandHardtMcCloskey2025.instDecidableEqSCAntecedentType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance AnandHardtMcCloskey2025.instReprSCAntecedentType : Repr SCAntecedentType

Equations

• AnandHardtMcCloskey2025.instReprSCAntecedentType = { reprPrec := AnandHardtMcCloskey2025.instReprSCAntecedentType.repr }

def AnandHardtMcCloskey2025.instReprSCAntecedentType.repr : SCAntecedentType → ℕ → Std.Format

Equations

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

def AnandHardtMcCloskey2025.SCAntecedentType.toSCPred : SCAntecedentType → Minimalist.SCPredCategory

Map SC antecedent types to their predicate category. Perception verb and causative complements are V-headed SCs; adjectival complements are A-headed; absolute with selects a P-headed SC (e.g., "the campaign on hold" — predicate on hold is a PP headed by the preposition on).

Equations

• AnandHardtMcCloskey2025.SCAntecedentType.perceptionVerb.toSCPred = Minimalist.SCPredCategory.V
• AnandHardtMcCloskey2025.SCAntecedentType.causativeHave.toSCPred = Minimalist.SCPredCategory.V
• AnandHardtMcCloskey2025.SCAntecedentType.causativeMake.toSCPred = Minimalist.SCPredCategory.V
• AnandHardtMcCloskey2025.SCAntecedentType.adjectivalConsider.toSCPred = Minimalist.SCPredCategory.A
• AnandHardtMcCloskey2025.SCAntecedentType.absoluteWith.toSCPred = Minimalist.SCPredCategory.P

structure AnandHardtMcCloskey2025.SCSluicingDatum : Type

Small clause sluicing example from the paper.

• sentence : String
• antecedent : String
• scAntecedent : String
• whPhrase : String
• elided : String
• antecedentType : SCAntecedentType
• grammatical : Bool
• corpusId : Option ℕ

def AnandHardtMcCloskey2025.instReprSCSluicingDatum.repr : SCSluicingDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance AnandHardtMcCloskey2025.instReprSCSluicingDatum : Repr SCSluicingDatum

Equations

• AnandHardtMcCloskey2025.instReprSCSluicingDatum = { reprPrec := AnandHardtMcCloskey2025.instReprSCSluicingDatum.repr }

def AnandHardtMcCloskey2025.perceptionSluice1a : SCSluicingDatum

Equations

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

def AnandHardtMcCloskey2025.perceptionSluice1b : SCSluicingDatum

Equations

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

def AnandHardtMcCloskey2025.causativeHaveSluice : SCSluicingDatum

Equations

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

def AnandHardtMcCloskey2025.absoluteWithSluice : SCSluicingDatum

Equations

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

theorem AnandHardtMcCloskey2025.argdomain_uniformity : Minimalist.argumentDomainCat Minimalist.Cat.C = Minimalist.Cat.v ∧ Minimalist.argumentDomainCat Minimalist.Cat.D = Minimalist.Cat.n ∧ Minimalist.argumentDomainCat Minimalist.Cat.V = Minimalist.Cat.V ∧ Minimalist.argumentDomainCat Minimalist.Cat.A = Minimalist.Cat.A ∧ Minimalist.argumentDomainCat Minimalist.Cat.P = Minimalist.Cat.P ∧ Minimalist.argumentDomainCat Minimalist.Cat.N = Minimalist.Cat.N

The argument domain is cross-categorial: the same definition (Def 4) applies uniformly to verbal, nominal, adjectival, and adpositional EPs. For full clauses/DPs, the boundary is at the first functional head (v/n); for SCs, the boundary is the lexical head itself.

theorem AnandHardtMcCloskey2025.sc_strictly_smaller_than_clause : Minimalist.fValue (Minimalist.argumentDomainCat Minimalist.Cat.V) < Minimalist.fValue (Minimalist.argumentDomainCat Minimalist.Cat.C) ∧ Minimalist.fValue (Minimalist.argumentDomainCat Minimalist.Cat.A) < Minimalist.fValue (Minimalist.argumentDomainCat Minimalist.Cat.C) ∧ Minimalist.fValue (Minimalist.argumentDomainCat Minimalist.Cat.P) < Minimalist.fValue (Minimalist.argumentDomainCat Minimalist.Cat.C) ∧ Minimalist.fValue (Minimalist.argumentDomainCat Minimalist.Cat.N) < Minimalist.fValue (Minimalist.argumentDomainCat Minimalist.Cat.C)

SC argument domains are strictly smaller than full clause argument domains: at F0 vs F1. This means the SIC imposes fewer constraints on SC sluicing — only the lexical head pair must match.

theorem AnandHardtMcCloskey2025.outside_argdomain_free : Minimalist.isInArgumentDomain Minimalist.Cat.T Minimalist.Cat.C = false ∧ Minimalist.isInArgumentDomain Minimalist.Cat.Mod Minimalist.Cat.C = false ∧ Minimalist.isInArgumentDomain Minimalist.Cat.Neg Minimalist.Cat.C = false ∧ Minimalist.isInArgumentDomain Minimalist.Cat.C Minimalist.Cat.C = false ∧ Minimalist.isInArgumentDomain Minimalist.Cat.Fin Minimalist.Cat.C = false

Everything outside the argument domain — T, Mod, C, and their interpretive properties (tense, modality, polarity, force) — may differ freely between antecedent and ellipsis site. The SIC is agnostic to these categories.

theorem AnandHardtMcCloskey2025.voice_mismatch_blocked : ¬Minimalist.Ellipsis.FormalMatching.structurallyIdentical Minimalist.Ellipsis.FormalMatching.passiveVP Minimalist.Ellipsis.FormalMatching.activeVP

Paper ex. (10)–(11): voice mismatches are blocked by the SIC. v[nonThematic] (unaccusative/passive) ≠ v[agentive] (transitive), and both are within the argument domain.

Ex. (10): "*All the rules around here have changed, but I just can't work out who." — unaccusative antecedent, transitive ellipsis.

Ex. (11a): "*It's important to establish when he was robbed and, more important, who." — passive antecedent, active ellipsis.

Both reduce to the same structural mismatch: v[nonThematic] vs v[agentive] within the argument domain.

def AnandHardtMcCloskey2025.strandedPrepEx13a : Phenomena.Ellipsis.Sluicing.SluicingDatum

Paper ex. (13a): stranded nonargument preposition with no antecedent source.

"The board believes that a 'one-size-fits-all' approach to financial market regulation is inappropriate. ... what form [government regulation is necessary IN]."

The stranded in marks a nonargument PP — merged above vP, outside the argument domain. The SIC does not require it to match.

Equations

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

def AnandHardtMcCloskey2025.strandedPrepEx13b : Phenomena.Ellipsis.Sluicing.SluicingDatum

Paper ex. (13b): stranded nonargument PP on with no antecedent source.

"When the officer asked me about her, I remembered meeting her but I couldn't say what date [I MET her ON]."

Equations

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

theorem AnandHardtMcCloskey2025.stranded_nonadjunct_pp_licensed : have antecedentPairs := [{ head := Minimalist.Cat.v, complement := Minimalist.Cat.V, voiceFlavor := some Minimalist.VoiceFlavor.agentive }, { head := Minimalist.Cat.V, complement := Minimalist.Cat.D }]; have ellipsisPairs := [{ head := Minimalist.Cat.v, complement := Minimalist.Cat.V, voiceFlavor := some Minimalist.VoiceFlavor.agentive }, { head := Minimalist.Cat.V, complement := Minimalist.Cat.D }, { head := Minimalist.Cat.P, complement := Minimalist.Cat.D, isArgumentPP := some false }]; Minimalist.Ellipsis.FormalMatching.structurallyIdentical (Minimalist.Ellipsis.FormalMatching.filterArgumentPairs antecedentPairs) (Minimalist.Ellipsis.FormalMatching.filterArgumentPairs ellipsisPairs)

The SIC correctly licenses sluicing with stranded nonargument PPs: filtering removes the nonargument PP from the SIC check, and the remaining argument-domain head pairs match.

def AnandHardtMcCloskey2025.argumentPPEx12c : Phenomena.Ellipsis.Sluicing.SluicingDatum

Paper ex. (12): The argument/nonargument PP contrast.

(12a) "They're furious but it's unclear who(m)" — OK (sprouted PP at who(m) not fully contained in ellipsis site after movement) (12b) "They're furious but it's unclear who at" — OK (pied-piped) (12c) "*They're furious but it's unclear who" — blocked: at is within the argument domain (selected by furious), has no antecedent source, and fails the SIC.

This is the key contrast: (12a-b) work because the PP at whom is either not fully within the ellipsis site (12a) or is matched by pied-piping (12b). (12c) fails because the argument-marking preposition at is inside the argument domain and must match.

Equations

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

theorem AnandHardtMcCloskey2025.argument_pp_blocks_sluicing : have antecedentPairs := [{ head := Minimalist.Cat.A, complement := Minimalist.Cat.D }]; have ellipsisPairs := [{ head := Minimalist.Cat.A, complement := Minimalist.Cat.D }, { head := Minimalist.Cat.P, complement := Minimalist.Cat.D, isArgumentPP := some true }]; Minimalist.Ellipsis.FormalMatching.filterArgumentPairs ellipsisPairs = ellipsisPairs ∧ ¬Minimalist.Ellipsis.FormalMatching.structurallyIdentical (Minimalist.Ellipsis.FormalMatching.filterArgumentPairs antecedentPairs) (Minimalist.Ellipsis.FormalMatching.filterArgumentPairs ellipsisPairs)

Argument PP at (selected by furious) is within the argument domain and must match. Since it has no counterpart in the antecedent's argument domain, the SIC blocks (12c).

def AnandHardtMcCloskey2025.failedSluiceEx15a : Phenomena.Ellipsis.Sluicing.SluicingDatum

Contrast: paper ex. (15a-b) — sluicing fails completely when the argument domain itself has no match.

"*He is very loyal, but I don't know who." — no vP in antecedent whose argument domain matches "who [he is loyal to]".

Equations

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

structure AnandHardtMcCloskey2025.CopularPseudosluice : Type

A copular pseudosluice: the antecedent is a nominal, and the elided clause is a copular clause whose argument domain is a small clause.

@cite{anand-hardt-mccloskey-2025} §5: These are NOT anomalous. The antecedent nominal provides the SC subject; the elided clause is [TP T be [SC subject predicate]], whose argument domain is just the SC. The SC in the antecedent context (the bare nominal) matches the SC argument domain of the elided clause.

• sentence : String
• nominalAntecedent : String
• whRemnant : String
• impliedCopularClause : String
• grammatical : Bool
• corpusId : Option ℕ

@[implicit_reducible]

instance AnandHardtMcCloskey2025.instReprCopularPseudosluice : Repr CopularPseudosluice

Equations

• AnandHardtMcCloskey2025.instReprCopularPseudosluice = { reprPrec := AnandHardtMcCloskey2025.instReprCopularPseudosluice.repr }

def AnandHardtMcCloskey2025.instReprCopularPseudosluice.repr : CopularPseudosluice → ℕ → Std.Format

Equations

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

def AnandHardtMcCloskey2025.copularEx18a : CopularPseudosluice

Equations

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

def AnandHardtMcCloskey2025.copularEx18b : CopularPseudosluice

Equations

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

def AnandHardtMcCloskey2025.copularEx19a : CopularPseudosluice

Equations

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

theorem AnandHardtMcCloskey2025.copular_pseudosluice_argdomain : Minimalist.argumentDomainCat Minimalist.Cat.N = Minimalist.Cat.N

The argument domain of a copular pseudosluice is an N-headed SC. be selects an SC complement; the SC predicate is nominal (N). This is smaller than a full clause's argument domain.

theorem AnandHardtMcCloskey2025.pseudosluice_copula_is_be : Minimalist.copulaVI Minimalist.voiceMiddle = Minimalist.CopulaForm.be

The copula in a pseudosluice spells out as BE (not HAVE): the implicit clause has expletive/middle Voice (no external argument introducing transitive Voice), triggering the elsewhere VI rule. This connects to @cite{myler-2016}'s copula theory.

theorem AnandHardtMcCloskey2025.copular_pseudosluice_sic : have scPairs := [{ head := Minimalist.Cat.N, complement := Minimalist.Cat.D }]; Minimalist.Ellipsis.FormalMatching.structurallyIdentical scPairs scPairs

Copular pseudosluice SIC: the argument domain of the implicit copular clause is an N-headed SC. The SIC requires only that the head pair ⟨N, D⟩ matches between the elided SC and the antecedent nominal. A nominal antecedent trivially provides this.

theorem AnandHardtMcCloskey2025.sic_checks_heads_not_nodes : Minimalist.Ellipsis.FormalMatching.structurallyIdentical [{ head := Minimalist.Cat.N, complement := Minimalist.Cat.D }] [{ head := Minimalist.Cat.N, complement := Minimalist.Cat.D }]

@cite{matushansky-2019} argues that small clauses lack a functional Pred head — the subject occupies the specifier of the predicate itself. The paper provides an indirect argument from ellipsis: if PredP existed, the SC node would be inside the argument domain, requiring a match in the antecedent. Since copular pseudosluices (18)–(19) are grammatical with nominal antecedents that have no SC node, either PredP does not exist (Matushansky) or the SIC checks only heads, not phrasal nodes.

@cite{anand-hardt-mccloskey-2025} Def 6 resolves this by requiring identity only for heads in ℋ, not for all nodes. The SC node itself is excluded from the matching calculation.

theorem AnandHardtMcCloskey2025.consistent_with_2021_corpus : Minimalist.isInArgumentDomain Minimalist.Cat.v Minimalist.Cat.C = true ∧ AnandHardtMcCloskey2021.MismatchDimension.argumentStructure.corpusCount = 0 ∧ Minimalist.isInArgumentDomain Minimalist.Cat.T Minimalist.Cat.C = false ∧ AnandHardtMcCloskey2021.MismatchDimension.tense.corpusCount > 0 ∧ Minimalist.isInArgumentDomain Minimalist.Cat.Mod Minimalist.Cat.C = false ∧ AnandHardtMcCloskey2021.MismatchDimension.modality.corpusCount > 0

The 2025 SIC revision is consistent with the 2021 corpus findings: every dimension inside the argument domain has 0 corpus attestations of mismatches; every dimension outside has nonzero attestations. This imports and extends the bridge theorems from @cite{anand-hardt-mccloskey-2021}.

theorem AnandHardtMcCloskey2025.stranded_prep_prediction : have withStrandedPrep := [{ head := Minimalist.Cat.v, complement := Minimalist.Cat.V, voiceFlavor := some Minimalist.VoiceFlavor.agentive }, { head := Minimalist.Cat.V, complement := Minimalist.Cat.D }, { head := Minimalist.Cat.P, complement := Minimalist.Cat.D, isArgumentPP := some false }]; ¬Minimalist.Ellipsis.FormalMatching.structurallyIdentical Minimalist.Ellipsis.FormalMatching.activeVP withStrandedPrep ∧ Minimalist.Ellipsis.FormalMatching.structurallyIdentical (Minimalist.Ellipsis.FormalMatching.filterArgumentPairs Minimalist.Ellipsis.FormalMatching.activeVP) (Minimalist.Ellipsis.FormalMatching.filterArgumentPairs withStrandedPrep)

The 2021 corpus found 17 cases of stranded prepositions with no antecedent source. @cite{anand-hardt-mccloskey-2025} §4 predicts this: nonargument PPs are outside the argument domain (P is at F0 but nonargument PPs merge above vP), so the SIC does not require matching. The prediction: filtering out nonargument PPs from both sides should make the remaining head pairs structurally identical.

def AnandHardtMcCloskey2025.scSluicingData : List SCSluicingDatum

Equations

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

def AnandHardtMcCloskey2025.copularPseudosluiceData : List CopularPseudosluice

Equations

• AnandHardtMcCloskey2025.copularPseudosluiceData = [AnandHardtMcCloskey2025.copularEx18a, AnandHardtMcCloskey2025.copularEx18b, AnandHardtMcCloskey2025.copularEx19a]