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 Step by Step Guide to Gödel’s Incompleteness Proof
2: The definition of the formal system




Note that (provided you have JavaScript enabled) clicking on (hideshow) will reveal further details, while clicking again will hide it. Also, clicking on (hideshow Gödel’s) will reveal relevant parts of Gödel’s text (shown in green), while clicking again will hide it. Please note that older browsers may not display some symbols correctly.


(like this)


(like this)


From this point onwards we will only be referring to Part 2 of Gödel’s paper, which contains the proof proper (the paper can be viewed online at English translation of Gödel’s original proof or as a PDF file at English translation of Gödel’s original proof, PDF file). To understand the guide from this point on, you will need to already have a good understanding of the fundamentals of what is called propositional logic and predicate logic (including the meaning of free variables and bound variables). A fairly good online guide that covers the basics can be viewed Propositional and Predicate Logic: here.


If there is any difficulty in following any part of the proof, please contact me and I will try to help. And if you have any suggestions as to how this guide might be improved, please contact me. This guide is intended to be read alongside the English translation of Gödel’s original proof which can be viewed Gödel’s Proof - English translation: here.


Defining a formal system

NB: It is important to bear in mind that, in Meltzer’s translation, the term ‘sign’ is used to refer (in general) to strings of symbols of the formal system. The proof also uses some distinctive terms (number‑signs, type‑n signs, relation‑signs, class‑signs, see below) to refer to certain kinds of strings of symbols.

But note that a single symbol is also referred to as a ‘sign’; it is a string with just one symbol. The term ‘basic sign’ is used to refer to either a single symbol or a string of symbols that represents a variable, see below. When you are reading the proof you need to be familiar with this terminology.


When reading Gödel’s proof, one should remember that Gödel is a proof of incompleteness for one specific formal system which Gödel defines in detail and which he calls the system P. Bear in mind that Gödel’s method, which he applies to this one particular system P, can in principle be applied to any formal system (provided it contains a certain amount of basic arithmetic, such as defining natural numbers and basic operations on those numbers).


From that point of view, you might say that the precise details of the formal system that Gödel uses in his proof are not of overriding importance, since Gödel’s argument could be applied to any formal system. But, having said that, if you don’t spend the time to become familiar with the terminology of the details below (and the corresponding parts of Gödel’s paper), you may have difficulty following the subsequent argument.



Definition of the formal system P

In the paragraph beginning “We proceed now to the rigorous development…”. Here Gödel sets out the definition of the formal system he will use for his proof. He calls this the system P.


The symbols of the formal system P

Every formula of the system P is constructed using seven single symbols (hideshow Gödel’s) along with symbols for variables (see below). The seven symbols are:


“The basic signs of the system P are the following:
     I. Constants: “~” (not), “∨” (or), “∀” (for all), “0” (nought), “f” (the successor of), “(”, “)” (brackets).”


0 and f are used to represent the natural numbers 0, 1, 2, 3, … as 0f0ff0fff0


~ is used to represent ‘not’ (note: in modern notation this would be ¬)


∨ is used to represent ‘or’


is used to represent ‘for all’ (note: where a is some formula, v∀(a) represents ‘for all v, a; whereas the common equivalent modern notation is ∀v (a) )


‘(’ and ‘)’ are used as opening and closing brackets.


Note that the above symbols of the formal system P are sometimes referred to as basic signs (the variables of the system are also referred by the same terminology, so you should be aware of this).


Classes in the formal system P

The other symbols that the formal system P uses are for variables. Before we consider the symbols used for variables, we need to know that the formal system P is defined as including a hierarchy of classes, where the lowest class is a collection of natural numbers, the next level of class is a class that contains classes of classes of natural numbers, and so on. The different levels of classes are referred to as different types of classes, and the lowest class is a type 1 class. These details of how the formal system manipulates classes are for the most part peripheral to the main argument of the proof, so when trying to understand how the proof operates, one should not get bogged down by these details. However, you do need to know what Gödel is referring to when he uses certain terms.


Note that in the system P brackets can have two purposes

  1. to separate parts of an expression, and
  2. to indicate membership of a class; for example, a(b) means b is a member of the class a.


Type 1 class:

The ‘type 1’ class (also called ‘first type’) refers to classes that contain natural numbers (symbol strings such as 0, f0, ff0, fff0, ), or variables for natural numbers. For the detailed definition of what this class contains see Signs of type 1 below.


Type 2 class:

The ‘type 2’ class (also called ‘second type’) refers to classes that contain type 1 classes.


Type 3 class:

The ‘type 3’ (also called ‘third type’) refers to classes that contain type 2 classes.


And so on, giving, in general,


Type n class:

This class refers to classes that contain classes of the next lower type (that is, classes whose type is n ‑ 1) - and these in turn contain classes of the next lower type (that is, classes whose type is n ‑ 2) - and so on, until you reach the class that contains natural numbers.


We can now define the symbols that are used for the variables of the system P.


Variables in the formal system P

Variables of type 1 have the domain of symbol strings of the form 0f0ff0fff0 (hideshow Gödel’s).

Represented by x1, y1, z1, …

Note that variables of type 1 are also called type 1 variables or variables for natural numbers.


“II. Variables of first type (for individuals, i.e. natural numbers including 0): ‘x1’, ‘y1’, ‘z1’,…

     Variables of second type (for classes of individuals): ‘x2’, ‘y2’, ‘z2’,…

     Variables of third type (for classes of classes of individuals): ‘x3’, ‘y3’, ‘z3’, … ”


Variables of type 2 have the domain of classes that contain symbol strings of the form 0f0ff0fff0 .

Represented by x2y2z2, …


Variables of type 3 have the domain of classes of classes of symbol strings of the form 0f0ff0fff0 .

Represented by x3y3z3, …


Variables of type n have the domain of classes of classes of classes … . (n‑1 levels).

Represented by xnynzn, … (Footnote: Note: It might be observed that there are a finite number of alphabetical symbols such as x, y, z, and that in the actual formal system, there are no symbols 123. However, there are several ways that the variables can be represented using only the symbols x, f and 0, for example: xf0xf0f0xf0f0f0, for x1y1z1, …, and xff0xff0ff0xff0ff0ff0, for x2y2z2, …, and so on. Hence there is no limit on the number of possible variables.)


Note that variables in the formal system P are sometimes referred to as basic signs (as are the single symbols of the system, see above).


Number‑signs, Type‑n signs, Relation‑signs and Class‑signs


This is a string of symbols of the form:

0f0ff0fff0, …

i.e., a number‑sign is a string of symbols that represents a number.


sign of type 1 (also called type 1 sign, or a sign of the first type)

This is either a number-sign (as defined above) or a string of symbols of the form

x1fx1ffx1, fffx1, or y1fy1, ffy1fffy1,

where x1y1, etc are variables for natural numbers.

i.e., A sign of type 1 is a string of symbols that can either represent a specific number, or a variable quantity (hideshow Gödel’s).


“By a sign of first type we understand a combination of signs of the form: a, fa, ffa, fffa, etc where a is either 0 or a variable of first type. In the former case we call such a sign a number‑sign.”


sign of type n (also called type n sign, or a sign of the nth type)

In Gödel’s proof, a sign of type n, where n > 1, is the same as a variable of type n. Note that this means that in the system P there are no symbols that represent specific classes (hideshow Gödel’s).


“For n>1 we understand by a sign of n‑th type the same as a variable of n‑th type.”


n‑place relation‑sign

This is a formula with n different free variables (formulas are defined below). Note that the symbol for the same free variable may occur several times in a formula, but this does not determine the n-place of the formula. It is the number of different free variables that determines the n-place of the formula (hideshow Gödel’s).


“A formula with just n free individual variables (and otherwise no free variables) we call an n‑place relation‑sign and for n=1 also a class‑sign.”



A class‑sign is a 1‑place relation‑sign, that is, a formula with only one free variable. As indicated above, note that this same variable may occur several times in the formula.


Formulas of the formal system

Gödel defines what constitutes a formula in the formal system (hideshow Gödel’s). This is required to ensure that a formula is a valid string of symbols of the formal system.


“Combinations of signs of the form a(b), where b is a sign of n‑th and a a sign of (n+1)‑th type, we call elementary formulae. The class of formulae we define as the smallest class containing all elementary formulae and, also, along with any a and b the following: ~(a), (a) ∨ (b), x∀(a) (where x is any given variable). We term (a) ∨ (b) the disjunction of a and b, ~(a) the negation and x∀(a) a generalization of a. A formula in which there is no free variable is called a propositional formula (free variable being defined in the usual way). A formula with just n free individual variables (and otherwise no free variables) we call an n‑place relation‑sign and for n=1 also a class‑sign.”


Elementary formula

These are of the form a(b) (as indicated above, this signifies b is a member of the class a)

where b is a type n sign

and a is the next higher type, i.e., a type n+1 sign. Elementary formulas may be thought of as the fundamental building blocks that all formulas are built of.



A formula can be one of the elementary formulas as defined above, or a formula of the form

where p and q are any formulas, and x is any variable. Note that this is a recursive definition since a formula is defined in terms of formulas; this means that when it is stated that p is a formula, then p itself must be either an elementary formula or a formula of the form ~ (p2), (p2) ∨ (q2) or x∀(p2), where p2and q2 themselves must be either elementary formulas or a formula of the form ~ (p3), (p3) ∨ (q3) or x∀(p3), and so on, until every pn or qn is an elementary formula.


Note that ‘n‑place relation‑signs’ and ‘class‑signs’ are particular types of formulas, see above.


Propositional formula

This is a formula with no free variable.


Substitution of a variable in a formula


Gödel introduces a term Subst a(v|b) to refer to the substitution of the variable v in the formula a by some symbol string of the formal system (represented here by b). By the definition, b must be of the same sign as the variable v (hideshow Gödel’s).


Note that, depending on what version of the translation you are using, Subst may be represented in this format:


which is the format used in Gödel’s original paper. The same applies to the format of the related Sb function which we will encounter later.


“By Subst a(v|b) (where a stands for a formula, v a variable and b a sign of the same type as v) we understand the formula derived from a, when we replace v in it, wherever it is free, by b. Where v does not occur in a as a free variable, we must put Subst a(v|b) = a. Note that ‘Subst’ is a sign belonging to metamathematics.”



Gödel says that given any valid formula, if we replace every variable of that formula by a variable that is one type higher, then we have created another valid formula. So if a formula contained only type 1 and type 2 variables, and we replace every type 2 variable by a type 3 variable, and we replace every type 1 variable by a type 2 variable, we then have another formula (hideshow Gödel’s)


“We say that a formula a is a type‑lift of another one b, if a derives from b, when we increase by the same amount the type of all variables appearing in b.”


Note: The notion of type‑lift is peripheral to the main argument of the proof.







Diverse opinions and criticisms are welcome, but messages that are frivolous, irrelevant or devoid of logical basis will be blocked (comments will be checked before appearing on this site). 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 - this will only be used to notify you of replies to your comments - it will never be used for any other purpose, will never be displayed and does not require verification. Comments are common to the entire website, so please indicate what section of the site you are commenting on.


If you cannot see any comments below, it may be that a plug-in on your browser is blocking Disqus comments from loading. Avast anti-virus in particular is known to do this, especially with Internet Explorer and Safari. See Disqus Browser plug-in/extension conflicts or Why isn’t the comment box loading?.



Please wait for comments to load …  


The Lighter Side



There’s something about Gödel by Francesco Berto

There is a new addition to the page Yet another flawed incompleteness proof, where Berto’s proof of incompleteness in his book There’s something about Gödel comes under scrutiny.



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).



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.



New page on Chaitin’s Constant

There is now a new page on Chaitin’s Constant (Chaitin’s Omega), which demonstrates that Chaitin has failed to prove that it is actually algorithmically irreducible.



Updated: Diagonal Lemma

Flawed proofs of the Diagonal Lemma by Panu Raatikainen and Vann McGee have been added to the Diagonal Lemma web page.

Previous Blog Posts  


16th Mar 2015 Bishops Dancing with Pixies?


23rd Feb 2015 Artificial Intelligence


31 Mar 2015 Cranks and Crackpots


30 Apr 2015 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 - 2016