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$



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

  • $\begingroup$ At a glance it's definitely consistent relative to $\mathsf{ZFC}$, since (unless I'm missing something) it's straightforwardly interpretable in it. $\endgroup$ Commented Sep 25, 2023 at 17:32
  • $\begingroup$ @NoahSchweber, I was thinking of interpreting $\sf ZFC$ in this system through defining ordered pairs, which I think its feasible, then define well founded extensional graphs, but the problem is in defining the latter, I need a kind of collective function that is definable in arithmetic. $\endgroup$ Commented Sep 25, 2023 at 18:01
  • 2
    $\begingroup$ Takeuti's "A Formalization of the Theory of Ordinal Numbers" might be relevant to your question. He proved that his theory of ordinals interprets $\mathsf{ZFC}$, although his theory is different from yours. $\endgroup$
    – Hanul Jeon
    Commented Sep 25, 2023 at 22:03

1 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).

  • $\begingroup$ At the very end, you mean “in PA+Con(ZFC)” not “in PA+Con(PA)”, right? $\endgroup$
    – Gro-Tsen
    Commented Sep 25, 2023 at 21:21
  • $\begingroup$ Yes, now fixed. Thanks! $\endgroup$ Commented Sep 25, 2023 at 21:22
  • $\begingroup$ How does one even express completeness theorems in the language of PA? $\endgroup$
    – Wojowu
    Commented Sep 25, 2023 at 22:26
  • 2
    $\begingroup$ @Wojowu There are various effective versions of completeness. But one general claim is the scheme: every consistent definable theory is contained in a complete consistent definable Henkin theory. This is a way of expressing the existence of an interpreted model. A more effective formulation is: every decidable theory has a decidable complete consistent Henkin theory. Basically, the proofs follow the classical Henkin proof, but note effectivity. $\endgroup$ Commented Sep 25, 2023 at 22:36

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.