How Goedel Sentences Work

Please help refine the following explanation and move any discussion to the bottom of the page.

The idea behind Goedel sentences is that they say something like "This statement cannot be proved by formal system such and so". On the face of it, this statement seems to be both true and unprovable by formal system such and so. But we have to be careful with such self-referential sentences. Similar constructions (like BertrandRussell's famous barber who shaves every man who doesn't shave himself -- the barber is a woman) have turned out to be paradoxical and meaningless. We have to be much more precise about what we mean by the words "statement", "proof" and "formal system".

Statements are made in a very precise formal language (first order logic). Many variations of such languages are known. We'll consider one such variation here.

Our language is made up of a number of symbols:

We haven't yet said what these symbols mean, but of course you can already guess what we mean by them. For the time being we'll leave it at that. For those who are interested in the details, see SyntaxOfFirstOrderLogic.

[derivability vs truth]

Now let's turn to the question of what exactly we'll accept as a proof. As many people will have found out as a child, you can always keep asking "why?" no matter what people answer. This gets annoying pretty quickly. We have to stop somewhere and consider some things as self-evident. These self-evident truths are called axioms. Many of the axioms commonly used in mathematics seem so obvious that they are almost as annoying as the child who keeps asking "why?". Many other self-evident truths would strictly speaking require a proof from the axioms. Asking "why?" doesn't add understanding in this case, but it does allow us to keep our set of axioms as small as possible, which is desirable for a number of reasons.

[Goedel numbers]

In Goedel's proof of incompleteness, he encodes the statements of the theory by mapping each statement to a unique natural number. The number that a statement is mapped to is referred to as the Goedel number of that statement.

[First order logic formula for computing whether a sentence with a given Goedel number n is a proof of a sentence with Goedel number m. Not many people will doubt this can be done in C++, therefore it must be possible in Prolog, which is a subset of first order logic.]

[By adding a simple "exists" we now have an arithmetical predicate F(x) with one free variable x that looks innocuous but is in fact logically equivalent to the statement "The sentence with Goedel number x cannot be derived in the system". From this sentence we can compute its Goedel number k. If we plug k into the free variable, we get the true but unprovable sentence F(k).]

This is not quite right...

It's an instructive mistake though, so I haven't changed it. The problem is that k is the Goedel code of F(x), not of F(k), and F(k) has some different Goedel code k'. Somehow, you have to tie up the recursion and get F to refer to itself. The solution is basically the same trick as you might have seen used by programs which print a listing of themselves. In this case, you need to use a code both as a sentence and as a verbatim number. Write a formula G(x) whose meaning is the following: "The result of substituting the number x for the free variable in the formula H(x) with code x is a statement that is not provable." Let k be the code of G(x), and consider the statement G(k). If G(k) is true, then the result of substituting k into G(x) is not provable, but this means G(k) is not provable. If G(k) is false, then the result of substituting k into G(x) is provable, but then G(k) is provable and the formal system is inconsistent. So any sufficiently powerful consistent formal system has unprovable statements. Thanks, I had missed that subtlety. I'll try to weave your correction into the explanation.

This is far too complicated. The following is sufficient. Perhaps the original author will consider using this simplified version?

The list below is sufficient, but I think the original is easier to understand and leads to more readable "code" to express derivability. But I agree the explanation is far too difficult. Since people will already have an understanding what the symbols mean, it is probably best if we don't give precise production rules and semantics yet.

True, but if you actually want to carry out the whole proof of Goedel, the way to go is to stick with the simpler notation, and then add "syntactic sugar" that says that a sentence like "Ex P(x)" actually means "(Ax(P(x)=>F)=>F)". But it is not clear to me if the intent of this page is to carry out the whole formal proof of Goedel, into every nitpicky detail, or that the goal is to give a "popular-scientific" explanation.

We haven't yet said what these symbols mean, but of course you can already guess what we mean by them. But before we go on to define the meaning of various combinations we want to give the rules that describe what the legal (grammatically correct) combinations of these symbols are. We'll use a BNF like notation.

Term -->Number 

|->Variable
|->( Term + Term)
|->( Term * Term)
Variable --> x 
|-> x Variable
Number--> /* empty */ 
|-> 1 Number
Number are indicated by a couple of 1's in a row: 0 is indicated by nothing; there can be no confusion.

Predicate: --> (Predicate & Predicate) 

|-> (Predicate | Predicate)
|-> (Predicate => Predicate)
|-> (Term=Term)
|-> (Term<Term)
|-> A Variable Predicate
|-> F

Something should be said about the axioms needed. To get an expressive language, we need some form of induction. Without induction, the formal system may be able to prove that (1+1 == 1+1) and (2+1 == 1+2) and (3+1 == 1+3) and so on, but it will not get the point that (forall n . n+1 == 1+n). So we want to add an axiom that says that for every predicate p (p(0) and (forall n . p(n) ==> p(n+1)) ==> forall n . p(n)). Actually this axiom defines the structure of our natural numbers.

Now for the Goedel Sentence itself. It is a sentence s of the form (forall n . not prooves(n,s))), with some trickery to get s to refer to s inside. The interesting bit is that without inducion this is trivially unprovable (and uninteresting), but with induction we get the famous contradiction and this sentence is still unprovable. The formal system will be able to show that 1 does not prove s, 2 does not prove s, 3 does not prove s, and so on, but be unable to generalize this to all numbers.

You don't need the full induction axiom, you can replace it with forall x . x = 0 or exists y such that Sy = x. The resulting system is called RobinsonArithmetic and it's the minimum amount of arithmetic needed to for GoedelsIncompletenessTheorem.

I lie all the time. 

"This statement is a lie."
The first lie is that you lie all the time. Sometimes you just make meaningless utterances. On the other hand, This assertion is false.

False or void? 

         :       Bah, just cheating, therefore meaningless.  In a cleanly defined language you cannot say "this statement".  (Okay, you could define fixed point semantics for such a language, but then your statement has no fixed point and is therefore still meaningless.)  Anything containing "this statement" is no proper characterization of Goedels work, it's a paraphrase at best.

(FlameBait Follows) If the intent of HowGoedelSentencesWork is either "to carry out the whole formal proof of Goedel, into every nitpicky detail" or "to give a 'popular-scientific' explanation", then I recommend simply replacing the above text with the URL to DouglasHofstadter's GoedelEscherBach. -- TomStambaugh

EditText of this page (last edited July 21, 2014) or FindPage with title or text search