In A Formalization of the Theory of Ordinal Numbers, Takeuty interprets $\sf ZFC$ in a first order theory extending first order arithmetic to the infinite ordinal realm, while at the same time extending primitive recursive functions as well to that realm. However, his exposition is quite lengthy. Here, I'm trying to copy the basics of his idea, but doing so with less axioms, and more usual definitions of primitive recursion, though those would be extended with limit recursions to cover processing over limit ordinals.

Does this theory interpret Takeuty's first order ordinal arithmetic? Or actually more generally put:

Is there an interpretation of $\sf ZFC$ in this kind of extended arithmetic?

Language: first order logic

Primitives: $\operatorname{Card}, <, \circ , \rho$

where $\operatorname{Card}$ is one place predicate symbol denoting "is a cardinal".

We'll denote this language by the language of infinite primitive recursive arithmetic.

(Note: infinite primitive recursive arithmetic here is not to be confused with being a quantifier free formulation of the natural numbers that tries to capture finitistic reasoning. On the contrary the reasoning here is not finitistic)

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$

Cardinality: if $\phi$ is a formula in two free variables; then: $\operatorname{Card}(x) \land y < x \land [\phi: prior(y) \to prior(x), \phi \text { is one-one}] \\ \to \phi \text { is not surjective }$

Successor Cardinals: $\forall x \, \exists y: \operatorname{Card}(y) \land y > x$

Replacement: $[\phi: \psi \to prior(l), \phi \text{ is one-one}] \to \exists k: \forall x (\psi(x) \to k > x)$

Define: $x=0 \iff x=\min_{(<)} y: y=y$

Define: $S(x)=y \iff y= \min_{(<)} z: z > x$

Infinity: $\exists l \neq 0: \forall r < l \exists s: r < s < l$

Composition: $ h \circ (g_1,..,g_m) (x_1,..,x_k)= h(g_1(x_1^k),..,g_m(x_1^k))$

limit Primitive Recursion: $\\\rho(g,h)(0,x_1,..,x_k)= g(x_1,..,x_k) \\ \rho(g,h)(S(y),x_1,..,x_k)= h(y,\rho(g,h)(y,x_1^k), x_1,..,x_k) \\ \rho(g,h)(l,x_1,..,x_k)= \lim_{i \to l} \rho(g,h)(i,x_1,..,x_k) $

/

Notation & Terminology:

• $x_1^k$ is the string of symbols $x_1,..,x_k$.

• $[\phi: \psi \to \pi, \phi \text { is one-one }]$ is the following formula: $$\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] )$$

• $prior(l)$ is the formula: $(x < l) $

• $( \phi \text { is not surjective})$ in the above expression, it is exactly the formula: $$\exists b < x: \forall a \, [a < y \to \neg \phi(a,b)]$$

• the expression $\lim_{i \to l} \rho(g,h)(i,x_1,..,x_k)$ is the formula: $ \min_{(<)} y: \forall i < l \, ( y > \rho(g,h)(i,x_1,..x_k))$