This page is keyboard accessible:
• Use Tab, Shift + Tab keys to traverse the main menu. To enter a sub-menu use the Right Arrow key. To leave a sub-menu use the Left Arrow or the Escape key.
• The Enter or the Space key opens the active menu item.
• To skip the menu and move to the main content, press Tab after the page loads to reveal a skip button.
• To get back to the top of the page anytime, press the Home key.
• For more information, click here: Accessibility   Close this tip.

Note: Full functionality of this web page requires JavaScript to be enabled in your browser.

A Simplified Explanation of Gödel’s proof - Part 2




Part 2: Formal Language Systems

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 true, but there isn’t any proof that proves them. 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.



If the proof rules aren’t well chosen, you might be able to prove a sentence as well as the opposite of that sentence. That is a big problem, since you can then prove that something is 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 proof 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 Gödel’s proof must be presenting the evidence that it is true. But no-one has ever actually explained where this vitally important piece of evidence that says that this formal sentence is ‘true’ in Gödel’s proof. Gödel’s proof is really saying 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 proof. 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 proof. 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?






Diverse opinions and criticisms are welcome, but messages that are frivolous, irrelevant or devoid of logical basis will be blocked. Difficulties in understanding the site content are usually best addressed by contacting me by e-mail. Note: you will be asked to provide an e-mail address - any address will do, it does not require verification. Your e-mail will only be used to notify you of replies to your comments - it will never be used for any other purpose and will not be displayed. If you cannot see any comments below, see Why isn’t the comment box loading?.

section divider

The Lighter Side


Paper on the diagonal proof

There is now a paper that deals with the matter of language and the diagonal proof, see On Considerations of Language in the Diagonal Proof.

section divider

Other recently added pages

The Myths of Platonism


Goodman’s Paradox


The Platonist Rod paradox


The Balls in the Urn Paradox


section divider

Lebesgue Measure

There is now a new page on a contradiction in Lebesgue measure theory.

section divider

Easy Footnotes

I found that making, adding or deleting footnotes in the traditional manner proved to be a major pain. So I developed a different system for footnotes which makes inserting or changing footnotes a doddle. You can check it out at Easy Footnotes for Web Pages (Accessibility friendly).

section divider

O’Connor’s “computer checked” proof

I have now added a new section to my paper on Russell O’Connor’s claim of a computer verified incompleteness proof. This shows that the flaw in the proof arises from a reliance on definitions that include unacceptable assumptions - assumptions that are not actually checked by the computer code. See also the new page Representability.

Previous Blog Posts

Moderate Platonism

Descartes’ Platonism

The duplicity of Mark Chu-Carroll

A John Searle Inanity

Man versus Machine

Fake News and Fake Mathematics

Ned Block’s Blockhead

Are we alone in the Universe?

Good Math, Bad Math?

Bishops Dancing with Pixies?

Artificial Intelligence

Cranks and Crackpots

The Chinese Room


For convenience, there are now two pages on this site with links to various material relating to Gödel and the Incompleteness Theorem


– a page with general links:

Gödel Links


– and a page relating specifically to the Gödel mind-machine debate:

Gödel, Minds, and Machines

Printer Friendly

All pages on this website are printer friendly, and will print the main content in a convenient format. Note that the margins are set by your browser print settings.

Note: for some browsers JavaScript must be enabled for this to operate correctly.


Comments on this site are welcome, please see the comment section.


Please note that this web site, like any other is a collection of various statements. Not all of this web site is intended to be factual. Some of it is personal opinion or interpretation.


If you prefer to ask me directly about the material on this site, please send me an e-mail with your query, and I will attempt to reply promptly.


Feedback about site design would also be appreciated so that I can improve the site.

Copyright © James R Meyer 2012 - 2018