Landau 2026: Silent Resumption [Lan26]

The Ellipsis-Internal Resumption (EIR) test distinguishes deep from surface anaphora ([HS76]). By the Ban on Vacuous Quantification ([Cho82]), an Ā-operator can bind into a null site iff the site has LF-visible structure to host a resumptive variable — iff it is a surface anaphor (ellipsis). EIR improves on the extraction test: resumptive dependencies are fixed at LF, so EIR failure cannot be bled by derivational timing and is unambiguously diagnostic of a deep anaphor.

allData gathers the paper's rows — Hebrew nP/DP/PP ellipsis (where the extraction test is unavailable: DPs are absolute islands and P-stranding is barred) and the cross-linguistic "mixed anaphors" (English do so, Dutch dat doen, Danish det, Korean null objects), all diagnosed deep.

Types

Anaphoric depth (deep/surface, [HS76]) is the framework-neutral substrate primitive Anaphor.Depth; EN/NCA/pro/do so/dat doen/det are .deep, VP-ellipsis/ENP/AE/PPE are .surface.

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 → ℕ → 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 }

BVQ and the EIR prediction

@[reducible, inline]

abbrev Landau2026.PassesEIR (d : Anaphor.Depth) : Prop

EIR prediction. A null site passes the Ellipsis-Internal Resumption test iff it has LF-visible internal structure (Anaphor.Depth.HasInternalStructure) — iff it is a surface anaphor. The paper's argument: by the BVQ ([Cho82]) an Ā-operator must bind a variable at LF; a resumptive pronoun is that variable, and it can only be hosted inside a site with internal structure; so binding into a null site is licensed iff the site is a surface anaphor. The prediction is therefore literally the substrate structural property, not a separate stipulation.

Equations

• Landau2026.PassesEIR d = d.HasInternalStructure

EIR vs the classic tests (extraction, agreement)

All three are Diagnostics over Anaphor.Depth: a pass means the site had structure to host the variable/trace (surface). They differ only in what a failure admits — and that single field is the paper's whole point. Extraction and agreement are the two reliable classic diagnostics ([Lan26], after [Mer01]); EIR is the new third one.

def Landau2026.eir : Diagnostic Bool Anaphor.Depth

The EIR test as a depth diagnostic. A pass is hostsVariable (surface structure hosts the resumptive); a failure can only be a deepAnaphor, because resumptive dependencies are established at LF and cannot be bled by derivational timing, nor blocked by islands.

Equations

• Landau2026.eir = Diagnostic.ofCauses (fun (pass : Bool) => if pass = true then {Anaphor.DepthCause.hostsVariable} else {Anaphor.DepthCause.deepAnaphor}) Anaphor.DepthCause.entails

def Landau2026.extraction : Diagnostic Bool Anaphor.Depth

The extraction test as a depth diagnostic. A pass is hostsVariable (surface); a failure is ambiguous — a deepAnaphor, or a surface site whose Ā-movement was derivationalBleeding (bled by ellipsis timing) or islandBlocking. That extra ambiguity is exactly the gap EIR closes.

Equations

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

@[simp]

theorem Landau2026.eir_consistent_true : eir.consistent true = {Anaphor.Depth.surface}

@[simp]

theorem Landau2026.eir_consistent_false : eir.consistent false = {Anaphor.Depth.deep}

@[simp]

theorem Landau2026.extraction_consistent_true : extraction.consistent true = {Anaphor.Depth.surface}

@[simp]

theorem Landau2026.extraction_consistent_false : extraction.consistent false = {Anaphor.Depth.deep, Anaphor.Depth.surface}

theorem Landau2026.eir_decides : eir.Decides Anaphor.Depth.testOutcome

Headline — Landau's contribution. EIR decides anaphoric depth: on every site the verdict recovers the depth exactly — a pass means surface (ellipsis), a failure means deep. This is what "a new test for ellipsis" amounts to, made precise as Diagnostic.Decides.

theorem Landau2026.extraction_not_decides : ¬extraction.Decides Anaphor.Depth.testOutcome

Extraction does not decide depth: on a deep site its verdict still admits surface (the failure could be a bled or island-blocked extraction), so it is inconclusive exactly where EIR is decisive.

theorem Landau2026.eir_refines_extraction : eir.Refines extraction

EIR strictly refines extraction: identical on a pass, but EIR resolves the failure extraction leaves open (its failure-causes are a subset).

def Landau2026.agreement : Diagnostic Bool Anaphor.Depth

The agreement test as a depth diagnostic. The other reliable classic diagnostic ([Lan26], after [Mer01]). A pass is hostsVariable (surface); a failure is ambiguous between a deepAnaphor and a surface site whose agreement was derivationalBleeding (bled by ellipsis timing). Agreement is not movement, so it has no island confound — but it is still inconclusive on failure. (It is also inapplicable in agreement-less languages, the analogue of extractionAvailable = false.)

Equations

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

@[simp]

theorem Landau2026.agreement_consistent_false : agreement.consistent false = {Anaphor.Depth.deep, Anaphor.Depth.surface}

theorem Landau2026.agreement_not_decides : ¬agreement.Decides Anaphor.Depth.testOutcome

Agreement, like extraction, does not decide depth: its failure also admits a bled-but-surface site. EIR escapes this confound too.

theorem Landau2026.eir_refines_agreement : eir.Refines agreement

EIR refines agreement too — so EIR decides depth where both reliable classic tests are inconclusive, escaping both their derivational-bleeding (and, for extraction, island) confounds. This is Landau's actual headline: EIR matches the confidence of the classic diagnostics while their failure-confounds it lacks.

Data

The empirical rows live in Data/Examples/Landau2026.json (typed LinguisticExamples — the paper's (18a)–(47b) stimuli). The study reads each row's EIR-relevant classification by projection: domain/depth/extraction from paperFeatures, and grammaticality straight off the example's judgment — passing EIR is the resumptive-binding sentence being acceptable.

def Landau2026.domainOf (e : Data.Examples.LinguisticExample) : NullDomain

The null-element domain of an EIR example (from paperFeatures).

Equations

• Landau2026.domainOf e = Landau2026.parseDomain✝ ((List.lookup "domain" e.paperFeatures).getD "nP")

def Landau2026.depthOf (e : Data.Examples.LinguisticExample) : Anaphor.Depth

The Hankamer–Sag Anaphor.Depth of an EIR example (from paperFeatures).

Equations

• Landau2026.depthOf e = Landau2026.parseDepth✝ ((List.lookup "depth" e.paperFeatures).getD "deep")

def Landau2026.eirGrammatical (e : Data.Examples.LinguisticExample) : Bool

Whether the example passes EIR — this is its grammaticality judgment: the resumptive-binding sentence is acceptable iff the site hosts the variable.

Equations

• Landau2026.eirGrammatical e = match e.judgment with | Features.Judgment.acceptable => true | x => false

def Landau2026.extractionAvailable (e : Data.Examples.LinguisticExample) : Bool

Whether the extraction test is applicable to the example's domain (false for the Hebrew nominal domains, which are absolute islands).

Equations

• Landau2026.extractionAvailable e = ((List.lookup "extractionAvailable" e.paperFeatures).getD "true" == "true")

Data collections

EN/NCA/pro/do so/dat doen/det are deep; ENP/AE/PPE/VP-ellipsis surface. Each example's comment in the JSON carries the construction notes.

def Landau2026.hebrewData : List Data.Examples.LinguisticExample

Equations

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

def Landau2026.mixedAnaphorData : List Data.Examples.LinguisticExample

Equations

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

def Landau2026.crossLingData : List Data.Examples.LinguisticExample

Equations

• Landau2026.crossLingData = Landau2026.Examples.englishVPE :: Landau2026.mixedAnaphorData

def Landau2026.allData : List Data.Examples.LinguisticExample

Equations

• Landau2026.allData = Landau2026.Examples.all

Summary properties

Every datum's observed grammaticality (eirGrammatical, off its judgment) matches the PassesEIR prediction read off its depth — the decide p = true ↔ p bridge between a recorded observation and the substrate structural property.

theorem Landau2026.all_eir_consistent (e : Data.Examples.LinguisticExample) : e ∈ allData → (eirGrammatical e = true ↔ PassesEIR (depthOf e))

All data are consistent: every example's EIR grammaticality matches the prediction read off its depth classification.

theorem Landau2026.hebrew_both_depths_all_domains : (∃ e ∈ hebrewData, depthOf e = Anaphor.Depth.deep ∧ domainOf e = NullDomain.nP) ∧ (∃ e ∈ hebrewData, depthOf e = Anaphor.Depth.surface ∧ domainOf e = NullDomain.nP) ∧ (∃ e ∈ hebrewData, depthOf e = Anaphor.Depth.deep ∧ domainOf e = NullDomain.DP) ∧ (∃ e ∈ hebrewData, depthOf e = Anaphor.Depth.surface ∧ domainOf e = NullDomain.DP) ∧ (∃ e ∈ hebrewData, depthOf e = Anaphor.Depth.deep ∧ domainOf e = NullDomain.PP) ∧ ∃ e ∈ hebrewData, depthOf e = Anaphor.Depth.surface ∧ domainOf e = NullDomain.PP

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

theorem Landau2026.hebrew_extraction_unavailable (e : Data.Examples.LinguisticExample) : e ∈ hebrewData → extractionAvailable e = false

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 (e : Data.Examples.LinguisticExample) : e ∈ mixedAnaphorData → depthOf e = Anaphor.Depth.deep

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

Integration with existing infrastructure

theorem Landau2026.hebrew_has_resumptive_strategy : Hebrew.relSheResumptive.npRel = RelativeClause.NPRelType.resumptive

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

theorem Landau2026.hebrew_resumptive_is_base_generated : Hebrew.relSheBoundResumptive.npRel.resumptiveKind = some RelativeClause.ResumptiveKind.bound

The EIR test relies on base-generated resumption. The paper's argument turns on resumptive dependencies being fixed at LF (binding, not movement), so ellipsis timing cannot bleed them — exactly ResumptiveKind.bound. The Sichel-refined Hebrew marker relSheBoundResumptive carries this kind, making the paper's "binding, not movement" mechanism true by construction against the relativization substrate ([Sic14]).

theorem Landau2026.resumptive_covers_genitive : Hebrew.relSheResumptive.Covers RelativeClause.AHPosition.genitive

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

theorem Landau2026.gap_excludes_genitive : ¬Hebrew.relSheGap.Covers RelativeClause.AHPosition.genitive

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