def Minimalism.selContains (sel : SelStack) (c : Cat) : Bool

Helper: does sel stack contain category?

Equations

• Minimalism.selContains sel c = List.any sel fun (x : Minimalism.Cat) => x == c

def Minimalism.selMatchesOpt (sel : SelStack) (oc : Option Cat) : Bool

Helper: check if option cat matches any in sel stack

Equations

• Minimalism.selMatchesOpt sel (some c) = Minimalism.selContains sel c
• Minimalism.selMatchesOpt sel none = false

partial def Minimalism.getCategory (so : SyntacticObject) : Option Cat

Get the category of an SO by finding the projecting head This must match the logic in label

partial def Minimalism.getProjectingLI (so : SyntacticObject) : Option LexicalItem

Get the LI of an SO (the projecting head)

def Minimalism.selectsB (selector selected : SyntacticObject) : Bool

X selects Y iff X's selectional requirements include Y's category

Selection is what triggers projection: the selector projects. When V[D] merges with DP, V selects D, so V projects.

Equations

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

def Minimalism.selects (selector selected : SyntacticObject) : Prop

Propositional version of selection

Equations

• Minimalism.selects selector selected = (Minimalism.selectsB selector selected = true)

instance Minimalism.instDecidableSelects (x y : SyntacticObject) : Decidable (selects x y)

Equations

• Minimalism.instDecidableSelects x y = inferInstanceAs (Decidable (Minimalism.selectsB x y = true))

def Minimalism.label : SyntacticObject → Option LexicalItem

The label of an SO - determined by which element projects

• For an LI token: its lexical item
• For a set {X, Y}: the label of whichever element selects the other

"The label of X is the label of the projecting element"

Equations

• One or more equations did not get rendered due to their size.
• Minimalism.label (Minimalism.SyntacticObject.leaf tok) = some tok.item

def Minimalism.labelCat (so : SyntacticObject) : Option Cat

Get the category from the label

Equations

• Minimalism.labelCat so = Option.map (fun (x : Minimalism.LexicalItem) => x.outerCat) (Minimalism.label so)

def Minimalism.sameLabel (x y : SyntacticObject) : Prop

Two SOs have the same label

Equations

• Minimalism.sameLabel x y = (Minimalism.label x = Minimalism.label y ∧ Minimalism.label x ≠ none)

def Minimalism.sameLabelB (x y : SyntacticObject) : Bool

Equations

• Minimalism.sameLabelB x y = match Minimalism.label x, Minimalism.label y with | some lx, some ly => lx.features == ly.features | x, x_1 => false

instance Minimalism.instDecidableSameLabel (x y : SyntacticObject) : Decidable (sameLabel x y)

Equations

• Minimalism.instDecidableSameLabel x y = inferInstanceAs (Decidable (Minimalism.label x = Minimalism.label y ∧ Minimalism.label x ≠ none))

def Minimalism.projectsIn (x y : SyntacticObject) : Prop

X projects in Y iff X's label = Y's label and X is immediately contained in Y

Equations

• Minimalism.projectsIn x y = (Minimalism.immediatelyContains y x ∧ Minimalism.sameLabel x y)

def Minimalism.projectsInB (x y : SyntacticObject) : Bool

Equations

• Minimalism.projectsInB x (Minimalism.SyntacticObject.leaf tok) = false
• Minimalism.projectsInB x (a.node b) = ((x == a || x == b) && Minimalism.sameLabelB x (a.node b))

instance Minimalism.instDecidableProjectsIn (x y : SyntacticObject) : Decidable (projectsIn x y)

Equations

• Minimalism.instDecidableProjectsIn x y = inferInstanceAs (Decidable (Minimalism.immediatelyContains y x ∧ Minimalism.sameLabel x y))

def Minimalism.projects (x root : SyntacticObject) : Prop

X projects iff X projects in some containing SO

Equations

• Minimalism.projects x root = ∃ (y : Minimalism.SyntacticObject), Minimalism.containsOrEq root y ∧ Minimalism.projectsIn x y

def Minimalism.isMinimalIn (x y : SyntacticObject) : Prop

X is minimal in Y iff X is a term of Y and X doesn't contain anything

From Harizanov: "A head is thus a strictly minimal element, one that does not contain anything (and is therefore an LI)"

+min = is a leaf/LI

Equations

• Minimalism.isMinimalIn (Minimalism.SyntacticObject.leaf tok) y = (Minimalism.isTermOf (Minimalism.SyntacticObject.leaf tok) y ∧ True)
• Minimalism.isMinimalIn (a.node b) y = (Minimalism.isTermOf (a.node b) y ∧ False)

def Minimalism.isMaximalIn (x y : SyntacticObject) : Prop

X is maximal in Y iff X is a term of Y and X doesn't project in anything in Y

+max = X is at the top of its projection chain (nothing contains X with same label)

From Harizanov: a phrase is +max, meaning it's a maximal projection

Equations

• Minimalism.isMaximalIn x y = (Minimalism.isTermOf x y ∧ ¬∃ (z : Minimalism.SyntacticObject), Minimalism.isTermOf z y ∧ Minimalism.projectsIn x z)

def Minimalism.isHeadIn (x y : SyntacticObject) : Prop

A head in Y: +minimal AND -maximal

From Harizanov (22b): "A head is an SO that is both +min and −max"

This means: X is an LI (doesn't contain anything) AND X projects (is contained by something with same label).

Footnote: "a head is an LI which projects"

Equations

• Minimalism.isHeadIn x y = (Minimalism.isMinimalIn x y ∧ ¬Minimalism.isMaximalIn x y)

def Minimalism.isPhraseIn (x y : SyntacticObject) : Prop

A phrase in Y: +maximal

From Harizanov (22a): "A phrase is an SO that is +max (and ±min)"

A phrase is a maximal projection - at the top of its projection chain.

Equations

• Minimalism.isPhraseIn x y = Minimalism.isMaximalIn x y

def Minimalism.isNonProjectingLI (x y : SyntacticObject) : Prop

An LI that doesn't project: +minimal AND +maximal

This is an LI that is simultaneously at the bottom (is a leaf) and top (doesn't project) of its chain. Not a "head" per (22b).

Equations

• Minimalism.isNonProjectingLI x y = (Minimalism.isMinimalIn x y ∧ Minimalism.isMaximalIn x y)

def Minimalism.verbEat : LIToken

A verb "eat" that selects D (needs an object)

Equations

• Minimalism.verbEat = { item := Minimalism.LexicalItem.simple Minimalism.Cat.V [Minimalism.Cat.D], id := 1 }

def Minimalism.nounPizza : LIToken

A noun "pizza" with no selectional requirements

Equations

• Minimalism.nounPizza = { item := Minimalism.LexicalItem.simple Minimalism.Cat.N [], id := 2 }

def Minimalism.detThe : LIToken

A determiner "the" that selects N

Equations

• Minimalism.detThe = { item := Minimalism.LexicalItem.simple Minimalism.Cat.D [Minimalism.Cat.N], id := 3 }

def Minimalism.theDP : SyntacticObject

Build: [D the] merges with [N pizza] → D projects (D selects N)

Equations

• Minimalism.theDP = (Minimalism.SyntacticObject.leaf Minimalism.detThe).node (Minimalism.SyntacticObject.leaf Minimalism.nounPizza)

def Minimalism.eatPizzaVP : SyntacticObject

Build: [V eat] merges with [DP the pizza] → V projects (V selects D)

Equations

• Minimalism.eatPizzaVP = (Minimalism.SyntacticObject.leaf Minimalism.verbEat).node Minimalism.theDP

inductive Minimalism.TreePos : Type

A position in a tree: path from root to an element. here = at this node left p = go left, then follow p right p = go right, then follow p

• here : TreePos
• left : TreePos → TreePos
• right : TreePos → TreePos

def Minimalism.instReprTreePos.repr : TreePos → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Minimalism.instReprTreePos.repr Minimalism.TreePos.here prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.TreePos.here")).group prec✝

instance Minimalism.instReprTreePos : Repr TreePos

Equations

• Minimalism.instReprTreePos = { reprPrec := Minimalism.instReprTreePos.repr }

def Minimalism.instDecidableEqTreePos.decEq (x✝ x✝¹ : TreePos) : Decidable (x✝ = x✝¹)

Equations

• Minimalism.instDecidableEqTreePos.decEq Minimalism.TreePos.here Minimalism.TreePos.here = isTrue ⋯
• Minimalism.instDecidableEqTreePos.decEq Minimalism.TreePos.here a.left = isFalse ⋯
• Minimalism.instDecidableEqTreePos.decEq Minimalism.TreePos.here a.right = isFalse ⋯
• Minimalism.instDecidableEqTreePos.decEq a.left Minimalism.TreePos.here = isFalse ⋯
• Minimalism.instDecidableEqTreePos.decEq a.left b.left = if h : a = b then h ▸ have inst := Minimalism.instDecidableEqTreePos.decEq a a; isTrue ⋯ else isFalse ⋯
• Minimalism.instDecidableEqTreePos.decEq a.left a_1.right = isFalse ⋯
• Minimalism.instDecidableEqTreePos.decEq a.right Minimalism.TreePos.here = isFalse ⋯
• Minimalism.instDecidableEqTreePos.decEq a.right a_1.left = isFalse ⋯
• Minimalism.instDecidableEqTreePos.decEq a.right b.right = if h : a = b then h ▸ have inst := Minimalism.instDecidableEqTreePos.decEq a a; isTrue ⋯ else isFalse ⋯

instance Minimalism.instDecidableEqTreePos : DecidableEq TreePos

Equations

• Minimalism.instDecidableEqTreePos = Minimalism.instDecidableEqTreePos.decEq

def Minimalism.atPosition : SyntacticObject → TreePos → Option SyntacticObject

Get the SO at a given position (if it exists)

Equations

• Minimalism.atPosition x✝ Minimalism.TreePos.here = some x✝
• Minimalism.atPosition (Minimalism.SyntacticObject.leaf a) a_1.left = none
• Minimalism.atPosition (Minimalism.SyntacticObject.leaf a) a_1.right = none
• Minimalism.atPosition (a.node a_1) p.left = Minimalism.atPosition a p
• Minimalism.atPosition (a.node b) p.right = Minimalism.atPosition b p

def Minimalism.parentPos : TreePos → Option TreePos

The parent position (one step up toward root)

Equations

• Minimalism.parentPos Minimalism.TreePos.here = none
• Minimalism.parentPos a.left = some a
• Minimalism.parentPos a.right = some a

def Minimalism.parentSO (root : SyntacticObject) (pos : TreePos) : Option SyntacticObject

Get the parent SO of a position

Equations

• Minimalism.parentSO root pos = match Minimalism.parentPos pos with | none => none | some pp => Minimalism.atPosition root pp

def Minimalism.siblingSO (root : SyntacticObject) (pos : TreePos) : Option SyntacticObject

Get the sibling SO at a position

Equations

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

def Minimalism.projectsAtPosition (x root : SyntacticObject) (pos : TreePos) : Prop

X projects AT POSITION p in root iff:

• X is at position p
• The parent at p has the same label as X

This is position-specific: checks projection only at this occurrence

Equations

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

def Minimalism.isMaximalAtPosition (x root : SyntacticObject) (pos : TreePos) : Prop

X is maximal AT POSITION p in root iff:

• X is at position p
• X does NOT project at position p (parent has different label or is root)

This captures Harizanov's "maximal in its derived position"

Equations

• Minimalism.isMaximalAtPosition x root pos = (Minimalism.atPosition root pos = some x ∧ ¬Minimalism.projectsAtPosition x root pos)

def Minimalism.isSpecifierAtPosition (x root : SyntacticObject) (pos : TreePos) : Prop

X is a specifier at position p iff:

• X is at position p
• X is maximal at p (doesn't project)
• X's sibling DOES project (the sibling is the "head" of the phrase)

Equations

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

def Minimalism.findPositions (x root : SyntacticObject) : List TreePos

Find positions where x occurs in root

Equations

• Minimalism.findPositions x root = Minimalism.findPositions.go x root Minimalism.TreePos.here []

def Minimalism.findPositions.go (x so : SyntacticObject) (pos : TreePos) (acc : List TreePos) : List TreePos

Equations

• Minimalism.findPositions.go x (Minimalism.SyntacticObject.leaf tok) pos acc = if (Minimalism.SyntacticObject.leaf tok == x) = true then pos :: acc else acc
• Minimalism.findPositions.go x (a.node b) pos acc = Minimalism.findPositions.go x b pos.right (Minimalism.findPositions.go x a pos.left (if (a.node b == x) = true then pos :: acc else acc))

def Minimalism.derivedSpecPosition : TreePos

The derived position in head-to-specifier movement is the specifier position. In {X, Y} where Y is the target (projects), X is at the LEFT (Spec) position

Equations

• Minimalism.derivedSpecPosition = Minimalism.TreePos.here.left

Free Relative Labeling Conflict (@cite{mueller-2013} §2.1)

Müller argues that Chomsky's labeling rules (2008:145) yield contradictory results for free relative clauses like "what you wrote":

• Rule 14a: In {H, α}, H an LI, H is the label → label = D (the pronoun)
• The selection-based algorithm (implementing 14b logic) → label = V (the clause)

This is underdetermined: the same structure is labeled DP when used as an object ("I read what you wrote") and CP when used as a complement of wonder ("I wonder what you wrote"). Chomsky (2013:47) acknowledges "many open questions" about free relative labeling.

Simplification: The SO freeRelSO models the surface structure without explicitly representing Internal Merge. The gap gapFR has a different token ID from whatFR rather than being a literal copy. The labeling conflict is independent of how the gap is represented.

def Minimalism.labelRule14a : SyntacticObject → Option Cat

Chomsky (2008:145) rule 14a: In {H, α} where H is a lexical item, H is the label. When one daughter is an LI, its category is the label.

Equations

• One or more equations did not get rendered due to their size.
• Minimalism.labelRule14a (Minimalism.SyntacticObject.leaf tok) = some tok.item.outerCat

def Minimalism.whatFR : LIToken

"what" — a wh-pronoun (category D, no selectional features).

Equations

• Minimalism.whatFR = { item := Minimalism.LexicalItem.simple Minimalism.Cat.D [], id := 100 }

def Minimalism.wroteFR : LIToken

"wrote" — a transitive verb (category V, selects D).

Equations

• Minimalism.wroteFR = { item := Minimalism.LexicalItem.simple Minimalism.Cat.V [Minimalism.Cat.D], id := 101 }

def Minimalism.gapFR : SyntacticObject

Object gap in D position (trace of "what").

Equations

• Minimalism.gapFR = Minimalism.SyntacticObject.leaf { item := Minimalism.LexicalItem.simple Minimalism.Cat.D [], id := 10100 }

def Minimalism.wroteGapFR : SyntacticObject

VP with gap: [wrote ___].

Equations

• Minimalism.wroteGapFR = (Minimalism.SyntacticObject.leaf Minimalism.wroteFR).node Minimalism.gapFR

def Minimalism.freeRelSO : SyntacticObject

Free relative SO: {what, [wrote ___]}. "what" has been internally merged (moved from object position).

Equations

• Minimalism.freeRelSO = (Minimalism.SyntacticObject.leaf Minimalism.whatFR).node Minimalism.wroteGapFR

theorem Minimalism.freeRel_rule14a_gives_D : labelRule14a freeRelSO = some Cat.D

Rule 14a labels the free relative as D (the pronoun "what" is an LI).

theorem Minimalism.freeRel_labelCat_gives_V : labelCat freeRelSO = some Cat.V

The selection-based labeling (implementing rule 14b's logic) labels it as V (the clause projects because "what" doesn't select the VP).

theorem Minimalism.freeRel_labeling_conflict : labelRule14a freeRelSO ≠ labelCat freeRelSO

Rules 14a and 14b conflict for free relatives: one gives D, the other V.

This is Müller's central argument against Chomsky's labeling algorithm. Free relatives like "what you wrote" function as DPs in object position ("I read what you wrote") and as CPs in complement-of-wonder position ("I wonder what you wrote") — but neither labeling rule can derive both labels from the same structure.

Coordination Labeling Failure (@cite{mueller-2013} §2.1)

When two phrases are coordinated ({DP₁, DP₂}), neither daughter is an LI (rule 14a fails) and neither selects the other (rule 14b fails). Chomsky (2013:46) stipulates a special case: when both daughters share a label, that shared label is the result. Müller argues this is an ad hoc fix that undermines the generality of the labeling algorithm.

def Minimalism.detA_coord : LIToken

A second determiner "a" (category D, selects N).

Equations

• Minimalism.detA_coord = { item := Minimalism.LexicalItem.simple Minimalism.Cat.D [Minimalism.Cat.N], id := 102 }

def Minimalism.nounBook : LIToken

"book" (category N, no selectional features).

Equations

• Minimalism.nounBook = { item := Minimalism.LexicalItem.simple Minimalism.Cat.N [], id := 103 }

def Minimalism.aBookDP : SyntacticObject

Second DP: {a, book}.

Equations

• Minimalism.aBookDP = (Minimalism.SyntacticObject.leaf Minimalism.detA_coord).node (Minimalism.SyntacticObject.leaf Minimalism.nounBook)

def Minimalism.coordDP : SyntacticObject

Coordinated structure: {theDP, aBookDP} — two phrases, neither is an LI.

Equations

• Minimalism.coordDP = Minimalism.theDP.node Minimalism.aBookDP

theorem Minimalism.coord_rule14a_fails : labelRule14a coordDP = none

Rule 14a fails for coordination: neither daughter is an LI.

theorem Minimalism.coord_neither_selects : selectsB theDP aBookDP = false ∧ selectsB aBookDP theDP = false

The selection-based algorithm gives D, but only because it falls through to the "both phrases" tie-breaking case — not because of a principled labeling mechanism. Neither phrase selects the other.

theorem Minimalism.coord_labelCat_artifact : labelCat coordDP = some Cat.D

The selection-based label of the coordinated structure. Gives D, but this is an artifact of tie-breaking, not selection.