An interpretation of intuitionistic analysis with restricted transfinite inductive definitions
type: Item
instance of: scholarly article
title: An interpretation of intuitionistic analysis with restricted transfinite inductive definitions
zbMATH Open document ID: 0675.03037
author: Mariko Yasugi
published in: Tsukuba Journal of Mathematics
publication date: 1988-01-01T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 03F50
zbMATH DE Number: 4104950
zbMATH Keywords: intuitionistic analysis
zbMATH Keywords: bar induction
zbMATH Keywords: successive inductive definitions
zbMATH Keywords: mr-translation
MaRDI profile type: Publication
full work available at URL: https://doi.org/10.21099/tkbjm/1496160832
OpenAlex ID: W1691232567
DOI: 10.21099/TKBJM/1496160832
description: scientific article; zbMATH DE number 4104950