Infinite axiom schemas - what comes before?

Question

The ZFC axioms constitute an infinite set. So too do the PA axioms. Presumably, then, we need a metatheory before we can even define these axiom systems.

What is the usual metatheory?

Do we even need one?

Answer 1

We don't define ZFC as a set of axioms in some metatheory. This basically works like this: for every ZFC axiom, we write a sequence of symbols on a sheet of paper, and say that these are "theorems" of ZFC. For axiom schema, instead of a single axiom, we write the rule "if you take any formula (usually subject to some constraints), and substitute it for $\phi$ in this following axiom schema, it will constitute a theorem of ZFC". Then, we introduce some rules that allow us to infer new "theorems" of ZFC from the ones we already know (the axioms). Then we say that a "theorem" of ZFC is a sequence of symbols that can be derived from "axioms" by a finitely many applications of the inference rules.

There's no metatheory. There are no sets. It's only rewriting symbols on a sheet of paper according to some rules.

Now, you can interpret the statements and rules inside some other (or even the same) theory, but this is only a mirror of the term rewriting process.