Landau 2026: Silent Resumption @cite{landau-2026}

A New Test for Ellipsis. Linguistic Inquiry, Early Access.

The EIR Test

The Ellipsis-Internal Resumption (EIR) test: a novel diagnostic for distinguishing deep from surface anaphora (@cite{hankamer-sag-1976}).

The argumentation chain:

1. BVQ (@cite{chomsky-1982}): at LF, every Ā-operator must bind some variable.
2. A resumptive pronoun inside a null constituent serves as a variable.
3. A resumptive pronoun can only exist inside a constituent with LF-visible internal structure.
4. Therefore: an Ā-operator can bind into a null element iff it is a surface anaphor (= ellipsis).

The EIR test has a distinctive advantage over the extraction test. When extraction fails out of a null element, the result is ambiguous: the element could be a deep anaphor (no structure → BVQ violation), or a surface anaphor where derivational timing bleeds Ā-extraction. When EIR fails, only the deep-anaphor explanation survives, because resumptive dependencies are established at LF without intermediate movement steps that ellipsis could bleed.

Hebrew Results

Three ellipsis types confirmed via EIR in domains where extraction is impossible (Hebrew DPs are absolute islands; P-stranding is barred):

• nP-ellipsis: previously established; EIR provides additional confirmation via EN/ENP contrast
• DP-ellipsis: debated; EIR provides novel argument for AE
• PP-ellipsis: novel; EIR provides first robust evidence for PPE

Cross-Linguistic Mixed Anaphors

EIR diagnoses contested "mixed anaphors" as deep:

• English do so — fails EIR (cf. VP-ellipsis, which passes)
• Dutch dat doen — fails EIR
• Danish det — fails EIR
• Korean null objects — fail EIR (supporting pro over AE)

inductive Landau2026.AnaphorDepth : Type

Anaphoric depth: whether a null element has internal syntactic structure at LF. @cite{hankamer-sag-1976}

• Deep: no LF-visible structure; content recovered pragmatically or deictically. EN, NCA, pro, do so, dat doen, det.
• Surface: full structure, phonologically deleted under identity with a linguistic antecedent. VP-ellipsis, ENP, AE, PPE.

• deep : AnaphorDepth
• surface : AnaphorDepth

@[implicit_reducible]

instance Landau2026.instDecidableEqAnaphorDepth : DecidableEq AnaphorDepth

Equations

• Landau2026.instDecidableEqAnaphorDepth x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Landau2026.instReprAnaphorDepth.repr : AnaphorDepth → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Landau2026.instReprAnaphorDepth : Repr AnaphorDepth

Equations

• Landau2026.instReprAnaphorDepth = { reprPrec := Landau2026.instReprAnaphorDepth.repr }

inductive Landau2026.NullDomain : Type

Syntactic domain of the null element.

• nP : NullDomain
• DP : NullDomain
• PP : NullDomain
• VP : NullDomain

@[implicit_reducible]

instance Landau2026.instDecidableEqNullDomain : DecidableEq NullDomain

Equations

• Landau2026.instDecidableEqNullDomain x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Landau2026.instReprNullDomain.repr : NullDomain → Nat → Std.Format

Equations

• Landau2026.instReprNullDomain.repr Landau2026.NullDomain.nP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Landau2026.NullDomain.nP")).group prec✝
• Landau2026.instReprNullDomain.repr Landau2026.NullDomain.DP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Landau2026.NullDomain.DP")).group prec✝
• Landau2026.instReprNullDomain.repr Landau2026.NullDomain.PP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Landau2026.NullDomain.PP")).group prec✝
• Landau2026.instReprNullDomain.repr Landau2026.NullDomain.VP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Landau2026.NullDomain.VP")).group prec✝

@[implicit_reducible]

instance Landau2026.instReprNullDomain : Repr NullDomain

Equations

• Landau2026.instReprNullDomain = { reprPrec := Landau2026.instReprNullDomain.repr }

def Landau2026.AnaphorDepth.hasStructure : AnaphorDepth → Bool

Step 1: A null element has LF-visible internal structure iff it is a surface anaphor.

Equations

• Landau2026.AnaphorDepth.surface.hasStructure = true
• Landau2026.AnaphorDepth.deep.hasStructure = false

def Landau2026.canContainVariable (d : AnaphorDepth) : Bool

Step 2: A resumptive pronoun (= variable) can only be hosted inside a constituent with internal structure; there must be a syntactic position for it to occupy.

Equations

• Landau2026.canContainVariable d = d.hasStructure

def Landau2026.bvqSatisfied (siteHasVariable : Bool) : Bool

Step 3: BVQ — an Ā-operator binding into a site is well-formed iff the site provides a variable to bind.

Equations

• Landau2026.bvqSatisfied siteHasVariable = siteHasVariable

def Landau2026.eirPrediction (d : AnaphorDepth) : Bool

EIR prediction, derived from the chain: structure → can host resumptive → BVQ satisfied → grammatical.

Equations

• Landau2026.eirPrediction d = Landau2026.bvqSatisfied (Landau2026.canContainVariable d)

theorem Landau2026.eir_iff_structure (d : AnaphorDepth) : eirPrediction d = d.hasStructure

The derivation chain collapses: EIR passes iff the null element has internal structure.

inductive Landau2026.Conclusion : Type

What can be concluded from a diagnostic test result.

• definitelySurface : Conclusion
• definitelyDeep : Conclusion
• inconclusive : Conclusion

@[implicit_reducible]

instance Landau2026.instDecidableEqConclusion : DecidableEq Conclusion

Equations

• Landau2026.instDecidableEqConclusion x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Landau2026.instReprConclusion : Repr Conclusion

Equations

• Landau2026.instReprConclusion = { reprPrec := Landau2026.instReprConclusion.repr }

def Landau2026.instReprConclusion.repr : Conclusion → Nat → Std.Format

Equations

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

def Landau2026.extractionConclusion (success : Bool) : Conclusion

The extraction test. Success is unambiguous (the operator binds a trace inside the overt structure → surface anaphor). Failure is ambiguous: it could mean the element is deep (no structure → BVQ), or that it is surface but derivational timing bleeds Ā-movement through the ellipsis site.

Equations

• Landau2026.extractionConclusion success = if success = true then Landau2026.Conclusion.definitelySurface else Landau2026.Conclusion.inconclusive

def Landau2026.eirConclusion (success : Bool) : Conclusion

The EIR test. Both outcomes are unambiguous. Resumptive dependencies are established purely at LF (binding, not movement), so there is no derivational step for ellipsis timing to bleed. EIR is also insensitive to island constraints, since resumption freely crosses islands.

Equations

• Landau2026.eirConclusion success = if success = true then Landau2026.Conclusion.definitelySurface else Landau2026.Conclusion.definitelyDeep

theorem Landau2026.eir_always_conclusive (b : Bool) : eirConclusion b ≠ Conclusion.inconclusive

EIR is never inconclusive.

theorem Landau2026.extraction_inconclusive_on_failure : extractionConclusion false = Conclusion.inconclusive

Extraction failure is inherently inconclusive.

theorem Landau2026.eir_refines_extraction (b : Bool) : extractionConclusion b = Conclusion.definitelySurface → eirConclusion b = Conclusion.definitelySurface

When extraction succeeds, it agrees with EIR: both conclude surface. This means EIR is a strict refinement — it agrees where extraction is informative, and resolves the cases where extraction is not.

structure Landau2026.EIRDatum : Type

A datum for the Ellipsis-Internal Resumption test.

• language : String
• nullElement : String
• domain : NullDomain
• depth : AnaphorDepth
• eirGrammatical : Bool

  Does the null element pass the EIR test? (= can it host a resumptive pronoun bound by an Ā-operator?)

• extractionAvailable : Bool

  Is extraction from this domain possible in the language? When false, the extraction test is inapplicable and EIR is the only viable syntactic diagnostic.

• abarContext : String
• source : String

@[implicit_reducible]

instance Landau2026.instReprEIRDatum : Repr EIRDatum

Equations

• Landau2026.instReprEIRDatum = { reprPrec := Landau2026.instReprEIRDatum.repr }

def Landau2026.instReprEIRDatum.repr : EIRDatum → Nat → Std.Format

Equations

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

def Landau2026.hebrewEN : EIRDatum

Empty noun (EN): deep anaphor. A bare n head; content recovered from a restricted deictic set (PERSON, THING, TIME, PLACE). No linguistic antecedent required. Fails EIR. NP-ellipsis in Hebrew is previously established; EIR provides additional confirmation.

Equations

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

def Landau2026.hebrewENP : EIRDatum

Elided noun phrase (ENP): surface anaphor. Full nP structure (root + arguments) deleted under identity with a linguistic antecedent; licensed by [E] on Num. Passes EIR: the resumptive pronoun inside the elided nP provides a variable.

Equations

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

def Landau2026.hebrewNCA_DP : EIRDatum

Null complement anaphora (NCA) / pro: deep anaphor. No internal structure; content recovered pragmatically. Fails EIR. The existence of AE in Hebrew was debated; the EIR test provides a novel argument.

Equations

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

def Landau2026.hebrewAE : EIRDatum

Argument ellipsis (AE) / DP-ellipsis: surface anaphor. Full DP structure deleted under identity with a linguistic antecedent. Passes EIR. Novel argument for AE in Hebrew.

Equations

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

def Landau2026.hebrewNCA_PP : EIRDatum

Null PP via NCA: deep anaphor. PP argument omitted; content recovered pragmatically. Fails EIR.

Equations

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

def Landau2026.hebrewPPE : EIRDatum

PP-ellipsis (PPE): surface anaphor. Full PP structure deleted under identity with a linguistic antecedent. Passes EIR. First robust evidence for PP-ellipsis; the paper argues this holds cross-linguistically, not only in Hebrew.

Equations

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

def Landau2026.englishVPE : EIRDatum

English VP-ellipsis: surface anaphor. Left-dislocated constituent binds a resumptive possessive inside the elided VP. Passes EIR. Contrastive baseline for do so.

Equations

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

def Landau2026.englishDoSo : EIRDatum

English do so: deep VP anaphor. Left-dislocation with resumptive binding into do so is ungrammatical. Ā-extraction is also impossible, but that is ambiguous between deep anaphor and derivational bleeding. EIR resolves the ambiguity: do so is deep. @cite{bruening-2019}

Equations

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

def Landau2026.dutchDatDoen : EIRDatum

Dutch dat doen 'do that': deep VP anaphor. Blocks most Ā-extractions. Fails EIR.

Equations

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

def Landau2026.danishDet : EIRDatum

Danish det 'it': deep VP anaphor. Allows A-dependencies but not Ā-dependencies. Fails EIR.

Equations

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

def Landau2026.koreanNullObj : EIRDatum

Korean null objects: deep anaphor (pro). Left-dislocation mandates a resumptive in Korean, but null objects fail to host one — supporting the pro analysis over AE.

Equations

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

def Landau2026.hebrewData : List EIRDatum

Equations

• Landau2026.hebrewData = [Landau2026.hebrewEN, Landau2026.hebrewENP, Landau2026.hebrewNCA_DP, Landau2026.hebrewAE, Landau2026.hebrewNCA_PP, Landau2026.hebrewPPE]

def Landau2026.mixedAnaphorData : List EIRDatum

Equations

• Landau2026.mixedAnaphorData = [Landau2026.englishDoSo, Landau2026.dutchDatDoen, Landau2026.danishDet, Landau2026.koreanNullObj]

def Landau2026.crossLingData : List EIRDatum

Equations

• Landau2026.crossLingData = [Landau2026.englishVPE] ++ Landau2026.mixedAnaphorData

def Landau2026.allData : List EIRDatum

Equations

• Landau2026.allData = Landau2026.hebrewData ++ Landau2026.crossLingData

theorem Landau2026.en_eir : hebrewEN.eirGrammatical = eirPrediction hebrewEN.depth

theorem Landau2026.enp_eir : hebrewENP.eirGrammatical = eirPrediction hebrewENP.depth

theorem Landau2026.nca_dp_eir : hebrewNCA_DP.eirGrammatical = eirPrediction hebrewNCA_DP.depth

theorem Landau2026.ae_eir : hebrewAE.eirGrammatical = eirPrediction hebrewAE.depth

theorem Landau2026.nca_pp_eir : hebrewNCA_PP.eirGrammatical = eirPrediction hebrewNCA_PP.depth

theorem Landau2026.ppe_eir : hebrewPPE.eirGrammatical = eirPrediction hebrewPPE.depth

theorem Landau2026.vpe_eir : englishVPE.eirGrammatical = eirPrediction englishVPE.depth

theorem Landau2026.do_so_eir : englishDoSo.eirGrammatical = eirPrediction englishDoSo.depth

theorem Landau2026.dat_doen_eir : dutchDatDoen.eirGrammatical = eirPrediction dutchDatDoen.depth

theorem Landau2026.danish_det_eir : danishDet.eirGrammatical = eirPrediction danishDet.depth

theorem Landau2026.korean_null_eir : koreanNullObj.eirGrammatical = eirPrediction koreanNullObj.depth

theorem Landau2026.all_eir_consistent : (allData.all fun (d : EIRDatum) => d.eirGrammatical == eirPrediction d.depth) = true

All data are consistent: every datum's observed EIR result matches the prediction from its depth classification.

theorem Landau2026.hebrew_both_depths_all_domains : (hebrewData.any fun (d : EIRDatum) => d.depth == AnaphorDepth.deep && d.domain == NullDomain.nP) = true ∧ (hebrewData.any fun (d : EIRDatum) => d.depth == AnaphorDepth.surface && d.domain == NullDomain.nP) = true ∧ (hebrewData.any fun (d : EIRDatum) => d.depth == AnaphorDepth.deep && d.domain == NullDomain.DP) = true ∧ (hebrewData.any fun (d : EIRDatum) => d.depth == AnaphorDepth.surface && d.domain == NullDomain.DP) = true ∧ (hebrewData.any fun (d : EIRDatum) => d.depth == AnaphorDepth.deep && d.domain == NullDomain.PP) = true ∧ (hebrewData.any fun (d : EIRDatum) => d.depth == AnaphorDepth.surface && d.domain == NullDomain.PP) = true

Hebrew has both deep and surface strategies in all three nominal domains (nP, DP, PP).

theorem Landau2026.hebrew_extraction_unavailable : (hebrewData.all fun (d : EIRDatum) => !d.extractionAvailable) = true

Extraction is unavailable for all Hebrew domains tested. This is precisely why the EIR test is needed: it provides syntactic evidence where the extraction test cannot.

theorem Landau2026.mixed_anaphors_deep : (mixedAnaphorData.all fun (d : EIRDatum) => d.depth == AnaphorDepth.deep) = true

All four cross-linguistic mixed anaphors are diagnosed as deep.

theorem Landau2026.hebrew_has_resumptive_strategy : Fragments.Hebrew.relSheResumptive.npRel = Core.NPRelType.resumptive

Hebrew has a productive resumptive strategy in relativization — the prerequisite for applying the EIR test. The same resumptive pronoun type that Core.NPRelType.resumptive models for relative clauses is what the EIR test probes for inside ellipsis sites.

theorem Landau2026.resumptive_covers_genitive : Fragments.Hebrew.relSheResumptive.covers Core.AHPosition.genitive = true

The resumptive strategy in Hebrew relativization covers the genitive position on the Accessibility Hierarchy, which is where possessive resumptive pronouns (the most common type in the EIR data) sit.

theorem Landau2026.gap_excludes_genitive : Fragments.Hebrew.relSheGap.covers Core.AHPosition.genitive = false

The gap strategy does NOT cover genitive — this is why possessive dependencies in Hebrew require resumption, making the EIR test applicable.