The following system I'd label as "Infinite Arithmetic" is simply an endeavor to extend second order arithmetic to the infinite ordinal world, and extending with it the representation of ordinals by binary numerals defined here as small binary tuples not ending by a tale of zeros. The aim is to interpret sets in this kind of arithmetic in a manner that bears great resemblance to Ackermann's interpretation of sets in finite arithmetic. Actually I think along these lines we could possibly get Set Theory to be bi-interpretable with Infinite Arithmetic. The question is about the extent to which this can be done without using concepts outside of arithmetic.
Language: bi-sorted first order logic with equality
Sorts: First sort written in lower case standing for ordinal numbers. Second sort written in upper case $(A,B,C,..;{\frak A,B,C}..)$ standing for classes of ordinal numbers.
Primitives: $=, <, + , \times,\epsilon, v$
$=,<,\epsilon$ are binary relations; $v$ is a partial unary function; and $+, \times$ are first sort total binary functions.
Syntactical restrictions: $<,+,\times$ only take first sort terms as arguments. $\epsilon$ relates first sort terms on the left to second sort on the right. $v$ sends second sort terms to first sort terms.
Axioms: The usual bi-sorted ID axioms, and:
Sorts: $\forall x \, \forall A: x \neq A$
Areflexive: $x \not < x$
Transitive: $x < y < z \to x < z$
Connected: $x \neq y \leftrightarrow [x < y \lor y < x]$
Well-Founded: if $\phi$ is a formula, then: $\phi(x) \to \exists a: \phi(a) \land \forall b: \phi(b) \to b \not < a$
Infinity: $\exists l: l \text{ is limit }$
Define: $l \text{ is limit} \iff \exists k \, (k < l) \land \forall r < l \exists s: r < s < l$
Replacement: if $\phi, \psi$ are formulas; then:
$[\phi: \psi \rightarrowtail y < l] \to \exists k: \forall x (\psi(x) \to k > x)$
Where, $[\phi: \psi \rightarrowtail \pi]$ is defined by: $\forall x \,[ \psi(x) \to \exists y: \pi(y) \land \phi(x,y)] \land \\ \forall a,b,c,d \, (\phi(a,b) \land \phi(c,d) \to [a=c \leftrightarrow b=d] )$
Define: $x=0 \iff \forall y: x \leq y $
Define: $S(x)=y \iff y > x \land \forall z > x \, (y \leq z)$
Addition: $ a + 0 = a \\ a + S(b) = S(a+b) \\ a + b = b + a \\ \lambda + \zeta = \underset {\alpha \to \zeta} \lim (\lambda + \alpha) \\\text{; for limits } \lambda, \zeta \text{; and } \lambda \geq \zeta $
Multiplication: $a \times 0 = 0 \\ a \times S(b) = a + (a \times b) \\ a \times b = b \times a \\ \lambda \times \zeta = \underset {\alpha \to \zeta} \lim (\lambda \times \alpha) \\\text{; for limits } \lambda, \zeta \text{; and } \lambda \geq \zeta$
Where, $\underset {\alpha \to \zeta} \lim f(\lambda,\alpha) = \min x: \forall \alpha < \zeta (x > f(\lambda,\alpha))$ Where: $(\min x: \phi(x,\lambda))=y \iff \\\phi(y, \lambda) \land \forall x \, (\phi(x,\lambda) \to y \leq x)$
Define: $\langle a, b \rangle= [(l_{(a,b)} \times l_{(a,b)}) \times b ] + [l_{(a,b)} \times a]$
Where $l_{(a,b)}$ is the smallest limit ordinal strictly bigger than both $a$ and $b$
So $\langle \rangle$ acts as an ordered pairing function.
Extensionality: $\forall X \forall Y \, (\forall a (a \ \epsilon \ X \leftrightarrow a \ \epsilon \ Y) \to X = Y)$
Comprehension: if $\phi$ is a formula in which $X$ is not free; then: $$\exists X \forall y \, (y \ \epsilon \ X \leftrightarrow \phi)$$
Define: $\operatorname {Card}(x) \iff \forall y < x \, \neg \exists f ( f: prior(x) \rightarrowtail prior(y) )$
Where: $prior(k) = A \iff \forall y \, (y \ \epsilon \ A \leftrightarrow y < k)$
where $f$ is a class of ordered pairs [defined above], fulfilling the usual requirements of being a function. And $\rightarrowtail$ here refer to being an injection defined as usual.
Successor Cardinals: $\forall x \, \exists y: \operatorname{Card}(y) \land y > x$
Uniqueness: $v X = v Y \to X=Y$
Define:
$\begin{align}\operatorname {binarytuple}({\frak A}) \iff & \operatorname {function}({\frak A}) \land \\ &\forall x \ \epsilon \ {\frak A} \, \exists y: x=\langle y ,0 \rangle \lor x= \langle y, 1 \rangle \land \\ &\forall a \forall b \forall c \, ( \langle b,c \rangle \ \epsilon \ {\frak A} \land a < b \to \exists z: \langle a,z \rangle \ \epsilon \ {\frak A}) \end{align} $
Define:
$\operatorname {Numeral}({\frak A}) \iff \\ \operatorname {binarytuple}({\frak A}) \land \exists l: l= \lim {\frak A}= \lim^+ {\frak A} $
Where $\lim; \lim^+$ are defined by:
$l = \lim {\frak A} \iff \forall x (\exists y \, (\langle x,y \rangle \ \epsilon \ {\frak A}) \leftrightarrow x < l)$
$l = \lim^+ {\frak A} \iff \forall x (\exists y \, (\langle y,1 \rangle \ \epsilon \ {\frak A} \land x \leq y) \leftrightarrow x < l)$
So, Numerals are small binary tuples not having an ending tale of zeros.
Valuation 1: $\operatorname {Numeral} ({\frak A}) \to \exists x: x=v \frak A$
Valuation 2: $\operatorname {Numeral}({\frak A}) \land \langle x, 1 \rangle \ \epsilon \ {\frak A} \to x < v{\frak A} $
Totality: $\forall x \exists {\frak A}: \operatorname {Numeral}({\frak A}) \land x=v {\frak A}$
Now, the motivation for the above is clearly intimate to arithmetic, it is just about extending arithmetic to the infinite realm and also extending representability of numbers by binary tuples to the infinite realm as well. However, doing so turns to enable us to define sets along lines vastly similar to Ackermann's interpretation in the finite realm.
Define: $\operatorname {Set}(x) \iff \exists {\frak A}: \operatorname {Numeral} ({\frak A}) \land x= v \frak A$
Define: $y \in x \iff \exists {\frak A}: \operatorname {Numeral}({\frak A}) \land \langle y,1 \rangle \ \epsilon \ {\frak A} \land x= v{\frak A}$
Here, with this axiomatization all ordinals would be sets. This would straightforwardly provide an interpretation of $\sf ZFC-Power$ over the ordinals of this theory. But, even without the last two axioms, I think that $\sf ZFC$ can still be interpreted over some ordinals that are hereditarily values of binary numerals through constructing $L$ within them.
If we want to get $\sf ZFC$ interpreted over all ordinals, i.e. $({\sf ORD}, \in) \models \sf ZFC$, and so obviate the need for interpreting it through $L$, then we need to add a third valuation axiom that is arithmetically motivated:
Valuation 3: ${\frak A,B} \text { are} \operatorname {Numerals} \land \lim {\frak A} < \lim {\frak B} \to v{\frak A} < v {\frak B}$
/
Is the valuation function $v$ dispensable with? That is, can it be definable in the language $\sf FOL(=,<,+,\times, \epsilon)$ of second order arithmetic?
Can a weaker valuation function $v^*$ satisfying just the axioms of uniqueness and first valuation, be defined in the language of second order arithmetic?
Is it possible to dispense with both $\epsilon$ and $v$ [or $v^*$] altogether? That is, define both in the language $\sf FOL(=,<,+,\times)$ of first order arithmetic using the rest of axioms of this theory?
