Complex LI formation — local primitives #
Inlined from the deleted Theories/Syntax/Minimalist/HeadMovement/Basic.lean
at 0.230.788 when the legacy Movement record was removed. This is the
only file that uses formComplexLI, so the substrate is co-located here.
If a second consumer arises, promote to its own file (most natural home:
Theories/Morphology/ per @cite{senturia-marcolli-2025} §1, where
amalgamation operations live in MCB-aligned terms).
Build a complex LIToken by combining two LIs' feature bundles.
The target's identity (id) is preserved; the mover's features are
appended. Used by both overt head-to-head incorporation and LF
abstract incorporation / cosuperscripting (@cite{baker-1988} GTC).
Equations
Instances For
Complex LI enables reprojection: the outer features project.
Overt head-to-head incorporation alias: complex head exists at PF.
Instances For
Abstract LF incorporation (@cite{baker-1988} GTC): heads share features at LF without a PF reflex.
Instances For
The two named aliases are definitionally equal.
Triadic constructions and Dative Shift — den Dikken's SC-in-SC analysis #
@cite{dendikken-1995} @cite{baker-1988} @cite{larson-1988}
@cite{dendikken-1995} chapters 3-4 extend the SC analysis from particle verb constructions (book ch. 2) to triadic constructions and Dative Shift. The central thesis: ditransitives instantiate a SC-in-SC template with an abstract copular verb BE between the matrix V and a lower SC, and an empty preposition that either remains in situ (prepositional dative frame) or undergoes Predicate Inversion + LF incorporation into BE (double object frame). Possessive HAVE is the suppletive surface result of this BE+TO incorporation (book §3.8).
D-structure template (book p. 132 ex. 52a; p. 271 ex. 4) #
[VP V [SC1 Spec_θ' [VP "BE" [SC2 Spec_θ' [XP X [SC3 NP_Th [PP P NP_Go]]]]]]]
V= matrix triadic verb (e.g. send, give)X= lexical particle if any (e.g. off in send a package off to Bob), empty otherwise (book §3.11 covers the particle-less case as a special case of the same template)SC3's predicate is the dative PP[PP P NP_Go]- Both
Spec_θ'positions are empty θ'-positions
DOC S-structure (book p. 132 ex. 52b) #
[VP V [SC1 Spec_θ' [VP "BE"+[P ∅]j [SC2 [PP_i tj NP_Go] [XP X [SC3 NP_Th t_i]]]]]]
Two operations relate (52a) → (52b):
Predicate Inversion (A-movement): the dative PP raises from the predicate position of SC3 to SpecSC2 (and onward to SpecSC1 per book fn. 20, omitted from the diagram). This is the same Predicate Inversion mechanism applied to applicatives + transitive causatives in book ch. 5.
P-incorporation: the empty head P_∅ incorporates into BE, producing the complex BE+P_∅. Per book §3.10.1, the incorporation appeals to @cite{baker-1988}'s Government Transparency Corollary for Case licensing of the embedded NP — consistent with the broader treatment of incorporation as LF reanalysis throughout the book (cf. ch. 2.4.3 on V-Prt reanalysis as LF, not overt). Same convention as the PVC analysis. UNVERIFIED: specific footnote number not pinned to text.
§3.8: HAVE = BE + incorporated dative P #
Cross-linguistic evidence (Russian U Ivana krasivye glaza "by Ivan pretty eyes" ≈ English Ivan has pretty eyes; French à-construction ↔ avoir construction; Latin mihi est ↔ habeo) supports treating possessive HAVE as the surface result of P-incorporation into an abstract copula. The DOC analysis applies this decomposition: the abstract BE in (52a) becomes BE+P_∅ at S-structure (52b), the syntactic source of HAVE.
§3.10: Motivation for movement #
In the prepositional dative the Theme NP undergoes Case-driven movement to receive Case from V. In the DOC, by contrast, the predicate moves: the empty-headed dative PP raises to SpecSC2, allowing the Theme NP to receive Case in situ via BE+P_∅ (which inherits Case-assigning capability from the incorporated P, per @cite{baker-1988}'s GTC). The Goal NP receives Case via further movement of the empty-headed PP to SpecSC1.
Cross-references #
- Book §3.2 contrasts with @cite{larson-1988}'s VP-shell analysis,
which derives the DOC from the prepositional dative via a
PASSIVE-style operation. den Dikken argues Larson's analysis fails
for triadic VPCs (book §3.2 ex. 4-6) because the particle's
position cannot be accommodated in Larson's flat VP shell.
See
Phenomena/ArgumentStructure/Studies/Larson1988.leanfor the predecessor formalization. - @cite{baker-1988} is the source of the Government Transparency Corollary used to license Case assignment after P-incorporation.
Scope #
This file formalises the structural template (52a)/(52b) for triadic constructions with and without a lexical particle, plus the BE+P decomposition of HAVE (§3.8). The book's full chapter 3-4 treatment also covers: empty dative P licensing across languages (§3.10.2), binding asymmetries from Predicate Inversion (ch. 4.6), Kichaga / German double-object peculiarities (ch. 4.5-4.6), and Romance causativised verbs (ch. 5.3.7). Those remain TODO; encoding them faithfully needs LF-reanalysis substrate that is not yet in linglib (see the SC/particles architectural target memo).
§1. Lexical items #
The abstract copular verb BE. Per book §3.7 / §3.8: an empty verbal head between matrix V and the lower SC, providing the incorporation site for the dative P. Not overtly realised in DOC (because the incorporated complex BE+P_∅ surfaces as the suppletive HAVE / as a null head in DOCs without an overt possessor).
Equations
Instances For
Empty (zero-headed) dative preposition. Per book §3.10.2: licensed in English DOCs by incorporation into BE; in German/Icelandic by overt dative Case morphology (book §3.10.2 ex. 54).
Equations
Instances For
The overt dative preposition to.
Equations
Instances For
The lexical particle position X. Filled by an overt particle in triadic VPCs (e.g. off in send a package off to Bob); empty in plain triadic verbs like give.
Equations
Instances For
The empty θ'-Spec position used in SC1 and SC2 of the template.
Equations
Instances For
§2. Theme and Goal arguments #
Two example pairs: a particle case (send a package off to Bob) and a particle-less case (give the book to Mary).
Equations
Instances For
Equations
Instances For
Equations
Instances For
§3. The triadic D-structure (book ex. 52a) #
For "send a package off to Bob":
The PP predicate of SC3: [PP to Bob].
Equations
Instances For
SC3 in (52a): [SC3 a-package [PP to Bob]] — Theme NP + dative PP.
Equations
- One or more equations did not get rendered due to their size.
Instances For
XP in (52a): [XP off SC3] — particle X with SC3 as complement.
Equations
Instances For
SC2 in (52a): [SC2 Spec_θ' XP].
Equations
- One or more equations did not get rendered due to their size.
Instances For
The lower VP of (52a): [VP BE SC2].
Equations
- One or more equations did not get rendered due to their size.
Instances For
SC1 in (52a): [SC1 Spec_θ' VP_BE].
Equations
- One or more equations did not get rendered due to their size.
Instances For
The triadic D-structure for send a package off to Bob.
Equations
- One or more equations did not get rendered due to their size.
Instances For
§4. The triadic D-structure for plain ditransitives (no particle) #
Per book §3.11, particle-less triadic verbs share the same template
with X = ∅. For "give the book to Mary":
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
The triadic D-structure for give the book to Mary.
Equations
- One or more equations did not get rendered due to their size.
Instances For
§5. The DOC S-structure (book ex. 52b) #
After Predicate Inversion (PP raises to SpecSC2) + LF P-incorporation (empty P incorporates into BE forming BE+P_∅, the source of HAVE).
For send Bob a package off (the DOC counterpart):
The PP [P_∅ Bob] after Predicate Inversion (now at SpecSC2).
Equations
- One or more equations did not get rendered due to their size.
Instances For
BE+P_∅ — the abstract complex head after LF P-incorporation;
the syntactic source of HAVE per book §3.8. Built via
formAbstractIncorporation, the LF-cosuperscripting variant of
head incorporation (consistent with den Dikken's general treatment
of incorporation as LF, see ch. 2.4.3 on V-Prt reanalysis). The
named alias makes the analytical commitment (LF, not PF) explicit
at the use site.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The complex BE+P head as a SyntacticObject (the surface HAVE).
Equations
Instances For
SC3 in (52b): the Theme NP and the trace t_i of the moved PP.
We represent the trace by P_empty alone (head, no complement),
since linglib has no first-class trace primitive.
Equations
- One or more equations did not get rendered due to their size.
Instances For
SC2 in (52b): [SC2 PP_i [XP off SC3]] — PP raised to Spec.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The lower VP in (52b): [VP BE+P_∅ SC2].
Equations
- One or more equations did not get rendered due to their size.
Instances For
SC1 in (52b): [SC1 Spec_θ' VP_HAVE].
Equations
- One or more equations did not get rendered due to their size.
Instances For
The triadic DOC S-structure for send Bob a package off.
Equations
- One or more equations did not get rendered due to their size.
Instances For
§6. The PD S-structure (no movement, no incorporation) #
The prepositional dative S-structure differs from D-structure only by Case-driven movement of the Theme NP (which we abstract over here); the SC-in-SC skeleton is unchanged.
The triadic PD S-structure for send a package off to Bob.
Equations
Instances For
§7. Structural facts #
D-structure for send a package off to Bob has the deep SC-in-SC-in-SC shape predicted by (52a) — 7 levels of right-branching.
The plain give the book to Mary triadic D-structure is structurally isomorphic to the send-off D-structure modulo lexical content (same template).
Note: triadicSStructure_DOC_send := triadicDStructure_send (file local
convention p. 270), so the post-S-structure-stipulation version of
inversion_changes_shape is trivially false. The genuine derivation
via predicateInversion is in §10 below; that gives a different SO
whose shape genuinely differs.
§7b. IsSmallClause witnesses for the SC-in-SC backbone #
Each of the three SCs (SC1, SC2, SC3) in the triadic D-structure
satisfies the IsSmallClause companion predicate (SmallClause.lean).
This is the unifying structural claim — the SC-in-SC architecture is
literally three nested instantiations of the same predicate.
Phase 1.0 substrate caveat: IsSmallClause is noncomputable because it
routes through outerCat/headCat, which are Phase 1.0 placeholders via
Quot.out on the FreeCommMagma carrier. Concrete-instance decide checks
fail at kernel reduction. TODO Phase 2: once LCA-based head selection lands,
restore by decide.
SC3: theme NP + dative PP-predicate (head category P).
SC2: empty θ'-Spec + XP-predicate (head category P, since particle or empty X-head defaults to P/V).
SC1: empty θ'-Spec + VP-predicate headed by abstract BE (head category V).
The post-Predicate-Inversion SC2 (with the raised PP at Spec
and the empty-P trace inside SC3) still satisfies IsSmallClause
— Predicate Inversion is structure-preserving in the SC sense.
§8. HAVE = BE + TO_∅ decomposition (book §3.8) #
The post-incorporation complex is genuinely complex (length > 1).
HAVE retains V as its outer category — the matrix projection is
verbal, with the incorporated P providing the inner feature.
Proved structurally via complex_li_outer_projects rather than
decide, which gets stuck on the proof obligation inside
LexicalItem.combine. The lemma applies regardless of overt-vs-LF
interpretation since both formAbstractIncorporation and
formOvertIncorporation reduce to formComplexLI.
§9. Connection to predecessor analysis (book §3.2) #
Book §3.2 argues that @cite{larson-1988}'s VP-shell analysis fails for triadic verb-particle constructions of the form send a package off to Bob: Larson's flat VP shell cannot accommodate the particle in a position consistent with both the binding asymmetries he derives and the constituency of the post-particle PP. den Dikken's SC-in-SC structure has X as a syntactic head taking SC3 as complement, naturally hosting the particle in this position.
The contrast is between paper analyses; the formalisation of
Larson's predictions lives in Studies/Larson1988.lean. The
contrast is anchored to den Dikken (the chronologically-later,
critiquing paper); per CLAUDE.md the comparison is hosted here.
The structural shape claim is captured by triadicDStructure_send_shape
above (the deep right-branching SC-in-SC pattern with XP as a
distinct constituent layer is what Larson's flat shell lacks).
§10. Predicate Inversion as a tree-rewriting operation #
Up to this point, the D-structure (sc1_send) and DOC S-structure
(sc1_send_post) have been independently stipulated. Book §3.10
crucially relies on Predicate Inversion as the operation that
relates them: the empty-headed dative PP raises from SC3-pred to
SpecSC2, and the empty P incorporates into BE forming HAVE.
Here we make the operation explicit. The DOC derivation starts from
a D-structure variant in which the dative PP already has the empty P
(book §3.10.2 ex. 54: in English, lacking dative Case morphology,
the empty P is licensed only by incorporation, which forces the DOC
derivation; the PD frame has overt to instead).
DOC D-structure variant of sc1_send with the empty dative P
(rather than overt to). This is the input to Predicate Inversion.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
The DOC D-structure (with empty P, before Predicate Inversion).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Predicate Inversion as a partial tree-rewriting operation on the SC1-shape used by triadic D-structures.
Pattern (D-structure):
[SC1 Spec₁ [VP V [SC2 Spec₂ [XP X [SC3 NP [PP P NP_obj]]]]]]
Result (S-structure after PI + P-incorporation):
[SC1 Spec₁ [VP V+P [SC2 [PP P NP_obj] [XP X [SC3 NP P]]]]]
The empty-P trace inside SC3 is represented as P reused in the
SC3 right-child slot — same encoding as sc3_send_post. The
incorporation step (V → V+P) uses formAbstractIncorporation
to honour book §3.10.1's LF-reanalysis attribution.
Returns none on non-matching shapes — the operation is genuinely
partial (Predicate Inversion applies only to certain SC1
configurations), and the Option codomain makes that explicit
so downstream proofs can't pass by accident on inapplicable input.
Phase 1.0 placeholder: predicateInversion is genuinely planar
(the .node spec1 (.node ...) pattern distinguishes left/right
children), so under MCB nonplanar SOs (FreeCommMagma carrier)
the pattern match no longer reduces. Phase 2 will lift through
a head-function-aware planar projection or use an explicit
RotorTree view.
The function body is the sorry: previously this was stubbed
as fun _ => none, which made the downstream _isSome = true
theorems falsifiable. Now sorry lives in the function body
itself, so the function's behaviour is correctly unknown; any
downstream theorem about it must accept that or carry its own
sorry. TODO Phase 2: restore body via head-function projection.
Equations
Instances For
The derivation theorem: applying predicateInversion to the
DOC D-structure yields exactly the (previously stipulated) DOC
S-structure sc1_send_post.
Phase 1.0 sorry: function body itself is sorried; this theorem
cannot be discharged until Phase 2 restores the function.
Predicate Inversion is genuinely applicable to the DOC D-structure. Phase 1.0 sorry: function body itself is sorried.
The PI-derived output is not structurally isomorphic to its input (Predicate Inversion is structure-changing). Phase 1.0 sorry: function body itself is sorried.
IsSmallClause witness for the post-inversion SC1.
Phase 1.0 sorry: blocked on noncomputable IsSmallClause.
The pre-PI DOC D-structure also satisfies IsSmallClause.
Phase 1.0 sorry: blocked on noncomputable IsSmallClause.