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 have branched. 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, are themselves surely 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 metamathematics, and we are proving theorems about which principles are provably valid, this would seem 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. This example therefore illustrates my point that there is really no coherent distinction into mathematics/metamathematics/meta-metamathematics.

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.