How to prove that Gödel's Incompleteness Theorems apply to ZFC?

Question

Let us denote Robinson Arithmetic as Q and Primitive Recursive Arithmetic as PRA. Let $T$ be a formal theory formulated in the language of arithmetic. According to this page on the Stanford Encyclopedia of Philosophy, the first incompleteness theorem applies to $T$ if $T$ contains Q, and the second incompleteness theorem applies if $T$ contains PRA. If $T$ is not formulated in the language of arithmetic, then the first and second incompleteness theorems hold for $T$ if we require that Q and PRA, respectively, can be interpreted in $T$. The Stanford page then goes on to say that

Roughly, a theory $T_1$ is interpretable in another theory $T_2$ if the primitive concepts and the range of the variables of $T_1$ are definable in $T_2$ so that it is possible to translate every theorem of $T_1$ into a theorem of $T_2.$

I am wondering what the precise definition is for $T_1$ to be interpretable in $T_2?$ Moreover, how would one go about showing that Q and PRA are interpretable in ZFC? Peter Smith's answer to a similar question clarifies that the conditions specified on the Stanford page leave out that $T$ must be effective (recursively axiomatizable). Smith goes on to say that

you show that you can interpret arithmetic in ZF(C), and -- with the appropriate renditions -- the axioms of Robinson Arithmetic are theorems of ZF(C), and so off you go again.

Once I have a precise definition for what it means for one theory to interpret another theory, my next question is, how do we prove that Q and PRA are interpretable in ZFC? If this would be an excessively long answer, then I would appreciate recommendations of relevant book titles.

When I was searching for ways to interpret an arithmetic theory in ZFC, I came across Henning Makholm's answer to this question. I see that, if $D$ is the domain of discourse, we can define the successor function $S:D\rightarrow D$ using the ZFC axioms as $S(x) = x\cup\{x\}.$ However, without the model of the von Neumann Universe, which defines an ordinal, how should we define addition and multiplication?

Answer 1

The notion of interpretability you want is called a relative interpretation of one first-order language $L_1$ in another first-order language $L_2$. I can't find a good online reference for this. The following is taken from memory from Mendelson's Introduction to Mathematical Logic.

For simplicity, let us assume $L_1$ has no function symbols. Then a relative interpretation comprises two things (1) a function mapping each $n$-place predicate symbol $p(x_1, \ldots, x_n)$ of $L_1$ to a formula $\phi_p(x_1, \ldots, x_n)$ of $L_2$ and (2) a formula $\delta(x)$ of $L_2$ (where all formulas have only the indicated variables free). You then map an arbitrary formula $\chi$ of $L_1$ to a formula $\chi^*$, say, of $L_2$ by replacing each instance of an $n$-place predicate $p(x_1, \ldots, x_n)$ by the corresponding instance of $\phi_p(x_1, \ldots, x_n)$, then replacing each formula of the form $\forall x.\chi$ by $\forall x. (\delta(x) \Rightarrow \chi)$ and finally replacing each formula of the form $\exists x.\chi$ by $\exists x.(\delta(x) \land \chi)$.

You can now define theory a $T_1$ over $L_1$ to be interpretable in a theory $T_2$ over $L_2$ if there exists a relative interpretation of $L_1$ in $L_2$ that maps theorems of $T_1$ to theorems of $T_2$. The idea is that in any model of $T_2$, $\delta(x)$ identifies the domain of discourse of $T_1$ and $\phi_p(x_1, \ldots, x_n)$ defines the interpretation of each predicate symbol $p(x_1, \ldots, x_n)$ of $L_1$. If $T_1$ is interpretable in $T_2$, then $T_2$ can prove (the interpretation of) any sentence provable in $T_1$ (and maybe many more).

The mathematical details of a relative interpretation of $Q$ or $PRA$ in $ZF$ are then as suggested by Asaf Karagila's answer. First of all you have to reformulate the language of arithmetic using just predicates (so for example, you replace + by a three-place predicate $P(x, y, z)$ whose intended interpretation is $z = x + y$). Then you take $\delta(x)$ to be $x \in \omega$, and map the predicate symbols to appropriate formulas denoting the usual set-theoretic representations of the functions and predicates of the language of arithmetic (which can all be defined in terms of the successor operation $n \mapsto n \cup \{n\}$ using quantification over subsets of $\omega$, $\omega^2$ and $\omega^3$, see the answers to Why are addition and multiplication included in the signature of first-order Peano arithmetic? and How to define multiplication in addition terms in monadic second order logic? for details). (Here I am writing as if $\omega$ was a constant in the language of ZF, whereas ZF is usually set up to have only one non-logical symbol $\in$, so that $x \in \omega$ has to be read as shorthand for some complicated formula asserting that $x$ belongs to every set that contains the empty set and is closed under successor.)

Answer 2

The ordinal arithmetic matches perfectly the usual arithmetic of the natural numbers when restricted to the finite ordinals. And not by accident, since both can be defined by recursion from the successor operator.

Then we can show that you get a model of Peano Axioms, even if you consider the second-order induction axiom. To see this, note the axioms about arithmetic hold because of the inductive definition (which is exactly what the relevant axioms in Peano say), and the induction axiom holds because $\omega$ is the smallest inductive set.

You can also use cardinal arithmetic, which also coincides with those two when it comes to finite ordinals.