Gödel Numbering

The technique known as Gödel Numbering, which is really something very simple, is the key to understanding why formal systems for arithmetic cannot be both complete and consistent.

What it Is

A Gödel numbering of a formal system is an encoding of formulae in the system into natural numbers, such that a formula is always uniquely recoverable from its code.

Yes, that is an isomorphism.

Example

One possible Gödel numbering of the MIU-system begins with assigning a code to each symbol:

M ⇔ 3
I ⇔ 1
U ⇔ 0

and then coding strings in the obvious way; for example:

MIUIU  ⇔ 31010
MU     ⇔ 30
IUMM   ⇔ 1033

Why It Matters

Once you have an encoding, you can talk about any formal system and its properties by talking about natural numbers and operations on numbers. For example, we can "translate" the inference rules of the MIU-system as follows:

Now the question "Is MU a theorem of the MIU-system?" is isomorphic to "Is 30 a MIU-number?"

Exercise: Use arithmetic reasoning to show that 3010 is a MIU-number.

The "discovery" by Gödel that typographical derivations in formal systems are isomorphic to arithmetic operations on natural numbers is thought by some to be a big deal (like the isomorphism between equations of two variables and curves in the plane).

Whether a big deal or not, we use isomorphisms like this to answer questions about a "hard" domain by mapping the problem into an "easier" domain and working there. We can then map the answer back out if we need to.

Exercise: Describe some instances of where this way of working is done. You'll undoubtedly need to do some research for this.

Something to Think About

Suppose you had a formal system that was r.e. but not recursive, and you came up with a Gödel numbering for it. Now consider the set of all numbers S that are not encodings of some theorem in the system. Could there exist a computer program that given some number can tell you whether or not it is in S?

Codes and Meaning

The statement "30 is a MIU-number" can be represented in TNT. It would be gazillions of characters long, but it can certainly be written.

But by the isomorphism, this TNT string is really just an encoding of the statement "MU is a theorem of the MIU-system," right? But wait — aren't ALL messages conveyed in some code? The page you are reading now is "coded" in English, right?

Hofstadter writes:

But in reality there is no such thing as an uncoded message ... only messages written in more familiar codes and ... less familiar codes. If the meaning of a message is to be revealed it must be pulled out of the code by some sort of mechanism, or isomorphism. ... When a code is familiar enough, it ceases appearing like a code; one forgets there is a decoding mechanism. The message is identified with its meaning.

and continues:

Gödel's isomorphism is a new information-revealer, just as the decipherments of ancient scripts were information-revealers.

leading to the moral of the story:

Meaning is an automatic by-product of our recognition of any isomorphism.

A Gödel Numbering for TNT

Okay, so we can encode any statement of the form "A is a theorem of formal system S" for any formula A of any formal system S, into a statement of number theory. Then we can use TNT (or other formalization of number theory) to see if that statement is true by seeing if the encoded statement is a theorem of TNT.

Wait... any formal system?

Self-Reference

You probably guessed the next question... any formal system including TNT?

Of course.

Now suppose we were able to encode a statement G, that says "G is not a TNT-number," or equivalently, "G is not a theorem of TNT." What can we say about G?

The second option looks worse, so we'll take the former. Looks like there are true statements that you can't derive in a formal system — true statements you can't prove. You can't have a "perfect" formalization of number theory.

What is this Sentence G?

We'll see how to make it later. It is not as easy as you might think; there is a neat little trick you have to employ to make a sentence truly self-referential.

TNT is Undecidable

Since neither G nor ~G is a theorem of TNT, TNT is undecidable. Said another way:

If we ask TNT whether the statement is true, TNT says neither yes nor no.

You can answer "mu."