I've mentioned in comments a couple of times that I don't consider formal systems to talk about themselves, and that consequently Gödelian problems are irrelevant. So what am I actually on about?
It's generally accepted in mathematical logic that a formal system which embodies Peano Arithmetic (PA) is able to talk about itself, by means of Gödel numberings; statements and proofs within the system can be represented as positive integers, at which point "X is a valid proof in the system" becomes equivalent to an arithmetical statement about #X, the Gödel number representing X. This is then diagonalised to produce the Gödel sentence (roughly, g="There is no proof X such that the last line of X is g", and incompleteness follows. We can also do things like defining □ ("box") as the function from S to "There is a proof X in PA whose last line is S" (intuitively, □S says "S is provable in PA"). This then also lets us define the Löb sentence, and many other interesting things.
But how do we know that □S ⇔ there is a proof of S in PA? Only by applying some meta-theory. And how do we know that statements reached in the meta-theory of the form "thus-and-such is true of PA" are true of PA? Only by applying a meta-meta-theory. There is no a-priori justification for the claim that "A formal system is in principle capable of talking about other formal systems", which claim is used by the proof that PA can talk about itself. (If I remember correctly, to prove that □ does what we think it does, we have to appeal to second-order arithmetic; and how do we know second-order arithmetic applies to PA? Either by invoking third-order arithmetic to analyse second-order arithmetic, or by recourse to an informal system.)
Note also that the above is not a strange loop through the meta-level; we justify our claims about arithmeticn by appeal to arithmeticn+1, which is a separate thing; we never find ourselves back at arithmeticn.
Thus the claim that formal systems can talk about themselves involves ill-founded recursion, what is sometimes called a "skyhook". While it may be a theorem of second-order arithmetic that "the strengthened finite Ramsey theorem is unprovable in PA", one cannot conclude from second-order arithmetic alone that the "PA" in that statement refers to PA. It is however provable in third-order arithmetic that "What second-order arithmetic calls "PA" is PA", but that hasn't gained us much - it only tells us that second- and third-order arithmetic call the same thing "PA", it doesn't tell us whether this "PA" is PA. Induct on the arithmetic hierarchy to reach the obvious conclusion. (Though note that none of this prevents the Paris-Harrington Theorem from being a theorem of n-th order arithmetic ∀n≥2)
What, then, is the motivation for the above? Well, it is a basic principle of my philosophy that the only objects that are real (in a Platonic sense) are formal systems (or rather, syntaxes). That is to say, my ontology is the setclass of formal systems. (This is not incompatible with the apparent reality of a physical universe; if this isn't obvious, I'll explain why in another post.) But if we allow these systems to have semantics, that is, we claim that there is such a thing as a "true statement", we start to have problems with completeness and consistency (namely, that we can't achieve the one and we can't prove the other, assuming PA). Tarski's undefinability theorem protects us from having to deal with systems which talk about truth in themselves (because they are necessarily inconsistent, assuming some basic properties), but if systems can talk about each other, and if systems can talk about provability within themselves (that is, if analogues to the □ function can be constructed), then nasty Gödelian things end up happening (most of which are, to a Platonist mathematician, deeply unsatisfying).
So instead we restrict the ontology to syntactic systems devoid of any semantics; the statement ""Foo" is true" is meaningless. There is a fact-of-the-matter as to whether a given statement can be reached in a given formal system, but that fact-of-the-matter cannot be meaningfully talked about in any formal system. This is a remarkably bare ontology (some consider it excessively so), but is at no risk from contradiction, inconsistency or paradox. For, what is "P∧¬P" but another, syntactic, sentence? Of course, applying a system which proves "P∧¬P" to the 'real world' is likely to be problematic, but the paradox or the inconsistency lies in the application of the system, and does not inhere in the system itself.
EDIT: I am actually aiming to get somewhere with this, it's not just for its own sake (although the ontological and epistemological status of mathematics is worth caring about for its own sake). In particular I want to set up a framework that lets me talk about Eliezer's "infinite set atheism", because I think he's asking a wrong question.
Followed up by: The Apparent Reality of Physics
Not so! From most interesting formal systems there are exponentially many possible deductions that can be made. All known agents can only make a bounded number of possible deductions. A widely believed conjecture implies that longer-lived agents could only make a polynomial number of possible deductions.
Um, that's not quite what I meant... if I prove a theorem you're unlikely to prove its negation, and if I tell you I have a proof of a theorem you're likely to be able to find one. Moreover, in the latter case, if you're not able to find a proof, then either I am mistaken in my belief that I have a proof, or you haven't looked hard enough (and in principle could find a proof if you did). That doesn't mean that every agent with "I think therefore I am" will deduce the existence of rice pudding and income tax, it only means that if one agent can ... (read more)