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?