Documentation

def Minimalism.instReprCatFeatures.repr :

CatFeatures → ℕ → Std.Format

Equations

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

Instances For

instance Minimalism.instReprCatFeatures :

Repr CatFeatures

Equations

Minimalism.instReprCatFeatures = { reprPrec := Minimalism.instReprCatFeatures.repr }

instance Minimalism.instDecidableEqCatFeatures :

DecidableEq CatFeatures

Equations

Minimalism.instDecidableEqCatFeatures = Minimalism.instDecidableEqCatFeatures.decEq

def Minimalism.instDecidableEqCatFeatures.decEq (x✝ x✝¹ : CatFeatures) :

Decidable (x✝ = x✝¹)

Equations

Minimalism.instDecidableEqCatFeatures.decEq { plusV := a, plusN := a_1 } { plusV := b, plusN := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

Instances For

instance Minimalism.instBEqCatFeatures :

BEq CatFeatures

Equations

Minimalism.instBEqCatFeatures = { beq := Minimalism.instBEqCatFeatures.beq }

def Minimalism.instBEqCatFeatures.beq :

CatFeatures → CatFeatures → Bool

Equations

Minimalism.instBEqCatFeatures.beq { plusV := a, plusN := a_1 } { plusV := b, plusN := b_1 } = (a == b && a_1 == b_1)
Minimalism.instBEqCatFeatures.beq x✝¹ x✝ = false

Instances For

def Minimalism.catFeatures :

Cat → CatFeatures

Compute @cite{chomsky-1970}'s [±V, ±N] features from Cat. Functional categories inherit features from their lexical anchor:

v, T, C inherit [+V, -N] from V
n, Num, Q, D inherit [-V, +N] from N

Equations

Minimalism.catFeatures Minimalism.Cat.V = { plusV := true, plusN := false }
Minimalism.catFeatures Minimalism.Cat.v = { plusV := true, plusN := false }
Minimalism.catFeatures Minimalism.Cat.Voice = { plusV := true, plusN := false }
Minimalism.catFeatures Minimalism.Cat.Appl = { plusV := true, plusN := false }
Minimalism.catFeatures Minimalism.Cat.T = { plusV := true, plusN := false }
Minimalism.catFeatures Minimalism.Cat.Foc = { plusV := true, plusN := false }
Minimalism.catFeatures Minimalism.Cat.Top = { plusV := true, plusN := false }
Minimalism.catFeatures Minimalism.Cat.Fin = { plusV := true, plusN := false }
Minimalism.catFeatures Minimalism.Cat.C = { plusV := true, plusN := false }
Minimalism.catFeatures Minimalism.Cat.SA = { plusV := true, plusN := false }
Minimalism.catFeatures Minimalism.Cat.Force = { plusV := true, plusN := false }
Minimalism.catFeatures Minimalism.Cat.Neg = { plusV := true, plusN := false }
Minimalism.catFeatures Minimalism.Cat.Mod = { plusV := true, plusN := false }
Minimalism.catFeatures Minimalism.Cat.Rel = { plusV := true, plusN := false }
Minimalism.catFeatures Minimalism.Cat.Pol = { plusV := true, plusN := false }
Minimalism.catFeatures Minimalism.Cat.Asp = { plusV := true, plusN := false }
Minimalism.catFeatures Minimalism.Cat.Evid = { plusV := true, plusN := false }
Minimalism.catFeatures Minimalism.Cat.N = { plusV := false, plusN := true }
Minimalism.catFeatures Minimalism.Cat.n = { plusV := false, plusN := true }
Minimalism.catFeatures Minimalism.Cat.Num = { plusV := false, plusN := true }
Minimalism.catFeatures Minimalism.Cat.Q = { plusV := false, plusN := true }
Minimalism.catFeatures Minimalism.Cat.D = { plusV := false, plusN := true }
Minimalism.catFeatures Minimalism.Cat.A = { plusV := true, plusN := true }
Minimalism.catFeatures Minimalism.Cat.a = { plusV := true, plusN := true }
Minimalism.catFeatures Minimalism.Cat.P = { plusV := false, plusN := false }
Minimalism.catFeatures Minimalism.Cat.Place = { plusV := false, plusN := false }
Minimalism.catFeatures Minimalism.Cat.Path = { plusV := false, plusN := false }

Instances For

def Minimalism.fValue :

Cat → ℕ

Grimshaw's F-value: the functional level within an extended projection.

F-values are globally aligned across category families to capture the verbal–nominal parallelism.

The nominal spine follows @cite{borer-2005}'s ordering: Q (classifier / individuation, CL#) is at F2, below Num (number / counting, #) at F3. This reflects the semantic composition order: individuation must precede counting (you can't count what hasn't been individuated). See Borer2005.lean for the formal argument.

F-level	Role	Verbal	Nominal
F0	Lexical (content)	V	N
F1	Categorizer	v, Voice, Appl	n (gender/class)
F2	Specification	T, Neg, Asp, Mod	Q (classifier/CL#)
F3	Inner edge	Fin	Num (number/#)
F4	Discourse/ref	Foc	D (definiteness)
F5	Topic	Top, Rel
F6	Clause/force	C, Force
F7	Speech act	SA

Verbal–nominal parallelism: The parallelism is robust at F0 (lexical anchors) and F1 (categorizers: v ↔ n). At F2–F3, the verbal and nominal spines are analogous but not isomorphic: T/Asp specify temporal properties while Q specifies individuation; Fin types the clause while Num types the nominal. The semantic functions differ, but both occupy the same structural zone.

The verbal C-domain is internally ordered per @cite{rizzi-1997}: Fin(F3) < Foc(F4) < Top(F5) < C(F6).

Equations

Instances For

def Minimalism.categoryConsistent (c1 c2 : Cat) :

Category consistency: two categories share [±V, ±N] features. This is the core constraint on Extended Projections — V and T are consistent (both [+V, -N]), but V and D are not.

Equations

Minimalism.categoryConsistent c1 c2 = (Minimalism.catFeatures c1 == Minimalism.catFeatures c2)

Instances For

def Minimalism.fMonotone (lower upper : Cat) :

F-value monotonicity: F-values must not decrease going up the tree. In an EP, each head's F-value is ≥ the one below it.

Equations

Minimalism.fMonotone lower upper = decide (Minimalism.fValue lower ≤ Minimalism.fValue upper)

Instances For

def Minimalism.perfectProjection (c1 c2 : Cat) :

Perfect projection: same [±V, ±N] AND same F-value. E.g., two V heads (F0, [+V, -N]) are perfect projections of each other. Distinct from EP extension, where F-value increases.

Equations

Minimalism.perfectProjection c1 c2 = (Minimalism.categoryConsistent c1 c2 && Minimalism.fValue c1 == Minimalism.fValue c2)

Instances For

def Minimalism.isLHead (c : Cat) :

Is this category a lexical head (F0)? L-heads are content categories: V, N, A, P.

Equations

Minimalism.isLHead c = (Minimalism.fValue c == 0)

Instances For

def Minimalism.isFHead (c : Cat) :

Is this category a functional head (F1+)? F-heads are functional categories: v, D, T, C.

Equations

Minimalism.isFHead c = decide (Minimalism.fValue c > 0)

Instances For

inductive Minimalism.CatFamily :

The four lexical category families, each defining an EP domain. All categories in an EP must belong to the same family.

verbal : CatFamily
nominal : CatFamily
adjectival : CatFamily
adpositional : CatFamily

Instances For

def Minimalism.instReprCatFamily.repr :

CatFamily → ℕ → Std.Format

Equations

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

Instances For

instance Minimalism.instReprCatFamily :

Repr CatFamily

Equations

Minimalism.instReprCatFamily = { reprPrec := Minimalism.instReprCatFamily.repr }

instance Minimalism.instDecidableEqCatFamily :

DecidableEq CatFamily

Equations

Minimalism.instDecidableEqCatFamily x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Minimalism.instBEqCatFamily :

BEq CatFamily

Equations

Minimalism.instBEqCatFamily = { beq := Minimalism.instBEqCatFamily.beq }

def Minimalism.instBEqCatFamily.beq :

CatFamily → CatFamily → Bool

Equations

Minimalism.instBEqCatFamily.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

def Minimalism.catFamily :

Cat → CatFamily

Map a category to its family. This determines which EP it can participate.

Equations

Instances For

structure Minimalism.CategorialFeatures :

@cite{panagiotidis-2015} categorial features: [N] and [V] as substantive, LF-interpretable features with semantic content.

[N] = sortal perspective / referentiality (capacity to introduce a discourse referent, following @cite{longobardi-1994}, @cite{longobardi-2005}; §4.3 p84)
[V] = temporal perspective / eventivity (capacity to anchor to time/events; §4.3 p85)

This contrasts with @cite{chomsky-1970}'s [±V, ±N] diacritics (see CatFeatures): Chomsky's features are arbitrary binary cross-classifiers, while Panagiotidis's are grounded in semantic substance. The key empirical difference is the status of P: Chomsky treats P as actively bearing [-V, -N]; Panagiotidis treats P as the default categorizer lacking both [N] and [V] (§4.3).

Interpretability distinction (§5.8): On categorizers (v, n, a), these features are interpretable — they provide the LF-legible interpretive perspective (sortal or temporal). On higher functional heads (T, C, D, etc.), these features are uninterpretable copies that serve only for Agree/selection. This formalization does not encode the interpretable/uninterpretable distinction but records which features are present, which suffices for EP consistency.

Despite the conceptual difference, the two systems produce the same four equivalence classes over categories (see chomsky_panagiotidis_agree).

hasN : Bool
hasV : Bool

Instances For

def Minimalism.instReprCategorialFeatures.repr :

CategorialFeatures → ℕ → Std.Format

Equations

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

Instances For

instance Minimalism.instReprCategorialFeatures :

Repr CategorialFeatures

Equations

Minimalism.instReprCategorialFeatures = { reprPrec := Minimalism.instReprCategorialFeatures.repr }

DecidableEq CategorialFeatures

instance Minimalism.instDecidableEqCategorialFeatures :

Equations

Minimalism.instDecidableEqCategorialFeatures = Minimalism.instDecidableEqCategorialFeatures.decEq

def Minimalism.instDecidableEqCategorialFeatures.decEq (x✝ x✝¹ : CategorialFeatures) :

Decidable (x✝ = x✝¹)

Equations

Minimalism.instDecidableEqCategorialFeatures.decEq { hasN := a, hasV := a_1 } { hasN := b, hasV := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

Instances For

instance Minimalism.instBEqCategorialFeatures :

BEq CategorialFeatures

Equations

Minimalism.instBEqCategorialFeatures = { beq := Minimalism.instBEqCategorialFeatures.beq }

def Minimalism.instBEqCategorialFeatures.beq :

CategorialFeatures → CategorialFeatures → Bool

Equations

Minimalism.instBEqCategorialFeatures.beq { hasN := a, hasV := a_1 } { hasN := b, hasV := b_1 } = (a == b && a_1 == b_1)
Minimalism.instBEqCategorialFeatures.beq x✝¹ x✝ = false

Instances For

def Minimalism.categorialFeatures :

Cat → CategorialFeatures

Map a category to @cite{panagiotidis-2015}'s categorial features.

Categorizers (n, v, a) bear the substantive features; functional heads in the same EP inherit them (just as in Grimshaw's consistency requirement). P and its extended projection bear neither feature — P is the default case.

Equations

Minimalism.categorialFeatures Minimalism.Cat.V = { hasN := false, hasV := true }
Minimalism.categorialFeatures Minimalism.Cat.v = { hasN := false, hasV := true }
Minimalism.categorialFeatures Minimalism.Cat.Voice = { hasN := false, hasV := true }
Minimalism.categorialFeatures Minimalism.Cat.Appl = { hasN := false, hasV := true }
Minimalism.categorialFeatures Minimalism.Cat.T = { hasN := false, hasV := true }
Minimalism.categorialFeatures Minimalism.Cat.Foc = { hasN := false, hasV := true }
Minimalism.categorialFeatures Minimalism.Cat.Top = { hasN := false, hasV := true }
Minimalism.categorialFeatures Minimalism.Cat.Fin = { hasN := false, hasV := true }
Minimalism.categorialFeatures Minimalism.Cat.C = { hasN := false, hasV := true }
Minimalism.categorialFeatures Minimalism.Cat.SA = { hasN := false, hasV := true }
Minimalism.categorialFeatures Minimalism.Cat.Force = { hasN := false, hasV := true }
Minimalism.categorialFeatures Minimalism.Cat.Neg = { hasN := false, hasV := true }
Minimalism.categorialFeatures Minimalism.Cat.Mod = { hasN := false, hasV := true }
Minimalism.categorialFeatures Minimalism.Cat.Rel = { hasN := false, hasV := true }
Minimalism.categorialFeatures Minimalism.Cat.Pol = { hasN := false, hasV := true }
Minimalism.categorialFeatures Minimalism.Cat.Asp = { hasN := false, hasV := true }
Minimalism.categorialFeatures Minimalism.Cat.Evid = { hasN := false, hasV := true }
Minimalism.categorialFeatures Minimalism.Cat.N = { hasN := true, hasV := false }
Minimalism.categorialFeatures Minimalism.Cat.n = { hasN := true, hasV := false }
Minimalism.categorialFeatures Minimalism.Cat.Num = { hasN := true, hasV := false }
Minimalism.categorialFeatures Minimalism.Cat.Q = { hasN := true, hasV := false }
Minimalism.categorialFeatures Minimalism.Cat.D = { hasN := true, hasV := false }
Minimalism.categorialFeatures Minimalism.Cat.A = { hasN := true, hasV := true }
Minimalism.categorialFeatures Minimalism.Cat.a = { hasN := true, hasV := true }
Minimalism.categorialFeatures Minimalism.Cat.P = { hasN := false, hasV := false }
Minimalism.categorialFeatures Minimalism.Cat.Place = { hasN := false, hasV := false }
Minimalism.categorialFeatures Minimalism.Cat.Path = { hasN := false, hasV := false }

Instances For

def Minimalism.categorialConsistent (c1 c2 : Cat) :

Consistency under Panagiotidis's system: two categories share [N]/[V] features.

Equations

Minimalism.categorialConsistent c1 c2 = (Minimalism.categorialFeatures c1 == Minimalism.categorialFeatures c2)

Instances For

theorem Minimalism.chomsky_panagiotidis_agree (c1 c2 : Cat) :

categoryConsistent c1 c2 = categorialConsistent c1 c2

Chomsky's [±V, ±N] and Panagiotidis's [N]/[V] produce the same equivalence classes over all categories. They agree on which pairs are EP-consistent.

The conceptual difference — P as [-V, -N] vs. P as default — is invisible to the consistency check: both systems group P only with itself.

structure Minimalism.ExtendedProjection :

An Extended Projection: a sequence of categories forming a projection chain with category consistency and F-value monotonicity.

The spine lists categories from lowest (lexical head) to highest (functional).

root : SyntacticObject
Root syntactic object of the EP
spine : List Cat
Categories along the spine, from lexical head (F0) upward
catConsistent : Bool
All spine categories share [±V, ±N] features
fMonotoneChain : Bool
F-values are non-decreasing along the spine

Instances For

def Minimalism.allCategoryConsistent :

List Cat → Bool

Check that a list of categories is category-consistent (all share the same [±V, ±N] features).

Equations

Minimalism.allCategoryConsistent [] = true
Minimalism.allCategoryConsistent [head] = true
Minimalism.allCategoryConsistent (c₁ :: c₂ :: rest) = (Minimalism.categoryConsistent c₁ c₂ && Minimalism.allCategoryConsistent (c₂ :: rest))

Instances For

def Minimalism.allFMonotone :

List Cat → Bool

Check that a list of categories has monotonically non-decreasing F-values.

Equations

Minimalism.allFMonotone [] = true
Minimalism.allFMonotone [head] = true
Minimalism.allFMonotone (c₁ :: c₂ :: rest) = (Minimalism.fMonotone c₁ c₂ && Minimalism.allFMonotone (c₂ :: rest))

Instances For

partial def Minimalism.computeEPSpine (so : SyntacticObject) :

List (SyntacticObject × Cat)

Compute the EP spine from a syntactic object by collecting categories along the head-projection chain. Returns pairs of (SO, Cat) from the deepest lexical head up to the root.

def Minimalism.mkExtendedProjection (so : SyntacticObject) :

ExtendedProjection

Build an ExtendedProjection from a syntactic object.

Equations

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

Instances For

def Minimalism.ExtendedProjection.isWellFormed (ep : ExtendedProjection) :

Is this EP well-formed? (category consistent AND F-monotone)

Equations

ep.isWellFormed = (ep.catConsistent && ep.fMonotoneChain)

Instances For

def Minimalism.ExtendedProjection.family (ep : ExtendedProjection) :

Option CatFamily

The family of an EP (determined by any element of the spine).

Equations

ep.family = Option.map Minimalism.catFamily ep.spine.head?

Instances For

def Minimalism.ExtendedProjection.lexicalAnchor (ep : ExtendedProjection) :

Option Cat

The lexical anchor of an EP (the F0 head at the bottom).

Equations

ep.lexicalAnchor = Option.filter Minimalism.isLHead ep.spine.head?

Instances For

def Minimalism.ExtendedProjection.highestHead (ep : ExtendedProjection) :

Option Cat

The highest functional head in the EP.

Equations

ep.highestHead = ep.spine.getLast?

Instances For

theorem Minimalism.verbal_chain_consistent :

categoryConsistent Cat.V Cat.v = true ∧ categoryConsistent Cat.v Cat.T = true ∧ categoryConsistent Cat.T Cat.C = true

The verbal chain V → v → T → C is category-consistent: all share [+V, -N] features.

The nominal chain N → n → Q → Num → D is category-consistent: all have [-V, +N] features. Q (CL#, individuation) is below Num (#, counting) per @cite{borer-2005}.

theorem Minimalism.verbal_fvalues_monotone :

fValue Cat.V ≤ fValue Cat.v ∧ fValue Cat.v ≤ fValue Cat.T ∧ fValue Cat.T ≤ fValue Cat.C

F-values increase monotonically along the verbal chain: V(0) ≤ v(1) ≤ T(2) ≤ C(3).

theorem Minimalism.nominal_fvalues_monotone :

fValue Cat.N ≤ fValue Cat.n ∧ fValue Cat.n ≤ fValue Cat.Q ∧ fValue Cat.Q ≤ fValue Cat.Num ∧ fValue Cat.Num ≤ fValue Cat.D

F-values increase along the nominal chain: N(0) ≤ n(1) ≤ Q(2) ≤ Num(3) ≤ D(4). Q (individuation) is below Num (counting) per @cite{borer-2005}.

theorem Minimalism.verbal_nominal_inconsistent :

categoryConsistent Cat.V Cat.N = false

V and N are NOT category-consistent (different [±V, ±N]).

theorem Minimalism.verbal_determiner_inconsistent :

categoryConsistent Cat.V Cat.D = false

V and D are NOT category-consistent (verbal ≠ nominal).

theorem Minimalism.f0_iff_lexical (c : Cat) :

isLHead c = true ↔ c = Cat.V ∨ c = Cat.N ∨ c = Cat.A ∨ c = Cat.P

F0 is exactly the lexical heads.

theorem Minimalism.fpos_iff_functional (c : Cat) :

isFHead c = true ↔ c = Cat.v ∨ c = Cat.n ∨ c = Cat.a ∨ c = Cat.Place ∨ c = Cat.Path ∨ c = Cat.Num ∨ c = Cat.Q ∨ c = Cat.Voice ∨ c = Cat.Appl ∨ c = Cat.D ∨ c = Cat.T ∨ c = Cat.Foc ∨ c = Cat.Top ∨ c = Cat.Fin ∨ c = Cat.C ∨ c = Cat.SA ∨ c = Cat.Force ∨ c = Cat.Neg ∨ c = Cat.Mod ∨ c = Cat.Rel ∨ c = Cat.Pol ∨ c = Cat.Asp ∨ c = Cat.Evid

F1+ is exactly the functional heads.

theorem Minimalism.same_family_consistent (c1 c2 : Cat) :

catFamily c1 = catFamily c2 → categoryConsistent c1 c2 = true

Categories in the same family are category-consistent.

theorem Minimalism.full_verbal_ep_consistent :

allCategoryConsistent [Cat.V , Cat.v , Cat.T , Cat.C ] = true

The full verbal EP spine [V, v, T, C] is category-consistent.

theorem Minimalism.full_verbal_ep_monotone :

allFMonotone [Cat.V , Cat.v , Cat.T , Cat.C ] = true

The full verbal EP spine [V, v, T, C] is F-monotone.

theorem Minimalism.full_nominal_ep_consistent :

allCategoryConsistent [Cat.N , Cat.n , Cat.Q , Cat.Num , Cat.D ] = true

The full nominal EP spine [N, n, Q, Num, D] is category-consistent.

theorem Minimalism.full_nominal_ep_monotone :

allFMonotone [Cat.N , Cat.n , Cat.Q , Cat.Num , Cat.D ] = true

The full nominal EP spine [N, n, Q, Num, D] is F-monotone.

theorem Minimalism.f0_corresponds_to_head :

isLHead Cat.V = true ∧ isLHead Cat.N = true ∧ isLHead Cat.A = true ∧ isLHead Cat.P = true

F0 categories correspond to BarLevel.zero (head), F1+ categories correspond to intermediate/maximal projections. This connects Grimshaw's F-level to X-bar bar levels.

Functional heads (F1+) extend the projection beyond the lexical head.

theorem Minimalism.verbal_nominal_parallel :

fValue Cat.V = fValue Cat.N ∧ fValue Cat.v = fValue Cat.n ∧ fValue Cat.T = fValue Cat.Q ∧ fValue Cat.Fin = fValue Cat.Num

The verbal and nominal spines are parallel at F0–F1: V ↔ N (lexical), v ↔ n (categorizer).

At F2–F3 the spines diverge: T (temporal specification, F2) pairs with Q (individuation, F2), while Fin (clause-typing, F3) pairs with Num (number, F3). These are structural analogs occupying the same EP zone, but their semantic functions differ. See borer_ordering_unique in Borer2005.lean for the formal argument that Q must be below Num.

def Minimalism.isCategorizer (c : Cat) :

Is this category a categorizer? Categorizers bear substantive, interpretable [N]/[V] features and combine with acategorial roots to yield categorized items.

Important: Panagiotidis (§4.5) argues categorizers are NOT functional heads — they are the only true lexical heads (roots being acategorial). Our F-value system (from @cite{grimshaw-2005}) places them at F1, which makes isFHead return true for categorizers. This reflects Grimshaw's architectural classification, not Panagiotidis's ontological claim about their nature.

Equations

Instances For

theorem Minimalism.categorizers_at_f1 :

fValue Cat.v = 1 ∧ fValue Cat.n = 1 ∧ fValue Cat.a = 1

All three categorizers are at F1 in @cite{grimshaw-2005}'s F-value system. @cite{panagiotidis-2015} predicts this parallelism; the F1 encoding is Grimshaw's.

theorem Minimalism.categorizer_parallel :

fValue Cat.v = fValue Cat.n ∧ fValue Cat.n = fValue Cat.a

The three categorizers are parallel: all at the same F-level.

catFamily Cat.a = CatFamily.adjectival

theorem Minimalism.a_in_adjectival_family :

The adjectival categorizer is in the adjectival family (parallel to v→verbal, n→nominal).

theorem Minimalism.adpositional_chain_consistent :

categoryConsistent Cat.P Cat.Place = true ∧ categoryConsistent Cat.Place Cat.Path = true

The adpositional chain P → Place → Path is category-consistent: all share [-V, -N] features. @cite{dendikken-2010}: PlaceP (locational) and PathP (directional) are functional projections above P.

theorem Minimalism.adpositional_fvalues_monotone :

fValue Cat.P ≤ fValue Cat.Place ∧ fValue Cat.Place ≤ fValue Cat.Path

F-values increase along the adpositional chain: P(0) ≤ Place(1) ≤ Path(2). Parallel to V(0) ≤ v(1) ≤ T(2) in the verbal domain.

catFamily Cat.Place = CatFamily.adpositional ∧ catFamily Cat.Path = CatFamily.adpositional

theorem Minimalism.place_path_adpositional :

Place and Path are in the adpositional family.

theorem Minimalism.locational_pp_wellformed :

allCategoryConsistent [Cat.P , Cat.Place ] = true ∧ allFMonotone [Cat.P , Cat.Place ] = true

The adpositional EP spine [P, Place] is well-formed (locational PP).

theorem Minimalism.directional_pp_wellformed :

allCategoryConsistent [Cat.P , Cat.Place , Cat.Path ] = true ∧ allFMonotone [Cat.P , Cat.Place , Cat.Path ] = true

The adpositional EP spine [P, Place, Path] is well-formed (directional PP). @cite{dendikken-2010}: directional PPs project PathP above PlaceP.

def Minimalism.splitCPVerbalEP :

List Cat

The verbal EP spine with @cite{rizzi-1997}'s split-CP layer: V → v → T → Fin → Foc → Top → C. Fin is the boundary between IP and CP; Foc and Top are discourse-related projections between Fin and C (= Force).

Equations

Minimalism.splitCPVerbalEP = [Minimalism.Cat.V , Minimalism.Cat.v , Minimalism.Cat.T , Minimalism.Cat.Fin , Minimalism.Cat.Foc , Minimalism.Cat.Top , Minimalism.Cat.C ]

Instances For

allCategoryConsistent splitCPVerbalEP = true

theorem Minimalism.splitCP_ep_consistent :

The split-CP spine is category-consistent: all heads share [+V, -N].

allFMonotone splitCPVerbalEP = true

theorem Minimalism.splitCP_ep_monotone :

The split-CP spine is F-monotone: 0 ≤ 1 ≤ 2 ≤ 3 ≤ 4 ≤ 5 ≤ 6. This is the key payoff of the fValue fix — before the fix, Fin/Foc/Top/C all had fValue 3, so any permutation would trivially pass.

theorem Minimalism.reverse_splitCP_not_monotone :

allFMonotone [Cat.Top , Cat.Foc , Cat.Fin ] = false

The reverse split-CP ordering [Top, Foc, Fin] is NOT monotone. This correctly rules out pathological orderings that the collapsed fValues (all = 3) would have accepted.

def Minimalism.negVerbalEP :

List Cat

Verbal EP with NegP: V → v → Neg → T → Fin → C. Represents a clause with an IP-internal negation layer.

Equations

Minimalism.negVerbalEP = [Minimalism.Cat.V , Minimalism.Cat.v , Minimalism.Cat.Neg , Minimalism.Cat.T , Minimalism.Cat.Fin , Minimalism.Cat.C ]

Instances For

allCategoryConsistent negVerbalEP = true

theorem Minimalism.neg_verbal_ep_consistent :

The verbal EP with NegP is category-consistent.

allFMonotone negVerbalEP = true

theorem Minimalism.neg_verbal_ep_monotone :

The verbal EP with NegP is F-monotone: 0 ≤ 1 ≤ 2 ≤ 2 ≤ 3 ≤ 6.

def Minimalism.fullRizziLP :

List Cat

Full Rizzi left periphery: V → v → T → Fin → Foc → Top → Force. Force is the clause-typing head when the CP is fully split.

Equations

Minimalism.fullRizziLP = [Minimalism.Cat.V , Minimalism.Cat.v , Minimalism.Cat.T , Minimalism.Cat.Fin , Minimalism.Cat.Foc , Minimalism.Cat.Top , Minimalism.Cat.Force ]

Instances For

allCategoryConsistent fullRizziLP = true

theorem Minimalism.fullRizziLP_consistent :

The full Rizzi left periphery is category-consistent.

allFMonotone fullRizziLP = true

theorem Minimalism.fullRizziLP_monotone :

The full Rizzi left periphery is F-monotone.

theorem Minimalism.force_equals_c_fvalue :

fValue Cat.Force = fValue Cat.C

Force and C have the same fValue (they're the same position when unsplit).

theorem Minimalism.neg_in_specification_domain :

fValue Cat.Neg = fValue Cat.T

Neg is in the specification domain (same F-level as T and Q).

New functional heads are all in the verbal family.

theorem Minimalism.nominal_functional_heads :

catFamily Cat.n = CatFamily.nominal ∧ catFamily Cat.Num = CatFamily.nominal ∧ catFamily Cat.Q = CatFamily.nominal

Nominal functional heads are in the nominal family.

structure Minimalism.ComplementSize :

The structural size of a clausal complement, determined by the highest functional head projected.

Complement size matters for tense Agree locality: a CP complement constitutes a phase boundary that blocks upward Agree for [uPAST], while a TP complement is transparent.

Also relevant for @cite{wurmbrand-2014}'s three-way infinitival classification (restructuring ≈ vP, propositional ≈ TP, full finite ≈ CP).

highestHead : Cat
The highest functional head in the complement

Instances For

def Minimalism.instDecidableEqComplementSize.decEq (x✝ x✝¹ : ComplementSize) :

Decidable (x✝ = x✝¹)

Equations

Minimalism.instDecidableEqComplementSize.decEq { highestHead := a } { highestHead := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

Instances For

DecidableEq ComplementSize

instance Minimalism.instDecidableEqComplementSize :

Equations

Minimalism.instDecidableEqComplementSize = Minimalism.instDecidableEqComplementSize.decEq

def Minimalism.instBEqComplementSize.beq :

ComplementSize → ComplementSize → Bool

Equations

Minimalism.instBEqComplementSize.beq { highestHead := a } { highestHead := b } = (a == b)
Minimalism.instBEqComplementSize.beq x✝¹ x✝ = false

Instances For

instance Minimalism.instBEqComplementSize :

BEq ComplementSize

Equations

Minimalism.instBEqComplementSize = { beq := Minimalism.instBEqComplementSize.beq }

instance Minimalism.instReprComplementSize :

Repr ComplementSize

Equations

Minimalism.instReprComplementSize = { reprPrec := Minimalism.instReprComplementSize.repr }

def Minimalism.instReprComplementSize.repr :

ComplementSize → ℕ → Std.Format

Equations

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

Instances For

def Minimalism.ComplementSize.fLevel (cs : ComplementSize) :

ℕ

The F-level of a complement (derived from fValue).

Equations

cs.fLevel = Minimalism.fValue cs.highestHead

Instances For

def Minimalism.ComplementSize.isPhaseSized (cs : ComplementSize) :

A complement is phase-sized (≥ CP) if its highest head is at or above the C level in the functional sequence.

Equations

cs.isPhaseSized = decide (Minimalism.fValue Minimalism.Cat.C ≤ cs.fLevel)

Instances For

def Minimalism.ComplementSize.transparentToTenseAgree (cs : ComplementSize) :

A complement is transparent to tense Agree if it is smaller than a full CP — i.e., the highest head is below C in the fseq.

@cite{egressy-2026}: TP complements (fValue 2) are transparent; CP complements (fValue 6) are opaque.

Equations

cs.transparentToTenseAgree = decide (cs.fLevel < Minimalism.fValue Minimalism.Cat.C)

Instances For

def Minimalism.ComplementSize.vP :

Standard complement sizes.

Equations

Minimalism.ComplementSize.vP = { highestHead := Minimalism.Cat.v }

Instances For

def Minimalism.ComplementSize.tP :

Equations

Minimalism.ComplementSize.tP = { highestHead := Minimalism.Cat.T }

Instances For

def Minimalism.ComplementSize.finP :

Equations

Minimalism.ComplementSize.finP = { highestHead := Minimalism.Cat.Fin }

Instances For

def Minimalism.ComplementSize.cP :

Equations

Minimalism.ComplementSize.cP = { highestHead := Minimalism.Cat.C }

Instances For

def Minimalism.ComplementSize.forceP :

Equations

Minimalism.ComplementSize.forceP = { highestHead := Minimalism.Cat.Force }

Instances For

def Minimalism.ComplementSize.saP :

Equations

Minimalism.ComplementSize.saP = { highestHead := Minimalism.Cat.SA }

Instances For

ComplementSize.vP.transparentToTenseAgree = true

theorem Minimalism.vP_transparent :

vP complements are transparent to tense Agree.

ComplementSize.tP.transparentToTenseAgree = true

theorem Minimalism.tP_transparent :

TP complements are transparent to tense Agree.

ComplementSize.finP.transparentToTenseAgree = true

theorem Minimalism.finP_transparent :

FinP complements are transparent to tense Agree.

ComplementSize.cP.transparentToTenseAgree = false

theorem Minimalism.cP_opaque :

CP complements are opaque to tense Agree.

ComplementSize.forceP.transparentToTenseAgree = false

theorem Minimalism.forceP_opaque :

ForceP complements are opaque to tense Agree.

ComplementSize.saP.transparentToTenseAgree = false

theorem Minimalism.saP_opaque :

SAP complements are opaque to tense Agree.

theorem Minimalism.complement_size_ordering :

ComplementSize.vP.fLevel < ComplementSize.tP.fLevel ∧ ComplementSize.tP.fLevel < ComplementSize.finP.fLevel ∧ ComplementSize.finP.fLevel < ComplementSize.cP.fLevel

Size ordering: vP < TP < FinP < CP.

inductive Minimalism.ForceHead :

The seven clause-type heads in @cite{westergaard-2009}'s split-ForceP. Each represents a possible target for verb movement.

@cite{westergaard-2009} splits @cite{rizzi-1997}'s ForceP into clause-type-specific projections: DeclP, IntP, PolP, ExclP, ImpP are all "flavors of Force" in the CP domain, while FinP and WhP handle embedded contexts. This decomposition allows V2 to be treated as multiple independent micro-parameters rather than a single macro-parameter.

All seven heads are at or above FinP. The five root-clause heads (Decl, Int, Pol, Excl, Imp) are finer-grained than @cite{rizzi-1997}'s single Force head — they are all at the Force level (F6). Fin° corresponds to Cat.Fin (F3); Wh° is at the Force level (F6).

Decl : ForceHead
Int : ForceHead
Pol : ForceHead
Excl : ForceHead
Imp : ForceHead
Fin : ForceHead
Wh : ForceHead

Instances For

instance Minimalism.instDecidableEqForceHead :

DecidableEq ForceHead

Equations

Minimalism.instDecidableEqForceHead x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Minimalism.instReprForceHead :

Repr ForceHead

Equations

Minimalism.instReprForceHead = { reprPrec := Minimalism.instReprForceHead.repr }

def Minimalism.instReprForceHead.repr :

ForceHead → ℕ → Std.Format

Equations

Minimalism.instReprForceHead.repr Minimalism.ForceHead.Decl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.ForceHead.Decl")).group prec✝
Minimalism.instReprForceHead.repr Minimalism.ForceHead.Int prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.ForceHead.Int")).group prec✝
Minimalism.instReprForceHead.repr Minimalism.ForceHead.Pol prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.ForceHead.Pol")).group prec✝
Minimalism.instReprForceHead.repr Minimalism.ForceHead.Excl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.ForceHead.Excl")).group prec✝
Minimalism.instReprForceHead.repr Minimalism.ForceHead.Imp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.ForceHead.Imp")).group prec✝
Minimalism.instReprForceHead.repr Minimalism.ForceHead.Fin prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.ForceHead.Fin")).group prec✝
Minimalism.instReprForceHead.repr Minimalism.ForceHead.Wh prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Minimalism.ForceHead.Wh")).group prec✝

Instances For

instance Minimalism.instBEqForceHead :

BEq ForceHead

Equations

Minimalism.instBEqForceHead = { beq := Minimalism.instBEqForceHead.beq }

def Minimalism.instBEqForceHead.beq :

ForceHead → ForceHead → Bool

Equations

Minimalism.instBEqForceHead.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

def Minimalism.instInhabitedForceHead.default :

ForceHead

Equations

Minimalism.instInhabitedForceHead.default = Minimalism.ForceHead.Decl

Instances For

instance Minimalism.instInhabitedForceHead :

Inhabited ForceHead

Equations

Minimalism.instInhabitedForceHead = { default := Minimalism.instInhabitedForceHead.default }

def Minimalism.ForceHead.isRootClause :

ForceHead → Bool

Whether a ForceHead is a root-clause head (in the Force domain) or a lower/embedded head.

Equations

Instances For

def Minimalism.ForceHead.toCat :

ForceHead → Cat

Map a ForceHead to the corresponding Cat. The five root-clause heads all map to Cat.Force (they are flavors of Force); Fin maps to Cat.Fin; Wh maps to Cat.C (embedded complementizer domain).

Equations

Instances For

theorem Minimalism.forceHead_verbal (fh : ForceHead) :

catFamily fh.toCat = CatFamily.verbal

All ForceHead values are in the verbal EP family.

structure Minimalism.V2Profile :

A V2 profile: for each clause-type head, whether verb movement to that head is required (+) or absent (−) in a given language/dialect.

This is the formalization of @cite{westergaard-2009}'s micro-parameter model: V2 is not one parameter but seven independent ones.

name : String
verbMovement : ForceHead → Bool

Instances For

def Minimalism.V2Profile.activeCount (p : V2Profile) :

ℕ

Count how many heads trigger verb movement in a profile.

Equations

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

Instances For

def Minimalism.V2Profile.differOnExactlyOne (p q : V2Profile) (fh : ForceHead) :

Prop

Whether two profiles differ on exactly one head.

Equations

p.differOnExactlyOne q fh = (p.verbMovement fh ≠ q.verbMovement fh ∧ ∀ (fh' : Minimalism.ForceHead), fh' ≠ fh → p.verbMovement fh' = q.verbMovement fh')

Instances For

inductive Minimalism.WhElementStatus :

The syntactic status of a wh-element: head (X°) or phrase (XP).

@cite{westergaard-2009} argues that monosyllabic wh-words (ka 'what', kem 'who', kor 'where' in the Tromsø dialect) are syntactic heads, while polysyllabic wh-constituents (korfor 'why', korsen 'how', katti 'when') are phrases. This distinction is supported by similar patterns in Italian dialects (@cite{poletto-pollock-2004}).

The distinction matters for V2: when a wh-head occupies Int°, it blocks verb movement to that position, making non-V2 possible. When a wh-phrase is in SpecIntP, Int° is free for the verb → V2 obligatory.

head : WhElementStatus
phrase : WhElementStatus

Instances For

DecidableEq WhElementStatus

instance Minimalism.instDecidableEqWhElementStatus :

Equations

Minimalism.instDecidableEqWhElementStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Minimalism.instReprWhElementStatus :

Repr WhElementStatus

Equations

Minimalism.instReprWhElementStatus = { reprPrec := Minimalism.instReprWhElementStatus.repr }

def Minimalism.instReprWhElementStatus.repr :

WhElementStatus → ℕ → Std.Format

Equations

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

Instances For

instance Minimalism.instBEqWhElementStatus :

BEq WhElementStatus

Equations

Minimalism.instBEqWhElementStatus = { beq := Minimalism.instBEqWhElementStatus.beq }

def Minimalism.instBEqWhElementStatus.beq :

WhElementStatus → WhElementStatus → Bool

Equations

Minimalism.instBEqWhElementStatus.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

def Minimalism.WhElementStatus.fromSyllableCount (n : ℕ) :

WhElementStatus

Determine wh-element status from syllable count. Monosyllabic → head; polysyllabic → phrase.

Equations

Minimalism.WhElementStatus.fromSyllableCount n = if n ≤ 1 then Minimalism.WhElementStatus.head else Minimalism.WhElementStatus.phrase

Instances For

WhElementStatus.fromSyllableCount 1 = WhElementStatus.head

theorem Minimalism.wh_mono_is_head :

Monosyllabic wh-words are heads.

WhElementStatus.fromSyllableCount 2 = WhElementStatus.phrase

theorem Minimalism.wh_poly_is_phrase :

Polysyllabic wh-words are phrases.