Proofs of Godel's incompleteness theorems

This article outlines proofs of Godel's incompleteness theorems . These are two mathematical theorems that are counted among the most important results of logic and that were proven by Kurt Gödel in 1930.

The first theorem of incompleteness says that no consistent system of axioms , whose theorems can be enumerated by an algorithm, can prove all true statements about natural numbers with addition and multiplication. The second sentence of incompleteness states that such a system cannot prove its own consistency .

First sentence of incompleteness

The first sentence of incompleteness can be formulated as follows:

Let be a recursively enumerable and consistent formal system in which Robinson arithmetic can be interpreted. Then is incomplete . (So ​​there are arithmetic formulas that are neither provable nor refutable.) ${\displaystyle T}$ ${\displaystyle T}$ ${\displaystyle T}$

The is Robinson arithmetic (also ) a weak form of arithmetic in first-order logic . This has the constant "zero", the successor function , which intuitively adds one to a given number, as well as the functions for addition and for multiplication. It has the following axioms, which formalize the elementary properties of natural numbers and arithmetic operations: ${\displaystyle Q}$ ${\displaystyle {\dot {0}}}$ ${\displaystyle {\dot {S}}}$ ${\displaystyle {\dot {+}}}$ ${\displaystyle {\dot {\times }}}$

• Zero has no predecessor: ${\displaystyle \neg ({\dot {S}}x\doteq {\dot {0}})}$
• If x + 1 = y + 1, then x = y: ${\displaystyle ({\dot {S}}x\doteq {\dot {S}}y)\rightarrow x\doteq y}$
• Every number is zero or has a predecessor: ${\displaystyle y\doteq {\dot {0}}\vee \exists x({\dot {S}}x\doteq y)}$
• Axiomatic definition of addition and multiplication:
  • ${\displaystyle x{\dot {+}}{\dot {0}}\doteq x}$
  • ${\displaystyle x{\dot {+}}{\dot {S}}y\doteq {\dot {S}}(x{\dot {+}}y)}$
  • ${\displaystyle x{\dot {\times }}{\dot {0}}\doteq {\dot {0}}}$
  • ${\displaystyle x{\dot {\times }}{\dot {S}}y\doteq (x{\dot {\times }}y){\dot {+}}x}$

The dots above the expressions indicate here and in the further course of the article that these expressions belong to the language under consideration. So (see below) is a formula of the formal system under consideration, while is a relation between natural numbers. The "numeral" of a natural number , the representation of the natural number in the system, is denoted by, the numeral of 4 is e.g. B. the term . ${\displaystyle {\dot {Beweis}}(x,y)}$ ${\displaystyle Beweis(n,m)}$ ${\displaystyle n}$ ${\displaystyle {\dot {n}}}$ ${\displaystyle {\dot {S}}{\dot {S}}{\dot {S}}{\dot {S}}{\dot {0}}}$

In the following it is assumed that Robinson arithmetic is itself. The proof can also be carried out for any other system in which the arithmetic can be interpreted in such a way that all functions from Robinson arithmetic can be defined by expressions of the new system in such a way that all the theorems of Robinson arithmetic in theorems of the other system pass over. In particular, it is assumed that the axiom system is decidable . Gödel originally proved the theorem for the much stronger system of Principia Mathematica . The proof for the Zermelo-Fraenkel set theory can also be carried out, which has the element relation as the only non-logical sign , but in which numbers can be interpreted as sets, so that all the theorems of Robinson arithmetic can be interpreted as theorems of set theory. The proof can also be adapted for a merely enumerable system of axioms. ${\displaystyle T}$ ${\displaystyle \in }$

The proof breaks down into four parts:

1. Arithmetizing the syntax: Each expression of the theory is assigned a number, the so-called Gödel number, from which the formula can again be effectively reconstructed. This numbering is extended to finite sequences of formulas.
2. Arithmetizing the provability relation: A formula is constructed so that for every pair of numbers and , is provable if and only if the Gödel number of a proof is a formula whose Gödel number is. ${\displaystyle {\dot {Beweis}}(x,y)}$ ${\displaystyle n}$ ${\displaystyle m}$ ${\displaystyle {\dot {Beweis}}({\dot {n}},{\dot {m}})}$ ${\displaystyle n}$ ${\displaystyle m}$
3. Construction of Gödel's theorem: A formula is constructed which informally says “I am not provable”, the so-called Gödel's theorem .
4. Proof of unprovability: It is shown that Godel's theorem can neither be proven nor refuted.

Arithmetic the syntax

The main problem in carrying out the proof described above seems to be that when constructing a statement equivalent to " is unprovable", it must contain a reference to . Godel's solution is to show that statements can be assigned to numbers in such a way that proving a statement can be replaced by checking whether the number assigned to the statement has some arithmetic property. This enables the construction of a self-referential formula that avoids infinite regress. ${\displaystyle p}$ ${\displaystyle p}$ ${\displaystyle p}$ ${\displaystyle p}$

The first step of the proof is to map formulas and finite sequences of formulas ( injectively ) to natural numbers. These numbers are called the god numbers of the formulas. First of all, a number is assigned to each symbol in the language of arithmetic, similar to the ASCII code, which assigns a unique number to each letter. There are various ways of doing this, here a sequence of digits is assigned directly to each character.

number symbol meaning 11 ${\displaystyle {\dot {0}}}$ zero 12 ${\displaystyle {\dot {S}}}$ Successor function 13 ${\displaystyle \doteq }$ equality 14th ${\displaystyle {\dot {+}}}$ addition 15th ${\displaystyle {\dot {\times }}}$ multiplication 16 ( left bracket 17th ) right bracket

number symbol meaning 18th ${\displaystyle x}$ a variable 19th ${\displaystyle '}$ Dash (for further variables x ', x' ', ...) 21st ${\displaystyle \exists }$ Existential quantifier 22nd ${\displaystyle \forall }$ Universal quantifier 23 ${\displaystyle \land }$ logical and 24 ${\displaystyle \lor }$ logical or 25th ${\displaystyle \neg }$ negation

One can see here that the symbol for implication ( ) used in the 2nd axiom is missing; is known to be equivalent to (at least in classical logic ). ${\displaystyle \to }$ ${\displaystyle p\to q}$ ${\displaystyle \neg p\vee q}$

The Gödel number of a formula is obtained by stringing together the Gödel numbers for each symbol in the formula. Every formula can be clearly reconstructed from its Gödel number. The Gödel number of a formula is denoted by. ${\displaystyle F}$ ${\displaystyle G(F)}$

With this Gödel numbering, for example, the sentence that expresses the commutative law of addition is given the number: ${\displaystyle \forall x\forall x'(x{\dot {+}}x'\doteq x'{\dot {+}}x)}$

22 18 22 19 16 18 14 19 13 19 14 18 17

(The spaces are for readability only.) Not all numbers represent formulas, for example stands

13 22 14 18

for " ", which is not a correct formula. ${\displaystyle \doteq \forall {\dot {+}}x}$

In the system, every natural number n is represented by its numeral. Conversely, every numeral also has a Gödel number, so the Gödel number is the same: ${\displaystyle {\dot {S}}{\dot {S}}{\dot {S}}{\dot {S}}{\dot {0}}}$

12 12 12 12 11.

The assignment of Godel numbers can be extended to finite sequences of formulas. To get the Godel number of a finite sequence of formulas, the numbers of the formulas are written one after the other and each separated by a zero. Since the Godel number of a single formula never contains a zero, every formula in the sequence can be uniquely reconstructed.

It is important that formal arithmetic can prove some simple facts. In particular, it must be able to prove that every number has a god number. It also has to prove that there is the Gödel number of a formula in which all occurrences of have been replaced by the Gödel number of for the Gödel number of a formula that has a free variable , and that this Gödel number is derived from the first can be obtained through an effective procedure. ${\displaystyle F(x)}$ ${\displaystyle m}$ ${\displaystyle F(m)}$ ${\displaystyle x}$ ${\displaystyle m}$

The provability relation

The formal system has axioms and rules of inference from which the formulas of the system can be proven. A formal proof in the system is thus a chain of formulas, each of which is either an axiom or can be obtained from earlier formulas by means of a rule of inference.

Since the formal system is decidable, one can effectively decide whether a given number is Godel number of an axiom. In the case of the finite axiomatized system , it is even sufficient to check whether the number for Gödel's number is equal to one of the seven axioms. ${\displaystyle Q}$

Inference rules can be represented as binary relations between Godel numbers of sequences of formulas. For example, there is an inference rule that gives you the formula from the formulas . Then, the relation means to this derivation rule that if and to in relation stands ( true) if the Godel number is a list of formulas and contains, and Godel number of a list of formulas consisting of the formulas in the by -coded list exists and additionally contains. Since every rule of derivation is a simple formal requirement, it is possible to effectively decide whether two numbers and are in relation . ${\displaystyle D_{1}}$ ${\displaystyle S_{1},S_{2}}$ ${\displaystyle S_{1}\wedge S_{2}}$ ${\displaystyle R_{1}}$ ${\displaystyle n}$ ${\displaystyle m}$ ${\displaystyle nR_{1}m}$ ${\displaystyle n}$ ${\displaystyle S_{1}}$ ${\displaystyle S_{2}}$ ${\displaystyle m}$ ${\displaystyle n}$ ${\displaystyle S_{1}\wedge S_{2}}$ ${\displaystyle n}$ ${\displaystyle m}$ ${\displaystyle R_{1}}$

The second step is to show that this Godel numbering can be used to express the concept of provability. A proof of a formula is a chain of formulas in which each is an axiom or arises from earlier statements by a rule of derivation, and in which the last statement is. This allows the Godel number of a proof to be defined using the method given above for coding finite sequences of formulas. In addition, a relation can be defined that is true (and provable) for two numbers and if and only if the Godel number of a proof of is, and is. ${\displaystyle S}$ ${\displaystyle S}$ ${\displaystyle Beweis(x,y)}$ ${\displaystyle x}$ ${\displaystyle y}$ ${\displaystyle x}$ ${\displaystyle S}$ ${\displaystyle y=G(S)}$

${\displaystyle Beweis(x,y)}$is an arithmetic relation, just like " ", only much more complicated. For all specific numbers and either the formula or its negation is provable (but not both). This is because the relationship between the numbers can be easily "checked". The construction of the formula depends crucially on the fact that the axiom system is decidable; without this assumption, the formula would not be constructible. ${\displaystyle x+y=6}$ ${\displaystyle n}$ ${\displaystyle m}$ ${\displaystyle {\dot {Beweis}}(m,n)}$ ${\displaystyle \lnot {\dot {Beweis}}(m,n)}$ ${\displaystyle {\dot {Beweis}}}$

A relation can now be defined that represents the metalinguistic statement " is provable": is provable if there is a number that codes a proof for : ${\displaystyle {\dot {Beweisbar}}(y)}$ ${\displaystyle F}$ ${\displaystyle F}$ ${\displaystyle x}$ ${\displaystyle F}$

${\displaystyle {\dot {Beweisbar}}(y)=\exists x({\dot {Beweis}}(x,y))}$

" " And " " are just an abbreviation for a certain, very long, arithmetic formula; the symbols " " and " " themselves do not belong to the language of the system. ${\displaystyle {\dot {Beweisbar}}(y)}$ ${\displaystyle {\dot {Beweis}}(x,y)}$ ${\displaystyle {\dot {Beweis}}}$ ${\displaystyle {\dot {Beweisbar}}}$

An important feature of the formula is that is provable when is provable. Because if it is provable, then there is a proof with a god number . Then it is true and, as stated above, provable. This makes the weaker existence statement even more provable. ${\displaystyle {\dot {Beweisbar}}(y)}$ ${\displaystyle {\dot {Beweisbar}}(G(p))}$ ${\displaystyle p}$ ${\displaystyle p}$ ${\displaystyle n}$ ${\displaystyle {\dot {Beweis}}({\dot {n}},G(p))}$ ${\displaystyle \exists x{\dot {Beweis}}(x,G(p))}$

The results of this section can be formalized with the help of the derivability symbol : ${\displaystyle \vdash }$

1. ${\displaystyle {\text{Falls Beweis(n,m) dann T}}\vdash {\dot {Beweis}}({\dot {n}},{\dot {m}})}$
2. ${\displaystyle {\text{Falls non Beweis(n,m) dann T}}\vdash \neg {\dot {Beweis}}({\dot {n}},{\dot {m}})}$
3. ${\displaystyle {\text{Falls Beweisbar(n) dann T}}\vdash {\dot {Beweisbar}}({\dot {n}})}$

Diagonalization

The next step is to construct a proposition that claims its own unprovability. The diagonal lemma can be used for this. This says that in arithmetic and stronger formal systems there is a statement for every formula with a free variable , so that the system has the equivalence ${\displaystyle F(x)}$ ${\displaystyle x}$ ${\displaystyle p}$

${\displaystyle p\Leftrightarrow F(G(p)).}$

proves. So you get a formula with the intuitive meaning “I have the quality .” If you substitute for the negation of , you get the statement with the meaning “My Gödel number is the Gödel number of an unprovable formula”, ie “I am unprovable”. ${\displaystyle F(x)}$ ${\displaystyle F}$ ${\displaystyle Beweisbar(x)}$ ${\displaystyle p}$

The formula isn't directly equal to ; rather , it means that if you do a certain calculation you get the number of an unprovable statement. If you now carry out this calculation, it turns out that the resulting number is the Godel number by itself. This construction is similar to the following natural language statement: ${\displaystyle p}$ ${\displaystyle \neg {\dot {Beweisbar}}(G(p))}$ ${\displaystyle p}$ ${\displaystyle p}$

"is unprovable in quotation marks and followed by itself." is in quotes and followed by itself unprovable.

This theorem does not refer directly to itself, but one gets the original statement when one carries out the given transformation, and thus the theorem claims its own unprovability. The proof of the diagonal lemma uses a similar method.

Proof of the independence of Godel's theorem

Assume now that the formal system is ω-consistent , and therefore consistent. Let be the statement constructed in the previous section. ${\displaystyle p}$

If it were provable, then it would be provable. But is equivalent to the negation of . This would make the system inconsistent as it would prove a statement and its negation. So it can not be provable, since the theory is consistent according to the assumption. ${\displaystyle p}$ ${\displaystyle {\dot {Beweisbar}}(G(p))}$ ${\displaystyle p}$ ${\displaystyle {\dot {Beweisbar}}(G(p))}$ ${\displaystyle p}$

If the negation of were provable, it follows from the consistency of the system that it is not provable. Therefore, no natural number can be the god number of a proof of . At the same time, the negation of is equivalent to . With this the system proves on the one hand the existence of a number with a certain property, but on the other hand proves for every digit that it does not have this property . This is impossible in a consistent system. Thus the negation of is not provable. ${\displaystyle p}$ ${\displaystyle p}$ ${\displaystyle n}$ ${\displaystyle p}$ ${\displaystyle p}$ ${\displaystyle {\dot {Beweisbar}}(G(p))}$ ${\displaystyle {\dot {n}}}$ ${\displaystyle \omega }$ ${\displaystyle p}$

This makes the statement undecidable: it can neither be proven nor refuted in the chosen system. The system is -inconsistent or incomplete. This reasoning can be applied to any formal system that meets the requirements. This means that all formal systems that meet the requirements are inconsistent or incomplete. ${\displaystyle p}$ ${\displaystyle \omega }$ ${\displaystyle \omega }$

It should be noted that it cannot be proven even if the system is consistent and inconsistent. The assumption of consistency is only necessary to show that the negation of is not provable. ${\displaystyle p}$ ${\displaystyle \omega }$ ${\displaystyle \omega }$ ${\displaystyle p}$

If you try to remove the incompleteness by adding one of the unprovable formulas or not as an axiom, you get a new formal system. The same process can be applied to this and one again receives a statement of the form “I cannot be proven in the new system.” And the new system is again inconsistent or incomplete. ${\displaystyle p}$ ${\displaystyle p}$ ${\displaystyle \omega }$

Generalization by Rosser

As shown in the previous section, the construction of Godel's theorem only allows the proof of incompleteness for -consistent systems. John Barkley Rosser showed in 1936 that the same technique can be used to show incompleteness for consistent but inconsistent systems. ${\displaystyle \omega }$ ${\displaystyle \omega }$

Using the diagonal lemma, a sentence can be constructed which has the metalinguistic meaning “If there is a proof for me, then there is a shorter proof for my negation”. This set is also known as the horse substitute : ${\displaystyle R}$

${\displaystyle T\vdash R\leftrightarrow \forall y({\dot {Beweis}}(y,\mathbf {G} (R))\rightarrow \exists z{\dot {<}}y{\dot {Beweis}}(z,\mathbf {G} (\neg R)))}$

Assuming the system is consistent and provable, whereby there is a proof with Gödel number . Then the system proves and thus the equivalent . Since it is possible to decide for all substitutions and the system is consistent after assumption, this statement is also true in . So there is a number that is Godel number of a proof of the negation of . The formal system thus proves a proposition and its negation, i.e. is inconsistent, a contradiction. ${\displaystyle R}$ ${\displaystyle n}$ ${\displaystyle \exists z{\dot {<}}{\dot {n}}{\dot {Beweis}}(z,\mathbf {G} (\neg R)))}$ ${\displaystyle {\dot {Beweis}}({\dot {0}},\mathbf {G} (\neg R)))\vee {\dot {Beweis}}({\dot {1}},\mathbf {G} (\neg R)))\vee ...\vee {\dot {Beweis}}({\dot {n-1}},\mathbf {G} (\neg R)))}$ ${\displaystyle {\dot {Beweis}}(x,y)}$ ${\displaystyle \mathbb {N} }$ ${\displaystyle m<n}$ ${\displaystyle R}$

Now assume that the system is consistent and the horse substitute is refutable, whereby there is a proof for the negation with Godel number . Since the system is consistent, it can not be proven. Then it can be proven: ${\displaystyle n}$ ${\displaystyle R}$

${\displaystyle T\vdash \forall y(y{\dot {\leq }}{\dot {n}}\rightarrow \neg {\dot {Beweis}}(y,\mathbf {G} (R)))}$

Since there is no proof for , there is no proof with Gödel number less than or equal to . So the formula is true. Since there are only finitely many numbers smaller , the formula is equivalent to a quantifier-free formula and thus also provable. ${\displaystyle R}$ ${\displaystyle n}$ ${\displaystyle n}$ ${\displaystyle (\neg {\dot {Beweis}}({\dot {0}},\mathbf {G} (R)))\wedge (\neg {\dot {Beweis}}({\dot {1}},\mathbf {G} (R)))\wedge ...\wedge (\neg {\dot {Beweis}}({\dot {n}},\mathbf {G} (R)))}$

${\displaystyle T\vdash \forall y(n{\dot {<}}y\rightarrow \exists z{\dot {<}}y\ {\dot {Beweis}}(z,\mathbf {G} (\neg R)))}$

For every number larger one finds a smaller number, the number of a proof of is. This follows directly from the fact that there is such a number. ${\displaystyle n}$ ${\displaystyle \neg R}$ ${\displaystyle m}$

However, this can be used to prove by counterposition and modus ponens :

${\displaystyle T\vdash \forall y({\dot {Beweis}}(y,\mathbf {G} (R))\rightarrow \exists z{\dot {<}}y{\dot {Beweis}}(z,\mathbf {G} (\neg R)))}$

which corresponds to the horse substitute . This is a contradiction because it cannot be proven after assumption. So the horse substitute is not refutable in a consistent system. ${\displaystyle R}$ ${\displaystyle R}$

Second sentence of incompleteness

The second sentence of incompleteness says:

Any sufficiently powerful consistent system cannot prove its own consistency.

A sufficient condition for “sufficiently powerful” is that the proof of the first incompleteness sentence can be formalized in the system. To do this, it must have a formula that expresses the provability in this system. In addition, this formula must satisfy the so-called Bernays-Löb axioms . These require that all formulas and the following conditions apply: ${\displaystyle Bew(x)}$ ${\displaystyle F}$ ${\displaystyle H}$

1. If then ${\displaystyle T\vdash F}$ ${\displaystyle T\vdash {\dot {Bew}}(\mathbf {G} (F))}$
2. ${\displaystyle T\vdash {\dot {Bew}}(\mathbf {G} (F\rightarrow H))\rightarrow ({\dot {Bew}}(\mathbf {G} (F))\rightarrow {\dot {Bew}}(\mathbf {G} (H)))}$
3. ${\displaystyle T\vdash {\dot {Bew}}(\mathbf {G} (F))\rightarrow {\dot {Bew}}(\mathbf {G} ({\dot {Bew}}(\mathbf {G} (F))))}$

Although this is not yet fulfilled in the system for which the first incompleteness theorem can already be shown, it is already fulfilled in primitive recursive arithmetic (PRA), and especially in stronger theories such as Peano arithmetic and set theory. ${\displaystyle Q}$

With the help of these properties, the first sentence of incompleteness can be formalized as follows. Let the statement constructed when proving the first sentence with the meaning “I am not provable.” Then the following three statements can be derived: ${\displaystyle F}$

• ${\displaystyle T\vdash {\dot {Bew}}(\mathbf {G} (F))\rightarrow {\dot {Bew}}(\mathbf {G} ({\dot {Bew}}(\mathbf {G} (F))))}$ (according to axiom 3)
• ${\displaystyle T\vdash {\dot {Bew}}(\mathbf {G} (Bew(\mathbf {G} (F))))\rightarrow {\dot {Bew}}(\mathbf {G} (\neg F))}$ (according to the definition of F)
• ${\displaystyle T\vdash {\dot {Bew}}(\mathbf {G} (F))\rightarrow ({\dot {Bew}}(\mathbf {G} (\neg F))\rightarrow {\dot {Bew}}(\mathbf {G} ({\dot {0}}\doteq {\dot {1}}))}$(from the tautology according to axiom 1 and 2) ${\displaystyle T\vdash F\rightarrow (\neg F\rightarrow {\dot {0}}\doteq {\dot {1}})}$

By counterposing these three sentences one gets the following sentence, which corresponds to the first incompleteness sentence:

• ${\displaystyle T\vdash \neg {\dot {Bew}}(\mathbf {G} ({\dot {0}}\doteq {\dot {1}}))\rightarrow \neg {\dot {Bew}}(\mathbf {G} (F))}$

To create a contradiction, suppose that T proves its consistency, that is . So true , so . According to axiom 1 then holds . But then T would be inconsistent, since it proves both and . So T , if it is consistent, cannot prove its own consistency. ${\displaystyle T\vdash \neg {\dot {Bew}}(\mathbf {G} ({\dot {0}}\doteq {\dot {1}}))}$ ${\displaystyle T\vdash \neg {\dot {Bew}}(\mathbf {G} (F))}$ ${\displaystyle T\vdash F}$ ${\displaystyle T\vdash {\dot {Bew}}(\mathbf {G} (F))}$ ${\displaystyle {\dot {Bew}}(\mathbf {G} (F))}$ ${\displaystyle \neg {\dot {Bew}}(\mathbf {G} (F))}$

Alternatively, the second incompleteness theorem can also be proven by Löb's theorem. According to this, for a system that fulfills the Bernays-Löb axioms, the statement only applies if it also applies. If now proves its own consistency, then and with it . According to Löb's theorem, therefore , is inconsistent. ${\displaystyle T}$ ${\displaystyle T\vdash {\dot {Bew}}(\mathbf {G} (P))\rightarrow P}$ ${\displaystyle T\vdash P}$ ${\displaystyle T}$ ${\displaystyle T\vdash \neg {\dot {Bew}}(\mathbf {G} \bot )}$ ${\displaystyle T\vdash ({\dot {Bew}}(\mathbf {G} \bot )\rightarrow \bot )}$ ${\displaystyle T\vdash \bot }$ ${\displaystyle T}$

Alternative evidence

Various other proofs of the incompleteness theorem are known which, unlike Gödel's proof, do not require a self-referential formula. Direct proofs of the first incompleteness theorem for special powerful systems such as Peano arithmetic or Zermelo-Fraenkel set theory can be obtained through various unprovable results for mathematical statements. In addition, there are also various proofs which, like Gödel's proof by formalizing paradoxes, show the incompleteness of all sufficiently powerful formal systems.

Stop problem

Alan Turing showed in 1937 that the first incompleteness theorem can be shown by means of the computability theory .

The stopping problem is the amount of Gödel numbers of pairs of Turing machines and words , so that input stops after a finite number of steps. The holding problem can also be defined for other predictability models in the same way. Turing showed that the holding problem cannot be decided . It can be shown that the holding problem can be represented arithmetically, i.e. there is an arithmetic formula so that it is true if and only if the input is held. Assume that the theory under consideration is complete and only proves arithmetically true formulas. Given a Turing machine and a word . Then one can systematically search through all the evidence in the theory until one finds evidence for or . Since the theory is complete, exactly one of the two formulas can actually be proven. But that would solve the holding problem, contradiction. So there are Turing machines and words that are neither provable nor refutable. ${\displaystyle T}$ ${\displaystyle w}$ ${\displaystyle T}$ ${\displaystyle w}$ ${\displaystyle A(x,y)}$ ${\displaystyle A(\mathbf {G} (T),\mathbf {G} (w))}$ ${\displaystyle T}$ ${\displaystyle w}$ ${\displaystyle T}$ ${\displaystyle w}$ ${\displaystyle A(\mathbf {G} (T),\mathbf {G} (w))}$ ${\displaystyle \neg A(\mathbf {G} (T),\mathbf {G} (w))}$ ${\displaystyle T}$ ${\displaystyle w}$ ${\displaystyle A(\mathbf {G} (T),\mathbf {G} (w))}$

Berry Paradox

George Boolos showed in 1989 that the first incompleteness theorem can be proven by formalizing the Berry paradox . This consists of the following natural language expression:

"The smallest natural number that cannot be defined with fewer than fourteen words."

Since every non-empty set of natural numbers has a smallest element and because only a finite number of numbers can be defined with less than fourteen words, this expression defines a number. The paradox now is that the named number supposedly cannot be named in less than fourteen words, but the phrase has only thirteen words.

This paradox is formalized by Boolos as follows. A formula names the number if the system under consideration proves that the only number with a property is: ${\displaystyle F(x)}$ ${\displaystyle n}$ ${\displaystyle T}$ ${\displaystyle n}$ ${\displaystyle F(x)}$

${\displaystyle T\vdash \forall x(F(x)\leftrightarrow x\doteq {\dot {n}})}$

Now there is an arithmetically definable predicate that is true if and only if an arithmetic formula with length names the number . The following predicates can then be defined: ${\displaystyle C(x,z)}$ ${\displaystyle z}$ ${\displaystyle x}$

${\displaystyle B(x,y)\leftrightarrow \exists z(z<y\wedge C(x,z))}$. "X can be named with fewer than y symbols"

${\displaystyle A(x,y)\leftrightarrow \neg B(x,y)\wedge \forall a(a{\dot {<}}x\rightarrow B(a,y))}$" Is the smallest number that cannot be defined with less than symbols" ${\displaystyle x}$ ${\displaystyle y}$

Now be the length of the formula . Then consider the formula “ is the smallest number that cannot be defined with less than symbols.” Since only a finite number of numbers can be defined with less than symbols, there must be a number so that is true, and there is exactly one smallest Number gives is also true. If this formula were provable, then the number would name n . However, the formula has far fewer characters than 10 · k, so the formula cannot be proven. ${\displaystyle k}$ ${\displaystyle A(x,y)}$ ${\displaystyle A(x,{\dot {10}}{\dot {\times }}{\dot {k}})}$ ${\displaystyle x}$ ${\displaystyle 10\times k}$ ${\displaystyle 10\times k}$ ${\displaystyle n}$ ${\displaystyle A(n,{\dot {10}}{\dot {\times }}{\dot {k}})}$ ${\displaystyle \forall x(A(x,{\dot {10}}{\dot {\times }}{\dot {k}})\leftrightarrow x\doteq {\dot {n}})}$ ${\displaystyle A(x,{\dot {10}}{\dot {\times }}{\dot {k}})}$ ${\displaystyle A(x,{\dot {10}}{\dot {\times }}{\dot {k}})}$ ${\displaystyle \forall x(A(x,{\dot {10}}{\dot {\times }}{\dot {k}})\leftrightarrow x\doteq {\dot {n}})}$

Gregory Chaitin showed in 1974 by a similar formalization of the Berry Paradox that for every formal system that does not prove false arithmetic statements there is a number , so that for any number the system cannot prove that its Kolmogorov complexity is greater than . ${\displaystyle n}$ ${\displaystyle n}$

Grelling-Nelson Antinomy

Another proof can be obtained from the Grelling-Nelson antinomy . A formula with a free variable is called autological if it can be proven. Now there is an arithmetic formula (for "Gödel-Grelling formula") with the meaning: " Is not the Gödel number of an autological formula." Now consider the formula with the meaning "The formula is not autological." Assume that the formula is provable. But then by definition it is autological and the system is inconsistent. So the formula is unprovable, but since it asserts this unprovability, it is also true. If the formula were refutable, then the system would be inconsistent, similar to Gödel's proof, i.e. it would prove a false statement. ${\displaystyle F(x)}$ ${\displaystyle F({\bf {G}}(F(x)))}$ ${\displaystyle GG(x)}$ ${\displaystyle x}$ ${\displaystyle GG({\bf {G}}(GG(x)))}$ ${\displaystyle GG(x)}$ ${\displaystyle GG(x)}$ ${\displaystyle GG({\bf {G}}(GG(x)))}$ ${\displaystyle \omega }$

literature

• Kurt Godel: On formally undecidable propositions of Principia Mathematica and related systems I . Monthly books for mathematics and physics 38, 1931, pp. 173–198, doi : 10.1007 / BF01700692 . Zentralblatt MATH .
• Kurt Gödel: Discussion on the Foundation of Mathematics: Knowledge 2 . Monthly books for math. And physics, 1931–32, pp. 147–148.
• J. Barkley Rosser: Extensions of some theorems of Godel and Church . In: Journal of Symbolic Logic . tape 1 , 1936, pp. 87-91 .

Individual evidence

1. ^ The proof sketch follows: Peter G. Hinman: Fundamentals of Mathematical Logic . AK Peters, 2005. , pp. 421-423.
2. ^ Alan Turing: On computable numbers, with an application to the decision problem , Proceedings of the London Mathematical Society, 2, 42 (1937), pp. 230-265. Online version
3. ↑ George Boolos: A New Proof of the Gödel Incompleteness Theorem . In: Notices of the American Mathematical Society . tape 36 , 1989, pp. 388-390 and 676 . , Reprinted in George Boolos: Logic, Logic, and Logic . Harvard University Press, 1998, ISBN 0-674-53766-1 .
4. ^ Gregory Chaitin: Information-theoretic limitations of formal systems . In: Journal of the ACM (JACM) . tape 21 , no. 3 . ACM, 1974, p. 403-424 .
5. ↑ George Boolos , John P. Burgess, and Richard Jeffrey: Computability and Logic . 4th edition. Cambridge University Press, 2002, ISBN 0-521-70146-5 . , Page 227

Web links

Wikiversity: Course: Introduction to Mathematical Logic (Osnabrück 2011-2012)  - Course materials