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. $0$ is a constand symbol, $<$ is a binary relation symbol between first sort objects, it denotes "strict smaller than", and $\langle, \rangle$, depicting "ordered pair", is a *total* binary function symbol on first sort objects; while $\in$ is a binary relation symbol from first sort objects to second sort objects.

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? Or most possibly along the line of building $\sf L$ inside it!

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

This can be adopted here in a way similar to what's presented at
**SO** set theory, by adding the following axiom:

**Power:** $\forall a \exists l \exists B \forall X [X \subseteq \{m: m < a\} \to \\\exists b < l \forall x (\langle x,b \rangle \in B \leftrightarrow x \in X)]$

Of course this addition would render axiom of Successor Cardinals redundant!.

I 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 '19 at 12:19