How to prove that Gödel's Incompleteness Theorems apply to ZFC?
Solution 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.)
Solution 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.