I'm only familiar with the very basics of mathematical logic, but over the last few days I have been looking into Gödel's incompleteness theorems and it seems to me (but I might simply be grossly misunderstanding something) that there's a certain circularity in the argument, or rather in the (perhaps philosophical) conclusion that no formal system can be sufficient to do all of mathematics. Let me explain.
As I understand, the original aim of Hilbert was to formalize all of mathematics; basically, he thought that one should be wary of intuitions and only prove statements by using a well-defined set of axioms and a set of deduction rules. Then Gödel came along and demonstrated with his first incompleteness theorem that (under very mild conditions) such an axiomatic system is necessarily incomplete, i.e. contains 'true' statements that are not formally provable within the system, which would undermine Hilbert's aim.
But it is my understanding that the proof of Gödel's theorem is a proof on a metalevel, i.e. the complete proof cannot be written down as a formal proof in the formal language about which the theorem makes its statement. Even though the Gödel numbering can be used to express a 'meta' statement as an arithmetical statement that can be mirrored inside the formal system and so on, in order to decide that this mirroring is indeed legitimate we need to look at the formal system 'from the outside'.
In Hilbert's view then, could we not argue that the proof of the theorem relies on 'appealing to intuition', as it cannot be formalized? Don't get me wrong, I think the proof is sound (as far as I understand it, which is only at a superficial level) but nevertheless, one could still take the position that ZFC, say, is the ultimate, correct axiomatic system to do all of mathematics with, and that would imply that Gödel's first incompleteness theorem is not a theorem at all (i.e. formally within ZFC) and hence one should be wary of taking its conclusion as being 'true'. From that perspective, it would seem that Hilbert's aim could still be defendable.
Any thoughts on this issue are appreciated.
EDIT: As pointed out in the answers, my idea that the proof of Gödel's incompleteness theorems cannot be formalized within ZFC was misguided. Indeed they have been formalized in ZFC. However, this seems to lead to another paradox (which is why I presumed that they couldn't be formalized within ZFC in the first place).
A common formulation (see e.g. [1]) of the first incompleteness theorem is this:
Theorem 1 In any 'sufficiently nice' formal system $F$, one can construct a sentence $G_F$ such that $F$ can neither prove $G_F$ nor prove $\neg G_F$. It can be shown, however, that $G_F$ is true.
(The last part of the theorem is pointed out only later in [1].) 'True' is supposed to mean 'true in the standard interpretation of the natural numbers', so showing $G_F$ to be true would amount to proving $G_F$ within ZFC, right? But now let's take $F$ to be ZFC.
Then the theorem asserts that $G_{\text{ZFC}}$ is neither provable nor disprovable within ZFC, but that it can be shown to be true, i.e. provable within ZFC!
This is a contradiction. What am I missing here?
EDIT: I think might have identified the error in my thinking, thanks to the answers. The point seems to be that if we want to apply the theorem to ZFC we must think about the situation as consisting of nested copies of ZFC.
Let $M$ be our metatheory, which I choose to be $M=$ZFC. Then within $M$ we can define a new formal system $F$, which we also define exactly as $F=ZFC$. So now we can talk about $F$ (i.e. ZFC) inside $M$ (i.e. ZFC). Then Gödel's first incompleteness theorem states that there exists a sentence in ZFC that can neither be proven nor disproven from the axioms, however, that by embedding ZFC in a 'meta' copy of itself, and using the same 'meta' axioms of ZFC to look at the inner copy, we can prove that sentence.
Is this summary correct? I'm still not 100% sure if I'm making sense.
I think you are conflating concepts. Gödel's Theorems can be formalized inside a sufficiently rich theory, in particular they can be formalized in ZFC! So if you insist ZFC (or any other sufficiently rich theory) is true, then you must also believe that Gödel's theorems are true, and so the theory is incomplete.
However, as you say, Gödel's theorems are on the meta level, so what's the difference? You can talk about the theory of ZFC inside the own theory of ZFC. The difference is that those results you will obtain ZFC are about "ZFC as seen from inside ZFC". As long as you think ZFC true (consistent), though, that doesn't really matter; ZFC will be incomplete.