| An MR-complete extension of extension of TRDB and its functional interpretation (2007) | |||||||||||||
Abstract | |||||||||||||
| In this paper, we extend a functional interpretation to transfinite types. To be more precise, we define a modified realizability interpretation of a constructive arithmetic with a certain inductive definition and bar-induction. The system is called TRDB. We also give an extension of TRDB, which is called S, and show that S is a complete system with respect to the modified realizability interpretation. In the second half, we define a truth-value of S-formulas under certain functionals, and show validity of S with respect to the truth-value. 1 Introduction In a previous work [5], Yasugi and Hayashi formulated a system of constructive arithmetic with transfinite recursion and bar induction. This system was called TRDB, which is a streamlined version of the system used by Yasugi in [4] to prove the accessibility of an order system. TRDB is, however, a mathematically interesting system on its own right. For this reason, it has been studied from various aspects. [5] re-formulates the ar... | |||||||||||||
Publication details | |||||||||||||
| |||||||||||||