Proofs of Gödel's theorem

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.

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

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.