# Is ZFC interpretable in a kind of an extended form of second order arithmetic?

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

• 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. – Wojowu Jul 11 at 12:19
• 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. – Emil Jeřábek Jul 11 at 14:22
• 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? – Matt F. Jul 11 at 17:29
• @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$. – Fedor Pakhomov Jul 11 at 19:05
• @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. – Fedor Pakhomov Jul 11 at 19:09