We know how to encode expressions in any formal language, or at least any language with only finitely many symbols, in the formal language of elementary arithmetic. The language of elementary arithmetic is a formal language with only finitely many symbols. It follows that we can encode arithmetic in arithmetic! Should we?
Encoding arithmetic in arithmetic can get somewhat confusing. Consider a natural number. It can be expressed in the language of arithmetic. In fact there are multiple ways to express it, but to limit confusion as much as possible let’s restrict ourselves to its representation as a 0 with apostrophes. Then there is a unique expression in the language for each natural number. The expression has an encoding, which is a natural number. It’s not the same natural number we started with though. It’s generally much larger.
At this point I should perhaps give an example but our encoding is a modified base \({ b }\) encoding, where \({ b }\) is the number of symbols in our language, plus a further two to get the extended language. We need \({ b }\) digits and for the language that will be slightly too many for the ordinary decimal digits plus the letters of the English alphabet. I could use a language with a less impoverished alphabet, but the unfamiliarity would probably make the example create more confusion than it would eliminate.
We now have a binary relation between natural numbers, which we would express in English as “… is the encoding of …”. Can we express it in the language of arithmetic? In other words, is this relation arithmetic? In fact it’s possible to prove that it is. One approach would be to note that finding the natural number from the encoding is a relatively straightforward computation. It’s deterministic but that doesn’t prevent us from using the recipe we’ve already developed for non-deterministic computations. This chapter is already quite proof-heavy though so I won’t give the details.