Note: Full functionality of this website 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
Page Contents
Page last updated 11 May 2021
Note that (provided you have JavaScript enabled) clicking on (show hide ) will reveal further details, while clicking again will hide it. Also, clicking on (show Gödel’s hide Gödel’s ) will reveal relevant parts of Gödel’s text (shown in green), while clicking again will hide it.
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). 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). There are several fairly good online guides that cover the basics, such as Propositional and Predicate Logic and Propositional Logic, Truth Tables, and Predicate Logic.
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 my English translation of Gödel’s original proof. (Footnote:
If you are following 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) to refer to certain kinds of strings of symbols.
But note that in Meltzer’s translation a single symbol is also referred to as a ‘sign’; it is a string with just one symbol, and you would need to be familiar with this terminology.)
Defining a formal system
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 ( hide Gödel’s show Gödel’s) along with symbols for variables (see below). The seven symbols are:
0 and f are used to represent the natural numbers 0, 1, 2, 3, … as 0, f0, ff0, fff0, …
¬ is used to represent negation (note: in older notation this might be represented by ¬ or an overbar, which is a line over the expression)
∨ 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). Some of the later definitions depend on this symbol order.)
‘(’ and ‘)’ are used as opening and closing brackets.
Note that the above symbols of the formal system P are sometimes referred to as ‘basic symbols’ (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
- to separate parts of an expression, and
- 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 Strings 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 0, f0, ff0, fff0, … ( hide Gödel’s show 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.
Variables of type 2 have the domain of classes that contain symbol strings of the form 0, f0, ff0, fff0, … .
Represented by x2, y2, z2, …
Variables of type 3 have the domain of classes of classes of symbol strings of the form 0, f0, ff0, fff0, … .
Represented by x3, y3, z3, …
Variables of type n have the domain of classes of classes of classes … . (n‑1 levels).
Represented by xn, yn, zn, … (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 1, 2, 3. However, there are several ways that the variables can be represented using only the symbols x, f and 0, for example: xf0, xf0f0, xf0f0f0, for x1, y1, z1, …, and xff0, xff0ff0, xff0ff0ff0, for x2, y2, z2, …, and so on. Hence there is no limit on the number of possible variables.)
Note that variables in the formal system P, although they are actually combinations of symbols, are sometimes referred to as ‘basic symbols’ (as are the single symbols of the system, see above).
Number‑strings, Type‑n strings, Relation‑strings and Class‑strings
This is a string of symbols of the form:
0, f0, ff0, fff0, …
i.e. a number‑string is a string of symbols that represents a number.
string of type 1 (also called type 1 string, or a string of the first type)
This is either a number-string (as defined above) or a string of symbols of the form
x1, fx1, ffx1, fffx1, … or y1, fy1, ffy1, fffy1, …
where x1, y1, etc are variables for natural numbers.
i.e. A string of type 1 is a string of symbols that can either represent a specific number, or a variable quantity ( hide Gödel’s show Gödel’s).
string of type n (also called type n string, or a string of the nth type)
In Gödel’s proof, a string 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 ( hide Gödel’s show Gödel’s). This means that to reference a specific class entails defining its properties and applying them to some variable. Once that is done, then every subsequent occurrence of that variable is subject to the original definition of its properties, and in this way one can refer to specific classes without having to give any of them a particular name.
n‑place relation‑string
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 ( hide Gödel’s show Gödel’s).
class‑string
A class‑string is a 1‑place relation‑string, 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 ( hide Gödel’s show Gödel’s). This is required to ensure that a formula is a valid string of symbols of the formal system.
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 string, and
a is the next higher type, i.e. a type n+1 string.
Elementary formulas may be thought of as the fundamental building blocks that all formulas are built of.
Formula
A formula can be one of the elementary formulas as defined above, or a formula of the form
| ¬ (p) | (which means ‘not’ p) | |
| (p) ∨ (q) | (which means p ‘or’ q) | |
| x∀(p) | (which means ‘for all’ x, p) |
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‑strings’ and ‘class‑strings’ are particular types of formulas, see above.
Propositional formula
This is a formula with no free variable.
Substitution of a variable in a formula
Subst
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 string type as the variable v ( hide Gödel’s show 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.
Type-lift
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 ( hide Gödel’s show Gödel’s)
Note: The notion of type‑lift is peripheral to the main argument of the proof.
Footnotes:
Interested in supporting this site?
You can help by sharing the site with others. You can also donate at 
where there are full details.
As site owner I reserve the right to keep my comments sections as I deem appropriate. I do not use that right to unfairly censor valid criticism. My reasons for deleting or editing comments do not include deleting a comment because it disagrees with what is on my website. Reasons for exclusion include:
Frivolous, irrelevant comments.
Comments devoid of logical basis.
Derogatory comments.
Long-winded comments.
Comments with excessive number of different points.
Questions about matters that do not relate to the page they post on. Such posts are not comments.
Comments with a substantial amount of mathematical terms not properly formatted will not be published unless a file (such as doc, tex, pdf) is simultaneously emailed to me, and where the mathematical terms are correctly formatted.
Reasons for deleting comments of certain users:
Bulk posting of comments in a short space of time, often on several different pages, and which are not simply part of an ongoing discussion. Multiple anonymous usernames for one person.
Users, who, when shown their point is wrong, immediately claim that they just wrote it wrong and rewrite it again - still erroneously, or else attack something else on my site - erroneously. After the first few instances, further posts are deleted.
Users who make persistent erroneous attacks in a scatter-gun attempt to try to find some error in what I write on this site. After the first few instances, further posts are deleted.
Difficulties in understanding the site content are usually best addressed by contacting me by e-mail.
Note: a password enables editing of comments, an email enables notification of replies
