Do people actually study this stuff anymore?
You betcha. Here's part of a course description written by Richard Grandy for a philosophy course he taught at Rice University in the Spring of 2003. The course was called "Incompleteness, undecidability and computability" (ahem, my underlining, of course):
The central focus of this course is Godel's Incompleteness Theorem which states that in any consistent formal system which is adequate for arithmetic there is a true but unprovable sentence. Three concepts are involved in the theorem--diagonal arguments, Goedel numbering and algorithms. Diagonal arguments and Goedel numbering coalesce in producing the infamous sentence which "says of itself" that it is unprovable. The concept of an algorithm is crucial in the general statement of the theorem because it applies only to formal systems. A formal system is one for which there is an algorithm to determine what is an axiom and what is a correct application of a rule of inference. Until we understand exactly what an algorithm is, the scope of the theorem is unclear.
A closely related result is Turing's theorem that for any class of algorithms to calculate functions of natural numbers there is a function which is not computable by an algorithm of that class. Church advanced the thesis, Church's thesis, that any computable function is computable by a specifiable class of algorithms. Thus combining these we can describe a function which is absolutely uncomputable.
Following the Snark theory that what you prove three times is true, we will prove Goedel's theorem by at least three different methods. One will be a non-constructive method, based on Turing's theorem and using a diagonal argument, which shows that some sentence is true and unprovable but gives no clue as to how to find it. Another will be a version of the original argument which painstakingly produces the sentence in question via Goedel numbering. I believe it is important to slog through the details of this construction to truly understand the theorem, though most students only appreciate this experience later.
Goedel also proved a less well-known Second Incompleteness Theorem, stating that a consistent formal system cannot prove its own consistency. We will explain why someone might have thought that a formal system could have proved its own consistency, and why it turns out it cannot. Having slogged through a detailed proof of the first theorem makes understanding the second theorem almost a snap. The reason it is not quite a snap is that it turns out to be somewhat subtle what it means to prove consistency.
We will also prove a more general form of Goedel's first theorem, after we understand the Kleene Hierarchy. Problems for which there is a decision procedure are the first stage of the hierarchy; problems for which there is either a proof procedure or a refutation procedure (but not both) are the next two stages. There are infinitely many higher stages of undecidability. The generalized Goedel theorem says that even if we had a non-formal system whose axioms were at some stage of this hierarchy, the system would be incomplete! The usual Goedel's theorem is just the simplest case of the general theorem.
Other topics will emerge as we discuss the main themes. We will investigate various definitions of "algorithm" and show that they are equivalent, giving support to Church's Thesis. We will show that there is no algorithm for determining if a sentence is a logical truth (as promised in 305). We will balance precariously exploring the edge of expressibility as we describe non-computable functions, argue that some sentences are true but unprovable, and describe some sets which are undefinable. All of these verge on effing the ineffable.
We will also spend some time on philosophical implications, or alleged philosophical implications, of the mathematical results. Roger Penrose has advanced arguments, based on Goedel and Turing's results, which he claims show that human capacities exceed those of computers. (His arguments are certainly overstated. He bases his claims on an alleged general human ability to see that the Goedel sentence for a formal system is true. At this point you will be one of a very very few humans who are able to construct the Godel sentence.) We will critically examine his arguments that you can also see that it is true, drawing on our deep understanding of Godel's theorem developed from the earlier exercises. As a result of this course you will either cease to be a computer (if he is right) or you will understand why Penrose's argument is wrong. You will also learn how many Goedel sentences there are and why Godel's theorem is very unlike the Heisenberg principle, to which it is often compared.
As time permits, we will also discuss systems which, in some respect, avoid Godel's theorem, and possibly look at some consistency proofs for number theory in order to understand how those proofs go beyond the deductive power of number theory.
We will also spend some time on philosophical implications, or alleged philosophical implications, of the mathematical results. Roger Penrose has advanced arguments, based on Goedel and Turing's results, which he claims show that human capacities exceed those of computers. (His arguments are certainly overstated. [snip]