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.

  • 4
    $\begingroup$ Your understanding that Gödel’s theorems only apply on the meta-level is incorrect. These theorems can be proved in any reasonable foundational theory. $\endgroup$ Dec 25, 2023 at 18:05
  • $\begingroup$ A correct statement of Gödel's incompleteness theorem has the consistency of $F$ as a hypothesis. In your words, stated for ZFC, it would be: "If ZFC is consistent, then there exists a sentence in ZFC that holds in $\mathbb{N}$ but that can neither be proven nor disproven from the axioms of ZFC". The bolded part is what you disregard when you get your "paradox". You get something that is neither provable nor disprovable within ZFC, but that can be shown to be true under the hypothesis that ZFC is consistent. You get a paradox only if ZFC proves the hypothesis, i.e. its own consistency. $\endgroup$
    – Z. A. K.
    Dec 29, 2023 at 16:19
  • $\begingroup$ By the way, as far as I can tell, all the statements of the theorem in the SEP get this right. It's much harder to see in your reworded formulation, simply because you combine consistency with the other assumptions (recursively enumerable axioms etc.) into "sufficiently nice". While ZFC proves these other premises, it does not prove its own consistency (at least as far as we know as of 2023), so you don't get to conclude that ZFC is incomplete inside ZFC. But Gödel's theorem is the whole conditional (if $F$ consistent then...) and ZFC proves that conditional, just not its premise when $F$=ZFC. $\endgroup$
    – Z. A. K.
    Dec 29, 2023 at 16:29
  • $\begingroup$ @Z.A.K. Thanks, that clears up a large part of my confusion. $\endgroup$
    – Inzinity
    Dec 29, 2023 at 17:23

2 Answers 2


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.

  • 2
    $\begingroup$ Besides, Hilbert wanted much much more out of a mathematical foundation. He expected to prove the consistency of all of math using only the strength of finite math, in his words a little bit. $\endgroup$
    – Julián
    Dec 25, 2023 at 15:40
  • $\begingroup$ My understanding was misguided then. However, a ZFC proof of the first incompleteness seems to lead to a contradiction (see the edit in my question), which is why I presumed they couldn't be formalized. I'm unsure as to what the error in my reasoning is. $\endgroup$
    – Inzinity
    Dec 28, 2023 at 10:46

You can download the second edition of my Introduction to Gödel's Theorems (originally CUP, now freely available) at https://www.logicmatters.net/resources/pdfs/godelbook/GodelBookLM.pdf

If you look at pp. 272 to 279, you'll find a discussion of the impact of Gödel's incompleteness theorems on Hilbert's program which should be more-or-less stand-alone comprehensible if you know a bit about the Gödelian results.

I won't try to summarise nine pages here, as indeed the issues get a bit involved -- Hilbert's somewhat unspecific ideas can be sharpened up in more than one way. Gödel's first theorem refutes one sharpened proposal, Gödel's second theorem refutes another sharpened proposal. Is there wriggle room left for another sharpened proposal that is still recognisably Hilbertian?

Well, you'll have to read to see what conclusion I came to!

  • $\begingroup$ Thanks for the nice reference. I'm currently reading it chapter by chapter. Hopefully, it will clear things up. $\endgroup$
    – Inzinity
    Dec 28, 2023 at 10:53

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .