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 Phenomena.Ellipsis.Studies.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

instance Phenomena.Ellipsis.Studies.Landau2026.instDecidableEqAnaphorDepth : DecidableEq AnaphorDepth

Equations

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

instance Phenomena.Ellipsis.Studies.Landau2026.instBEqAnaphorDepth : BEq AnaphorDepth

Equations

• Phenomena.Ellipsis.Studies.Landau2026.instBEqAnaphorDepth = { beq := Phenomena.Ellipsis.Studies.Landau2026.instBEqAnaphorDepth.beq }

def Phenomena.Ellipsis.Studies.Landau2026.instBEqAnaphorDepth.beq : AnaphorDepth → AnaphorDepth → Bool

Equations

• Phenomena.Ellipsis.Studies.Landau2026.instBEqAnaphorDepth.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Ellipsis.Studies.Landau2026.instReprAnaphorDepth.repr : AnaphorDepth → Nat → Std.Format

Equations

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

instance Phenomena.Ellipsis.Studies.Landau2026.instReprAnaphorDepth : Repr AnaphorDepth

Equations

• Phenomena.Ellipsis.Studies.Landau2026.instReprAnaphorDepth = { reprPrec := Phenomena.Ellipsis.Studies.Landau2026.instReprAnaphorDepth.repr }

inductive Phenomena.Ellipsis.Studies.Landau2026.NullDomain : Type

Syntactic domain of the null element.

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

instance Phenomena.Ellipsis.Studies.Landau2026.instDecidableEqNullDomain : DecidableEq NullDomain

Equations

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

instance Phenomena.Ellipsis.Studies.Landau2026.instBEqNullDomain : BEq NullDomain

Equations

• Phenomena.Ellipsis.Studies.Landau2026.instBEqNullDomain = { beq := Phenomena.Ellipsis.Studies.Landau2026.instBEqNullDomain.beq }

def Phenomena.Ellipsis.Studies.Landau2026.instBEqNullDomain.beq : NullDomain → NullDomain → Bool

Equations

• Phenomena.Ellipsis.Studies.Landau2026.instBEqNullDomain.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Ellipsis.Studies.Landau2026.instReprNullDomain.repr : NullDomain → Nat → Std.Format

Equations

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

instance Phenomena.Ellipsis.Studies.Landau2026.instReprNullDomain : Repr NullDomain

Equations

• Phenomena.Ellipsis.Studies.Landau2026.instReprNullDomain = { reprPrec := Phenomena.Ellipsis.Studies.Landau2026.instReprNullDomain.repr }

def Phenomena.Ellipsis.Studies.Landau2026.AnaphorDepth.hasStructure : AnaphorDepth → Bool

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

Equations

• Phenomena.Ellipsis.Studies.Landau2026.AnaphorDepth.surface.hasStructure = true
• Phenomena.Ellipsis.Studies.Landau2026.AnaphorDepth.deep.hasStructure = false

def Phenomena.Ellipsis.Studies.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

• Phenomena.Ellipsis.Studies.Landau2026.canContainVariable d = d.hasStructure

def Phenomena.Ellipsis.Studies.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

• Phenomena.Ellipsis.Studies.Landau2026.bvqSatisfied siteHasVariable = siteHasVariable

def Phenomena.Ellipsis.Studies.Landau2026.eirPrediction (d : AnaphorDepth) : Bool

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

Equations

• Phenomena.Ellipsis.Studies.Landau2026.eirPrediction d = Phenomena.Ellipsis.Studies.Landau2026.bvqSatisfied (Phenomena.Ellipsis.Studies.Landau2026.canContainVariable d)

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

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

inductive Phenomena.Ellipsis.Studies.Landau2026.Conclusion : Type

What can be concluded from a diagnostic test result.

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

instance Phenomena.Ellipsis.Studies.Landau2026.instDecidableEqConclusion : DecidableEq Conclusion

Equations

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

def Phenomena.Ellipsis.Studies.Landau2026.instBEqConclusion.beq : Conclusion → Conclusion → Bool

Equations

• Phenomena.Ellipsis.Studies.Landau2026.instBEqConclusion.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Ellipsis.Studies.Landau2026.instBEqConclusion : BEq Conclusion

Equations

• Phenomena.Ellipsis.Studies.Landau2026.instBEqConclusion = { beq := Phenomena.Ellipsis.Studies.Landau2026.instBEqConclusion.beq }

instance Phenomena.Ellipsis.Studies.Landau2026.instReprConclusion : Repr Conclusion

Equations

• Phenomena.Ellipsis.Studies.Landau2026.instReprConclusion = { reprPrec := Phenomena.Ellipsis.Studies.Landau2026.instReprConclusion.repr }

def Phenomena.Ellipsis.Studies.Landau2026.instReprConclusion.repr : Conclusion → Nat → Std.Format

Equations

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

def Phenomena.Ellipsis.Studies.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

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

def Phenomena.Ellipsis.Studies.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

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

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

EIR is never inconclusive.

theorem Phenomena.Ellipsis.Studies.Landau2026.extraction_inconclusive_on_failure : extractionConclusion false = Conclusion.inconclusive

Extraction failure is inherently inconclusive.

theorem Phenomena.Ellipsis.Studies.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 Phenomena.Ellipsis.Studies.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

def Phenomena.Ellipsis.Studies.Landau2026.instReprEIRDatum.repr : EIRDatum → Nat → Std.Format

Equations

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

instance Phenomena.Ellipsis.Studies.Landau2026.instReprEIRDatum : Repr EIRDatum

Equations

• Phenomena.Ellipsis.Studies.Landau2026.instReprEIRDatum = { reprPrec := Phenomena.Ellipsis.Studies.Landau2026.instReprEIRDatum.repr }

def Phenomena.Ellipsis.Studies.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 Phenomena.Ellipsis.Studies.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 Phenomena.Ellipsis.Studies.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 Phenomena.Ellipsis.Studies.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 Phenomena.Ellipsis.Studies.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 Phenomena.Ellipsis.Studies.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 Phenomena.Ellipsis.Studies.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 Phenomena.Ellipsis.Studies.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 Phenomena.Ellipsis.Studies.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 Phenomena.Ellipsis.Studies.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 Phenomena.Ellipsis.Studies.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 Phenomena.Ellipsis.Studies.Landau2026.hebrewData : List EIRDatum

Equations

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

def Phenomena.Ellipsis.Studies.Landau2026.mixedAnaphorData : List EIRDatum

Equations

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

def Phenomena.Ellipsis.Studies.Landau2026.crossLingData : List EIRDatum

Equations

• Phenomena.Ellipsis.Studies.Landau2026.crossLingData = [Phenomena.Ellipsis.Studies.Landau2026.englishVPE] ++ Phenomena.Ellipsis.Studies.Landau2026.mixedAnaphorData

def Phenomena.Ellipsis.Studies.Landau2026.allData : List EIRDatum

Equations

• Phenomena.Ellipsis.Studies.Landau2026.allData = Phenomena.Ellipsis.Studies.Landau2026.hebrewData ++ Phenomena.Ellipsis.Studies.Landau2026.crossLingData

theorem Phenomena.Ellipsis.Studies.Landau2026.en_eir : hebrewEN.eirGrammatical = eirPrediction hebrewEN.depth

theorem Phenomena.Ellipsis.Studies.Landau2026.enp_eir : hebrewENP.eirGrammatical = eirPrediction hebrewENP.depth

theorem Phenomena.Ellipsis.Studies.Landau2026.nca_dp_eir : hebrewNCA_DP.eirGrammatical = eirPrediction hebrewNCA_DP.depth

theorem Phenomena.Ellipsis.Studies.Landau2026.ae_eir : hebrewAE.eirGrammatical = eirPrediction hebrewAE.depth

theorem Phenomena.Ellipsis.Studies.Landau2026.nca_pp_eir : hebrewNCA_PP.eirGrammatical = eirPrediction hebrewNCA_PP.depth

theorem Phenomena.Ellipsis.Studies.Landau2026.ppe_eir : hebrewPPE.eirGrammatical = eirPrediction hebrewPPE.depth

theorem Phenomena.Ellipsis.Studies.Landau2026.vpe_eir : englishVPE.eirGrammatical = eirPrediction englishVPE.depth

theorem Phenomena.Ellipsis.Studies.Landau2026.do_so_eir : englishDoSo.eirGrammatical = eirPrediction englishDoSo.depth

theorem Phenomena.Ellipsis.Studies.Landau2026.dat_doen_eir : dutchDatDoen.eirGrammatical = eirPrediction dutchDatDoen.depth

theorem Phenomena.Ellipsis.Studies.Landau2026.danish_det_eir : danishDet.eirGrammatical = eirPrediction danishDet.depth

theorem Phenomena.Ellipsis.Studies.Landau2026.korean_null_eir : koreanNullObj.eirGrammatical = eirPrediction koreanNullObj.depth

theorem Phenomena.Ellipsis.Studies.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 Phenomena.Ellipsis.Studies.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 Phenomena.Ellipsis.Studies.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 Phenomena.Ellipsis.Studies.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 Phenomena.Ellipsis.Studies.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 Phenomena.Ellipsis.Studies.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 Phenomena.Ellipsis.Studies.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.