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?
Best Answer
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:
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.