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

  • 6
    $\begingroup$ Because we consider formulas and derivations as mathematical objects themselves that we can order and count; this is so because we have formally and rigorously defined them through the usual inductive (or recursive) definitions. Thus, we may use structural induction to prove "properties" of these mathematical objects. $\endgroup$ Aug 2, 2017 at 9:16
  • 2
    $\begingroup$ Usual mathematical theories are quite simple mathematical objects; thus, their meta-math does not requires "very powerful" set theoretical resources. AC (or some equivalent, like Konig's Lemma) is needed for example in the proof of the Completeness Theorem. $\endgroup$ Aug 2, 2017 at 9:19
  • 2
    $\begingroup$ @Mauro ALLEGRANZA emmm......Is it really so rigorous? Can we prove the consistency of meta-math? What confuses me most is why can we use "set theoretical resources" to study logic. I always thought that we have logic first and then set theory...... $\endgroup$
    – 183orbco3
    Aug 2, 2017 at 9:32
  • 3
  • 1
    $\begingroup$ I'm guessing you can have a long and distinguished career as a mathematician without ever being able to formally prove that the number of left brackets in a formula will be equal to the number of right brackets. $\endgroup$ Aug 2, 2017 at 15:28

4 Answers 4


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

  • 1
    $\begingroup$ I like your answer! I tend to be also confused like OP and started to understand that it is not that important nor interesting to try to organize all mathematics like a computer program, with things linearly ordered. We can define certain things in term of other things, and vice versa (like categories with universal algebra but we can also categorify universal algebra). Sometimes we need a concept to define that same concept in a right way… this confuses me. I had a high school teacher who said math was like a card castle… a very strange-looking one then. $\endgroup$ Aug 2, 2017 at 11:06
  • 1
    $\begingroup$ @DenisdeBernardy: The father of all examples of this is Gödel's incompleteness theorems. They lead to further examples, such as results of the form "ZFC cannot prove such-and-such, because if it did, it would also prove its own consistency" -- for example in this recent answer of mine. $\endgroup$ Aug 2, 2017 at 19:04
  • 2
    $\begingroup$ @DenisdeBernardy My favourite example is the Ax-Grothendieck theorem, which states that any injective polynomial self-map of a finite-dimensional complex vector space is surjective. The proof rests on model theory, which asserts that any first-order statement is true for complex numbers iff it is true for all finite fields of sufficiently high characteristic. The theorem can be stated in such first-order form, and its finite-field analogue is obvious. This kind of reasoning requires good formal understanding of logic, truth and manipulations with them. Another example is Ax-Kochen theorem. $\endgroup$ Aug 2, 2017 at 23:33
  • 3
    $\begingroup$ @AntonFetisov: "any first-order statement is true for complex numbers iff it is true for all finite fields of sufficiently high characteristic" is not true -- consider for example the statement "there is a number that is not a square." The Ax-Grothendieck argument you reference depends on the statement being true for the algebraic closures of those finite fields too. $\endgroup$ Aug 2, 2017 at 23:54
  • 1
    $\begingroup$ @user525966: Yes, that sounds like a fair representation of what I'm saying. $\endgroup$ Sep 19, 2018 at 15:21

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.


Metamathematics is mathematics applied to the study of mathematics. Thus, metamathematics is mathematics, and using induction in metamathematics is as unproblematic as using derivatives when studying differential equations.

The confusion might be based on the fact that metaphysics is clearly not physics but could be considered the branch of philosophy that studies the presuppositions of physics. There is a tendency to view metamathematics as another word for the philosophy of mathematics. While there is clearly a certain overlap between the two, they simply aren't the same thing. Philosophy of math often uses metamathematics as a tool, in much the same way that analytic philosophy sometimes uses symbolic logic or the philosophy of science sometimes uses Bayes' theorem. The philosophy of mathematics isn't exhausted by questions for which metamathematics is the appropriate tool. At least part of the philosophy of mathematics is concerned with arguing for the validity of mathematical reasoning, including that of induction. Obviously, it would be question-begging to use induction to prove the validity of induction, and in some contexts you would be perfectly correct to object to such things. But, when dealing with the mathematical theory of formal logic, such worries are misplaced.


I am reminded of this remark at the beginning of Kleene's book Mathematical Logic:

"It will be very important as we proceed to keep in mind this distinction between the logic we are studying (the object logic) and our use of logic in studying it (the observer's logic). To any student who is not ready to do so, we suggest that he close the book now, and pick some other subject instead, such as acrostics or beekeeping."

From pages 3 and 4 of Stephen Kleene's book Mathematical Logic


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .