Concatinative Set Theory

Concatinative Set Theory:

The main idea of this theory is for numbers to be defined as functions over bundles of sticks after similarity, two bundles would be called similar if they look similar, all sticks are similar, addition of similar things to similar things would result in similar things. This theory builds the bundles of sticks through the concatenation function, which suffice to define the addition operator and individual numbers, then the set concept [in particular sets of disjoint bundles] comes into play actually to formalize multiplication.

Language: first order logic with equality

Sorts: two, represented in upper and lower cases.

Extralogical Primitives: ‘‘.,≅,#,∈", denoting contactination, a first sort partial binary function; similarity, a first sort binary relation; number, a total first sort unary function; and set membership, a binary relation; respectively.

Define: stick(a)⟺¬∃xy:a=x.y

Bundles: ∀x∃a∃b:stick(a)∧(x=a∨x=a.b)

Define (P): a P b ⟺ a=b ∨∃x(b=a.x)

P is read as "is a part of"

Identity: a=b ⟺ ∀c(c P a ⟺ c P b) 

Symmetry:  a.b=b.a

Associativity: (a.b).c=a.(b.c)

Define: a,b are separate¬      ⟺ ¬∃dxy[a=d.x∧b=d.y] 

Discernibility: ∃c (a.b=c)⟺ a≠b∧  a,b are separate 

Increment: ∀x∃y∃z:z=x.y

Equivalence: x≅x∧(x≅y→y≅x)∧(x≅y∧y≅z→x≅z)

Uniformity: stick(a)∧stick(b)⟹a≅b

Propagation: a.b=c⟹c≆a∧c≆b

Similarity: ∀x,y,a,b (x≅y⟹[x.a≅y.b⟺a≅b])

Numbers: #x=#y⟺x≅y

Define (1): x=1≡df∃y(stick(y)∧x=#y)

Define (+): x+y=z⟺∃a∃b (x=#a∧y=#b∧z=#(a.b))

Membership: ∀X¬∃A(A∈X)

Extensionality: ∀A∀B(∀z(z∈A↔z∈B)⟹A=B)

Discreteness: ∀X∀a,b∈X(a≠b⟹ a,b are separate)

Choice: ∀x∈A ∃!stick t (t∈C(A)∧ t P x)∧ 

∀t∈C(A)(stick(t)∧∃z∈A(t P z))

Heaping: ∀X ∃c ∀stick t (tP c⟺∃m∈X (t P m))

We denote such a set c by h(X).

Iteration ∀a,b ∃X:∀m∈X(#m=#a)∧#h(C(X))=#b

Define (××): x×y=z≡df∃M:∀m∈M(#m=x)∧#h(C(M))=y∧z=#h(M)

Comprehension: if ϕ is a formula in which X doesn't occur, then all closures of: 

∀ab(ϕ(a)∧ϕ(b)∧a≠b→a,b are separate)

∧∃k∀b(ϕ(b)→bPk)

∃X∀y(y∈X↔ϕ)

are axioms.

\Theory definition finished.

Now this theory is stronger than Q, since it can prove commutativity of addition and I think of multiplication as well.

The question is:

What's the consistency strength of Concatinative Set Theory?

This question has been posted to Math.StackExchange, under title:

A more powerful approach:

De-axiomatize discreteness, and define:

Discrete (X)  ⟺ ∀a,b∈X(a≠b⟹ a,b are separate)

Now precondition choice by Discrete(A) that is nonempty. 

And also add that X in iteration is a nonempty discrete set, and do the same with M in multiplication definition.

Now we empower comprehension by removing the first pre-condition of it, i.e. remove that the predicates must be separate! That way we only keep the second pre-condition, and thereby we can get Power Set theorem! that is for every set X we take the set {h(X)} and then we take the set of all "parts" of h(X), those are defined as the set of all p where p=h(X) or there exists l such that h(X)=p.l. This way we can get a set in which all choice heaps extracted sequentially from X are elements of!!!!!  so there would exists a set K such that:

"h(C(X)) \in K \land \forall  y,S,b (y \in K \land y=h(C(S)) \land b=h(C(S-)) \to b \in K)"

where S- is the set of all elements of X skimmed of elements of C(S).

S- = { y-i |y \in S \land  i \in C(S) \land \exists j: y=j.i }  

where z=y-i  \iff  [(stick(y) \land z=y) \lor \exists j (y=j.i & z=j)]

Now the existence of the above *inductive* set K is nice, because together with the new schema of comprehension we can get the intersection of all such sets K, and we get our desired set, which would be equal to the sets in the definition of b x a  for any a x b. Therefore proving commutativity of multiplication. 

Now how far we are from Peano arithmetic? 

If we add two axioms:

x <  y  ⟹  x P y

Then I'd think that PA would be provable! Another intuitive axiom to be added is:

#x≅x