What is Metamathematics?

Mathematics consists in various theories. Theories of numbers, functions and sets. For example,

(1) the successor of no natural number is $0$.
(2) distinct natural numbers have distinct successors.
(3) if P holds for 0 and holds for $n+1$ whenever it holds for $n$, then it holds for all $n$.

or

(4) there is an empty set.
(5) if $x$ and $y$ are sets, then $\{x,y\}$ is a set.
(6) if $x$ is a set, then $\{y \in x \mid Py\}$ is a set.
and so on.

The objects (or the prima facie objects: the values of variables) of mathematics are numbers, functions, sets, spaces, structures, fields, categories, and so on.

Metamathematics, then, is the the study of mathematical theories. Its objects are mathematical theories. For example, we have a lot of knowledge about formalized mathematical theories:

(7) for any numbers $n, k$, we have: $Q \vdash \underline{n+k} = \underline{n} + \underline{k}$.
(8) $Q \nvdash \forall x \forall y(x + y = y + x)$.
(9) If $PA$ is consistent, then $PA + \neg Con(PA)$ is consistent.
(10) $PA$ is not finitely axiomatizable.
(11) If every finite subset of $T$ has a model, then $T$ has a model.

Within metamathematics, the objects referred to needn't only be syntactical entities. It is routine in metamathematics to talk of numbers, functions, sets and models, as well as syntactic strings, formulas, derivations, and theories.

There is a sense also in which metamathematics counts as part of mathematics. For the statements (7)-(11) above will all be found in various mathematics textbooks (called, e.g., A Mathematical Introduction to Logic, Computability and Logic, and so on), used in mathematics courses. One uses ordinary (informal) mathematical assumptions and methods to prove the results (7)-(11). This isn't to say that one can always close the gap between the object language theory and the metalanguage theory. (Tarski's theorem suggests that in some deep sense, one cannot.)

An interesting point is that the theories one has most understanding of in metamathematics (I mean the theories that we have definite results about, such as (7)-(11)) are theories like: $Q$, $PRA$, $I \Sigma_n$, $ACA_0$, $Z_2$, $Z$, $ZF$, etc. These are generally formalized theories given in formalized languages. So, such theories are not exactly the same as the informal theories that the mathematician themself might know and use. Presumably, there is some formalization relationship whereby the assumptions of informal number theory can be formalized into---i.e., translated into---say, the language of $PA$, and then proved.

There is an important metamathematical thesis concerning informal mathematical theories. This thesis grew out of the classic foundational work of Frege, Dedekind, Cantor, Peano, Zermelo and Russell, from say 1879 (Begriffsschrift) to 1910-2 (Principia Mathematica). It lacks a standard name, so let me call it the Z Thesis (you can read "Z" as "Zermelo", or just as "some kind of set theory, like $Z$, $ZF$, etc."):

The Z Thesis
Virtually all (say, 99.9%) informal mathematics can be formalized and proved in $ZFC$.

Indeed, often in something a lot weaker, such as a subsystem of second-order arithmetic. But, in fact, it turns out that very simple systems of arithmetic are more or less equivalent to simple systems of set theory. In particular, $PA$ is intimately related to $Z$ set theory with the negation of the axiom of infinity.

The Z Thesis is not a normative claim that informal mathematics should be reduced to set theory; it is a descriptively factual claim that it can be. This is developed in fairly rigorous detail in any introductory set theory textbook and in many first-year university mathematics courses, where the notions of pair, relation, function, sequence, etc., are all defined in set-theoretic terms.

The Z Thesis implies that:

Virtually all informal mathematics can be formalized (or "modelled", or "implemented", if you prefer) in a foundational theory whose basic concepts are:

$x \in y$ ("$x$ is an element of $y$")
$x = y$ ("$x$ is identical to $y$")

This is very puzzling. So far as I am aware, no one has any idea why this is so.

The Z Thesis connects informal mathematics to a certain underlying foundational system, which may be formalized quite precisely (i.e., $ZFC$). It has a certain empirical, or, to be more precise, historical aspect to it. For informal mathematics is what mathematician have done for centuries, and it is curious that what they have come up has this property (reducibility to a theory of membership and identity).

There are several other kinds of metamathematical claim---claims about mathematical theories---that relate to other disciplines.

First, cognitive science (broadly construed, to include psychology, neuroscience, linguistics and computer science). How is mathematical language cognized? How are mathematical theories recognized, conjectured, posited or learnt?

Second, epistemology & metaphysics. How are mathematical theories justified? What is modal status of mathematical theories? What is the structure of mathematicized scientific theories (i.e., the standard theories of science)?