An interpretation of intuitionistic analysis with restricted transfinite inductive definitions (Q1121882)

The article considers a system of intuitionistic analysis S(I), which is characterized by bar induction as well as successive inductive definitions along some accessible orderings. The `admissible' formulas of S(I) are restricted so that the modified realizability (mr-) translation can be consistently applied. The mr-translation of S(I) is then realized in the `two-storied universe of transfinite mechanisms', which is defined in the author's preceding work reviewed above (see Zbl 0675.03036). The universe of such mechanisms is a computational system which constructively interpretes some systems of intuitionistic analysis. The reason why the author investigates systems such as S(I) and the mr- translation is metamathematical interest. That is, S(I) is an (a modest) extension of ASOD, a system in which proof-theory to a certain extent can be formalized, and the mr-translation of the implication matches its proof-theoretical interpretation. A counter-example to the mr-translation of `non-admissible' formulas is given in the end.