One of my favourite books is Gödel, Escher, Bach, by Douglas Hofstadter. If you’re patient enough to read it all, I highly recommend it: it’s a great book about mathematics and cognitive science.

One of the main goals of the book is to motivate, and sketch a proof of, Gödel’s first incompleteness theorem. At one point, he provides some exercises in transcribing number theoretical statements in a specific implementation of Peano arithmetic he calls TNT. They’re pretty easy, but there are a couple that can really stump you if you haven’t taken any first-order logic courses, like me.

It would befit me to detail Hofstadter’s notation for TNT, but it’s not really anything out of the ordinary. We denote material implication with the archaic symbol, and negation with the tilde , but otherwise it is bog-standard, and the particulars are not that important.

Here is the relevant passage from Chapter 8 of GEB—in my 20th Anniversary Edition, it is on page 215.

A Few More Translation Exercises

And now, a few practice exercises for you, to test your understanding of the notation of TNT. Try to translate the first four of the following N-sentences into TNT-sentences, and the last one into an open well-formed formula.

All natural numbers are equal to 4.
There is no natural number which equals its own square.
Different natural numbers have different successors.
If 1 equals 0, then every number is odd.
is a power of 2.

The last one you may find a little tricky. But is it nothing, compared to this one:

is a power of 10.

Strangely, this one takes great cleverness to render in our notation. I would caution you to try it only if you are willing to spend hours and hours on it—and if you know quite a bit of number theory!

Let’s just jump right into it. I know you’re excited to see me bend over backwards to translate that last one, but I don’t like to just skip to the end of a story, however trite the crescendo.

The first few exercises are pretty much freebies, so I won’t say too much about them. Note that, as with any translation, we sometimes have to massage our goal a bit to be able to translate accurately.

All natural numbers are equal to 4.

.

There is no natural number which equals its own square.

. Note that by convention, all binary arithmetical operations must be delimited with parentheses . This was probably done to avoid worrying about disambiguation, especially later on when proving the incompleteness theorem.

Different natural numbers have different successors.

. Just as the arithmetical operations got parens, the binary logical connectives must be delimited with angle brackets . Don’t cross the streams and all that.

If 1 equals 0, then every number is odd.

. I interpret this exercise as a gentle reminder to keep your quantifiers as tight as possible.

is a power of 2.

Okay, finally something juicy. Here we must create a formula with one free variable, , which is true iff is a power of two. We have no way to directly transcribe exponentiation, as our only operations are and . So how can we state that property sufficiently simply to implement that in first order logic?

By the Fundamental Theorem of Arithmetic, every nonzero number which is not a power of two has an odd factor besides . Every odd number is a factor of , so that case is handled as well. Conversely, every factor of a power of two is either equal to or is even. So we’ll use that reformulation.

Recall that if we want to talk about a number , then we have to write it as for . Also recall that there’s nothing wrong with using in both the antecedent and the consequent, because of the tightness of my quantifier bindings.

is a power of 10.

Now we’re going to have to be even more clever than last time. The previous solution worked because 2 was prime, and we were able to get away with not caring which power of two was. But 10 isn’t a prime, and even if we want to say that , we’ll somehow need to know what that exponent is.

Well, here’s a slick math trick. Let’s just say we know what is. Since we don’t really know how to read off easily from , we’ll just sweep that problem under the rug with an . So as long as we can calculate in TNT, we can stipulate that and be done with it.

How do we do that? Well, let’s just compute the way we usually do. Namely, start with , then multiply it by times. This gives a sequence of numbers, . What makes this sequence nice is that it has some defining characteristics which are very easily beheld, even by our good friend Giuseppe: to wit, , and for all .

We can view this sequence as a certificate that equals , by asking that , and it looks like TNT is in principle smart enough to be able to verify this, since all we really need is multiplication by ten. Clearly, a certificate for can only exist iff is a power of ten, so our issue now is to write this certificate in a language that TNT can understand. It would suffice to encode as some fixed-length tuple of numbers, because then we can just existentially quantify those suckers and go home.

Our saviour comes in the form of the Chinese Remainder Theorem. If we have a pairwise-coprime set of moduli that are sufficiently large, then we can solve the system of equations

for . That guarantees the existence of an encoding. Turning that on its head, given and , we can access as the remainder of dividing by . For convenience, let’s define a relation for saying that is the remainder when dividing by :

So now we just need a convenient collection of pairwise coprime to use. I’ll go with , where is a sufficently large and highly divisible number, so that (1) , and (2) the are coprime. We can guarantee this works, because e.g. has precisely the properties we want. So our certificate will provide and . We also need to know to know when to stop and compare to .

We now have our certificate scheme , and can find one for any valid . They can get pretty large, though, especially using our overly generous estimate for . For example, works to prove that , since and . However, in our safe estimate, we took so that the least result CRT can give us is . will certify that , but our safe estimate gives and some value of .

In any case, we have enough to solve the problem, so let’s assemble the parts. Our solution will be , where

Thankfully, that’s it, and we’re done. Those poor souls who wish to prove that this method of exponentiation is well-defined in Peano Arithmetic have it way way worse because they have to fiddle with Cantor coding probably and use induction to prove the arbitrary extension of sequences. It’s a real stinker, and mathematicians are fine with this because the mere existence of a proof is good enough to justify the Laconic axiom set.

To close out, I’ve gone and done the obvious thing, which was to inline all the definitions to give you one long string of pure TNT. I’ve thrown in a couple of optimizations to shave off what I could—including obviating an by using everywhere we’d otherwise use —but we’re still at 201 symbols. So brace yourselves…

Exercise. (For all the code golfers out there.) Find a formula with less than 200 symbols. Can you beat 193?