Anaphor — Hankamer & Sag's deep/surface anaphora theory

[HS76]'s theory of (unbounded) anaphoric processes. The organizing distinction is control (pragmatic/deictic vs syntactic) — the conceptual entry point of H&S's argument — with depth (deep vs surface) as the conclusion. A deep anaphor is interpreted at an underlying/semantic level, can be pragmatically (deictically) controlled, and needs only a coherent semantic referent (definite pronouns, do it, null complement anaphora, pro). A surface anaphor is derived by deletion under identity with a surface antecedent, so it requires a coherent syntactic antecedent (VP-ellipsis, sluicing, gapping, argument ellipsis). Pragmatic controllability is the conceptual cut, not a reliable test on its own: [Lan26], following [Mer01], holds the reliable classic diagnostics to be extraction and agreement — this file models extraction and Landau's EIR test (Syntax/Anaphora/Diagnostic.lean).

Depth is the genus, not an ellipsis classification: ellipsis ⊊ surface anaphora ⊊ anaphora, and the deep values (do so, NCA, pro) are precisely the non-ellipsis anaphors. Ellipsis-specific machinery (deletion domains, [E]-feature, ellipsis-type taxonomy) lives in Syntax/Minimalist/Ellipsis/ and consumes this axis — an EllipsisType is a HasDepth carrier with depth .surface.

This is the unbounded-anaphora axis, orthogonal to (and a sibling of) the binding-theoretic Principle-A/B/C axis (Features.BindingClass / the Bound capability): H&S explicitly set aside bounded anaphora (reflexivization) as a separate, always-syntactic process. A reflexive is a Bound.IsAnaphor; do so is an Anaphor.Depth.deep.

Other H&S diagnostics are not modeled here: the missing-antecedent test (itself judged unreliable by [Lan26]), the coherent-semantic-entity requirement on deep anaphora, and the Backwards Anaphora Constraint.

Main declarations

• Anaphor.Depth — deep/surface (the conclusion).
• Anaphor.Control — pragmatic/syntactic (H&S's organizing distinction).
• Anaphor.Depth.HasInternalStructure / Anaphor.Depth.control — the structural property and the depth→control map; allowsPragmaticControl_iff_… proves the typology's two correlated properties coincide by construction.
• Anaphor.HasDepth — the carrier capability (the depth-axis analogue of Bound).

inductive Anaphor.Depth : Type

Hankamer & Sag's deep/surface classification of (unbounded) anaphoric processes [HS76].

• deep : Depth
• surface : Depth

@[implicit_reducible]

instance Anaphor.instDecidableEqDepth : DecidableEq Depth

Equations

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

def Anaphor.instReprDepth.repr : Depth → Nat → 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✝

@[implicit_reducible]

instance Anaphor.instReprDepth : Repr Depth

Equations

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

inductive Anaphor.Control : Type

How an anaphoric relation is controlled [HS76]: a pragmatic (deictic) anaphor can be controlled by the nonlinguistic context with no linguistic antecedent; a syntactic anaphor requires a coherent linguistic antecedent in surface structure. This is H&S's organizing distinction; depth is the conclusion drawn from it.

• pragmatic : Control
• syntactic : Control

@[implicit_reducible]

instance Anaphor.instDecidableEqControl : DecidableEq Control

Equations

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

@[implicit_reducible]

instance Anaphor.instReprControl : Repr Control

Equations

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

def Anaphor.instReprControl.repr : Control → Nat → Std.Format

Equations

• Anaphor.instReprControl.repr Anaphor.Control.pragmatic prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Anaphor.Control.pragmatic")).group prec✝
• Anaphor.instReprControl.repr Anaphor.Control.syntactic prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Anaphor.Control.syntactic")).group prec✝

def Anaphor.Depth.HasInternalStructure : Depth → Prop

The defining structural property: surface anaphora project syntactically present internal structure (deletion under identity), deep anaphora do not. Every account of the distinction ([HS76], [Mer01], [Lan26]) shares this much; they differ on the level (H&S: surface structure; Merchant/Landau: LF — the difference EIR turns on).

Equations

• Anaphor.Depth.surface.HasInternalStructure = True
• Anaphor.Depth.deep.HasInternalStructure = False

@[implicit_reducible]

instance Anaphor.Depth.instDecidablePredHasInternalStructure : DecidablePred HasInternalStructure

Equations

• Anaphor.Depth.surface.instDecidablePredHasInternalStructure = isTrue trivial
• Anaphor.Depth.deep.instDecidablePredHasInternalStructure = isFalse ⋯

theorem Anaphor.Depth.hasInternalStructure_surface : surface.HasInternalStructure

theorem Anaphor.Depth.not_hasInternalStructure_deep : ¬deep.HasInternalStructure

@[simp]

theorem Anaphor.Depth.hasInternalStructure_iff_surface (d : Depth) : d.HasInternalStructure ↔ d = surface

def Anaphor.Depth.control : Depth → Control

The control type a depth determines [HS76]: deep anaphora allow pragmatic (deictic) control; surface anaphora are syntactically controlled (deletion under identity with a surface antecedent).

Equations

• Anaphor.Depth.deep.control = Anaphor.Control.pragmatic
• Anaphor.Depth.surface.control = Anaphor.Control.syntactic

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

A depth allows pragmatic control iff it is deep — the conceptual cut H&S start from, here a consequence of control, not a separate stipulation.

Equations

• d.AllowsPragmaticControl = (d.control = Anaphor.Control.pragmatic)

@[implicit_reducible]

instance Anaphor.Depth.instDecidablePredAllowsPragmaticControl : DecidablePred AllowsPragmaticControl

Equations

• d.instDecidablePredAllowsPragmaticControl = Anaphor.Depth.instDecidablePredAllowsPragmaticControl._aux_1 d

@[simp]

theorem Anaphor.Depth.allowsPragmaticControl_iff_not_hasInternalStructure (d : Depth) : d.AllowsPragmaticControl ↔ ¬d.HasInternalStructure

The depth typology's two correlated properties coincide by construction: a depth allows pragmatic control iff it lacks internal structure (is deep). This is definitional given the 2-element typology — the empirical content is which anaphors get which depth, tested against data in the consuming study, not this biconditional.

The HasDepth capability

class Anaphor.HasDepth (α : Type u_1) : Type u_1

A carrier whose every element has a Hankamer & Sag Anaphor.Depth — the depth-axis analogue of Bound (the binding-class axis). An ellipsis-type record, a paper's datum struct, or a syntactic object each supplies its own instance.

• depth : α → Depth

  The deep/surface depth of every element.

def Anaphor.HasDepth.IsDeep {α : Type u_1} [HasDepth α] (a : α) : Prop

a is a deep anaphor (no internal structure; pragmatic control).

Equations

• Anaphor.HasDepth.IsDeep a = (Anaphor.HasDepth.depth a = Anaphor.Depth.deep)

def Anaphor.HasDepth.IsSurface {α : Type u_1} [HasDepth α] (a : α) : Prop

a is a surface anaphor (deletion under identity; syntactic control).

Equations

• Anaphor.HasDepth.IsSurface a = (Anaphor.HasDepth.depth a = Anaphor.Depth.surface)

def Anaphor.HasDepth.HasInternalStructure {α : Type u_1} [HasDepth α] (a : α) : Prop

The element's structural property, via its depth.

Equations

• Anaphor.HasDepth.HasInternalStructure a = (Anaphor.HasDepth.depth a).HasInternalStructure

@[implicit_reducible]

instance Anaphor.instDecidableIsDeep {α : Type u_1} [HasDepth α] (a : α) : Decidable (HasDepth.IsDeep a)

Equations

• Anaphor.instDecidableIsDeep a = id inferInstance

@[implicit_reducible]

instance Anaphor.instDecidableIsSurface {α : Type u_1} [HasDepth α] (a : α) : Decidable (HasDepth.IsSurface a)

Equations

• Anaphor.instDecidableIsSurface a = id inferInstance

@[implicit_reducible]

instance Anaphor.instDecidableHasInternalStructure {α : Type u_1} [HasDepth α] (a : α) : Decidable (HasDepth.HasInternalStructure a)

Equations

• Anaphor.instDecidableHasInternalStructure a = id inferInstance

@[simp]

theorem Anaphor.HasDepth.hasInternalStructure_iff_isSurface {α : Type u_1} [HasDepth α] (a : α) : HasInternalStructure a ↔ IsSurface a

IsSurface is exactly having internal structure.