History of Science and Mathematics Stack Exchange is a question and answer site for people interested in the history and origins of science and mathematics. It only takes a minute to sign up.
Sign up to join this community
I was rewriting the Wikipedia article for metamathematics, and it was very difficult to find any references after the 1930s. The most important works seem to have been Gödel's completeness and incompleteness theorem.
Is there a field of mathematics today that is the spiritual successor to metamathematics as studied by Gödel, Hilbert, and the authors of Principia Mathematica?
Nowadays, metamathematics is a standard part of the landscape of mathematical logic.
On the one hand, most work on foundations of mathematics should probably be considered metamathematical. The standard foundation is set-theoretic, with ZFC and its variants being the usual formalizations. But this is by far not the only option and, for instance, there is recent work on what we now call univalent foundations based on abstract homotopy theory. In a sense this is perhaps closer to Principia than ZFC, since type theory plays a serious role. On the other hand, the approach is really category theoretic, and categories were not really conceived at the time of Principia. Although this new approach is receiving a large amount of attention, the logicians community at large is only beginning to understand its scope and possibilities. A recent series of threads at the FOM (foundations of mathematics) email list illustrates the current tension.
A large fraction of research in standard areas of mathematical logic is driven by metamathematical considerations, even if not in the sense of revised foundations.
For instance, reverse mathematics (also mentioned in another answer) studies the question of what set-existence axioms are actually needed for standard mathematical arguments. Typical results here argue that a standard theorem (such as the intermediate value theorem in classical analysis) is equivalent to or, at least, implies (over a reasonably weak background theory where the discussion takes place) an abstract "existence" axiom (e.g., every infinite binary tree has an infinite branch) or an instance of mathematical induction.
Proof theory deals with theories as mathematical objects, and studies their strength, based on either the length of proofs (suitably defined) when compared to some standard options, or in more subtle ways (such as considerations of the so-called proof-theoretic ordinals). For instance, within Peano arithmetic, the standard first-order system of axioms for number theory, we can easily define Turing machines, the usual formalization of "computer programs". We can then state whether a binary relation <' on the natural numbers is recursive, meaning that there is an algorithm (a Turing machine) that can decide of any pair of numbers n,m, whether or not n<'m. Many recursive relations are actually well-orderings, and given such a relation R and a theory T (extending Peano arithmetic) we can ask whether T can prove that R is a well-ordering. In general, the length of the provable well-orderings is significantly small, when compared with the length of all recursive well-orderings. We can then compare theories by checking which ones can prove well-orderability of longer (recursive) well-orderings. Based on this description, this seems a bit eccentric, but this is closely tied up with how much transfinite induction the theory can formalize and prove, so these proof-theoretic ordinals are actually very reasonable yardsticks of the power of expression and strength of theories.
In set theory, one of the standard themes is the comparison of consistency strength of theories. From Gödel's work, we know that a reasonable theory T cannot prove its own consistency, so if a theory T manages to prove the consistency of a theory S, this gives us a natural way in which T is stronger than S. The resulting consistency strength hierarchy is a fascinating mathematical object. It turns out that for natural extensions T of ZFC, we tend to be able to identify a large cardinal axiom that when added to ZFC results in a theory equiconsistent with T. This gives us a large cardinal companion of T, and the purely mathematical study of large cardinals then reflects the study of strengths of theories. That there is such a thing at all is remarkable. Inner model theory is the area of set theory that most directly concerns itself with trying to explain this phenomenon. The actual identification of the companion of a theory, on the other hand, is nowadays a mostly combinatorial question, thanks to Cohen's development of the forcing method.
References on univalent foundations can be found here and here. On reverse mathematics, see for example here in addition to the link given at the other answer. On proof theory, see here. For the consistency strength hierarchy in set theory, see here, although many papers and talks by John Steel are also relevant. Also, many of my posts in MathOverflow and Math.Stackexchange are related to this topic. Let me single out this one.
There are various more recent works on subjects that can be considered as metamathematics.
For example, Reverse Mathematics was started by Harvey Friedman in the mid-seventies.
Recently, there was quite a bit of excitement around Homotopy Type Theory and Univalent Foundations not only but also as it ties in nicely with effort to have automatically checkable proof.
And, needless to say, there is various other work in proof theory and other branches of mathematical logic. The issue that you might be perceiving is what is expressed in an answer on MathOverflow to a question around metamathematics; the problems are still studied but not anymore perceived as meta-mathematics but rather "just regular mathematics."
Taking your question in a somewhat different direction on might argue that efforts to make more and more of mathematics amenable to formal verification via proof assistants or even automated theorem proving is as natural and current continuation of early effort to formalize mathematics.
