Informally the following theory is a kind of extension of second order arithmetic, where numbers are not limited to naturals, instead here we have formation of further numbers by setting limits on sets of numbers, so here the set of all naturals have a limit, if a set is equinumerous to a set that has a limit, then it has a limit, and to form successor cardinals we stipulate that: all numbers whose anterior sets (i.e.; sets of all numbers strictly smaller than them) are equinumerous to the anterior set of a number, do also have a limit. This way we extend the set of numbers to include all possible numbers that can be accessible from below, in a way that is in some sense analogous to ordinal formation in $\small \sf ZFC$.

FORMAL EXPOSITION:

**Language:** Bi-sorted first order logic + primitives of :$ \ 0, < ,=, \in, \langle \rangle$

*Sorting:* First sort: Lower case standing for *numbers*.

Second sort: Upper case for *Sets of numbers*.

Those sorts are totally disjoint.

Formulation: The equality relation is allowed between both sorts. $0, <, \langle \rangle$ only apply to the first sort, while $\in$ is a relation from the first to the second sort only.

From those we have the following axioms about sorting:

$\forall x \forall Y (x \neq Y)$

$\exists x (x = 0)$

$\exists x (x = \langle a,b \rangle)$

** Axioms:** those of equality theory +

**Asymmetry:**$ x < y \to \neg (y < x)$

**Transitivity:** $ x < y \land y < z \to x < z$

**Connectedness:** $ x \neq y \leftrightarrow [x < y \lor y < x]$

**Well foundedness:**$ \exists x \phi(x) \to \exists x \ [\phi(x) \land \forall y (\phi(y)\to x \leq y)]$

**Start:**$\not \exists x (x < 0)$

**Succession:**$\forall x \exists y (x < y)$

**Extensionality:** $\forall z (z \in X \leftrightarrow z \in Y) \to X=Y$

**Comprehension:** $\exists X \forall y (y \in X \leftrightarrow \phi(y))$

*Define*: $X = \{y:\phi(y)\} \equiv_{def} \forall y (y \in X \leftrightarrow \phi(y))$

**Ordered pairs:** $\langle m,n \rangle = \langle o,p \rangle \to m=o \land n=p$

*Define*: $Nat(x) \equiv_{def} \forall y \leq x (\forall z < y \exists k (z < k < y) \to y=0)$

**Infinity:** $\exists l \ \forall x (Nat(x) \to x < l)$

*Define*: $|X|=|Y| \equiv_{def} \exists F(F: X \to Y \land F \text { is a bijection })$

**Size:** $\forall x,S (|\{y: y < x\}|= |S| \to \exists l \forall s \in S (s < l))$

**Successor cardinals:** $\forall x \exists y \forall z ( |\{r: r < z\}|=| \{k:k < x\} | \to z < y )$

Question: Can this theory interpret ZFC?

It is known that $\small \sf ZFC-Infinity+ \text { all sets are finite}$, can be interpreted in $\small \sf PA$ using the Ackermann functions. Can the whole of $\small \sf ZFC$ find an interpretation in this theory along generally similar lines?

[**Addendum:**] based on Emil Jeřábek comment that similar coined systems had an axiom for power set, I'll make the following note:

If we replace the ordered pair primitive $``\langle \rangle"$ by a primitive labeling *partial* function $``^*"$ from Sets to numbers, and axiomatize instead:

**Labels:** $X^* = Y^* \to X=Y$

**Power:** $\exists l \forall X [\phi(X) \to \forall x \in X (x < l)] \to \\\exists l \forall X [\phi(X) \to \exists k (k= X^* \land k < l)]$

Then I'd think this can interpret exponentiation and powering in general, and I think it would interpret $\small \sf ZFC$.

However the above presented system deliberately omitted this point in order to check if the system without it is still capable of interpreting $\small \sf ZFC$?

limitelement below x. $\endgroup$ – Wojowu Jul 11 at 12:19