Can a universal induction rule be formulated?

Question

$\newcommand{\Con}{\operatorname{Con}}$The intention of Hilbert's program was to start with a simple logic and then justify more complex logics from there. So, we get a sequence of logics: $$ L_1 → L_2 → L_3 \to \cdots $$

His initial idea was to justify a succession by $L_n \vdash \Con(L_{n+1})$. This idea was derailed by Gödel's second incompleteness theorem. You can't prove the consistency of a more complex system if you can't prove your own consistency.

However, we might think of other ways of succession. The next obvious one is to use relative consistency, $L_n \vdash \Con(L_n) → \Con(L_{n+1})$. Unfortunately this also fails due to Gödel, because more complex logics can prove the consistency of the lesser complex logics. If $L_{n+1} \vdash \Con(Ln)$ and $L_n \vdash \Con(L_n) → \Con(L_{n+1})$ and $L_{n+1}$ can prove everything of $L_n$, then that would imply $L_{n+1} \vdash \Con(L_{n+1})$.

A number of times is suggest to have the succession as follows: $L_{n+1} = L_n + \Con(L_n)$. The funny thing about this is that it defies Gödel, now we can make consistency proofs in the succession (although Gödel still applies for the whole system). Unfortunately the successor logic can not do much more except for the consistency proof.

A closer look learns that the strength of a system is often determined by the expressiveness allowed for the induction hypothesis. An example is $I\Sigma_1$ where the induction scheme is limited to $\Sigma_1$ sentences. $I\Sigma_2$ can prove the consistency of $I\Sigma_1$. Also the classifications in reverse mathematics are partly based on what is allowed for the induction hypothesis.

The means that if we have a logic and extend it with additional expressiveness and that expressiveness is also allowed for the induction hypothesis, then the system will get stronger.

More expressiveness leads to more strength

This devastating for Hilbert's program. A more complex logic is not just a handy way to deal with certain concepts, as it is with higher level computer languages compared to the Turing machine, but it also adds more truth.

However, we humans accept easily higher level constructs for induction hypothesis in a succession. When we create a succession:

1) We prove that the new logic is a conservative extension of the original one, not taking induction into account.

2) Well, for the induction we just “intuitively” accept it.

Let's call this the “universal induction” principle. This principles informally says we can just accept anything as induction hypothesis. As far I know we have never encountered a paradox in this area.

My question is, is there a way to formalize this universal induction principle? I don't think this question can directly be answered. A positive answer would be a major development in Hilbert's program. A negative answer is probably not possible, because the question is not a precise mathematical question.

Is there some literature that thinks the same way?

If not and if you think it is possible, what are the restrictions we must set and in which we must formulate this?

If you think it is not possible, what are the arguments against?

Although the question is not mathematical precise, I hope it is not voted down for this reason. I am thinking about this, made a little progression and like to hear the opinion of the community.

Answer 1

I think the program you are outlining will not work: there is a limit to how far we can get by looking at induction on $\omega$, and once we pass to arbitrary induction schemes - where the real power is - the intuitive clarity of induction principles breaks down.

First of all, we do have theories with "complete induction": namely, a set theory like ZFC! ZFC proves that $\omega$ is well-ordered, and also that every formula defines a subset of $\omega$ via separation. So, in a precise sense, ZFC proves that "any formulable" induction principle holds of $\omega$. For example, ZFC proves that induction along $\omega$ holds for all formulas of finite-order arithmetic (and vastly, vastly more). In particular, if you're interested in statements about first-order arithmetic, I don't see how we could get past (or even to) the arithmetic consequences of ZFC.

However, induction still has strength even at the ZFC level and beyond - just not in terms of $\omega$ anymore. Instead, proof-theoretic ordinals become the focus: we look at principles asserting that certain (notations for) linear orders are well-founded (note that while there are some issues expressing this in first-order arithmetic, this is trivial in set theory). Indeed, the real strength of $\Sigma_{n+1}$-induction over $I\Sigma_n$ is that the proof-theoretic ordinal for $I\Sigma_n$ can be "analyzed" in a $\Sigma_{n+1}$ way; so the fact that we're managing to stick everything into $\omega$ is really a coincidence of the low proof-theoretic ordinals of the theories involved.

For these broader induction principles, I find the intuitive picture you outline to be fundamentally flawed: it is not true that we accept statements of the form "--- is well-ordered" uniformly. Indeed, we can easily cook up truly bizarre notations; and conversely, the notations arising in the analysis of even fairly weak (from a ZFC-perspective) systems like $\Pi^1_2$-$CA_0$ are pretty bizarre, to be completely honest.

Answer 2

My question is, is there a way to formalize this universal induction principle?

How about the (infinitary) Hilbert $\omega$-rule:

$$P(1), P(2), P(3), \cdots\over \forall n P(n) $$

Not sure if that's the kind of thing you were looking for but it captures the "true" integers by starting out with them.