My opinion is that there is no crisp distinction between
mathematics, metamathematics and meta-metamathematics, and the
subjects thoroughly blend one into another in such a way that
prevents any coherent distinction.

Furthermore, even the categorization of particular topics as
mathematics or metamathematics has changed radically over time,
and many topics that were formerly considered metamathematics are
now just mathematics. For example, the ultrapower construction was
born in metamathematics, but is now widely seen as a fundamental
mathematical construction. The method of forcing was initially
used only for relative consistency proofs, but is now saturated
with a mixture of infinite combinatorics, ideals, Boolean
algebras, topology, transfinite limits, and so on. Computability
theory was born in purely philosophical speculation about what it
means for a human to undertake a computable procedure, but gave
birth to complexity theory and other extremely applied
mathematical topics. Is the polynomial time
hierarchy regarded today as metamathematics? I don't think so, but
it is a part of complexity theory, which is a part of
computability theory, which is traditionally considered
metamathematics. The study of large cardinals is tied to
fundamental issues in logic, such as definability and
constructiblity, but also involves at its core essentially
mathematical questions about infinite combinatorics, measure
theory, complex systems of embeddings and so on. Where does the
mathematics end and the metamathematics begin? It is all wrapped
up together.

The term metamathematics has traditionally included the entire
subjects of model theory, set theory, proof theory and
computability theory, but I think this kind of usage of the term
is simply no longer accurate, since huge parts of these subjects
are now more mathematical than metamathematical. I think that the
term "metamathematics" may have made more sense as a unifying
umbrella term in an earlier age, when many mathematicians were
simply less familiar with these subjects than is the case today.

Consider my work with Benedikt Löwe on the modal logic of forcing. The main theorem is that
the ZFC provably valid principles of forcing are exactly those in
the modal theory known as S4.2. Now, the principles under
consideration, the principles of forcing, can themselves surely
be considered as metamathematical, as they concern how truth varies in the generic
multiverse, the Kripke model of possible worlds consisting of the
set-theoretic universe in the context of all its forcing
extensions. Since the principles are thus metamathematics, and we are
proving theorems about which principles are provably valid, one could consider this to be solidly a case of meta-metamathematics. But if
you look at the paper, I think you will mainly find just plain old
mathematics, with detailed inductions and finite partial order
combinatorics and some infinite combinatorics and forcing
iterations, mixed in with some modal logic, which is essentially finite combinatorics. This example therefore illustrates my point that there
is really no coherent distinction into
mathematics/metamathematics/meta-metamathematics.

4more comments