Documentation

structure Minimalism.InternalMerge :

Type

Internal Merge: re-merging an SO already contained in the structure.

This is movement: the mover is extracted from within the target and re-merged at a higher position.

Traditional view: This creates displacement/copies.

target : SyntacticObject
The structure containing the mover
mover : SyntacticObject
The element that moves (already in target)
result : SyntacticObject
The result of merging
distinct : self.target ≠ self.mover
Inputs must be distinct
containment : contains self.target self.mover
THE KEY PRECONDITION: Mover is already contained in target
is_merge : self.result = merge self.mover self.target
The result is formed by merge (mover goes to specifier position)

Instances For

theorem Minimalism.external_internal_same_operation :

(∀ (em : ExternalMerge), em.result = merge em.α em.β) ∧ ∀ (im : InternalMerge), im.result = merge im.mover im.target

THEOREM 1 (Same Operation): Both External and Internal Merge use the same underlying merge function.

The operation itself is identical - only the preconditions differ.

structure Minimalism.GeneralMerge :

Type

A general Merge operation that abstracts over both types

left : SyntacticObject
First input (the one that ends up on the left)
right : SyntacticObject
Second input (the one that ends up on the right)
result : SyntacticObject
The result
distinct : self.left ≠ self.right
Inputs must be distinct
is_merge : self.result = merge self.left self.right
Result is merge of inputs

Instances For

def Minimalism.ExternalMerge.toGeneral (em : ExternalMerge) :

GeneralMerge

External Merge is a special case of General Merge

Equations

em.toGeneral = { left := em.α, right := em.β, result := em.result, distinct := ⋯, is_merge := ⋯ }

Instances For

def Minimalism.InternalMerge.toGeneral (im : InternalMerge) :

GeneralMerge

Internal Merge is a special case of General Merge

Equations

im.toGeneral = { left := im.mover, right := im.target, result := im.result, distinct := ⋯, is_merge := ⋯ }

Instances For

theorem Minimalism.merge_exhaustive (gm : GeneralMerge) :

¬contains gm.left gm.right ∧ ¬contains gm.right gm.left ∨ contains gm.left gm.right ∨ contains gm.right gm.left

THEOREM 2 (Exhaustivity): Every General Merge is either External or Internal (no third kind).

The containment precondition is the ONLY distinguishing feature.

theorem Minimalism.merge_preconditions_partition (α β : SyntacticObject) :

¬contains α β ∧ ¬contains β α ↔ ¬(contains α β ∨ contains β α)

The preconditions are mutually exclusive and exhaustive

theorem Minimalism.label_of_merge_when_selects (α β : SyntacticObject) (h : selects α β) :

label (merge α β) = label α

When α selects β, the label of {α, β} equals the label of α

theorem Minimalism.label_of_merge_when_right_selects (α β : SyntacticObject) (h : selects β α) (hna : ¬selects α β) :

label (merge α β) = label β

When β selects α (and α doesn't select β), the label of {α, β} equals the label of β

theorem Minimalism.mutual_selection_breaks_symmetry (α β : SyntacticObject) (hαβ : selects α β) (hβα : selects β α) (hdistinct : label α ≠ label β) :

label (merge α β) ≠ label (merge β α)

Mutual selection with distinct labels breaks labeling symmetry.

This is the key theorem: if both α and β select each other, and they have different labels, then label (merge α β) ≠ label (merge β α). This violates the set-theoretic nature of Merge, where {α,β} = {β,α}.

theorem Minimalism.no_mutual_preserves_symmetry (α β : SyntacticObject) (h_no_mutual : ¬(selects α β ∧ selects β α)) (h_some : selects α β ∨ selects β α) :

label (merge α β) = label (merge β α)

No mutual selection (with some selection) preserves labeling symmetry.

When at least one element selects the other, but not mutually, labeling is symmetric: label (merge α β) = label (merge β α).

theorem Minimalism.labeling_symmetric_iff (α β : SyntacticObject) (h_some : selects α β ∨ selects β α) :

label (merge α β) = label (merge β α) ↔ ¬(selects α β ∧ selects β α) ∨ label α = label β

MAIN THEOREM: Labeling symmetry characterization.

When at least one element selects the other, labeling is symmetric if and only if there's no mutual selection OR the labels are equal.

This shows NoMutualSelection is NECESSARY (not just empirically observed) for labeling to be well-defined on unordered sets {α, β}.

def Minimalism.NoMutualSelection (α β : SyntacticObject) :

No mutual selection: at most one of α, β can select the other.

Within the Minimalist formalism, this is algebraically required: labeling_symmetric_iff shows that without it (and with distinct labels), label (merge α β) ≠ label (merge β α), violating the set-theoretic nature of Merge where {α, β} = {β, α}.

Equations

Minimalism.NoMutualSelection α β = ¬(Minimalism.selects α β ∧ Minimalism.selects β α)

Instances For

theorem Minimalism.sameLabel_when_selects (α β : SyntacticObject) (h : selects α β) (hne : label α ≠ none) :

sameLabel α (merge α β)

When α selects β, α and {α,β} have the same label

theorem Minimalism.label_leaf_is_some (tok : LIToken) :

label (SyntacticObject.leaf tok) = some tok.item

Helper: label of a leaf is always some

theorem Minimalism.label_leaf_ne_none (tok : LIToken) :

label (SyntacticObject.leaf tok) ≠ none

Helper lemma: label of a leaf is never none

theorem Minimalism.label_ne_none_is_some (α : SyntacticObject) (h : label α ≠ none) :

∃ (li : LexicalItem ), label α = some li

Corollary: if label α ≠ none, then label returns some LI

theorem Minimalism.label_always_some (α : SyntacticObject) :

label α ≠ none

For any SO, label never returns none. This follows from the structure: every SO contains a leaf, and label always finds it.

theorem Minimalism.getProjectingLI_some_implies_label_some (α : SyntacticObject) (li : LexicalItem) :

getProjectingLI α = some li → label α ≠ none

Corollary: getProjectingLI returning some implies label is not none

theorem Minimalism.selects_implies_has_label (α β : SyntacticObject) (h : selects α β) :

label α ≠ none

If α selects β, then α has a label (not none).

theorem Minimalism.sameLabel_when_right_selects (α β : SyntacticObject) (h : selects β α) (hna : ¬selects α β) :

sameLabel β (merge α β)

When β selects α and α doesn't select β, β and {α,β} have the same label

theorem Minimalism.labeling_uniform_external (em : ExternalMerge) (h_selects : selects em.α em.β) :

projectsIn em.α em.result

THEOREM 3 (Labeling Uniformity): The labeling algorithm works identically for External and Internal Merge.

What projects depends on selectional relations, not on whether the merge was external or internal.

theorem Minimalism.labeling_uniform_internal (im : InternalMerge) (h_selects : selects im.mover im.target) :

projectsIn im.mover im.result

theorem Minimalism.selection_determines_projection (gm : GeneralMerge) :

selects gm.left gm.right → projectsIn gm.left gm.result

COROLLARY: Selection determines projection, not merge type

theorem Minimalism.external_merge_uniform (em : ExternalMerge) :

em.result = merge em.α em.β

Property 1 for External Merge: Operation doesn't depend on element nature

theorem Minimalism.internal_merge_uniform (im : InternalMerge) :

im.result = merge im.mover im.target

Property 1 for Internal Merge: Operation doesn't depend on element nature

theorem Minimalism.external_merge_labeling (em : ExternalMerge) (h : selects em.α em.β) :

projectsIn em.α em.result

Property 2 for External Merge: Labeling depends on selection

theorem Minimalism.internal_merge_labeling (im : InternalMerge) (h : selects im.mover im.target) :

projectsIn im.mover im.result

Property 2 for Internal Merge: Labeling depends on selection

theorem Minimalism.external_merge_either_projects (em : ExternalMerge) (h_acyclic : NoMutualSelection em.α em.β) :

(selects em.α em.β → projectsIn em.α em.result) ∧ (selects em.β em.α → projectsIn em.β em.result)

Property 3 for External Merge: Either element can project.

Requires NoMutualSelection: selection on categories must be acyclic, so at most one of α, β can select the other.

theorem Minimalism.internal_merge_either_projects (im : InternalMerge) (h_acyclic : NoMutualSelection im.mover im.target) :

(selects im.mover im.target → projectsIn im.mover im.result) ∧ (selects im.target im.mover → projectsIn im.target im.result)

Property 3 for Internal Merge: Either element can project.

Requires NoMutualSelection: selection on categories must be acyclic.

theorem Minimalism.harizanov_unification :

(∀ (em : ExternalMerge), em.result = merge em.α em.β) ∧ (∀ (im : InternalMerge), im.result = merge im.mover im.target) ∧ (∀ (em : ExternalMerge), selects em.α em.β → projectsIn em.α em.result) ∧ (∀ (im : InternalMerge), selects im.mover im.target → projectsIn im.mover im.result) ∧ (∀ (em : ExternalMerge), NoMutualSelection em.α em.β → (selects em.α em.β → projectsIn em.α em.result) ∧ (selects em.β em.α → projectsIn em.β em.result)) ∧ ∀ (im : InternalMerge), NoMutualSelection im.mover im.target → (selects im.mover im.target → projectsIn im.mover im.result) ∧ (selects im.target im.mover → projectsIn im.target im.result)

THEOREM (Harizanov Unification): Both merge types satisfy all three properties.

Property 3 requires NoMutualSelection (acyclicity of selection on categories).

theorem Minimalism.movement_uniform_position (im : InternalMerge) :

∃ (sister : SyntacticObject ), im.result = im.mover.node sister

THEOREM 4 (Movement Uniformity): "The properties of movement do not depend on the nature of the moving element"

Whether the mover is a head or a phrase, Internal Merge works the same way. The mover always ends up in the left daughter position of the result.

theorem Minimalism.mover_is_left_daughter (im : InternalMerge) :

immediatelyContains im.result im.mover

The mover is always the left daughter after Internal Merge

theorem Minimalism.target_is_right_daughter (im : InternalMerge) :

immediatelyContains im.result im.target

The target is always the right daughter after Internal Merge

theorem Minimalism.mover_can_project (im : InternalMerge) (h_mover_selects : selects im.mover im.target) :

projectsIn im.mover im.result

THEOREM 5 (Mover Can Project): "A moved element can project after movement"

This is non-trivial: traditionally, only the target was thought to project. But if the mover has unvalued selectional features that can be satisfied by the target, the mover can project (= head-to-head movement).

theorem Minimalism.target_can_project (im : InternalMerge) (h_target_selects : selects im.target im.mover) (h_acyclic : NoMutualSelection im.mover im.target) :

projectsIn im.target im.result

Target can also project (standard case).

Requires NoMutualSelection: selection on categories must be acyclic.

theorem Minimalism.projection_dichotomy (im : InternalMerge) (h_one_selects : selects im.mover im.target ∨ selects im.target im.mover) (h_acyclic : NoMutualSelection im.mover im.target) :

projectsIn im.mover im.result ∨ projectsIn im.target im.result

The dichotomy: either mover or target projects (one must).

Requires NoMutualSelection: selection on categories must be acyclic.

theorem Minimalism.merge_unification :

(∀ (em : ExternalMerge) (im : InternalMerge), em.result = merge em.α em.β ∧ im.result = merge im.mover im.target) ∧ (∀ (em : ExternalMerge), ¬contains em.α em.β ∧ ¬contains em.β em.α) ∧ (∀ (im : InternalMerge), contains im.target im.mover) ∧ ∀ (α β : SyntacticObject), α ≠ β → ¬contains α β ∧ ¬contains β α ∨ contains α β ∨ contains β α

MAIN THEOREM (Merge Unification): Internal and External Merge are the same operation under different preconditions.

Formally: there exists a single function merge such that both EM and IM are instances of applying this function, differing only in whether the containment precondition holds.

def Minimalism.isHeadMovement (im : InternalMerge) :

Head movement is just Internal Merge where the mover is a head

Equations

Minimalism.isHeadMovement im = Minimalism.isHeadIn im.mover im.target

Instances For

def Minimalism.isPhrasalMovement (im : InternalMerge) :

Phrasal movement is Internal Merge where the mover is a phrase

Equations

Minimalism.isPhrasalMovement im = Minimalism.isPhraseIn im.mover im.target

Instances For

theorem Minimalism.head_phrasal_same_merge (im₁ im₂ : InternalMerge) (h₁ : isHeadMovement im₁) (h₂ : isPhrasalMovement im₂) :

im₁.result = merge im₁.mover im₁.target ∧ im₂.result = merge im₂.mover im₂.target

THEOREM: Head and phrasal movement use the same Internal Merge

theorem Minimalism.head_vs_phrasal_projection (im : InternalMerge) (h_acyclic : NoMutualSelection im.mover im.target) :

(isHeadMovement im ∧ selects im.mover im.target → projectsIn im.mover im.result) ∧ (selects im.target im.mover → projectsIn im.target im.result)

The difference is in what projects, not in the operation.

Requires NoMutualSelection: selection on categories must be acyclic.

structure Minimalism.StrictPartialOrder (α : Type u_1) (R : α → α → Prop) :

Containment is a strict partial order: irreflexive, asymmetric, transitive. This is an algebraic property of tree structure, not a stipulation.

irrefl (x : α) : ¬R x x
asymm (x y : α) : R x y → ¬R y x
trans (x y z : α) : R x y → R y z → R x z

Instances For

theorem Minimalism.contains_irrefl' (x : SyntacticObject) :

¬contains x x

No element contains itself (well-foundedness of trees)

StrictPartialOrder SyntacticObject contains

theorem Minimalism.contains_is_strict_partial_order :

Containment on syntactic objects forms a strict partial order

theorem Minimalism.strict_partial_order_trichotomy {α : Type u_1} {R : α → α → Prop} (spo : StrictPartialOrder α R) (x y : α) (hne : x ≠ y) :

R x y ∧ ¬R y x ∨ R y x ∧ ¬R x y ∨ ¬R x y ∧ ¬R y x

TRICHOTOMY THEOREM (Order Theory): For any strict partial order, element pairs fall into exactly one of three cases. This is algebraic - it follows from the definition of strict partial order.

theorem Minimalism.trichotomy_mutually_exclusive {α : Type u_1} {R : α → α → Prop} (spo : StrictPartialOrder α R) (x y : α) :

¬(R x y ∧ R y x)

The trichotomy cases are mutually exclusive

theorem Minimalism.merge_partition_from_trichotomy (α β : SyntacticObject) (hne : α ≠ β) :

(contains α β ∨ contains β α) ∨ ¬contains α β ∧ ¬contains β α

COROLLARY: Internal/External partition follows from trichotomy.

Grouping "R x y" and "R y x" gives COMPARABLE (Internal Merge). The third case is INCOMPARABLE (External Merge).

This is why the partition isn't a "choice" - it's forced by order theory.

theorem Minimalism.accessibility_is_separate_from_partition (α β : SyntacticObject) :

α ≠ β → (contains α β ∨ contains β α) ∨ ¬contains α β ∧ ¬contains β α

The "choices" Collins & Stabler mention are about ACCESSIBILITY, not partition.

Different workspace conditions determine which pairs are ACCESSIBLE for Merge:

"A ∈ W ∧ B ∈ W" → only incomparable pairs accessible (External only)
"A ∈ W ∧ (A contains B ∨ B ∈ W)" → standard (External + Internal)
"A ∈ W ∧ B contained in W" → adds sideward merge

But the PARTITION of pairs into comparable/incomparable is algebraic. The "choice" is which partition cells are accessible, not the partition itself.

def Minimalism.AccessCondition :

Type

Accessibility conditions as predicates on (workspace, element, element) triples

Equations

Minimalism.AccessCondition = (Set Minimalism.SyntacticObject → Minimalism.SyntacticObject → Minimalism.SyntacticObject → Prop)

Instances For

def Minimalism.externalOnly :

External-only: both must be roots

Equations

Minimalism.externalOnly W A B = (A ∈ W ∧ B ∈ W)

Instances For

def Minimalism.standardAccess :

Standard (Chomsky): A is root, B is either in A or a root

Equations

Minimalism.standardAccess W A B = (A ∈ W ∧ (Minimalism.contains A B ∨ B ∈ W))

Instances For

def Minimalism.sidewardAccess :

Sideward: A is root, B is anywhere in W

Equations

Minimalism.sidewardAccess W A B = (A ∈ W ∧ ∃ (C : Minimalism.SyntacticObject ), C ∈ W ∧ Minimalism.containsOrEq C B)

Instances For

def Minimalism.fullAccess :

Full: both anywhere in W

Equations

Minimalism.fullAccess W A B = ((∃ (C : Minimalism.SyntacticObject ), C ∈ W ∧ Minimalism.containsOrEq C A) ∧ ∃ (D : Minimalism.SyntacticObject ), D ∈ W ∧ Minimalism.containsOrEq D B)

Instances For

def Minimalism.morePermissive (c1 c2 : AccessCondition) :

One condition is more permissive than another

Equations

Minimalism.morePermissive c1 c2 = ∀ (W : Set Minimalism.SyntacticObject) (A B : Minimalism.SyntacticObject), c2 W A B → c1 W A B

Instances For

morePermissive standardAccess externalOnly ∧ morePermissive sidewardAccess standardAccess ∧ morePermissive fullAccess sidewardAccess

theorem Minimalism.accessibility_chain :

The conditions form a chain: external ⊂ standard ⊂ sideward ⊂ full

theorem Minimalism.chomsky_choice_is_minimal :

(∀ (W : Set SyntacticObject) (A B : SyntacticObject), A ∈ W → contains A B → standardAccess W A B) ∧ ∀ (W : Set SyntacticObject) (A B : SyntacticObject), contains A B → ¬B ∈ W → ¬externalOnly W A B

THEOREM (Minimality of Chomsky's Choice): Standard access is the MINIMAL extension of external-only that allows Internal Merge.

"Minimal" means: any condition that allows Internal Merge and is at most as permissive as standard must equal standard on Internal cases.

def Minimalism.internalOnly :

The pure Internal Merge condition (without External)

Equations

Minimalism.internalOnly W A B = (A ∈ W ∧ Minimalism.contains A B)

Instances For

theorem Minimalism.standard_is_join_of_external_internal (W : Set SyntacticObject) (A B : SyntacticObject) :

standardAccess W A B ↔ externalOnly W A B ∨ internalOnly W A B

THEOREM (Join Characterization): Standard access is exactly the join of External and Internal conditions. This is why Chomsky's choice is canonical - it's a lattice-theoretic join.

morePermissive C standardAccess

theorem Minimalism.standard_is_least_upper_bound (C : AccessCondition) (hext : morePermissive C externalOnly) (hint : morePermissive C internalOnly) :

Standard is the LEAST condition containing both External and Internal

theorem Minimalism.contains_implies_ne {x y : SyntacticObject} (h : contains x y) :

x ≠ y

Containment implies distinctness (uses contains_irrefl from Containment.lean)

def Minimalism.Movement.toInternalMerge (m : Movement) :

InternalMerge

Convert a Movement to an InternalMerge

Equations

m.toInternalMerge = { target := m.target, mover := m.mover, result := m.result, distinct := ⋯, containment := ⋯, is_merge := ⋯ }

Instances For

def Minimalism.HeadToSpecMovement.toInternalMerge (m : HeadToSpecMovement) :

InternalMerge

HeadToSpecMovement is an instance of InternalMerge

Equations

m.toInternalMerge = m.toInternalMerge

Instances For

def Minimalism.HeadToHeadMovement.toInternalMerge (m : HeadToHeadMovement) :

InternalMerge

HeadToHeadMovement is an instance of InternalMerge

Equations

m.toInternalMerge = m.toInternalMerge

Instances For

theorem Minimalism.head_movement_is_internal_merge :

(∀ (m : HeadToSpecMovement), m.result = merge m.mover m.target) ∧ ∀ (m : HeadToHeadMovement), m.result = merge m.mover m.target

THEOREM (Head Movement Unification): Both head movement types are instances of the same InternalMerge operation.

This completes Harizanov's unification: head-to-spec and head-to-head are not different operations, but the same InternalMerge with different labeling outcomes.

theorem Minimalism.head_movement_types_same_merge_different_labeling (h2s : HeadToSpecMovement) (h2h : HeadToHeadMovement) :

h2s.result = merge h2s.mover h2s.target ∧ h2h.result = merge h2h.mover h2h.target ∧ projectsIn h2s.target h2s.result ∧ ¬isMaximalIn h2h.mover h2h.result

The difference between head-to-spec and head-to-head is purely in labeling

theorem Minimalism.all_movement_is_internal_merge (m : Movement) :

∃ (im : InternalMerge ), im.mover = m.mover ∧ im.target = m.target ∧ im.result = m.result

COROLLARY: All movement (head or phrasal) reduces to InternalMerge