MathOverflow will be down for maintenance for approximately 3 hours, starting Monday evening (06/24/2013) at approximately 9:00 PM Eastern time (UTC-4).

3 Corrected three small typos

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 mentio9ned mentioned in Kotlarski's book).

If you don't want full generality ("for every rec.axrec. 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 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.

2 added 58 characters in body

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

1

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 mentio9ned 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 be proved unprovable 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.