As far as I know, Gödel's first incompleteness theorem is usually presented in the context of natural numbers, addition and multiplication, and is rather technical. However, I know the following "shortcut" to the theorem: suppose we had a sound and complete system for mathematics, then if it's sufficiently general we could formalize statements about halting and solve the halting problem by enumerating proofs until we found one that decides halting for a given program, contradiction. I think one could even construct the true, unprovable sentence by repeating the proof of unsolvability of the halting problem.

I don't know the original proof but with this I don't feel like I'm missing out. I don't know how to formalize Turing machines in arithmetic but I just take it as a theorem about "sufficiently general" mathematics, where surely such a formalization exists.

Now I tried to understand the completeness theorem from Papadimitriou's book but it felt like the proof was longer than it could be in an ideal world. Are there perhaps similar shortcuts to Gödel's completeness and second incompleteness theorems?

  • 1
    $\begingroup$ "Complete and sound system for mathematics" seems to be a much stronger condition than "a system that represents addition and multiplication of natural numbers" $\endgroup$ Apr 4, 2021 at 17:42
  • $\begingroup$ I believe you need more than that. You al,so need the ability to express second order logic. $\endgroup$ Apr 5, 2021 at 5:23

1 Answer 1


Short version: your first incompleteness theorem shortcut works (after some fixing), but I strongly suspect that no shortcuts exist for the completeness or second incompleteness theorems. For the former, we have concrete obstacles in the form of unavoidable interactions with noncomputable sets and the axiom of choice; for the latter, a serious assumption about the expressibility of the theory in question (which cannot be "built in" directly a la the first incompleteness theorem shortcut) is implicit in even the statement of the theorem being proved.

Incidentally, re: the first incompleteness theorem you may be interested in this old Mathoverflow question of mine (which I've also linked below in a different context). I think the breadth of the answers there provide a good contrast with the relative paucity of proofs of the completeness and second incompleteness theorems.

First, let me confirm (with caveats) the outline you've described: it does work (once some details are filled in and the often-forgotten hypothesis of computable axiomatizability is added). Specifically, we can whip up a theory directly treating Turing machines which is computably axiomatizable, and prove via the usual analysis of the halting problem (+ a bit of care) that this theory is incomplete. If we further introduce the notion of computable inseparability we can prove the stronger result that this theory is essentially incomplete (= there is no consistent completion of this theory which is computably axiomatizable); in my opinion this latter is the "right" version of the incompleteness theorem, and this doesn't take much more work.

A drawback of this approach is that it applies to a narrower class of theories. The "ultimate form" of the first incompleteness theorem is "Every sufficiently rich consistent computably axiomatizable theory is incomplete," and the notion of "sufficiently rich" provided by your outline is unnecessarily strong. In fact the first incompleteness theorem applies to extremely weak theories - see e.g. the discussion in this paper of Beklemishev. In my opinion this is not merely superficial, it's an important feature of the topic. That said, if all you care about is the existence of a point beyond which we can't have completeness (+ computable axiomatizability and consistency of course) then this isn't directly relevant to that; but still, though, don't dismiss it out of hand!

OK, now what about the completeness theorem?

In my opinion the completeness theorem is actually significantly harder and less intuitive than the incompleteness theorem(s). I know of two proofs, Gödel's original proof (see Section $4$ of this paper of Avigad) and Henkin's later proof (which is the standard one). I've summarized Henkin's argument a couple times on this site; see e.g. here, as well as 1 and 2 for some further discussion.

I don't want to recap all that, but very briefly the key idea is the following:

For every theory $T$ there is a natural "associated structure" $\mathcal{M}$ which is a plausible candidate for a model of $T$ - basically, $\mathcal{M}$ consists of the terms of $T$ modulo $T$-provable equivalence.

After hitting on that idea, we then pin down a property of $T$ which ensures that the corresponding $\mathcal{M}$ does in fact satisfy $T$ and subsequently show that every $T$ can be extended to a $T'$ with this property which is consistent if the original $T$ is. This is really a second new idea on its own, but in my opinion is less transformative than the "term model" idea above.

Now first of all in my opinion this is an absolutely beautiful argument and one shouldn't look for a shortcut at all. Independently of that however I don't know of a shortcut, and I suspect none exists. (Gödel's original argument does go a different way, but it's not particularly shorter and in my opinion is far less illuminating.) Why is that? Well, we can prove that the completeness theorem needs some heavy machinery in a couple senses:

  • There are computably axiomatizable consistent theories (even ones consisting of a single sentence!) without computable models.

  • The full version of the completeness theorem (e.g. for all theories in all languages, not just the "nice" languages we usually work with) is not provable in $\mathsf{ZF}$ alone.

So the completeness theorem has unavoidable interactions with both noncomputable sets and the axiom of choice. Given that, I think the existing proofs are about as good as we could hope for (although I would be delighted by a genuinely different third proof, regardless of how complicated it is - maybe someone here knows about one?).

Finally, what about the second incompleteness theorem?

Well, this is proved as a corollary of the proof of the first incompleteness theorem (it doesn't seem to follow from the mere statement of the first incompleteness theorem), so it's reasonable to hope that the shortcut proof of the first incompleteness theorem should similarly yield the second as a corollary. This wouldn't be a separate shortcut, but an extension of the original shortcut.

The issue is that the second incompleteness theorem is really taking for granted the ability of the theory in question to talk about its own proof system: if we don't have that, we can't even state the second incompleteness theorem! At this point there is an unavoidable "catch-our-tail" argument we need to make: we can't (as we did in the shortcut) simply whip up a theory which is automatically sufficiently expressive, since richer theories have (at first glance) more complicated proof systems. So we do have to do some work here, and at this point we're starting to recapitulate the standard proof of the first incompleteness theorem. The only thing the original shortcut helps us with is talking about computable functions in a simpler way; beyond that it doesn't really simplify things. In fact, because of the "referential prerequisite" of the second incompleteness theorem, I think that it cannot have a substantive shortcut. Of course this is a vague claim, but I do think it's true in a reasonable sense.

  • $\begingroup$ Thank you. Reading your summary of the completeness proof brought back memories of what felt off about the proof, namely the whole thing about terms feels rather artificial to me. Do you have a recommended source for a full proof of the completeness theorem or perhaps a proof of the second incompleteness theorem with a simpler way of talking about computable functions (like handwaving it away as I did ;) )? $\endgroup$
    – acupoftea
    Apr 4, 2021 at 19:59
  • $\begingroup$ @acupoftea "the whole thing about terms feels rather artificial to me." I disagree. Note that that's exactly the analogy of the free group (or free whatever): we look at the terms we can build from a given alphabet, and mod out by the relations the theory imposes. If you want to avoid (closed) terms, e.g. because theories like $\mathsf{ZFC}$ don't have any in the first place, you can do so as well: work instead with "pseudoterms," that is formulas in one free variable which the theory proves have unique solutions. Every closed term $t$ has a corresponding pseudoterm, namely "$x=t$." (cont'd) $\endgroup$ Apr 4, 2021 at 20:32
  • $\begingroup$ But even when we don't have many terms, we still may have lots of pseudoterms. For instance, in $\mathsf{ZFC}$ the formula "$\forall y(\neg y\in x)$" is a pseudoterm (corresponding intuitively to $\emptyset$). We can then form the "pseudoterm model" instead of the "term model," and nothing substantive will change. (Note that the idea of passing from pseudoterms to terms is already implicit in a technique we've seen before, namely Skolemization.) (cont'd) $\endgroup$ Apr 4, 2021 at 20:34
  • $\begingroup$ Besides being motivated by things like free groups, pseudoterm models can be motivated as an attempt to get a "syntactic analogue" of the set of definable elements of a given structure $M$. For many naturally-occurring $M$s the set of definable elements of $M$ satisfies a lot of the basic properties of $M$ itself (e.g. consider the true natural numbers inside a nonstandard model of true arithmetic); the pseudoterms are basically an attempt to "guess the model" ahead of time, which is a very natural thing to do when trying to build a model in the first place. (cont'd) $\endgroup$ Apr 4, 2021 at 20:36
  • 1
    $\begingroup$ (Incidentally, note that "pseudoterm" is not standard terminology.) As for sources, I like the presentation of the completeness theorem in Boolos/Burgess/Jeffrey. For the second incompleteness theorem, the point of that part of my answer is that handwaving computable functions really won't save you much time, so I don't know of any. $\endgroup$ Apr 4, 2021 at 20:38

You must log in to answer this question.

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