Stack Exchange network consists of 183 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.
@ImperishableNight Yes, this is a family of proofs parametrized by the complexity of assumed induction, the complexity of proven induction and the length of induction in terms of ordinals $\omega_n$. Though, these proofs are quite similar and could be expressed in an extended language with a new predicate $P$ as getting $\omega_{n+1}$-induction for $P$ from $\omega_{n+1}$-induction for $\Sigma_1(P)$.
It may be worth to mention that PA proves full induction for each well ordering $\alpha < \varepsilon_0$. The result is presented, e.g., in a textbook by Kotlarski, A Model–Theoretic Approach to Proof Theory (Theorem 4.1), attributed to Gentzen.
In the article we only conjectured that TC is a minimal essentially undecidable theory. We weren't able to show that leaving TC1, the associativity, gives a theory with a decidable extension. The problem is that it seems that an adaptation of the classical method of shortening cuts does not work without the associativity assumed (so we do not get essential undecidability of such a weaker theory). But we could not show that it actually has a decidable extension.
