An accessibility proof of ordinal diagrams in intuitionistic theories for iterated inductive definitions (Q1057857)

Let \(ID^ i_{\xi}\) and \(ID_{\xi}\) be the intuitionistic and classical theories, respectively, of \(\xi\)-iterated positive inductive definitions (which are known to be proof-theoretically equivalent). Let \(| O(\xi +1,1)|\) be the order type of \(O(\xi +1,1)\), the system of ordinal diagrams ordered by \(<_ 0\). It is shown that each diagram in \(O(\omega +1,1)\) is provably accessible in \(ID^ i_{\omega}\). Thus \(| O(\omega +1,1)|\) does not exceed the supremum \(| ID_{\omega}|\) of the decidable well-orderings provably accessible in \(ID_{\omega}\). In a forthcoming paper the author will use the accessibility of the diagrams in \(O(\omega +1,1)\) to prove the consistency of the theory \((\Pi^ 1_ 1-CA)+BI\) of second order arithmetic with \(\Pi^ 1_ 1\)-comprehension and bar induction on decidable trees. Since Buchholz, Pohlers, and Sieg have shown that this theory is proof-theoretically equivalent to \(ID_{\omega}\), the author concludes \(| O(\omega +1,1)| =| ID_{\omega}|\), which is the main conclusion of the paper. The author conjectures that \(| O(\xi +1,1)| =| ID_{\xi}|\) holds for all ordinals \(\xi\).