Why can we use induction when studying metamathematics?

Solution 1:

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).

Solution 2:

This is not at all intended to be an answer to your question. (I like Henning Makholm's answer above.) But I thought you might be interested to hear Thoralf Skolem's remarks on this issue, because they are quite pertinent—in particular one of his points goes exactly to your question about proving that every formula has equal numbers of left and right brackets—but they are much too long to put in a comment.

Set-theoreticians are usually of the opinion that the notion of integer should be defined and that the principle of mathematical induction should be proved. But it is clear that we cannot define or prove ad infinitum; sooner or later we come to something that is not definable or provable. Our only concern, then, should be that the initial foundations be something immediately clear, natural, and not open to question. This condition is satisfied by the notion of integer and by inductive inferences, but it is decidedly not satisfied by set-theoretic axioms of the type of Zermelo's or anything else of that kind; if we were to accept the reduction of the former notions to the latter, the set-theoretic notions would have to be simpler than mathematical induction, and reasoning with them less open to question, but this runs entirely counter to the actual state of affairs.

In a paper (1922) Hilbert makes the following remark about Poincaré's assertion that the principle of mathematical induction is not provable: “His objection that this principle could not be proved in any way other than by mathematical induction itself is unjustified and is refuted by my theory.” But then the big question is whether we can prove this principle by means of simpler principles and without using any property of finite expressions or formulas that in turn rests upon mathematical induction or is equivalent to it. It seems to me that this latter point was not sufficiently taken into consideration by Hilbert. For example, there is in his paper (bottom of page 170), for a lemma, a proof in which he makes use of the fact that in any arithmetic proof in which a certain sign occurs that sign must necessarily occur for a first time. Evident though this property may be on the basis of our perceptual intuition of finite expressions, a formal proof of it can surely be given only by means of mathematical induction. In set theory, at any rate, we go to the trouble of proving that every ordered finite set is well-ordered, that is, that every subset has a first element. Now why should we carefully prove this last proposition, but not the one above, which asserts that the corresponding property holds of finite arithmetic expressions occurring in proofs? Or is the use of this property not equivalent to an inductive inference?

I do not go into Hilbert's paper in more detail, especially since I have seen only his first communication. I just want to add the following remark: It is odd to see that, since the attempt to find a foundation for arithmetic in set theory has not been very successful because of logical difficulties inherent in the latter, attempts, and indeed very contrived ones, are now being made to find a different foundation for it—as if arithmetic had not already an adequate foundation in inductive inferences and recursive definitions.

(Source: Thoralf Skolem, “Some remarks on axiomatized set theory”, address to the Fifth Congress of Scandinavian Mathematicians, August 1922. English translation in From Frege to Gödel, p299–300. Jean van Heijenoort (ed.), Harvard University Press, 1967.)

I think it is interesting to read this in the light of Henning Makholm's excellent answer, which I think is in harmony with Skolem's concerns. I don't know if Hilbert replied to Skolem.