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$.


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$?

  • 1
    $\begingroup$ In light of Emil's comment, I think your definition of Nat is incorrect - it states that there is no minimal element below x, while it should rather state that there is no limit element below x. $\endgroup$
    – Wojowu
    Jul 11, 2019 at 12:19
  • 3
    $\begingroup$ Koepke in “Ordinals, Computations, and Models of Set Theory” gives a theory SO in the same second-order language that is mutually interpretable with ZFC. The most striking difference from your theory is that SO includes a powerset axiom. $\endgroup$ Jul 11, 2019 at 14:22
  • 2
    $\begingroup$ There is a substantial literature on similar theories, e.g. mathoverflow.net/questions/230504/…. Why should mathematicians focus on the ideas here, when there are proved and published results about so many better-developed alternatives? $\endgroup$
    – user44143
    Jul 11, 2019 at 17:29
  • 3
    $\begingroup$ @ZuhairAl-Johar I am almost sure that it is possible to interpret $\mathsf{ZFC}$ in this system via development of $L$ inside it. Namely to do it via codes for constructive sets. A constructive code of a level $\alpha$ is a string $c=(\alpha,\varphi(x,\vec{y}),\vec{p})$, where $\vec{p}$ are codes of levels $<\alpha$; here $c$ denotes the set $ev(c)=\{x\mid L_{\alpha}\models \varphi(x,\vec{ev}(\vec{p}))\}$. And the key part of check would be to show for any externally fixed $n$ (using axiom Size) that for every $\alpha$ there exists $\beta>\alpha$ such that $L_{\beta}\equiv_n L$. $\endgroup$ Jul 11, 2019 at 19:05
  • 3
    $\begingroup$ @ZuhairAl-Johar This will give the axiom of Collection in $L$. And next formalizing standard fact about $L$ in your system to show that $L$ is a model of $\mathsf{ZFC}$. Here we should obtain PowerSet axiom from existence of successor cardinals. However, of course, it would require a lot of routine work to really check that all indeed works fine. $\endgroup$ Jul 11, 2019 at 19:09

1 Answer 1


I think the theory presented here is equi-consistent with ZFC since it interpret Takeuti's system presented in his article: Construction of the set theory from the theory of ordinal numbers.

All axioms 1.1 - 1.17 can be captured in the extended form of second order arithmetic presented in this posting.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.