Dimensioned parthood

Mereological syntax replaces set-theoretic Merge by Subjoin, which makes one syntactic object a proper part of another. Parthood comes in two dimensions: the first subjunction to an object makes a 1-part, interpreted as the extended-projection complement, the second a 2-part, the specifier, and there is no third (Dimensionality). Parthood is transitive within a dimension but not across dimensions, which is what makes 2-parts locality domains.

This file defines the parthood structure Parthood α on a type of objects, its immediate and transitive parthood relations, the Subjoin operation, rank functions as certificates of acyclicity, and how parthood chains leave a domain closed under parenthood.

Main definitions

• MereologicalSyntax.Parthood — the 1-part and 2-part functions.
• Parthood.Imm n x y — x is the immediate n-part of y; Parthood.NPart n is its transitive closure, the n-part relation; Parthood.WithinDim — an n-part for some n; Parthood.Descendant — parthood through both dimensions.
• Parthood.subjoin — Subjoin, filling the next free dimension of the target.

Main statements

• Parthood.lt_of_descendant — a rank increasing along immediate parthood increases along Descendant; hence Parthood.not_descendant_of_le and Parthood.acyclic_of_rank.
• Parthood.nPart_iff_of_unique — an n-part chain from an object with a unique parent passes through that parent.
• Parthood.exit_of_nPart — an n-part chain leaving a domain closed under parenthood except at b leaves in b's own dimension of attachment, and reaches b first.

References

• [adger-2025]

inductive MereologicalSyntax.Dim : Type

The two dimensions of parthood: 1-parts are extended-projection complements, 2-parts are specifiers.

• one : Dim
• two : Dim

@[instance_reducible]

instance MereologicalSyntax.instDecidableEqDim : DecidableEq Dim

Equations

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

def MereologicalSyntax.instReprDim.repr : Dim → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance MereologicalSyntax.instReprDim : Repr Dim

Equations

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

@[instance_reducible]

instance MereologicalSyntax.instFintypeDim : Fintype Dim

Equations

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

structure MereologicalSyntax.Parthood (α : Type u_1) : Type u_1

A dimensioned parthood structure on α: each object has at most one 1-part and at most one 2-part (Dimensionality).

• onePart : α → Option α

  The 1-part of an object, if any.

• twoPart : α → Option α

  The 2-part of an object, if any.

theorem MereologicalSyntax.Parthood.ext {α : Type u_1} {x y : Parthood α} (onePart : x.onePart = y.onePart) (twoPart : x.twoPart = y.twoPart) : x = y

theorem MereologicalSyntax.Parthood.ext_iff {α : Type u_1} {x y : Parthood α} : x = y ↔ x.onePart = y.onePart ∧ x.twoPart = y.twoPart

@[instance_reducible]

instance MereologicalSyntax.Parthood.instDecidableEqOfFintype {α : Type u_1} [Fintype α] [DecidableEq α] : DecidableEq (Parthood α)

Equations

• P.instDecidableEqOfFintype Q = decidable_of_iff (P.onePart = Q.onePart ∧ P.twoPart = Q.twoPart) ⋯

def MereologicalSyntax.Parthood.part {α : Type u_1} (P : Parthood α) : Dim → α → Option α

The n-part of an object, if any.

Equations

• P.part MereologicalSyntax.Dim.one = P.onePart
• P.part MereologicalSyntax.Dim.two = P.twoPart

Parthood relations

def MereologicalSyntax.Parthood.Imm {α : Type u_1} (P : Parthood α) (n : Dim) (x y : α) : Prop

x is the immediate n-part of y.

Equations

• P.Imm n x y = (P.part n y = some x)

@[instance_reducible]

instance MereologicalSyntax.Parthood.instDecidableImmOfDecidableEq {α : Type u_1} (P : Parthood α) [DecidableEq α] (n : Dim) (x y : α) : Decidable (P.Imm n x y)

Equations

• P.instDecidableImmOfDecidableEq n x y = MereologicalSyntax.Parthood.instDecidableImmOfDecidableEq._aux_1 P n x y

def MereologicalSyntax.Parthood.NPart {α : Type u_1} (P : Parthood α) (n : Dim) : α → α → Prop

x is an n-part of y: parthood is transitive within a dimension.

Equations

• P.NPart n = Relation.TransGen (P.Imm n)

def MereologicalSyntax.Parthood.WithinDim {α : Type u_1} (P : Parthood α) (x y : α) : Prop

x is a part of y within a single dimension.

Equations

• P.WithinDim x y = (P.NPart MereologicalSyntax.Dim.one x y ∨ P.NPart MereologicalSyntax.Dim.two x y)

def MereologicalSyntax.Parthood.Descendant {α : Type u_1} (P : Parthood α) : α → α → Prop

x is reachable from y through parts of either dimension.

Equations

• P.Descendant = Relation.TransGen fun (x y : α) => P.Imm MereologicalSyntax.Dim.one x y ∨ P.Imm MereologicalSyntax.Dim.two x y

theorem MereologicalSyntax.Parthood.NPart.imm {α : Type u_1} {P : Parthood α} {n : Dim} {x y : α} (h : P.Imm n x y) : P.NPart n x y

theorem MereologicalSyntax.Parthood.NPart.trans {α : Type u_1} {P : Parthood α} {n : Dim} {x y z : α} (h₁ : P.NPart n x y) (h₂ : P.NPart n y z) : P.NPart n x z

theorem MereologicalSyntax.Parthood.descendant_of_imm {α : Type u_1} {P : Parthood α} {n : Dim} {x y : α} (h : P.Imm n x y) : P.Descendant x y

theorem MereologicalSyntax.Parthood.descendant_of_nPart {α : Type u_1} {P : Parthood α} {n : Dim} {x y : α} (h : P.NPart n x y) : P.Descendant x y

theorem MereologicalSyntax.Parthood.descendant_of_withinDim {α : Type u_1} {P : Parthood α} {x y : α} (h : P.WithinDim x y) : P.Descendant x y

theorem MereologicalSyntax.Parthood.Descendant.trans {α : Type u_1} {P : Parthood α} {x y z : α} (h₁ : P.Descendant x y) (h₂ : P.Descendant y z) : P.Descendant x z

Rank certificates

theorem MereologicalSyntax.Parthood.lt_of_descendant {α : Type u_1} {P : Parthood α} (rank : α → ℕ) (hrank : ∀ (n : Dim) (x y : α), P.Imm n x y → rank x < rank y) {x y : α} (h : P.Descendant x y) : rank x < rank y

theorem MereologicalSyntax.Parthood.not_descendant_of_le {α : Type u_1} {P : Parthood α} (rank : α → ℕ) (hrank : ∀ (n : Dim) (x y : α), P.Imm n x y → rank x < rank y) {x y : α} (h : rank y ≤ rank x) : ¬P.Descendant x y

theorem MereologicalSyntax.Parthood.acyclic_of_rank {α : Type u_1} {P : Parthood α} (rank : α → ℕ) (hrank : ∀ (n : Dim) (x y : α), P.Imm n x y → rank x < rank y) (x : α) : ¬P.Descendant x x

An increasing rank certifies that no object is a part of itself.

Chains through unique parents and out of domains

theorem MereologicalSyntax.Parthood.nPart_iff_of_unique {α : Type u_1} {P : Parthood α} {n : Dim} {x u : α} (hu : P.Imm n x u) (hx : ∀ (m : Dim) (y : α), P.Imm m x y → m = n ∧ y = u) {z : α} : P.NPart n x z ↔ z = u ∨ P.NPart n u z

An n-part chain from an object whose only parent is u, in dimension n, stops at u or continues from it.

theorem MereologicalSyntax.Parthood.not_nPart_of_unique {α : Type u_1} {P : Parthood α} {n : Dim} {x u : α} (hx : ∀ (m : Dim) (y : α), P.Imm m x y → m = n ∧ y = u) {m : Dim} (hmn : m ≠ n) (z : α) : ¬P.NPart m x z

An object whose only parent is in dimension n is not an m-part of anything, m ≠ n.

theorem MereologicalSyntax.Parthood.not_nPart_of_no_parent {α : Type u_1} {P : Parthood α} {n : Dim} {x : α} (hx : ∀ (y : α), ¬P.Imm n x y) (z : α) : ¬P.NPart n x z

theorem MereologicalSyntax.Parthood.exit_of_nPart {α : Type u_1} {P : Parthood α} {S : Set α} {b : α} {d : Dim} (hS : ∀ x ∈ S, x ≠ b → ∀ (n : Dim) (y : α), P.Imm n x y → y ∈ S) (hb : ∀ (n : Dim) (y : α), P.Imm n b y → n = d) {n : Dim} {x y : α} (h : P.NPart n x y) (hx : x ∈ S) (hy : y ∉ S) : n = d ∧ (x = b ∨ P.NPart d x b)

A domain S closed under parenthood except at b, which is attached only in dimension d: an n-part chain from inside S to outside it runs in dimension d and reaches b first.