Proofs of Gödel's theorem I am interested in different contexts in which Gödel's incompleteness theorems arise. Besides traditional  Gödelian proof via arithmetization and formalization of liar paradox it may also be obtained from undecidability results of Turing and Church. In the context of complexity theory, it is not hard to see that Gödel's theorem (as well as Turing's result) follows from the following Chaitin's result: there exists some natural number N such that for any program P of size more than N it is impossible to prove (say, in ZFC) that it is the smallest (in the sense of size, i. e. number of bits) of those programs which have the same inputs-outputs as P has. The number N depends on particular axiomatic system (say, ZFC) and is not very large so that it actually can be calculated.
If You know other ways towards Gödel's incompleteness theorems, please, present them. Particularly, can Goedel's theorem be obtained without use of self-referential ideas? 
 A: For Goedel's first incompleteness theorem, you can appeal to the existence of any computably (recursively) enumerable set $A$ that's not computable (recursive).  Specifically, suppose $T$ is an $\omega$-consistent, computable theory powerful enough to represent all computable functions.  Let $f$ be a total computable function listing all Natural numbers in $A$, and let $F$ represent $f$ in the theory $T$.  Then there must exist $n \in \mathbb{N}$ for which: 
(1) $T \nvdash \exists m F(m, n)$ nor (2) $T \nvdash \lnot\exists m F(m, n)$ 
Otherwise we could determine whether or not any given $n$ is in $A$ by effectively listing all theorems of $T$ until we received one of these statements, contradicting the fact that $A$ is not computable.  Specifically, (1) would tell us that $n \in A$ by the $\omega$-consistency of $T$ (i.e., there exists a true Natural number $m$ so $f(m) = n$) while (2) would tell us that $n \notin A$ because it is never listed by $f$.
If I recall correctly, a proof along these lines is mentioned in An Introduction to Kolmogorov Complexity and Its Applications by Ming Li and Paul Vitányi.
A: Gregor Lafitte's short paper: "G\"odel incompleteness revisited" is 
is a freely downloadable nice and concise overview of different kinds 
of proofs with a long list of references:
hal.archives-ouvertes.fr/docs/00/27/45/64/PDF/74-89.pdf
Supplement of 11th October 2011:
In a recent paper `The Surprise Examination Paradox and the Second
Incompleteness Theorem', Notices of the AMS Volume 57, Number 11 (it
can be downloaded from http://www.ams.org/notices/201011/rtx101101454p.pdf),
the authors give a new proof for Godel’s second incompleteness
theorem, based on Kolmogorov complexity, Chaitin’s incompleteness
theorem, and an argument that resembles the surprise examination
paradox.
A: Possibly the least "self-referential" argument for Gödel's incompleteness theorem
is the one due to Gentzen. His ordinal analysis of proofs in PA shows that any
ordering that PA can prove to be a well-ordering has ordinal less than
$\varepsilon_0$. Hence any ordering, definable in PA, that happens to be a
well-ordering of length at least $\varepsilon_0$ cannot be proved to be a well-ordering in PA.
A: This is a comment on a post by Andreas Blass here.
I have not read Kripke's statement, apart from Andreas's sketch above, but it sounds familiar from elsewhere, so let me comment a bit on the family of results and the many discussions about a family of unprovable statements of the form "for every $n$ there is a finite set that approximates a model of your theory T to the degree $n$" (where "to the degree $n$" is specified separately each time).
The first such statement found in print belongs to Paris and Harrington (see the original article in the Handbook for Mathematical Logic), and is sometimes referred to as "half-baked Paris-Harrington Principle". It says "for every $n$ there exists a finite  sequence of points that acts as diagonal indiscernibles for the first $n$ $\Delta_0$ formulas", where "diagonal indiscernibility" or "Paris indiscernibility" is the condition that for any $c_{i_0} < c_{i_1}<\dots< c_{i_k} < c_{j_1} <\dots< c_{j_k}$ in the sequence, we have: for every parameter $a < c_{i_0}$, the following holds: 
$\forall x_1 < c_{i_1} \exists x_2 < c_{i_2}\dots \phi(a, x_1, x_2... x_k)$ < -- > $\forall x_1 < c_{j_1} \exists x_2 < c_{j_2}\dots \phi(a, x_1, x_2, ...x_k)$.
Since that time statements of this form became routine intermediate steps in unprovability proofs. For example Shelah tried to modify this statement and came up with something that should be of strength $\Pi_1^1\text{-CA}_0$ (see "On logical sentences in PA").
The same idea is the core of most of Harvey Friedman's proofs in the last 25 years, but at higher levels of sophistication. For example for Proposition C, Friedman has 9 intermediate statements of this shape ("the Transmutations"), where the notion of indiscernibility changes at each step. And for Proposition B you need perhaps only 6 transmutations. 
When I was entering the subject in 2002 -- 2003, I wrote a naive article draft on half-baked PH and beyond, tinkering and trying to generalize. But then I realized that this topic is widely developed and discussed in the unprovability community, so since this piece already entered the unprovability community's knowledge pot long before me, perhaps none of it is publishable.
One more thought: there are two or three ways of dressing unprovability proofs. Paris's original dressing was via cuts in models of arithmetic, but after Harrington's simplification of n-densities, they wrote the proof for the Handbook in the finitistic way, via half-baked Paris-Harrington + compactness as I sketched above. After that Paris and his co-workers returned to thinking in terms of cuts in models of arithmetic. Both ways of dressing the proof are equally good, but each person usually chooses one.
A: Dear Sergei and John. There is just too much to say. If I give you 3 pointers - it will not mean that these are good starting points or that these are the most important developments.
The Jones polynomial is from JSL 43 (1978), no 2. but me and De Smet recently enhanced the polynomial a bit (shortened it by 7 symbols)... :)
Friedman's book is on his homepage. The introduction is quite readable, and contains a long list of unprovable statements.
You can also have a look at my "Brief introduction" on my homepage, although I am a bit ashamed of that naive paper of mine written 6 years ago. I am now writing a long better piece, with all motivations and explanations, and the Arithmetical Splitting story.... but it will take some time.
A: Apart from usual proofs with diagonalization, have a look at model-theoretic proofs (Kotlarski's proof, Kreisel's left-branch proof, etc..), then there are some other proofs that formalize paradoxes (Kikuchi's, Boolos's, etc... there are about a dozen, most of them mentioned in Kotlarski's book).
If you don't want full generality ("for every rec. ax. theory T") then of course almost every proof in modern Unprovability Theory does not use any self-reference (you build a model of your theory by hands, using some unprovable combinatorial principle). Have a look at some easy recent accessible model-theoretic proofs of the Paris-Harrington Principle.
At the low end of the consistency strength spectrum (ISigma_n, PA, ATR_0), for theories that already have good classifications of their provably recursive functions, PH and other unprovable statements can also be proved unprovable using ordinal analysis (e.g. Ketonen-Solovay style), without using diagonalization tricks.
For higher ends of the strength spectrum (SMAH, SRP, etc), H. Friedman's highly technical results also don't use any diagonalization.  This is a huge powerful machinery, and much new research is happening there.
MDRP theory gives interesting examples: have a look at the Jones polynomial expression: you can indeed substitute numbers into it and hit every consistency statement by its instances. There are similar ones for n-consistency for each n.
There is much more to say: this is a big subject, with huge bibliography. And, yes, much of the body of results in the subject is unpublished.  I can give more pointers if necessary.
A: Saul Kripke gave a proof of incompleteness using nonstandard models and a notion of "fulfillability".  Roughly speaking, a sequence fulfills a (prenex) formula if the formula is true when its successive quantifiers are bounded by the terms of the sequence.  Kripke apparently never published this, but Hilary Putnam presented in a lecture, subsequently published as "Nonstandard models and Kripke's proof of the Gödel theorem", Notre Dame Journal of Formal Logic 41 (2000) pp. 53-58.  The MathSciNet review by Alex Wilkie reads:

"This paper was developed from a lecture given by the author at Beijing University in 1984 which described Kripke's notion of fulfillability and how it may be used to give a proof of the incompleteness of Peano arithmetic. Putnam has decided to publish it now because Kripke has still not published it himself. The point of this proof is that it is semantic and avoids self-reference, but is much simpler than the Paris-Harrington argument. It achieves this simplicity by considering a sentence that directly expresses the existence of long (finite) sequences of natural numbers that verify all the bounded approximations of the Peano Axioms, rather than deducing this existence, as Paris and Harrington had to, from a version of Ramsey's Theorem. Thus the simplicity comes at the cost of mathematical naturality. Also, although it is not made explicit in this paper, one still has to go through the process of Gödel numbering and the construction of a uniform satisfaction predicate for bounded quantifier formulas." 

A: In a recent AMS notices article, Shira Kritchman and Ran Raz give a proof of Godel's Second Incompleteness Theorem based on the Surprise Examination Paradox.
A: I am amazed that nobody has mentioned Chaitin's information-theoretic argument.
In brief:  Fix a computer language that's capable of doing arithmetic.  Define the length of a program to be the number of keystrokes you need to enter it into your computer.  For each pair of natural numbers $c,n$, consider the statement
$A_{c,n}$:  No program of length less than $c$ can print the number $n$.  
Clearly for any fixed $c$, there are infinitely many true statements of the form $A_{c,n}$.  
Now for each $c$, write a program called $P_c$ that inspects every possible string of symbols (say in alphabetical order) and asks "Is this string a proof of any statement of the form $A_{n,c}$?''  If the answer is yes, $P_c$ prints $n$ and then stops.  If not, it proceeds to the next string of symbols.
Note that the length of $P_c$ can be taken to grow pretty slowly with $c$.  This is because you can convert, say, the program $P_{10}$ into the program $P_{10000}$ by just changing all the $10's$ to $100000$'s, which just sprinkles in a few extra zeros.  Thus there exists a $C$ such that the length of $P_C$ is less than $C$.  
Now if $P_C$ prints the number $n$, we have a proof of $A_{C,n}$, which implies that $P_{C}$ cannot print the number $n$.  Therefore $P_C$ never stops.  Thus there can be no proof of any statement of the form $A_{C,n}$, even though infinitely many of these statements are true.
