A Simplified Explanation of Gödel’s Incompleteness Proof:
Part 2

Formal Language Systems

Page last updated 11 May 2021

The first step in Gödel’s proof is the notion that a formal language can be completely and precisely defined. That requires that every symbol that can be used in the language is defined – that is the alphabet of the language. That includes every symbol that is used.

So while in English, we say that the English alphabet has 26 letters, we actually use other symbols as well – such as commas, full stops, spaces, and so on. Letters alone do not allow the creation of everything that can be said in English. It could be said that in English there are two types of alphabet. The alphabet of just the letters, and the complete alphabet that includes every punctuation mark as well as the actual letters.

Given a complete alphabet of a formal language, the next thing required is a definition of the rules of grammar for the symbols of this complete alphabet. If the rules of grammar can be completely defined, then that tells us precisely which combinations of the symbols of this complete alphabet are valid expressions of the formal language. We are only interested in the valid expressions, which we will call sentences (although some people call the sentences of the formal language formulas). As long as we’ve defined the complete alphabet and the complete rules of grammar, then we’re able to say if a sentence is a valid sentence, and we have completely defined the formal language.

Proofs in the formal language

A formal language of itself does not prove anything. So we need to be able to define precisely what a proof in the formal language is. A proof must consist of some sentences of the formal language. That means it will be a group of formal sentences. We assume that we don’t have any unnecessary sentences, so that every sentence has some part to play in the proof. If every sentence is necessary, it must have some interaction, some relationship with at least one other sentence in the group. And obviously there has to be some direct relationship between the sentence that’s proved and at least one sentence of the group.

Because of that, you can say that it follows from one or more sentences of the group. To be able to say that it follows from some other sentences, you must be able to define what that means.

The rules of inference

There must be rules that clearly state how one sentence can follow from one or more other sentences.

These rules are what are called the ‘rules of inference’.

In considering these rules, it is important to remember that we aren’t attaching any meaning to the sentences at all. We look at the formal expressions only as meaningless combinations of symbols. And that means that the rules are only rules about how to take one or more expressions – that is combinations of symbols. By following the rules, we come up with a new expression – a new combination of symbols.

As a very simple example, we suppose that we have say, the sentences abc and def, and that there is a rule saying that you can combine the first two symbols of one sentence with the second two symbols of the other sentence, so that you end up with abef. Note that that isn’t an actual rule that we use – it only demonstrates the principle.

The axioms of the formal system

Every proof has to use at least one axiom. The axioms for a formal language are formal expressions that don’t have proofs but are the fundamental expressions of the formal language from which all proofs are constructed from.

The axioms are taken to be the initial fundamentally “correct” sentences of the system. There isn’t any proof that proves them, and every system has to have these axioms which are assumptions upon which everything else is buiilt. They are the building blocks for all proofs.

For example, suppose (for the sake of illustration only) that

‘1 + 1 = 2’ is an axiom.

Then if the rules allow it you might be able to take that axiom, and end up with a new expression

‘1 + 1 + 1 = 2 + 1’

which, since it follows from the axioms and the rules of the formal system, can be said to be a proved expression of the formal language.

Note that the above is only intended to demonstrate the principle, not any actual formal language proof system.

Proof sequences in the formal system

When you use a formal language proof system to make a proof, you have to start somewhere. You start with at least one axiom, and you have a set of rules that allow you to make a new sentence. You can do that several times, and get several new sentences. You can take two of those sentences and follow the rules to make another sentence, and so on, and so on. Every sentence that you make in that way is proved. And you can keep going on and on, making more proved sentences. Every proved sentence will have a list of sentences that go together to prove it. That list of sentences that go together to make a proof is called a proof sequence (or a proof schema).

Consistency

If the proof rules aren’t well chosen, you might be able to prove a sentence as well as the opposite of that sentence (the negation of that sentence). That is a big problem, since you can then prove that something is correct and incorrect (“true” and “false”) at the same time. That means that you’ve got a contradiction. A formal language that doesn’t result in contradictions is called a consistent language. Gödel’s paper only applies to formal languages that don’t result in contradictions.

Completeness and Incompleteness

We assume that we have defined a consistent formal language that refers to numbers and has expressions that can be interpreted as making propositions about numbers. If we could say that the formal language proof system was complete, then for every proposition about numbers that could be made in that formal language, there would always be a proof of that proposition – or else a proof of its negation. So if the formal language proof system was ‘complete’, there would be no proposition about numbers that, given enough time, we could not produce a proof for it – even if the proof was very long, theoretically, it must be possible to construct the proof using only the axioms and rules of the system.

Gödel’s proof says that no matter what your formal language is, and no matter what your axioms are, and what your proof rules are, Gödel’s proof can always define a formal expression which cannot be proved by those axioms and proof rules – and neither can its negation. And if Gödel’s proof is correct, that means that every formal language proof system is what is called ‘incomplete’. Hence the name of Gödel’s proof as his incompleteness proof.

A further aspect of Gödel’s proof is that the formal expression that the proof comes up with is shown by the proof to be ‘true’, provided that the formal system is consistent.

Now, remember that the proof rules take no account of the meaning of the formal sentences. But if there isn’t any formal proof of a formal sentence, you might wonder how can the formal sentence given by Gödel’s theorem be ‘true’, since the sentences of the formal system can be created without attaching any meaning at all to the formal system. And you would be right to question that. The notion that the formal sentence given by Gödel’s proof is ‘true’ is a notion that relies on the presumption that in some way there is evidence to prove that it is ‘true’.

But if Gödel’s proof says that there is a formal sentence that is true but not provable by the formal language, then that proof must be presenting the evidence that it is true. But no-one has ever actually explained where this vitally important piece of evidence occurs in Gödel’s proof, and which says that this formal sentence is ‘true’.

Gödel’s paper is really claiming that the language of his proof is more powerful that any possible formal language. If that’s true, then you might wonder what is it about that language that makes it more powerful than a formal language. Surely, you say, there has to be some additional axiom that isn’t precisely defined in Gödel’s paper. Or else that there’s some proof rule for at least one step in the proof that isn’t precisely defined in Gödel’s paper. Because if that axiom or rule was precisely defined, you would think that that rule or axiom could be defined for a formal language. But if Gödel used some axiom or rule that could never be precisely defined, how could it be justified? Wouldn’t relying on such an axiom or rule simply be an act of blind faith, without any rhyme or reason?