Ellipsis as catena-targeting

[Osb19]'s central thesis: VP ellipsis, gapping, pseudogapping, sluicing, stripping, and fragment answers all elide a catena (connected in the dependency graph) that is not in general a constituent (the projection of any single node). The structural reason is that in a flat DG analysis the verb's projection always includes its subject, so even ordinary VP ellipsis already removes a non-projection set of words.

Main declarations

• EllipsisType — the six English ellipsis types Osborne classifies as catena-targeting.
• gappingTree, gappingElided — the worked Osborne example "Fred eats beans and Jim rice"; consumed by Studies/Osborne2019Ellipsis.lean to bridge to the phenomenon-level gapping taxonomy.
• gapping_elided_is_catena, gapping_elided_not_constituent — the catena-not-constituent divergence for that example.

Implementation notes

• The per-paper trees for the other five ellipsis types and the paper-level aggregate theorems live in the corresponding Studies/ file rather than the substrate, per the project's anchoring rule that single-paper empirical replication does not belong in the framework layer.
• Predicate-shape definitions (isCatena, isConstituent) inherit the substrate-wide Bool convention; statements are ... = true / = false.

Ellipsis type taxonomy

inductive DepGrammar.Ellipsis.EllipsisType : Type

Ellipsis types in English ([Osb19], Ch. 12–13).

• vpEllipsis : EllipsisType
• gapping : EllipsisType
• pseudogapping : EllipsisType
• stripping : EllipsisType
• sluicing : EllipsisType
• fragmentAnswer : EllipsisType

def DepGrammar.Ellipsis.instReprEllipsisType.repr : EllipsisType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance DepGrammar.Ellipsis.instReprEllipsisType : Repr EllipsisType

Equations

• DepGrammar.Ellipsis.instReprEllipsisType = { reprPrec := DepGrammar.Ellipsis.instReprEllipsisType.repr }

@[implicit_reducible]

instance DepGrammar.Ellipsis.instDecidableEqEllipsisType : DecidableEq EllipsisType

Equations

• DepGrammar.Ellipsis.instDecidableEqEllipsisType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

Worked example: gapping

def DepGrammar.Ellipsis.gappingTree : DepTree

DG tree for the pre-ellipsis second clause of "Fred eats beans and Jim eats rice": eats(0) heads Jim(1) (nsubj) and rice(2) (obj).

Equations

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

def DepGrammar.Ellipsis.gappingElided : List ℕ

Gapping elides the verb alone: {eats} = {0}.

Equations

• DepGrammar.Ellipsis.gappingElided = [0]

theorem DepGrammar.Ellipsis.gapping_elided_is_catena : Catena.isCatena gappingTree.deps gappingElided = true

The elided material in gapping is a catena (a singleton is trivially connected).

theorem DepGrammar.Ellipsis.gapping_elided_not_constituent : Catena.isConstituent gappingTree.deps 3 gappingElided = false

The elided material in gapping is not a constituent: the verb's projection also contains its subject and object.