We’ll start with a puzzle, taken from Hofstader’s Godel, Escher, Bach. In this puzzle, we are going to learn to speak in a restricted language. We will be talking about integers, so our variables will always stand for integers. We have available to us the ordinary arithmetic operations , , , and the relations , , , , , . We have the logical connectives: "AND", "OR", "NOT", "IF … THEN" and the quantifiers "THERE EXISTS" and "FOR ALL".
So we can say " is prime", because we just say "There do not exist and , both , with ." Or we can say “Every nonnegative integer is a sum of four squares”; we just say “If then there exist , , and such that .” The technical phrase here is that we are speaking the first order language of integers.
Puzzle: Within this limited vocabulary, express the statement .
Why is this puzzle important? In Godel’s proof of the undecidability of Peano Arithmetic, he took theorems and proofs and encoded them as integers. He then needed to express “ is a proof of ” as a sentence in the vocabulary of first order logic. When you think about how challenging the above puzzle is, and how much more complicated “ is a proof of ” is than ““, this should astonish you.
There are a lot of great popular introductions to the overall structure of Godel’s proof. Most of them gloss over HOW Godel solved this technical problem. My goal in this post is to discuss precisely this point, and ignore the larger questions. I will take the view that expressing things in the first order language of arithmetic is a worthwhile goal in its own right, and will show you how surprisingly strong this language is.
Below the fold, I’ll solve the puzzle. Then I’ll show how to express some more serious ideas.
First, a basic construction:
By ““, we mean “ and there exists such that .”
So, when we write , this is a statement of first order logic.
Now, without further ado, the solution:
There exist , and such that
- For all , there exist and such that , and .
I urge you to stare at this a lot, and convince yourself that it works. For any finite sequence ; we can find such that .
This is the trick everything else will be based on. By giving only three integers , we have managed to encode an entire sequence of integers. Obviously, we could modify this trick to say “” or “ is the -th Fibonacci number.”
The next statement says that the recursion, starting at , terminates:
There exist nonnegative integers , , and such that
- For all , there exist and such that , , if is even then and, if is odd, then .
Now, we are encoding a list of length by giving a quadruple of positive integers. It will be convenient to have a way to encode a list by just one integer. That’s easy enough. Just take the previous example and change it to read
There is a nonnegative integer such that there exist nonnegative integers , , and with and
Of course, I use binomial coefficients as a convenient shorthand. The right hand side is some polynomial in , which we could write out in full if we wanted.
The point is, given any nonnegative integer , there is exactly one way to express it as this sum of binomial coefficients. So we can encode four integers in one. And those four integers, in turn, can encode a list of finite length.
We’re going to be using this idea a lot, so let’s create notation. will mean “the -th term of the list encoded by ” and will be “the length of the list encoded by .” I could always unravel this to talk about and if I wanted to. (But I don’t!)
Here’s a nice example:
If is prime, then there is some with such that
- and .
- For to , , and, for to , .
- For , there is a such that .
Do you see what’s going on here? is a list of lists, encoding the first rows of Pascal’s triangle. This states the (true) theorem that is divisible by .
The ability to talk about lists of lists is incredibly powerful. It can also be very confusing. In one of Douglass Hofstadter’s essays, he says something like: “Godel’s paper isn’t a mathematical paper at all; it’s a LISP compiler!” And, indeed, most of the length of the paper comes down to saying how to convert very simple statements about lists into very long statements about arithmetic relations between integers.
In this analogy, the first order language of arithmetic is assembly language. What is C? This is the first order language of hereditarily finite lists of integers. Our variables will denote either integers or finite lists whose elements are either integers or finite lists whose elements are either integers or finite lists , so something like
The important point is that we do not have infinite branching or infinite nesting.
We will, again, have all the logical symbols "AND", "OR", "NOT", "IF … THEN" and the quantifiers "THERE EXISTS" and "FOR ALL". We will have the statements “is an integer” and “is a list”. For integers, we will have all the arithmetic operations and relations we had before. We also have basic operations on lists. For example, if is a list and an integer, we have the operations and .
The next few screens will address some technical points. To keep you interested, here is another puzzle:
Puzzle 2: Let be the function which takes a hereditarily finite list of integers and returns the list where every integer, at any level of nesting, has been doubled. Express the sentence in the first order language of hereditarily finite sets of integers.
There is one very technical point to warn you about. Since the language of arithmetic only has integers, we have to use integers both to encode lists and to encode integers. We can solve this in many ways; a traditional solution is to use odd integers for lists and even integers for actual integers. So the sentence
in the language of hereditarily finite lists of integers.
has to be compiled to
in the language of integers.
I will completely hide this issue from you in the future, but the first book I read about this didn’t point it out, and it freaked me out for a while when I realized the issue existed.
Hereditarily finite lists of integers are a vastly nicer language than integers. There is one immediate problem. Depending on exactly how we set up our encoding of lists by integers, we might be able to encode the list that contains itself. We could probably dodge that by choosing our encoding right, but it’s easier to just write down a statement that says that is hereditarily finite. Here’s a solution; it is worth reading carefully:
There is a list such that and, for between and , either
- is an integer
- is a list and, for between and , there is a , with , such that .
Do you see how this works? Every subobject which occurs anywhere in , at any depth of nesting, must occur as an object of . As an imperfect analogy, you can think of this as like the way that very complicated data structures are flattened into a linear computer memory.
We can use this trick to define recursive functions on hereditarily finite lists, the same was as we used lists to define recursive functions on numbers. For example, we now give the solution to puzzle 2.
There are two lists and , with , with and and such that,
for between and , either
- and are integers with
- and are lists of the same length and, for between and , there is a such that and .
Again, I encourage you to stare at this until you see that it says what it is supposed to.
So we can do recursion! We are now something like ‘s of the way to LISP.
There is an important point which I’ve glossed over. We can have two different integers encode the same list. All the
code first order sentences which I have written so far will work just fine if you read the symbol to mean “are the same actual integer, in the low level encoding.” But we also do need a way to say that two lists are equal, however they are encoded. To solve this, take the block above and just remove the multiplication by . We’ll write for this more general notion of equality.
At this point, you should be able to write Godel’s proof. Assign numbers to characters like , , and so forth. Figure out how to say things like “ is a grammatical sentence, containing the unbound variable .” Keep pushing and, now that we have a decent language for handling lists and recursion, it is not that hard to write sentences that say we have a valid proof.
I’m going to go in a different direction, and explain why I started writing this post. Over at Math Overflow, I asked the question “What is induction up to ?” I didn’t realize it at the time, but I was basically asking someone to write me a multi-screen blogpost. So, now that I understand, I have written that post. Let me explain how to encode .
I’ll say that
if one of the following is true:
- and are integers with
- is an integer and a list
- and are lists and either
- There is some , with such that
- , for
- for .
This gives us a total ordering on all hereditarily finite lists of integers. (Thanks to Allison Miller for pointing out that my previous definition didn’t work.) Roughly, we do a depth first search of and , looking for where they first differ. We rank large integers above small integers, and lists above integers.
Exercise for the reader: convince yourself that the relationship really can be written in the first order language of hereditarily finite lists of integers. This will get you a lot of practice in unfolding recursions.
Now that we can compare lists, we can sort lists of lists.
is sorted if either
- is an integer or
- is a list so that
- for and
- is sorted for .
SOME PREVIOUS ERRORS ARE NOW FIXED Define a pure list to be a list whose elements are either pure lists or the empty list. (Details are left to you at this point.) So, something like .
Now, I can define . The ordinal is the set of all pure sorted lists, under the relation .
Here are the first few elements of , along with their more standard notations:
I think you can see why no one wanted to write out a complete answer to “How do you encode in the first order language of integers?” on Math Overflow!