Linear Correspondence Axiom

@cite{chomsky-1995} @cite{kayne-1994}

Formalizes the core of @cite{kayne-1994}'s The Antisymmetry of Syntax: the Linear Correspondence Axiom (LCA), which derives linear (temporal) precedence of terminal elements from asymmetric c-command in the hierarchical structure.

Key definitions

• dominatedTerminals: d(X) — the set of terminals dominated by X (alias for terminalNodes from Core/Basic.lean)
• lcaPrecedesIn: the derived precedence relation on terminals
• SatisfiesLCAIn: the LCA as a well-formedness condition (strict total order)

Main results

• Outer precedes inner (outer_precedes_inner): in [x [y z]] where all three are leaves, x precedes both y and z
• Specifier precedes head and complement (spec_precedes_head_complement): alias for outer_precedes_inner
• Head precedes complement internals (head_precedes_complement): alias for outer_precedes_inner
• No right specifier (no_right_specifier)
• Adjunction is left-adjunction (adjunction_left_only)
• Sister terminals are unordered (sister_terminals_unordered)

def Minimalism.dominatedTerminals : SyntacticObject → List SyntacticObject

d(X): the set of terminals dominated by (or equal to) X. Corresponds to Kayne's d function (p. 16).

Equations

• Minimalism.dominatedTerminals = Minimalism.terminalNodes

theorem Minimalism.dominatedTerminals_leaf (tok : LIToken) : dominatedTerminals (SyntacticObject.leaf tok) = [SyntacticObject.leaf tok]

d(leaf) is the singleton containing the leaf.

theorem Minimalism.dominatedTerminals_node (l r : SyntacticObject) : dominatedTerminals (l.node r) = dominatedTerminals l ++ dominatedTerminals r

d(node l r) is d(l) ++ d(r).

def Minimalism.lcaPrecedesIn (root a b : SyntacticObject) : Prop

Tree-relative LCA precedence. Terminal a precedes terminal b within root iff there exist subterms X, Y of root such that X asymmetrically c-commands Y (within root), a ∈ d(X), and b ∈ d(Y).

Equations

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

structure Minimalism.SatisfiesLCAIn (root : SyntacticObject) : Prop

The LCA holds for a tree root iff lcaPrecedesIn root is a strict total order on its terminal nodes: irreflexive, transitive, and total (every pair of distinct terminals is ordered).

• irrefl (t : SyntacticObject) : t ∈ terminalNodes root → ¬lcaPrecedesIn root t t

  No terminal precedes itself.

• trans (a b c : SyntacticObject) : a ∈ terminalNodes root → b ∈ terminalNodes root → c ∈ terminalNodes root → lcaPrecedesIn root a b → lcaPrecedesIn root b c → lcaPrecedesIn root a c

  Precedence is transitive.

• total (a b : SyntacticObject) : a ∈ terminalNodes root → b ∈ terminalNodes root → a ≠ b → lcaPrecedesIn root a b ∨ lcaPrecedesIn root b a

  Every pair of distinct terminals is ordered.

theorem Minimalism.outer_cCommandsIn_inner_left (x y z : SyntacticObject) (hne : x ≠ y.node z) : cCommandsIn (x.node (y.node z)) x y

In root = node x (node y z), x c-commands y within root. Works for arbitrary SOs, not just leaves.

theorem Minimalism.outer_cCommandsIn_inner_right (x y z : SyntacticObject) (hne : x ≠ y.node z) : cCommandsIn (x.node (y.node z)) x z

In root = node x (node y z), x c-commands z within root. Works for arbitrary SOs, not just leaves.

theorem Minimalism.outer_precedes_inner (x y z : LIToken) (hne_xy : x ≠ y) (hne_xz : x ≠ z) (hne_yz : y ≠ z) : have root := (SyntacticObject.leaf x).node ((SyntacticObject.leaf y).node (SyntacticObject.leaf z)); lcaPrecedesIn root (SyntacticObject.leaf x) (SyntacticObject.leaf y) ∧ lcaPrecedesIn root (SyntacticObject.leaf x) (SyntacticObject.leaf z)

Outer precedes inner under the LCA. For root = node (leaf x) (node (leaf y) (leaf z)) where all three are distinct leaves, x precedes both y and z in lcaPrecedesIn root.

This is Kayne's key result (1994, pp. 35-36): the outer daughter asymmetrically c-commands everything in its sister's projection, so all its terminals precede all terminals of the inner daughters.

Subsumes both "specifier precedes head/complement" and "head precedes complement internals".

theorem Minimalism.spec_precedes_head_complement (spec head compl : LIToken) (hne_sh : spec ≠ head) (hne_sc : spec ≠ compl) (hne_hc : head ≠ compl) : have root := (SyntacticObject.leaf spec).node ((SyntacticObject.leaf head).node (SyntacticObject.leaf compl)); lcaPrecedesIn root (SyntacticObject.leaf spec) (SyntacticObject.leaf head) ∧ lcaPrecedesIn root (SyntacticObject.leaf spec) (SyntacticObject.leaf compl)

Specifier precedes head and complement under the LCA. Alias for outer_precedes_inner with conventional names.

theorem Minimalism.head_precedes_complement (head a b : LIToken) (hne_ha : head ≠ a) (hne_hb : head ≠ b) (hne_ab : a ≠ b) : have root := (SyntacticObject.leaf head).node ((SyntacticObject.leaf a).node (SyntacticObject.leaf b)); lcaPrecedesIn root (SyntacticObject.leaf head) (SyntacticObject.leaf a) ∧ lcaPrecedesIn root (SyntacticObject.leaf head) (SyntacticObject.leaf b)

Head precedes complement internals. Alias for outer_precedes_inner with conventional names.

theorem Minimalism.no_right_specifier (head compl spec : SyntacticObject) (hne_hc_node : head.node compl ≠ spec) : have root := (head.node compl).node spec; cCommandsIn root spec head

Right specifiers are LCA-incompatible. In root = node (node head compl) spec, spec's sister is node head compl, which contains head. So spec c-commands head. But head's sister (within the tree) is compl, which does not contain spec (spec is in the other branch).

The LCA therefore orders spec's terminals BEFORE head's terminals. But the PF string has head before spec (right-specifier position). This contradiction means right specifiers are ruled out: the LCA forces specifiers to the left.

theorem Minimalism.adjunction_left_only (mover target : SyntacticObject) : linearize (mover.node target) = linearize mover ++ linearize target

Head-to-head adjunction must be left-adjunction. When a moving head mover adjoins to a target, the linearization function places mover's material before target's material (left-adjunction). This matches Kayne's result (1994, pp. 22-24).

At the level of the complex head node mover target in isolation, two sister leaves symmetrically c-command each other (the sister- terminal limitation). The ordering emerges from the embedding context. But linearize — which gives the unique LCA-compatible order for well-formed trees — always places left daughters before right daughters, establishing left-adjunction.

theorem Minimalism.sister_terminals_unordered (a b : LIToken) (hne : a ≠ b) : ¬asymCCommandsIn ((SyntacticObject.leaf a).node (SyntacticObject.leaf b)) (SyntacticObject.leaf a) (SyntacticObject.leaf b)

Sister terminals are unordered by the LCA. For root = node (leaf a) (leaf b), leaf a and leaf b are sisters: each c-commands the other (via its sister). So neither asymmetrically c-commands the other, and lcaPrecedesIn does not order them.

This is not a defect but a feature: in well-formed BPS, sister terminals don't arise. Complements are always phrases (nodes), and heads project, so the complement of a head is always node X Y, not a bare leaf.