Deep and surface anaphora

[HS76] divide anaphoric processes into two kinds. A surface anaphor is derived by deletion under identity with a linguistic antecedent, so its site keeps the syntactic structure of the elided phrase: VP-ellipsis, sluicing, NP-ellipsis and argument ellipsis are surface anaphora. A deep anaphor is a pro-form with no internal structure, interpreted as a pronoun is: null complement anaphora, pro, empty nouns and do it are deep. This file defines the classification, its defining property, and the conditions a model of null anaphora must meet to realize it: a surface site leaves some syntactic position unpronounced, and a deep site leaves none. The classification is of anaphoric processes, not nominals, and is independent of the binding classes of Binding.BindingClass.

Main definitions

• Anaphor.Depth: the depth of an anaphoric process, deep or surface.
• Anaphor.Depth.HasInternalStructure: the site of the anaphor contains syntactic structure, which holds of surface anaphora and of no others.
• Anaphor.DepthModel: a model of null sites that realizes the classification, assigning each site a depth and the positions it leaves unpronounced.

Main results

• Anaphor.DepthModel.depth_eq_surface_iff: in any model, a site is surface exactly when it leaves some position unpronounced.
• Anaphor.DepthModel.depth_eq_surface_of_silences: a dependency that ends inside a site finds a surface anaphor there.

Implementation notes

The classification is defined by internal structure alone, and a framework realizes it by giving a DepthModel: [E]-deletion in Syntax/Minimalist/Ellipsis.lean is one model, and a framework with another source of unpronounced structure, or with none, supplies its own. The other properties Hankamer and Sag associated with depth, such as pragmatic control and the missing-antecedent phenomenon, are tests for that structure, and a test is stated with the data of the study that applies it. [Mer13a] keeps extraction, agreement and inverse scope as diagnostics of ellipsis and sets pragmatic control aside, since an ellipsis can be pragmatically controlled under limited conditions; [Lan26] adds a test that decides depth where extraction and agreement cannot, and Studies/Landau2026.lean shows when a test decides depth.

References

• [HS76]
• [Mer13a]
• [Lan26]

inductive Anaphor.Depth : Type

The depth of an anaphoric process [HS76]. A surface anaphor is derived by deletion under identity and keeps the structure of the elided phrase; a deep anaphor is a pro-form without internal structure.

• deep : Depth
• surface : Depth

@[instance_reducible]

instance Anaphor.instDecidableEqDepth : DecidableEq Depth

Equations

• Anaphor.instDecidableEqDepth x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Anaphor.instReprDepth : Repr Depth

Equations

• Anaphor.instReprDepth = { reprPrec := Anaphor.instReprDepth.repr }

def Anaphor.instReprDepth.repr : Depth → ℕ → Std.Format

Equations

• Anaphor.instReprDepth.repr Anaphor.Depth.deep prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Anaphor.Depth.deep")).group prec✝
• Anaphor.instReprDepth.repr Anaphor.Depth.surface prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Anaphor.Depth.surface")).group prec✝

@[instance_reducible]

instance Anaphor.instFintypeDepth : Fintype Depth

Equations

• Anaphor.instFintypeDepth = { elems := { val := ↑Anaphor.Depth.enumList, nodup := Anaphor.Depth.enumList_nodup }, complete := Anaphor.instFintypeDepth._proof_1 }

def Anaphor.Depth.HasInternalStructure (d : Depth) : Prop

The site of an anaphor has internal structure when the anaphor is surface: deletion leaves the structure of the elided phrase in place, and a deep anaphor has none.

Equations

• d.HasInternalStructure = (d = Anaphor.Depth.surface)

@[instance_reducible]

instance Anaphor.Depth.instDecidablePredHasInternalStructure : DecidablePred HasInternalStructure

Equations

• x✝.instDecidablePredHasInternalStructure = Anaphor.Depth.instDecidablePredHasInternalStructure._aux_1 x✝

class Anaphor.DepthModel (S : Type u_1) (P : outParam (Type u_2)) : Type (max u_1 u_2)

A model of anaphoric depth: null sites S, each assigned a depth, and the syntactic positions P a site leaves unpronounced. The two conditions are Hankamer and Sag's: a surface anaphor contains unpronounced structure, and a deep anaphor contains none.

• depth : S → Depth

  The depth the model assigns to a null site.

• Silences : S → P → Prop

  Silences s p: the position p lies inside the site s and is not pronounced.

• exists_silences_of_surface (s : S) : depth s = Depth.surface → ∃ (p : P), Silences s p

  A surface anaphor leaves some position unpronounced.

• not_silences_of_deep (s : S) (p : P) : depth s = Depth.deep → ¬Silences s p

  A deep anaphor leaves no position unpronounced.

theorem Anaphor.DepthModel.depth_eq_surface_of_silences {S : Type u_1} {P : Type u_2} [DepthModel S P] {s : S} {p : P} (h : Silences s p) : depth s = Depth.surface

theorem Anaphor.DepthModel.depth_eq_surface_iff {S : Type u_1} {P : Type u_2} [DepthModel S P] {s : S} : depth s = Depth.surface ↔ ∃ (p : P), Silences s p

theorem Anaphor.DepthModel.depth_eq_deep_iff {S : Type u_1} {P : Type u_2} [DepthModel S P] {s : S} : depth s = Depth.deep ↔ ∀ (p : P), ¬Silences s p

theorem Anaphor.DepthModel.hasInternalStructure_depth_iff {S : Type u_1} {P : Type u_2} [DepthModel S P] {s : S} : (depth s).HasInternalStructure ↔ ∃ (p : P), Silences s p