Syntactic objects of mereological syntax

Mereological syntax builds structure by Subjoin, which makes one syntactic object a part of another, rather than by Merge, which collects two objects into a set: no new object is created, so no labeling algorithm is needed. Dimensionality allows each object one 1-part, the extended-projection complement, and one 2-part, the specifier.

This file defines the tree-shaped syntactic objects SynObj over the category labels MLabel, Subjoin on them, the complementation line (the 1-part chain, along which objects spell out together), and the correspondence of that line with the extended projection. Object identity across positions, and hence movement and Angular Locality, need the general parthood structure Parthood of Mereological/Parthood.lean.

Main definitions

• MereologicalSyntax.MLabel, MLabel.toCat? — category labels and their Minimalist.Cat counterparts.
• MereologicalSyntax.SynObj, MereologicalSyntax.subjoin — objects with at most two parts and Subjoin in the next free dimension.
• SynObj.compLine, MereologicalSyntax.labelInOnePartChain — the complementation line and visibility along it.

References

• [adger-2025]
• [grimshaw-2005]
• [wang-sun-2026]

Labels

inductive MereologicalSyntax.MLabel : Type

Category labels for syntactic objects in mereological syntax.

Labels that overlap with Minimalist.Cat (N, V, D, Q, etc.) are bridged via MLabel.toCat?. Labels specific to [adger-2025]'s analysis (Cl, Deg, Adv, O, Pred) have no Cat equivalent.

• N : MLabel
• Cl : MLabel
• Q : MLabel
• Num : MLabel
• D : MLabel
• Mod : MLabel
• Deg : MLabel
• A : MLabel
• Adv : MLabel
• V : MLabel
• v : MLabel
• T : MLabel
• C : MLabel
• Asp : MLabel
• O : MLabel
• Pred : MLabel

@[instance_reducible]

instance MereologicalSyntax.instDecidableEqMLabel : DecidableEq MLabel

Equations

• MereologicalSyntax.instDecidableEqMLabel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance MereologicalSyntax.instReprMLabel : Repr MLabel

Equations

• MereologicalSyntax.instReprMLabel = { reprPrec := MereologicalSyntax.instReprMLabel.repr }

def MereologicalSyntax.instReprMLabel.repr : MLabel → ℕ → Std.Format

Equations

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

Bridge to Minimalist.Cat

def MereologicalSyntax.MLabel.toCat? : MLabel → Option Minimalist.Cat

Map mereological labels to Minimalist.Cat where possible.

Labels shared with the Minimalist framework map to their Cat equivalent. Labels specific to mereological syntax return none.

Equations

• MereologicalSyntax.MLabel.N.toCat? = some Minimalist.Cat.N
• MereologicalSyntax.MLabel.V.toCat? = some Minimalist.Cat.V
• MereologicalSyntax.MLabel.v.toCat? = some Minimalist.Cat.v
• MereologicalSyntax.MLabel.T.toCat? = some Minimalist.Cat.T
• MereologicalSyntax.MLabel.C.toCat? = some Minimalist.Cat.C
• MereologicalSyntax.MLabel.D.toCat? = some Minimalist.Cat.D
• MereologicalSyntax.MLabel.Q.toCat? = some Minimalist.Cat.Q
• MereologicalSyntax.MLabel.Num.toCat? = some Minimalist.Cat.Num
• MereologicalSyntax.MLabel.A.toCat? = some Minimalist.Cat.A
• MereologicalSyntax.MLabel.Asp.toCat? = some Minimalist.Cat.Asp
• MereologicalSyntax.MLabel.Mod.toCat? = some Minimalist.Cat.Mod
• MereologicalSyntax.MLabel.Cl.toCat? = none
• MereologicalSyntax.MLabel.Deg.toCat? = none
• MereologicalSyntax.MLabel.Adv.toCat? = none
• MereologicalSyntax.MLabel.O.toCat? = none
• MereologicalSyntax.MLabel.Pred.toCat? = none

Syntactic Objects

inductive MereologicalSyntax.SynObj : Type

A syntactic object in mereological syntax.

Each object has a label and at most two subparts, enforcing Dimensionality ([adger-2025]):

• leaf l: bare object, no parts (0 dimensions)
• sub₁ l x: x is 1-part of l (complement, dim 1)
• sub₁₂ l x y: x is 1-part, y is 2-part (specifier, dim 2)

The first subjunction is always dimension 1; the second dimension 2. No third subjunction is possible (the type has no 3-part constructor).

In projectionist terms: 1-part ≈ complement, 2-part ≈ specifier.

• leaf : MLabel → SynObj
• sub₁ : MLabel → SynObj → SynObj
• sub₁₂ : MLabel → SynObj → SynObj → SynObj

def MereologicalSyntax.instReprSynObj.repr : SynObj → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance MereologicalSyntax.instReprSynObj : Repr SynObj

Equations

• MereologicalSyntax.instReprSynObj = { reprPrec := MereologicalSyntax.instReprSynObj.repr }

def MereologicalSyntax.instDecidableEqSynObj.decEq (x✝ x✝¹ : SynObj) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• MereologicalSyntax.instDecidableEqSynObj.decEq (MereologicalSyntax.SynObj.leaf a) (MereologicalSyntax.SynObj.leaf b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• MereologicalSyntax.instDecidableEqSynObj.decEq (MereologicalSyntax.SynObj.leaf a) (MereologicalSyntax.SynObj.sub₁ a_1 a_2) = isFalse ⋯
• MereologicalSyntax.instDecidableEqSynObj.decEq (MereologicalSyntax.SynObj.leaf a) (MereologicalSyntax.SynObj.sub₁₂ a_1 a_2 a_3) = isFalse ⋯
• MereologicalSyntax.instDecidableEqSynObj.decEq (MereologicalSyntax.SynObj.sub₁ a a_1) (MereologicalSyntax.SynObj.leaf a_2) = isFalse ⋯
• MereologicalSyntax.instDecidableEqSynObj.decEq (MereologicalSyntax.SynObj.sub₁ a a_1) (MereologicalSyntax.SynObj.sub₁₂ a_2 a_3 a_4) = isFalse ⋯
• MereologicalSyntax.instDecidableEqSynObj.decEq (MereologicalSyntax.SynObj.sub₁₂ a a_1 a_2) (MereologicalSyntax.SynObj.leaf a_3) = isFalse ⋯
• MereologicalSyntax.instDecidableEqSynObj.decEq (MereologicalSyntax.SynObj.sub₁₂ a a_1 a_2) (MereologicalSyntax.SynObj.sub₁ a_3 a_4) = isFalse ⋯

@[instance_reducible]

instance MereologicalSyntax.instDecidableEqSynObj : DecidableEq SynObj

Equations

• MereologicalSyntax.instDecidableEqSynObj = MereologicalSyntax.instDecidableEqSynObj.decEq

Accessors

def MereologicalSyntax.SynObj.label : SynObj → MLabel

Equations

• (MereologicalSyntax.SynObj.leaf a).label = a
• (MereologicalSyntax.SynObj.sub₁ a a_1).label = a
• (MereologicalSyntax.SynObj.sub₁₂ a a_1 a_2).label = a

def MereologicalSyntax.SynObj.onePart : SynObj → Option SynObj

Equations

• (MereologicalSyntax.SynObj.leaf a).onePart = none
• (MereologicalSyntax.SynObj.sub₁ a a_1).onePart = some a_1
• (MereologicalSyntax.SynObj.sub₁₂ a a_1 a_2).onePart = some a_1

def MereologicalSyntax.SynObj.twoPart : SynObj → Option SynObj

Equations

• (MereologicalSyntax.SynObj.leaf a).twoPart = none
• (MereologicalSyntax.SynObj.sub₁ a a_1).twoPart = none
• (MereologicalSyntax.SynObj.sub₁₂ a a_1 a_2).twoPart = some a_2

def MereologicalSyntax.SynObj.isFull : SynObj → Bool

Whether the object has reached its dimensional maximum (2 parts).

Equations

• (MereologicalSyntax.SynObj.sub₁₂ a a_1 a_2).isFull = true
• x✝.isFull = false

Subjoin

def MereologicalSyntax.subjoin (x y : SynObj) : Option SynObj

Subjoin x to y: make x a part of y in the next available dimension. Returns none if y already has two parts (dimensionality violation).

• First subjunction → 1-part (dimension 1)
• Second subjunction → 2-part (dimension 2)

Equations

• MereologicalSyntax.subjoin x (MereologicalSyntax.SynObj.leaf a) = some (MereologicalSyntax.SynObj.sub₁ a x)
• MereologicalSyntax.subjoin x (MereologicalSyntax.SynObj.sub₁ a a_1) = some (MereologicalSyntax.SynObj.sub₁₂ a a_1 x)
• MereologicalSyntax.subjoin x (MereologicalSyntax.SynObj.sub₁₂ a a_1 a_2) = none

Complementation Line and Visibility

def MereologicalSyntax.SynObj.compLine : SynObj → List MLabel

The complementation line (1-part chain): labels reachable by iterating the 1-part relation. Objects in this line can collectively spell out at the topmost node (marked by @ in [wang-sun-2026]).

Equations

• (MereologicalSyntax.SynObj.leaf a).compLine = [a]
• (MereologicalSyntax.SynObj.sub₁ a a_1).compLine = a :: a_1.compLine
• (MereologicalSyntax.SynObj.sub₁₂ a a_1 a_2).compLine = a :: a_1.compLine

def MereologicalSyntax.labelInOnePartChain (l : MLabel) : SynObj → Bool

Is there an object with label l in root's 1-part chain?

Captures within-dimension-1 transitivity: if A <₁ B <₁ C, then A is reachable from C. Crucially, 2-parts of objects in the chain are NOT traversed — this restricted transitivity prevents cross-dimensional visibility ([adger-2025]).

Equations

• MereologicalSyntax.labelInOnePartChain l (MereologicalSyntax.SynObj.leaf a) = false
• MereologicalSyntax.labelInOnePartChain l (MereologicalSyntax.SynObj.sub₁ a a_1) = (a_1.label == l || MereologicalSyntax.labelInOnePartChain l a_1)
• MereologicalSyntax.labelInOnePartChain l (MereologicalSyntax.SynObj.sub₁₂ a a_1 a_2) = (a_1.label == l || MereologicalSyntax.labelInOnePartChain l a_1)

def MereologicalSyntax.SynObj.containsLabel (l : MLabel) : SynObj → Bool

Does root contain a sub-object with label l at any depth, in any dimension? Traverses both 1-parts and 2-parts.

Equations

• MereologicalSyntax.SynObj.containsLabel l (MereologicalSyntax.SynObj.leaf a) = (l == a)
• MereologicalSyntax.SynObj.containsLabel l (MereologicalSyntax.SynObj.sub₁ a a_1) = (l == a || MereologicalSyntax.SynObj.containsLabel l a_1)
• MereologicalSyntax.SynObj.containsLabel l (MereologicalSyntax.SynObj.sub₁₂ a a_1 a_2) = (l == a || MereologicalSyntax.SynObj.containsLabel l a_1 || MereologicalSyntax.SynObj.containsLabel l a_2)

Extended Projection Bridge

theorem MereologicalSyntax.nominal_ep_valid : have cats := List.filterMap MLabel.toCat? [MLabel.N, MLabel.Q, MLabel.D]; Minimalist.allCategoryConsistent cats = true ∧ Minimalist.allFMonotone cats = true

The nominal 1-part chain [N, Q, D] (leaf-to-root order), after mapping through toCat?, is a valid Extended Projection: all categories share [-V, +N] features (category-consistent) and F-values increase monotonically (N=0 ≤ Q=2 ≤ D=4).

The classifier label Cl is filtered out (no Cat equivalent). This does not affect EP validity — Cl spells out at Q and is not a separate EP layer in [grimshaw-2005]'s system.

theorem MereologicalSyntax.verbal_ep_valid : have cats := List.filterMap MLabel.toCat? [MLabel.V, MLabel.v, MLabel.T, MLabel.C]; Minimalist.allCategoryConsistent cats = true ∧ Minimalist.allFMonotone cats = true

The verbal 1-part chain [V, v, T, C] is a valid Extended Projection: all categories share [+V, -N] features and F-values increase (V=0 ≤ v=1 ≤ T=2 ≤ C=6).

theorem MereologicalSyntax.toCat_preserves_family : Option.map Minimalist.catFamily MLabel.N.toCat? = some Minimalist.CatFamily.nominal ∧ Option.map Minimalist.catFamily MLabel.Q.toCat? = some Minimalist.CatFamily.nominal ∧ Option.map Minimalist.catFamily MLabel.Num.toCat? = some Minimalist.CatFamily.nominal ∧ Option.map Minimalist.catFamily MLabel.D.toCat? = some Minimalist.CatFamily.nominal ∧ Option.map Minimalist.catFamily MLabel.V.toCat? = some Minimalist.CatFamily.verbal ∧ Option.map Minimalist.catFamily MLabel.v.toCat? = some Minimalist.CatFamily.verbal ∧ Option.map Minimalist.catFamily MLabel.T.toCat? = some Minimalist.CatFamily.verbal ∧ Option.map Minimalist.catFamily MLabel.C.toCat? = some Minimalist.CatFamily.verbal

All MLabel-to-Cat mappings preserve EP family: nominal labels map to the nominal family, verbal labels to the verbal family.

theorem MereologicalSyntax.nominal_verbal_disjoint : Option.map Minimalist.catFamily MLabel.N.toCat? ≠ Option.map Minimalist.catFamily MLabel.V.toCat? ∧ Option.map Minimalist.catFamily MLabel.D.toCat? ≠ Option.map Minimalist.catFamily MLabel.C.toCat?

Nominal and verbal labels map to different EP families — confirming that cross-EP 1-part chains would fail category consistency.