Poincaré and the principle of induction

In his popularization book "Science and Hypothesis" (1905), Henri Poincaré argues that mathematics cannot be reduced to logic or set theory and that there is always the need to appeal to external principles belonging to our intuition to set up the foundations of mathematics. He singled out the principle of induction as one of these principles. Poincaré's criticism was made at a time where set theory was in its infancy and crippled with paradoxes, and I thought that his viewpoint was rebutted after his death by the progress of set theory.

To my surprise though, browsing through modern logic and set theoretic books such as Jech's, I see the principle of induction used informally for example to establish consistency of first order predicate logic or several basic set theoretic statements, through induction on formulas. This seems to imply that no consistency result can be derived without appeal to this principle, informally.

Let me emphasize that point, in the style of Poincaré: at the moment the principle of induction is formalized in modern set-theoretical mathematics, consistency of first order logic is needed in order to assert its truth, and such consistency actually relies on the principle of induction.

So, was Poincaré right in asserting that the principle of induction is part of our intuition and is irreducible to logic, set theory or more generally mathematical formalization, in the sense that it is needed to lay out the very first foundations of mathematics?

Of course set theory in the main is concerned with induction, particularly transfinite induction. Adrian Mathias describes set theory as the study of well-founded recursive definitions, which is an account that I think many set theorists find accurate. And of course this places recursion and therefore also induction at the very center of the subject.

Set theory, in this sense, is concerned with induction at its core. The cumulative conception of the set-theoretic universe, which underlies essentially all the central conceptions of set theory currently, is inherently generated by a transfinite recursion. So it is hard to understand how one would want to understand a version of set theory without any induction in it.

Some philosophers of set theory (well, OK, I am thinking of myself, but I am not alone) regard the enormous success of set theory as a foundation of mathematics as essentially fulfilling the principal goals of logicism to found mathematics on logic, if one regards the main set theory principles (including the axioms of infinity and also the axiom of choice) as essentially logical in nature. And I think this is a view to which you alluded in your question. But there is not universal agreement with this view, and the matter remains contentious.

Meanwhile, the fact that set theory is essentially involving induction and recursion, particularly in the transfinite, seems to contradict some other things in the first part of your question.

In the second part of your question, however, your example is not actually about set theory proper, but rather about the metatheory of set theory. Induction on formulas in set theory is a method used to show, for example, as a metatheoretic claim that every instance of an infinite scheme of theorems is actually a theorem. For example, we use this when proving the reflection theorem and in many other cases. Metatheoretic induction is also used pervasively not just in set theory, but in the model theory of other theories. As Qiaochu mentions in his comment on your question, we use recursion on formulas to define what the formulas are in the first place.

In this sense, there is something a little anachronistic about your question. The concerns of logicism and the problem of founding mathematics on logic were focused on the core principles of mathematics, rather than on the metatheoric methods. Indeed, the theory/metatheory distinction was simply not very clear at the time of Poincaré. This didn't come for many decades later.

One way to take your question is to inquire: could there be a metatheory for set theory and the foundations of mathematics that has no induction principle?

For this, the answer is yes.

First, let me say that there is no universal agreement on what the right metatheoretic commitments should be in the foundations of mathematics. In part this is because there is little need actually to articulate a precise metatheory.

Many logicians adopt PA as their main convenient meta theory, or even ZFC in a set-theoretic context. However, all the main metatheoretic results in set theory can be established in PA. For example, in PA we can prove that if ZF is consistent, then so is ZFC+CH and also ZFC+$\neg$CH. We can prove in PA that the method of forcing is effective in creating new models of set theory from a given model, and this is the sense in which PA serves as a robust metatheory.

Meanwhile, some logicians emphasize that one can make things work in much weaker metatheories, such as $I\Delta_0$ and even PRA.

The case of PRA is important for your question, since it includes no explicit induction principle. So this would seem to be a positive answer to your question. However, the central axioms of PRA posit the recursive definitions of all the primitive recursive functions, and so PRA trucks heavily with recursion, even when it lacks an explicit induction scheme. I would find it a little absurd to hold the view that PRA has nothing to do with recursion, just because it lacks the explicit induction scheme.

My own larger view is that any sufficient mathematical theory serves as a suitable metatheory for the models and theories that are available in it. In this sense, we don't just have theory and metatheory, but rather the more accurate picture is that there is an enormous variety of metatheoretic contexts, provided by all the various models of various theories that we might consider. So we can use models of ZFC or ZFC+large cardinals fruitfully as metatheoretic contexts, and it is insightful to compare diverse metatheoretic situations in terms of their agreement or especially their disagreement on metatheoretic matters.

This kind of view pushes one to pluralism not only in the object theory, but in the metatheory as well. We already know quite well, for example, how the question whether a given theory is consistent or whether it proves a given theorem is not an absolute thing, but depends on the metatheoretic context in which the question is asked.