Gödel’s incompleteness theorems
Gödel’s first and second incompleteness theorems^{} are perhaps the most celebrated results in mathematical logic. The basic idea behind Gödel’s proofs is that by the device of Gödel numbering, one can formulate properties of theories and sentences^{} as arithmetical properties of the corresponding Gödel numbers, thus allowing 1st order arithmetic to speak of its own consistency, provability of some sentence and so forth.
The original result Gödel proved in his classic paper On Formally Undecidable Propositions^{} in Principia Mathematica and Related Systems can be stated as
Theorem 1
No theory $\mathrm{T}$ axiomatisable in the type system of PM (i.e., in Russell’s theory of types) which contains Peanoarithmetic and is $\omega $consistent proves all true theorems of arithmetic (and no false ones).
Stated this way, the theorem is an obvious corollary of Tarski’s result on the undefinability of truth. This can be seen as follows. Consider a Gödel numbering G, which assigns to each formula^{} $\varphi $ its Gödel number ${}^{\lceil}\varphi ^{\rceil}$. The set of Gödel numbers of all true sentences of arithmetic is ${\{}^{\lceil}{\varphi}^{\rceil}\mid \mathbb{N}\vDash \varphi \}$, and by Tarski’s result it isn’t definable by any arithmetic formula. But assume there’s a theory $T$ an axiomatisation ${\mathrm{\mathbf{A}\mathbf{x}}}_{T}$ of which is definable in arithmetic and which proves all true statements of arithmetic. But now $\exists P(P$ is a proof of $x$ from ${\mathrm{\mathbf{A}\mathbf{x}}}_{T})$ defines the set of (Gödel numbers of) true sentences of arithmetic, which contradicts Tarski’s result.
The proof given above is highly nonconstructive. A much stronger version can actually be extracted from Gödel’s paper, namely that
Theorem 2
There is a primitive recursive function^{} Gödel, such that if $T$ is a theory with a p.r. axiomatisation $\alpha $, and if all primitive recursive functions are representable in $T$ then $\mathrm{N}\mathrm{\vDash}\mathrm{\text{G\xf6del}}\mathit{}\mathrm{(}\alpha \mathrm{)}$ but $T\mathrm{\u22a2\u0338}\mathrm{\text{G\xf6del}}\mathit{}\mathrm{(}\alpha \mathrm{)}$
This second form of the theorem is the one usually proved, although the theorem is usually stated in a form for which the nonconstructive proof based on Tarski’s result would suffice. The proof for this stronger version is based on a similar idea as Tarski’s result.
Consider the formula $\exists P(P$ is a proof of $x$ from $\alpha )$, which defines a predicate
$${\mathrm{Prov}}_{\alpha}(x)$$ 
which represents provability from $\alpha $. Assume we have numerated the open formulae with one variable in a sequence ${B}_{i}$, so that every open formula occurs. Consider now the sentence $\mathrm{\neg}{\mathrm{Prov}}_{\alpha}({B}_{x})$, which defines the nonprovability from $\alpha $ predicate. Now, since $\mathrm{\neg}{\mathrm{Prov}}_{\alpha}({B}_{x})$ is an open formula with one variable, it must be ${B}_{k}$ for some $k$. Thus we can consider the closed sentence ${B}_{k}(k)$. This sentence is equivalent^{} to $\mathrm{\neg}{\mathrm{Prov}}_{\alpha}(subst{(}^{\lceil}\mathrm{\neg}{\mathrm{Prov}}_{\alpha}{(x)}^{\rceil}),k))$, but since $subst{(}^{\lceil}\mathrm{\neg}{\mathrm{Prov}}_{\alpha}{(x)}^{\rceil}),k)$ is just ${B}_{k}(k)$, it “asserts its own unprovability”.
Since all the steps we took to get the undecided but true sentence $subst{(}^{\lceil}\mathrm{\neg}{\mathrm{Prov}}_{\alpha}{(x)}^{\rceil}),k)$ is just ${B}_{k}(k)$ were very simple mechanic manipulations of Gödel numbers guaranteed to terminate in bounded^{} time, we have in fact produced the p.r. function Gödel required by the statement of the theorem.
The first version of the proof can be used to show that also many nonaxiomatisable theories are incomplete. For example, consider $PA$ + all true ${\mathrm{\Pi}}_{1}$ sentences. Since ${\mathrm{\Pi}}_{1}$ truth is definable at ${\mathrm{\Pi}}_{2}$level, this theory is definable in arithmetic by a formula $\alpha $. However, it’s not complete^{}, since otherwise $\exists p(p$ is a proof of $x$ from $\alpha )$ would be the set of true sentences of arithmetic. This can be extended to show that no arithmetically definable theory with sufficient expressive power is complete.
The second version of Gödel’s first incompleteness theorem suggests a natural way to extend theories to stronger theories which are exactly as sound as the original theories. This sort of process has been studied by Turing, Feferman, Fenstad and others under the names of ordinal logics and transfinite recursive progressions of arithmetical theories.
Gödel’s second incompleteness theorem concerns what a theory can prove about its own provability predicate, in particular whether it can prove that no contradiction^{} is provable. The answer under very general settings is that a theory can’t prove that it is consistent, without actually being inconsistent.
The second incompleteness theorem is best presented by means of a provability logic. Consider an arithmetic theory $T$ which is p.r. axiomatised by $\alpha $. We extend the language^{} this theory is expressed in with a new sentence forming operator $\mathrm{\square}$, so that any sentence in parentheses prefixed by $\mathrm{\square}$ is a sentence. Thus for example, $\mathrm{\square}(0=1)$ is a formula. Intuitively, we want $\mathrm{\square}(\varphi )$ to express the provability of $\varphi $ from $\alpha $. Thus the semantics of our new language is exactly the same as that of the original language, with the additional rule that $\mathrm{\square}(\varphi )$ is true if and only if $\alpha \u22a2\varphi $. There is a slight difficulty here; $\varphi $ might itself contain boxed expressions, and we haven’t yet provided any semantics for these. The answer is simple, whenever a boxed expression $\mathrm{\square}(\psi )$ occurs within the scope of another box, we replace it with the arithmetical statement ${\mathrm{Prov}}_{\alpha}(\psi )$. Thus for example the truth of $\mathrm{\square}(\mathrm{\square}(0=1))$ is equivalent to $\alpha \u22a2{\mathrm{Prov}}_{\alpha}{(}^{\lceil}0={1}^{\rceil})$. Assuming that $\alpha $ is strong enough to prove all true instances of ${\mathrm{Prov}}_{\alpha}{(}^{\lceil}{\varphi}^{\rceil})$ we can in fact interprete the whole of the new boxed language by the translation. This is what we shall do, so formally $\alpha \u22a2\varphi $ (where $\varphi $ might contain boxed sentences) is taken to mean $\alpha \u22a2\varphi *$ where $\varphi *$ is obtained by replacing the boxed expressions with arithmetical formulae as above.
There are a number of restrictions^{} we must impose on $\alpha $ (and thus on $\mathrm{\square}$, the meaning of which is determined by $\alpha $). These are known as HilbertBernays derivability conditions and they are as follows

•
if $\alpha \u22a2\varphi $ then $\alpha \u22a2\mathrm{\square}(\varphi )$

•
$\alpha \u22a2\mathrm{\square}(\varphi )\to \mathrm{\square}\mathrm{\square}(\varphi )$

•
$\alpha \u22a2\mathrm{\square}(\varphi \to \psi )\to (\mathrm{\square}\varphi \to \mathrm{\square}\psi )$
A statement $Cons$ asserts the consistency of $\alpha $ if its equivalent to $\mathrm{\neg}\mathrm{\square}(0=1)$. Gödel’s first incompleteness theorem shows that there is a sentence ${B}_{k}(k)$ for which the following is true $\mathrm{\neg}\mathrm{\square}(0=1)\to \mathrm{\u25c7}({B}_{k}(k))\wedge \mathrm{\u25c7}(\mathrm{\neg}({B}_{k}(k))$, where $\mathrm{\u25c7}$ is the dual of $\mathrm{\square}$, i.e. $\mathrm{\u25c7}(\varphi )\leftrightarrow \mathrm{\neg}\mathrm{\square}(\mathrm{\neg}\varphi )$. A careful analysis reveals that this is provable in any $\alpha $ which satisfied the derivability conditions, i.e. $\alpha \u22a2\mathrm{\neg}\mathrm{\square}(0=1)\to \mathrm{\u25c7}({B}_{k}(k))\wedge \mathrm{\u25c7}(\mathrm{\neg}({B}_{k}(k))$. Assume now that $\alpha $ can prove $\mathrm{\neg}\mathrm{\square}(0=1)$, i.e. that $\alpha $ can prove its own consistency. Then $\alpha $ can prove $\mathrm{\u25c7}({B}_{k}(k))\wedge \mathrm{\u25c7}(\mathrm{\neg}({B}_{k}(k))$. But this means that $\alpha $ can prove ${B}_{k}(k)$! Thus $\alpha $ is inconsistent.
Title  Gödel’s incompleteness theorems 
Canonical name  GodelsIncompletenessTheorems 
Date of creation  20130322 13:50:36 
Last modified on  20130322 13:50:36 
Owner  mathcam (2727) 
Last modified by  mathcam (2727) 
Numerical id  13 
Author  mathcam (2727) 
Entry type  Theorem 
Classification  msc 03B10 
Classification  msc 03F45 
Related topic  BeyondFormalism 
Defines  Gödel’s first incompleteness theorem 
Defines  incompleteness theorem 
Defines  HilbertBernays derivability conditions 
Defines  provability logic 