I am looking for references for theorems of the form:


1) Any proof of theorem $X$ requires $n$ applications of induction axioms


and especially


2) Any proof of theorem $X$ requires $n$ nested applications of induction axioms.


I've seen similar statements for applications of axioms other than induction axioms (and I'd be happy to receive references for those, too, but I am particularly interested in induction)



Cases where multiple induction steps are provably required
Here is a reference for one way of making precise sense of your question and answering it:



> 
> Stefan Hetzl and Tin Lok Wong (2017): "Some observations on the logical foundations of inductive theorem proving", Logical Methods in Computer Science, Volume 13, Issue 4, doi:[10.23638/LMCS-13(4:10)2017](https://doi.org/10.23638/LMCS-13%284:10%292017), arXiv:[1704.01930](https://arxiv.org/abs/1704.01930)
> 
> 
> 


In Section 2.4 they show the following. Let $\text{PA}^-$ be the theory of the non-negative parts of discretely ordered rings (language: $\langle 0,1,+,\times,<\rangle$—see the paper for an axiomatization). Then for each theorem $\sigma$ of PA there is a formula $\varphi(x)$ such that $\text{PA}^-$ proves $\varphi(0)$ and $\forall x(\varphi(x)\implies\varphi(x+1))$ and $\forall x.\varphi(x)\implies\sigma$. Thus in this sense one application of induction always suffices.


