Can set theory be interpreted in infinite arithmetic?

Question

Is the following system of infinite arithmetic consistent?

If so, can it interpret $\sf ZFC$?

Language: first order logic

Primitives: $\operatorname{Card}, <, + , \times,\text{^}$

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

We'll denote this language by the language of arithmetic.

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$

Addition: $ a + 0 = a \\ a + S(b) = S(a+b) \\ a + b = b + a \\ \lambda + \zeta = \lim (\lambda + \alpha)_{\alpha<\zeta} \\\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 = \lim (\lambda \times \alpha)_{\alpha < \zeta} \\\text{; for limits } \lambda, \zeta \text{; and } \lambda \geq \zeta$

Exponentiation: $a \text{^} 0 = 1 \\ a \text{^} S(b) = a \times (a \text{^} b) \\ a \text{^} \lambda= \lim (a^\kappa)_{\kappa < \lambda} \text{; for limit }\lambda$

/

Terminology:

• $[\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)]$

Answer 1

Without considering your system of arithmetic too closely, let me mention that ZFC is interpretable in Peano arithmetic, if one augments PA with the assertion that ZFC is consistent.

That is, ZFC is interpretable in PA+Con(ZFC).

The reason is that PA is strong enough to prove the completeness theorem. Since this theory knows that ZFC is consistent, it can build the Henkin model of ZFC, by completing the theory to a complete consistent Henkin theory, which provides an interpretation of ZFC in PA+Con(ZFC).