Mereological Syntax

@cite{adger-2025}

Core formalization of mereological syntax (@cite{adger-2025}), where syntactic structures are built by subjoin (establishing parthood) rather than merge (creating sets). Each syntactic object is an independent entity with a label; no projection or labeling algorithm is needed.

Core Concepts

1. Subjoin: x < y — x is proper part of y. No new label is created (contrast merge, which unions two objects and requires labeling).
2. Dimensionality: Max 2 subjunctions per object. First → 1-part (≈ complement, dimension 1). Second → 2-part (≈ specifier, dimension 2).
3. Parthood axioms: Irreflexive, within-dimension transitive, asymmetric. Transitivity does NOT cross dimensions.
4. Spell-out: Objects in a complementation line (1-part chain) can collectively spell out at the topmost node.

Axioms Enforced by the Type

• Dimensionality (max 2): three constructors — leaf (0), sub₁ (1), sub₁₂ (2).
• Irreflexivity / asymmetry: enforced by the tree structure (no cycles).
• Within-dimension transitivity: labelInOnePartChain follows only 1-parts.
• No cross-dimension transitivity: 2-parts are not traversed.

Extended Projection Bridge

Label sequences along the 1-part chain correspond to @cite{grimshaw-2005}'s Extended Projection. MLabel.toCat? maps mereological labels to Minimalism.Cat where possible, and the EP bridge theorems (§ 8) verify that standard 1-part chains are category-consistent and F-monotone.

Limitations

angularLocalityOK operates on labels rather than node identities. When multiple nodes share a label, this is lossy. For node-identity-based AL (supporting multiparthood), see SynGraph.satisfiesAL in SynGraph.lean.

inductive MereologicalSyntax.MLabel : Type

Category labels for syntactic objects in mereological syntax.

Labels that overlap with Minimalism.Cat (N, V, D, Q, etc.) are bridged via MLabel.toCat?. Labels specific to @cite{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 MereologicalSyntax.instDecidableEqMLabel : DecidableEq MLabel

Equations

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

instance MereologicalSyntax.instBEqMLabel : BEq MLabel

Equations

• MereologicalSyntax.instBEqMLabel = { beq := MereologicalSyntax.instBEqMLabel.beq }

def MereologicalSyntax.instBEqMLabel.beq : MLabel → MLabel → Bool

Equations

• MereologicalSyntax.instBEqMLabel.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

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.

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

Map mereological labels to Minimalism.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 Minimalism.Cat.N
• MereologicalSyntax.MLabel.V.toCat? = some Minimalism.Cat.V
• MereologicalSyntax.MLabel.v.toCat? = some Minimalism.Cat.v
• MereologicalSyntax.MLabel.T.toCat? = some Minimalism.Cat.T
• MereologicalSyntax.MLabel.C.toCat? = some Minimalism.Cat.C
• MereologicalSyntax.MLabel.D.toCat? = some Minimalism.Cat.D
• MereologicalSyntax.MLabel.Q.toCat? = some Minimalism.Cat.Q
• MereologicalSyntax.MLabel.Num.toCat? = some Minimalism.Cat.Num
• MereologicalSyntax.MLabel.A.toCat? = some Minimalism.Cat.A
• MereologicalSyntax.MLabel.Asp.toCat? = some Minimalism.Cat.Asp
• MereologicalSyntax.MLabel.Mod.toCat? = some Minimalism.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

inductive MereologicalSyntax.SynObj : Type

A syntactic object in mereological syntax.

Each object has a label and at most two subparts, enforcing Dimensionality (@cite{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

instance MereologicalSyntax.instReprSynObj : Repr SynObj

Equations

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

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

Equations

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

instance MereologicalSyntax.instDecidableEqSynObj : DecidableEq SynObj

Equations

• MereologicalSyntax.instDecidableEqSynObj = MereologicalSyntax.instDecidableEqSynObj.decEq

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 MereologicalSyntax.instBEqSynObj : BEq SynObj

Equations

• MereologicalSyntax.instBEqSynObj = { beq := MereologicalSyntax.instBEqSynObj.beq }

def MereologicalSyntax.instBEqSynObj.beq : SynObj → SynObj → Bool

Equations

• One or more equations did not get rendered due to their size.
• MereologicalSyntax.instBEqSynObj.beq (MereologicalSyntax.SynObj.leaf a) (MereologicalSyntax.SynObj.leaf b) = (a == b)
• MereologicalSyntax.instBEqSynObj.beq (MereologicalSyntax.SynObj.sub₁ a a_1) (MereologicalSyntax.SynObj.sub₁ b b_1) = (a == b && MereologicalSyntax.instBEqSynObj.beq a_1 b_1)
• MereologicalSyntax.instBEqSynObj.beq x✝¹ x✝ = false

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

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

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 @cite{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 (@cite{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)

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

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

Follows only 2-part edges: if A <₂ B <₂ C, then A is reachable from C via this chain. 1-parts are NOT traversed — the dual of labelInOnePartChain.

Equations

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

def MereologicalSyntax.labelWithinDimPartOf (l : MLabel) (root : SynObj) : Bool

Is label l a within-dimension transitive part of root?

True when l is reachable by following ONLY 1-part edges or ONLY 2-part edges from root, never crossing dimensions (@cite{adger-2025}). This is the parthood relation relevant to Angular Locality.

Equations

• MereologicalSyntax.labelWithinDimPartOf l root = (MereologicalSyntax.labelInOnePartChain l root || MereologicalSyntax.labelInTwoPartChain l root)

def MereologicalSyntax.SynObj.onePartChainObjs : SynObj → List SynObj

Collect all SynObj nodes along the transitive 1-part chain of root (not including root itself).

Equations

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

def MereologicalSyntax.angularLocalityOK (l : MLabel) (target : SynObj) : Bool

Angular Locality (@cite{adger-2025}, definition 29):

γ can subjoin to β only if there is an α such that γ is a within-dimension transitive n-part of α AND α is a transitive 1-part of β.

Caveat: This operates on labels, not node identities. When multiple nodes share a label, this function is an approximation. For node-identity-based AL with multiparthood support, see SynGraph.satisfiesAL in SynGraph.lean.

Equations

• MereologicalSyntax.angularLocalityOK l target = target.onePartChainObjs.any fun (x : MereologicalSyntax.SynObj) => MereologicalSyntax.labelWithinDimPartOf l x

theorem MereologicalSyntax.nominal_ep_valid : have cats := List.filterMap MLabel.toCat? [MLabel.N, MLabel.Q, MLabel.D]; Minimalism.allCategoryConsistent cats = true ∧ Minimalism.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 @cite{grimshaw-2005}'s system.

theorem MereologicalSyntax.verbal_ep_valid : have cats := List.filterMap MLabel.toCat? [MLabel.V, MLabel.v, MLabel.T, MLabel.C]; Minimalism.allCategoryConsistent cats = true ∧ Minimalism.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 Minimalism.catFamily MLabel.N.toCat? = some Minimalism.CatFamily.nominal ∧ Option.map Minimalism.catFamily MLabel.Q.toCat? = some Minimalism.CatFamily.nominal ∧ Option.map Minimalism.catFamily MLabel.Num.toCat? = some Minimalism.CatFamily.nominal ∧ Option.map Minimalism.catFamily MLabel.D.toCat? = some Minimalism.CatFamily.nominal ∧ Option.map Minimalism.catFamily MLabel.V.toCat? = some Minimalism.CatFamily.verbal ∧ Option.map Minimalism.catFamily MLabel.v.toCat? = some Minimalism.CatFamily.verbal ∧ Option.map Minimalism.catFamily MLabel.T.toCat? = some Minimalism.CatFamily.verbal ∧ Option.map Minimalism.catFamily MLabel.C.toCat? = some Minimalism.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 Minimalism.catFamily MLabel.N.toCat? ≠ Option.map Minimalism.catFamily MLabel.V.toCat? ∧ Option.map Minimalism.catFamily MLabel.D.toCat? ≠ Option.map Minimalism.catFamily MLabel.C.toCat?

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