In fact I don’t understand the meaning of the word “metamathematics”. I just want to know, for example, why can we use mathematical induction in the proof of logical theorems, like The Deduction Theorem, or even some more fundamental proposition like “every formula has equal numbers of left and right brackets”?
What exactly can we use when talking about metamathematics? If induction is OK, then how about axiom of choice/determincacy? Can I use axiom of choice on collection of sets of formulas?(Of course it may be meaningless. By the way I don’t understand why we can talk about a “set” of formulas either)
I have asked one of my classmates about these, and he told me he had stopped thinking about this kind of stuff. I feel like giving up too……
This is not an uncommon confusion for students that are introduced to formal logic for the first time. It shows that you have a slightly wrong expectations about what metamathematics is for and what you’ll get out of it.
You’re probably expecting that it ought to go more or less like in first-year real analysis, which started with the lecturer saying something like
In high school, your teacher demanded that you take a lot of facts about the real numbers on faith. Here is where we stop taking those facts on faith and instead prove from first principles that they’re true.
This led to a lot of talk about axioms and painstaking quasi-formal proofs of things you already knew, and at the end of the month you were able to reduce everything to a small set of axioms including something like the supremum principle. Then, if you were lucky, Dedekind cuts or Cauchy sequences were invoked to convince you that if you believe in the counting numbers and a bit of set theory, you should also believe that there is something out there that satisfies the axioms of the real line.
This makes it natural to expect that formal logic will work in the same way:
As undergraduates, your teachers demanded that you take a lot of proof techniques (such as induction) on faith. Here is where we stop taking them on faith and instead prove from first principles that they’re valid.
But that is not how it goes. You’re still expected to believe in ordinary mathematical reasoning for whichever reason you already did — whether that’s because they make intuitive sense to you, or because you find that the conclusions they lead to usually work in practice when you have a chance to verify them, or simply because authority says so.
Instead, metamathematics is a quest to be precise about what it is you already believe in, such that we can use ordinary mathematical reasoning about those principles to get to know interesting things about the limits of what one can hope to prove and how different choices of what to take on faith lead to different things you can prove.
Or, in other words, the task is to use ordinary mathematical reasoning to build a mathematical model of ordinary mathematical reasoning itself, which we can use to study it.
Since metamathematicians are interested in knowing how much taken-on-faith foundation is necessary for this-or-that ordinary-mathematical argument to be made, they also tend to apply this interest to their own reasoning about the mathematical model. This means they are more likely to try to avoid high-powered reasoning techniques (such as general set theory) when they can — not because such methods are forbidden, but because it is an interesting fact that they can be avoided for such-and-such purpose.
Ultimately though, it is recognized that there are some principles that are so fundamental that we can’t really do anything without them. Induction of the natural numbers is one of these. That’s not a problem: it is just an interesting (empirical) fact, and after we note down that fact, we go on to use it when building our model of ordinary-mathematical-reasoning.
After all, ordinary mathematical reasoning already exists — and did so for thousands of years before formal logic was invented. We’re not trying to build it here (the model is not the thing itself), just to better understand the thing we already have.
To answer your concrete question: Yes, you can (“are allowed to”) use the axiom of choice if you need to. It is good form to keep track of the fact that you have used it, such that you have an answer if you’re later asked, “the metamathematical argument you have just carried out, can that itself be formalized in such-and-such system?” Formalizing metamathematical arguments within your model has proved to be a very powerful (though also confusing) way of establishing certain kinds of results.
You can use the axiom of determinacy too, if that floats your boat — so long as you’re aware that doing so is not really “ordinary mathematical reasoning”, so it becomes doubly important to disclose faithfully that you’ve done so when you present your result (lest someone tries to combine it with something they found using AC instead, and get nonsense out of the combination).