Finite-VP divergence: catena ⊋ constituent

The finite VP (verb + complements, excluding subject) is the textbook demonstration of [Osb19]'s thesis that constituency and connectedness come apart in dependency grammar: in a flat DG analysis, the finite VP is a catena (connected in the dependency graph) but not a constituent (the verb's complete subtree includes the subject). The phrase-structure analysis groups verb and complements under a VP node, so it predicts the opposite.

Five standard constituency tests for the finite VP (Osborne 2019, Ch. 2, ex. 25) — topicalization, clefting, pseudoclefting, do-so substitution, answer fragments — pattern with the DG prediction on four out of five items, the proform-substitution case being the well-known exception. Empirical writeups of those judgments live in paper-anchored Studies files; this module formalizes only the structural DG-side claim.

Main declarations

• billPlaysChess, sheReadsEverything — small DG example trees from Osborne 2019 Ch. 2.
• vp_is_catena_*, vp_not_constituent_* — the divergence theorems for each tree.
• exists_catena_not_constituent — the universal witness (any internal node forms a singleton catena that is not a constituent).

Implementation notes

• Predicate-shape definitions (isCatena, isConstituent) inherit the substrate-wide Bool convention; statements are ... = true / = false.
• No PSTree straw-man: phrase-structure analyses are formalized in the HPSG and Minimalism directories, not re-stipulated here. Genuine DG-vs-PSG rivalry theorems should branch off those formalizations rather than a hand-rolled inductive PSTree.

Example trees from [Osb19]

def DepGrammar.VPDivergence.billPlaysChess : DepTree

DG tree for "Bill plays chess" (Ch. 2, ex. 24): plays(0) heads Bill(1) (nsubj) and chess(2) (obj).

Equations

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

def DepGrammar.VPDivergence.sheReadsEverything : DepTree

DG tree for "She reads everything" (Ch. 2, ex. 12): same shape as "Bill plays chess", confirming the divergence is structural.

Equations

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

The finite-VP divergence

For each tree, the verb-plus-object set {0, 2} is connected in the dependency graph (a catena) but is not the projection of any node (the verb's projection includes the subject).

theorem DepGrammar.VPDivergence.vp_is_catena_billPlaysChess : Catena.isCatena billPlaysChess.deps [0, 2] = true

theorem DepGrammar.VPDivergence.vp_not_constituent_billPlaysChess : Catena.isConstituent billPlaysChess.deps 3 [0, 2] = false

theorem DepGrammar.VPDivergence.vp_is_catena_sheReadsEverything : Catena.isCatena sheReadsEverything.deps [0, 2] = true

theorem DepGrammar.VPDivergence.vp_not_constituent_sheReadsEverything : Catena.isConstituent sheReadsEverything.deps 3 [0, 2] = false

Universal witness

The two-tree examples instantiate a general phenomenon: any internal node forms a singleton catena that fails to be a constituent.

theorem DepGrammar.VPDivergence.exists_catena_not_constituent (deps : List Dependency) (v w : ℕ) (hvw : v ≠ w) (hedge : parentEdge deps v w) : Catena.isCatena deps [v] = true ∧ ¬projection deps v = [v]

For any tree with an edge v → w (v ≠ w), the singleton [v] is a catena but projection deps v ≠ [v] (the projection contains w).