Derivations in mereological syntax

A derivation builds syntactic objects by licensed subjunctions. Subjoining x to y is licensed when nothing subjoins to itself (Irreflexivity), the new part lands in the next free dimension of y (Dimensionality), a part moves only as Angular Locality allows, and an object that is not yet a part joins only an object that is not a part either (Mereological Extension), so that external subjunction always targets a root.

Licensed subjunction only adds parthood edges, and it keeps structures well formed. Moving a part creates no new parts of anything: Angular Locality only lets a part subjoin to an object that already contains it, and always as a 2-part. Two consequences hold along whole derivations. A domain stays a domain, so an object leaves a 2-part only from that 2-part's edge, which is successive cyclicity. And once the 2-part slot of a 2-part b is filled by c, nothing inside b other than c and the parts of c ever leaves b: a filled 2-part is a strong island.

Main definitions

• Parthood.Subjoins P x y Q: subjoining x to y is licensed in P and yields Q.
• Parthood.Derives: derivation by licensed subjunctions, and Parthood.Reaches P x y: some derivation from P makes x a part of y.

Main statements

• Parthood.Subjoins.imm_two_of_isPart: a part always subjoins as a 2-part.
• Parthood.Derives.acyclic: derivations preserve Irreflexivity.
• Parthood.IsDomain.eq_or_nPart_two_of_derives: an object escapes a 2-part only from its edge.
• Parthood.IsDomain.not_reaches: a filled 2-part is an island in every derivation.

References

• [Adg25]

structure MereologicalSyntax.Parthood.Subjoins {α : Type u_1} [DecidableEq α] (P : Parthood α) (x y : α) (Q : Parthood α) : Prop

Subjoining x to y is licensed in P and yields Q.

• ne : x ≠ y

  Nothing subjoins to itself (Irreflexivity).

• subjoin_eq : P.subjoin x y = some Q

  The new part lands in the next free dimension of y (Dimensionality).

• canSubjoin : P.IsPart x → P.CanSubjoin x y

  A part moves only as Angular Locality allows.

• extension : ¬P.IsPart x → ¬P.IsPart y

  An object that is not yet a part joins only an object that is not a part either (Mereological Extension).

@[instance_reducible]

instance MereologicalSyntax.Parthood.instDecidableSubjoinsOfFintype {α : Type u_1} [DecidableEq α] {P Q : Parthood α} {x y : α} [Fintype α] : Decidable (P.Subjoins x y Q)

Equations

• MereologicalSyntax.Parthood.instDecidableSubjoinsOfFintype = decidable_of_iff (x ≠ y ∧ P.subjoin x y = some Q ∧ (P.IsPart x → P.CanSubjoin x y) ∧ (¬P.IsPart x → ¬P.IsPart y)) ⋯

def MereologicalSyntax.Parthood.Step {α : Type u_1} [DecidableEq α] (P Q : Parthood α) : Prop

Q arises from P by one licensed subjunction.

Equations

• P.Step Q = ∃ (x : α) (y : α), P.Subjoins x y Q

def MereologicalSyntax.Parthood.Derives {α : Type u_1} [DecidableEq α] : Parthood α → Parthood α → Prop

Q arises from P by licensed subjunctions.

Equations

• MereologicalSyntax.Parthood.Derives = Relation.ReflTransGen MereologicalSyntax.Parthood.Step

theorem MereologicalSyntax.Parthood.Subjoins.derives {α : Type u_1} [DecidableEq α] {P Q : Parthood α} {x y : α} (h : P.Subjoins x y Q) : P.Derives Q

theorem MereologicalSyntax.Parthood.Derives.refl {α : Type u_1} [DecidableEq α] (P : Parthood α) : P.Derives P

theorem MereologicalSyntax.Parthood.Derives.trans {α : Type u_1} [DecidableEq α] {P Q R : Parthood α} (h₁ : P.Derives Q) (h₂ : Q.Derives R) : P.Derives R

What one licensed subjunction changes

theorem MereologicalSyntax.Parthood.Subjoins.le {α : Type u_1} [DecidableEq α] {P Q : Parthood α} {x y : α} (h : P.Subjoins x y Q) : P ≤ Q

theorem MereologicalSyntax.Parthood.Subjoins.imm_iff {α : Type u_1} [DecidableEq α] {P Q : Parthood α} {x y : α} (h : P.Subjoins x y Q) : ∃ (n : Dim), P.nextDim y = some n ∧ ∀ (m : Dim) (a b : α), Q.Imm m a b ↔ P.Imm m a b ∨ m = n ∧ a = x ∧ b = y

theorem MereologicalSyntax.Parthood.Subjoins.imm_two_of_isPart {α : Type u_1} [DecidableEq α] {P Q : Parthood α} {x y : α} (h : P.Subjoins x y Q) (hx : P.IsPart x) : Q.Imm Dim.two x y

A part always subjoins as a 2-part: Angular Locality requires its target to have a 1-part already.

theorem MereologicalSyntax.Parthood.Subjoins.descendant_iff_of_isPart {α : Type u_1} [DecidableEq α] {P Q : Parthood α} {x y : α} (h : P.Subjoins x y Q) (hx : P.IsPart x) {u v : α} : Q.Descendant u v ↔ P.Descendant u v

Moving a part creates no new parts of anything: the mover is already inside its target.

theorem MereologicalSyntax.Parthood.Subjoins.descendant_iff_of_not_isPart {α : Type u_1} [DecidableEq α] {P Q : Parthood α} {x y : α} (h : P.Subjoins x y Q) (hx : ¬P.IsPart x) {u v : α} : Q.Descendant u v ↔ P.Descendant u v ∨ (u = x ∨ P.Descendant u x) ∧ v = y

External subjunction makes x and its parts parts of the root y, and nothing else changes.

theorem MereologicalSyntax.Parthood.Subjoins.descendant_of_isPart {α : Type u_1} [DecidableEq α] {P Q : Parthood α} {x y : α} (h : P.Subjoins x y Q) {u v : α} (hv : P.IsPart v) (huv : Q.Descendant u v) : P.Descendant u v

A licensed subjunction creates no new parts of an object that is already a part.

theorem MereologicalSyntax.Parthood.Subjoins.acyclic {α : Type u_1} [DecidableEq α] {P Q : Parthood α} {x y : α} (h : P.Subjoins x y Q) (hP : P.Acyclic) : Q.Acyclic

Along derivations

theorem MereologicalSyntax.Parthood.Derives.le {α : Type u_1} [DecidableEq α] {P Q : Parthood α} (h : P.Derives Q) : P ≤ Q

theorem MereologicalSyntax.Parthood.Derives.descendant_of_isPart {α : Type u_1} [DecidableEq α] {P Q : Parthood α} (h : P.Derives Q) {u v : α} (hv : P.IsPart v) (huv : Q.Descendant u v) : P.Descendant u v

A derivation creates no new parts of an object that is already a part.

theorem MereologicalSyntax.Parthood.Derives.acyclic {α : Type u_1} [DecidableEq α] {P Q : Parthood α} (h : P.Derives Q) (hP : P.Acyclic) : Q.Acyclic

theorem MereologicalSyntax.Parthood.Derives.dimensional {α : Type u_1} [DecidableEq α] {P Q : Parthood α} (h : P.Derives Q) (hP : P.Dimensional) : Q.Dimensional

theorem MereologicalSyntax.Parthood.Derives.eq_or_descendant_of_nPart_two {α : Type u_1} [DecidableEq α] {P Q : Parthood α} {b c γ : α} (h : P.Derives Q) (hc : P.Imm Dim.two c b) (hγ : Q.NPart Dim.two γ b) : γ = c ∨ P.Descendant γ c

Once c is the 2-part of b, a derivation brings onto the edge of b only c and the parts of c.

theorem MereologicalSyntax.Parthood.Derives.not_canSubjoin_of_not_descendant {α : Type u_1} [DecidableEq α] {P Q : Parthood α} {γ β : α} (h : P.Derives Q) (hβ : P.IsPart β) (hγβ : ¬P.Descendant γ β) : ¬Q.CanSubjoin γ β

The target must contain the mover in every derivation: an object never comes to subjoin to a part that does not already contain it, so lowering and sideward subjunction stay impossible.

theorem MereologicalSyntax.Parthood.Derives.not_imm_of_not_descendant {α : Type u_1} [DecidableEq α] {P Q : Parthood α} {γ β : α} {n : Dim} (h : P.Derives Q) (hβ : P.IsPart β) (hγβ : ¬P.Descendant γ β) : ¬Q.Imm n γ β

def MereologicalSyntax.Parthood.Reaches {α : Type u_1} [DecidableEq α] (P : Parthood α) (x y : α) : Prop

Some derivation from P makes x a part of y.

Equations

• P.Reaches x y = ∃ (Q : MereologicalSyntax.Parthood α), P.Derives Q ∧ ∃ (n : MereologicalSyntax.Parthood.Dim), Q.Imm n x y

theorem MereologicalSyntax.Parthood.Subjoins.reaches {α : Type u_1} [DecidableEq α] {P Q : Parthood α} {x y : α} (h : P.Subjoins x y Q) : P.Reaches x y

theorem MereologicalSyntax.Parthood.Reaches.of_derives {α : Type u_1} [DecidableEq α] {P Q : Parthood α} {a b : α} (h : P.Derives Q) (hQ : Q.Reaches a b) : P.Reaches a b

Domains along derivations

theorem MereologicalSyntax.Parthood.IsDomain.subjoins {α : Type u_1} [DecidableEq α] {P Q : Parthood α} {x y : α} {S : Set α} {b : α} (hD : P.IsDomain S b) (h : P.Subjoins x y Q) : Q.IsDomain S b

A licensed subjunction keeps a domain a domain: a part inside it subjoins outside only from the edge of b, and then as a 2-part.

theorem MereologicalSyntax.Parthood.IsDomain.derives {α : Type u_1} [DecidableEq α] {P Q : Parthood α} {S : Set α} {b : α} (hD : P.IsDomain S b) (h : P.Derives Q) : Q.IsDomain S b

theorem MereologicalSyntax.Parthood.IsDomain.eq_or_nPart_two_of_derives {α : Type u_1} [DecidableEq α] {P Q : Parthood α} {S : Set α} {b γ β : α} (hD : P.IsDomain S b) (h : P.Derives Q) {n : Dim} (hγ : γ ∈ S) (hβ : β ∉ S) (hγβ : Q.Imm n γ β) : γ = b ∨ Q.NPart Dim.two γ b

In every derivation, an object inside a domain of b that has become a part of something outside it is b itself or a 2-part of b, which is successive cyclicity.

theorem MereologicalSyntax.Parthood.IsDomain.not_reaches {α : Type u_1} [DecidableEq α] {P : Parthood α} {S : Set α} {b c γ β : α} (hD : P.IsDomain S b) (hc : P.Imm Dim.two c b) (hγ : γ ∈ S) (hγb : γ ≠ b) (hγc : γ ≠ c) (hdc : ¬P.Descendant γ c) (hβ : β ∉ S) : ¬P.Reaches γ β

A filled 2-part is a strong island: once c is the 2-part of b, no derivation makes an object inside a domain of b, other than b, c and the parts of c, a part of anything outside the domain.