I am looking for examples of proofs of Godel's (First) Incompleteness Theorem which are *essentially different* from (Rosser's improvement of) Godel's original proof.

This is partly inspired by questions two previously asked questions: 

(https://mathoverflow.net/questions/59106/proofs-of-godels-theorem) 

(https://mathoverflow.net/questions/3776/when-are-two-proofs-of-the-same-theorem-really-different-proofs)

To give an example of what I mean: The Godel/Rosser proof (see http://www.jstor.org/pss/2269059 for an exposition) shows that any consistent sufficiently strong axiomatizable theory is incomplete. The proof uses a substantial amount of recursion theory: the representability of primitive recursive functions and the diagonal lemma (roughly the same as Kleene's Recursion Theorem) are essential ingredients. The second incompleteness theorem - that no consistent sufficiently strong axiomatizable theory can prove its own consistency - is essentially a corollary to this proof, and a rather natural one at that. On the other hand, in 2000 Hilary Putnam published (https://doi.org/10.1305/ndjfl/1027953483) an alternate proof of Godel's first incompleteness theorem, due to Saul Kripke around 1984. This proof uses much less recursion theory, instead relying on some elementary model theory of nonstandard models of arithmetic. The theorem proven is slightly weaker, since Kripke's proof requires $\Sigma^0_2$-soundness, which is stronger than mere consistency (although still weaker than Godel's original assumption of $\omega$-consistency). 

Kripke's proof is clearly sufficiently different from the Godel/Rosser proof that it deserves to be considered a genuinely separate object. What makes the difference seem really impressive, at least to me, is that Kripke's proof yields a different corollary than that of Godel/Rosser. In a short paragraph, Putnam shows (and I do not know whether this part of his paper is due to Kripke) that Kripke's argument proves that there is no consistent finitely axiomatizable extension of $PA$. This is not a result which I know to follow from the Godel/Rosser proof; moreover, the Second Incompleteness Theorem, which is a corollary to Godel/Rosser's proof, does not seem easily derivable from Kripke's proof.

Motivated by this, say that two proofs of (roughly) the same theorem are *essentially different* if they yield different natural corollaries. Clearly this is a totally subjective notion, but I think it has enough shared meaning to be worthwhile.

My main question, then, is:

1) What other essentially different proofs of something resembling Godel's First Incompleteness Theorem are known? In other words, is there some other proof of something close to "every consistent axiomatizable extension of $PA$ is incomplete" which does not yield Godel's Second Incompleteness Theorem as a natural corollary?

I am especially interested in proofs which don't yield the nonexistence of consistent finitely axiomatizable extensions of $PA$, either, and in proofs which do yield *some* natural corollary. I don't particularly care about the precise version of the First Incompleteness Theorem proved: if it applies to systems in the language of second-order arithmetic, if it assumes $\omega$-consistency, or if it only applies to systems stronger than $ATR_0$, say, that's all the same to me. However, I *do* require that the version of the incompleteness theorem proved apply to all sufficiently strong systems with whatever consistency property is needed; so, for example, I would not consider the work of Paris and Harrington to be a good example of this.

The only other potential example of such an essentially different proof that I know of is the proof(s) by Jech and Woodin (see https://andrescaicedo.files.wordpress.com/2010/11/2ndincompleteness1.pdf), but I don't understand that proof at a level such that I would be comfortable saying that it is in fact an essentially different proof. It seems to me to be rather similar to the original proof. Perhaps someone can enlighten me?


Of course, entirely separate from my main question, my characterization of the difference between the specific two proofs of the incompleteness theorem mentioned above may be incorrect. So I'm also interested in the following question:

2) Is it in fact the case that Kripke's proof does not yield Second Incompleteness as an natural corollary, and that Godel/Rosser's proof does not easily yield the nonexistence of a consistent finitely axiomatizable extension of PA as a natural corollary?