Landau (2026): Silent Resumption: A New Test for Ellipsis

This file formalizes the ellipsis-internal resumption test of [Lan26]. By the ban on vacuous quantification ([Cho82]) an Ā-operator binds into a null site only if the site has structure at LF to host a resumptive variable, so a resumptive dependency into a null site diagnoses a surface anaphor in the sense of [HS76]. A failed extraction has two possible sources, the paper's two reasons for the star: the site is a deep anaphor with no structure to host the dependency, or it is a surface anaphor and ellipsis applied in the derivation bled the dependency. An island around the site blocks extraction for a further reason, independent of ellipsis. Movement is exposed to both of these confounds and agreement to the first; a resumptive dependency is formed at LF and is exposed to neither. A test decides depth when the depth of a site factors through its outcome, and a dependency decides depth exactly when it is exposed to no confound (Dependency.decides_iff), so of the three only resumption does (Dependency.decides_iff_eq_resumption). The paper's Hebrew nominal and prepositional ellipses, whose domains are all islands, and its cross-linguistic mixed anaphors are rows of Data/Examples/Landau2026.json. The resumption judgments are the test's predictions (eir_matches), extraction fails on every Hebrew row (hebrew_extraction_fails), and the judgments alone fix a deep anaphor and an ellipsis in each Hebrew domain (hebrew_domains) and the deep status of the mixed anaphors (mixed_anaphors_deep).

Implementation notes

A site is modelled by its depth and the confounds present at it, and a test by the dependency it forms into the site. The paper does not say whether islands block agreement, and nothing below depends on it: agreement fails to decide depth on the timing confound alone. The rows' texts and judgments agree with the August 2025 preprint of the paper; the example numbers the rows carry run two below the preprint's throughout and have not been checked against the published version. The domain of a null site is the category of its head, Minimalist.Cat.

References

• [Lan26]
• [HS76]
• [Cho82]

Sites and dependencies

inductive Landau2026.Confound : Type

What can block a dependency into a surface site: ellipsis applied in the derivation before the dependency was formed, bleeding it, or an island around the site.

• timing : Confound
• island : Confound

@[instance_reducible]

instance Landau2026.instDecidableEqConfound : DecidableEq Confound

Equations

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

def Landau2026.instReprConfound.repr : Confound → ℕ → Std.Format

Equations

• Landau2026.instReprConfound.repr Landau2026.Confound.timing prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Landau2026.Confound.timing")).group prec✝
• Landau2026.instReprConfound.repr Landau2026.Confound.island prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Landau2026.Confound.island")).group prec✝

@[instance_reducible]

instance Landau2026.instReprConfound : Repr Confound

Equations

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

structure Landau2026.Site : Type

A null site, given by the depth of its anaphor and the confounds present at it.

• depth : Anaphor.Depth

  The depth of the anaphor at the site.

• confounds : Finset Confound

  The confounds present at the site.

inductive Landau2026.Dependency : Type

The dependency a test forms into a null site: extraction moves an operator out of it, agreement probes into it, and the EIR test binds a resumptive pronoun inside it.

• movement : Dependency
• agreement : Dependency
• resumption : Dependency

@[instance_reducible]

instance Landau2026.instDecidableEqDependency : DecidableEq Dependency

Equations

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

@[instance_reducible]

instance Landau2026.instReprDependency : Repr Dependency

Equations

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

def Landau2026.instReprDependency.repr : Dependency → ℕ → Std.Format

Equations

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

def Landau2026.Dependency.exposure : Dependency → Finset Confound

The confounds a dependency is exposed to. Movement is formed in the derivation and is constrained by islands; agreement is formed in the derivation, so ellipsis can bleed it; a resumptive dependency is formed at LF and is indifferent to islands.

Equations

• Landau2026.Dependency.movement.exposure = {Landau2026.Confound.timing, Landau2026.Confound.island}
• Landau2026.Dependency.agreement.exposure = {Landau2026.Confound.timing}
• Landau2026.Dependency.resumption.exposure = ∅

def Landau2026.Site.Hosts (s : Site) (d : Dependency) : Prop

A site hosts a dependency when it has internal structure for the dependency to end in and no confound the dependency is exposed to is present.

Equations

• s.Hosts d = (s.depth.HasInternalStructure ∧ Disjoint d.exposure s.confounds)

@[instance_reducible]

instance Landau2026.instDecidableHosts (s : Site) (d : Dependency) : Decidable (s.Hosts d)

Equations

• Landau2026.instDecidableHosts s d = { decide := decide s.depth.HasInternalStructure && decide (Disjoint d.exposure s.confounds), reflects_decide := ⋯ }

def Landau2026.Dependency.Decides (d : Dependency) : Prop

A test decides depth when the depth of a site is determined by whether the site hosts the test's dependency.

Equations

• d.Decides = Function.FactorsThrough Landau2026.Site.depth fun (x : Landau2026.Site) => x.Hosts d

theorem Landau2026.Site.Hosts.depth_eq_surface {s : Site} {d : Dependency} (h : s.Hosts d) : s.depth = Anaphor.Depth.surface

A site that hosts any dependency is a surface anaphor: the success of a test is always conclusive.

theorem Landau2026.Site.Hosts.mono {s : Site} {d d' : Dependency} (h : s.Hosts d) (hle : d'.exposure ⊆ d.exposure) : s.Hosts d'

A dependency exposed to fewer confounds is hosted wherever one exposed to more is.

theorem Landau2026.Site.Hosts.resumption {s : Site} {d : Dependency} (h : s.Hosts d) : s.Hosts Dependency.resumption

Resumption succeeds wherever any dependency does.

theorem Landau2026.Site.hosts_resumption_iff {s : Site} : s.Hosts Dependency.resumption ↔ s.depth = Anaphor.Depth.surface

theorem Landau2026.Site.depth_eq_of_iff_hosts_resumption {s : Site} {p : Prop} [Decidable p] (h : p ↔ s.Hosts Dependency.resumption) : s.depth = if p then Anaphor.Depth.surface else Anaphor.Depth.deep

Whatever confounds a site contains, the outcome of resumption into it fixes its depth.

theorem Landau2026.Dependency.decides_iff {d : Dependency} : d.Decides ↔ d.exposure = ∅

A dependency decides depth exactly when it is exposed to no confound. Otherwise a deep site and a surface site where a confound blocks the dependency both fail it.

theorem Landau2026.Dependency.decides_iff_eq_resumption {d : Dependency} : d.Decides ↔ d = resumption

Of the three dependencies, only resumption decides depth: a failed extraction or a failed agreement is compatible with a surface site, a failed resumption is not.

theorem Landau2026.exists_hosts_resumption_not_movement : ∃ (s : Site), s.Hosts Dependency.resumption ∧ ¬s.Hosts Dependency.movement

The analysis predicts surface sites where ellipsis bleeds extraction but a resumptive pronoun is hosted; the paper reports no such case yet. The Hebrew rows show the same split with an island in place of timing (hebrew_extraction_fails, eir_matches).

The paper's examples

Every row is a resumptive dependency into a null site, and its judgment is the outcome of the EIR test. The depth of the site, its domain, and whether the domain is an island are read from the row's paper features.

def Landau2026.depths : List (String × Anaphor.Depth)

Equations

• Landau2026.depths = [("deep", Anaphor.Depth.deep), ("surface", Anaphor.Depth.surface)]

def Landau2026.domains : List (String × Minimalist.Cat)

Equations

• Landau2026.domains = [("nP", Minimalist.Cat.n), ("DP", Minimalist.Cat.D), ("PP", Minimalist.Cat.P), ("VP", Minimalist.Cat.V)]

def Landau2026.barriers : List (String × Finset Confound)

The confounds a row's extractionAvailable feature records: a domain out of which extraction is unavailable is an island.

Equations

• Landau2026.barriers = [("true", ∅), ("false", {Landau2026.Confound.island})]

def Landau2026.site? (e : Datum) : Option Site

The site of a row: its recorded depth, and the island confound when extraction out of its domain is unavailable.

Equations

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

def Landau2026.hebrewData : List Datum

Equations

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

def Landau2026.mixedAnaphorData : List Datum

Equations

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

theorem Landau2026.site?_isSome (e : Datum) : e ∈ Examples.all → (site? e).isSome = true

Every row records a depth and whether its domain is an island, so each theorem below speaks about all the rows.

theorem Landau2026.eir_matches (e : Datum) : e ∈ Examples.all → ∀ (s : Site), site? e = some s → (e.judgment = Judgment.acceptable ↔ s.Hosts Dependency.resumption)

The judgments are the predictions of the EIR test: binding a resumptive pronoun inside the null site is acceptable exactly when the site hosts the dependency.

theorem Landau2026.hebrew_extraction_fails (e : Datum) : e ∈ hebrewData → ∀ (s : Site), site? e = some s → ¬s.Hosts Dependency.movement

Every Hebrew domain tested is an island, so extraction fails on every Hebrew row, surface or deep, and cannot diagnose ellipsis there.

theorem Landau2026.hebrew_domains (c : Minimalist.Cat) : c ∈ [Minimalist.Cat.n, Minimalist.Cat.D, Minimalist.Cat.P] → ∀ (δ : Anaphor.Depth), ∃ e ∈ hebrewData, e.parse? "domain" domains = some c ∧ ∀ (s : Site), (e.judgment = Judgment.acceptable ↔ s.Hosts Dependency.resumption) → s.depth = δ

Hebrew has both a deep anaphor and ellipsis in each of the nP, DP and PP domains: for each domain and depth, some row's resumption judgment is accounted for only by a site of that depth.

theorem Landau2026.mixed_anaphors_deep (e : Datum) : e ∈ mixedAnaphorData → ∀ (s : Site), (e.judgment = Judgment.acceptable ↔ s.Hosts Dependency.resumption) → s.depth = Anaphor.Depth.deep

The mixed anaphors do so, dat doen, det and the Korean null object are deep: their resumption is unacceptable, so any site that accounts for the judgment is deep, whatever confounds it contains.