Labeled Mereology

To Atomic General Extensional Mereology + Bottom, add a primitive one place partial function symbol L, signifying "the label of", an add axioms:

• 1. Distinctiveness: Lx=Ly→x=y 

  2. Labels: ∀x(∃y(x=Ly)↔[atom(x)∧x≠B]) 

     1. Where B stands for Bottom.

     2. Define: set(x)⟺∃y (y=Lx) 

  3. Introduction: atom(x)→set(x) 

  4. Labeling: if F is a definable partial function symbol from sets to sets, then all closures of:

• • 1. set(Σx:arg(x,F))→set(ΣF(x):arg(x,F)) 

    2. are axioms.

    3. Where: arg(x,F)≡df∃y(F(x)=y)

    4. and Σ is the Mereological Genuine unrestricted sum3 operator.

In English: If the sum of all arguments of a function (from sets to sets), is a set; then the sum of all images of those arguments under that function is a set too.

• 1. Infinity: ∃ set x ∀y (y atom of x→Ly P x) 

Define class membership ∈  as:

In English: a member of a class is what's labeled by a part of that class.

This is basically Lewis's definition of class membership; and in this mereological milieu it is fully extensional! (Note: In David Lewis terminology L  would be called the "Singleton" function)

What I've noticed here is the simplicity of the "labeling" scheme! Speaking about sums is the basic buildup in Mereology (as opposed to sets in set theory). This scheme readily interprets: Set union, Power, Separation, and Replacement; and thereby interpreting: pairing, Boolean union, and Collection. Actually the Labeling principle is just preservation of labeling under functional replacement of sets by sets, so it is in some sense the labeled-Mereological embodiment of the Replacement scheme for sets! But here it is much more powerful!

To note is that the Set Theory that readily emerges from this labeled-Mereological system is the one with the axioms of: Extensionality; Empty; Singletons; Infinity; and

Replacement*: if F is a definable partial function, then all closures of:

; are axioms.

Where: ‘‘x=⋃z:ϕ"is defined as:

; and ‘‘arg(x,F)"  defined as above.

Which is as strong as ZFC.

However, clearly this exposition is not readily figured out in the context of set theory, since unions are not the building bricks of set theory; members are!

This shows that labeled Mereology can stand as strong as set theory even when capturing tenets of the later in its own terms. And in some sense it appears to give a nice interpretation of the membership relation ∈ in nominalistic terms, thereby offering an interpretation of it that is in some sense nearer to the concrete realm!

Questions

• 1. Had the above system been studied before by nominalists?

  2. If so, are there known extensions of it that genuinely stem from its nature as to prove existence of large cardinals?

  3. In particular are there known set theoretic based large cardinal principles that when captured in labeled Mereology gives rise to more powerful counterparts?

That was a question I've posted on MathOverflow.