On the intuitionistic strength of monotone inductive definitions
On the intuitionistic strength of monotone inductive definitions
复制标题
论单调归纳定义的直观强度
DOI：
--
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
S. Tupailo
中科院分区：
文献类型：
--
作者：
S. Tupailo
抽象的。我们在这里证明了直觉主义理论T0↾+UMIDN。甚至显式数学的EETJ↾+UMIDN，都有-CA0的强度。在第一节中，我们给出了经典的二阶μ-微积分的双重否定翻译，它在[Mö02]中被证明具有-CA0的强度。在第二节中，我们解释了EETJμ+UMIDN理论中的直觉↾演算。关于T0中单调归纳定义的强度的问题是由S.Feferman在1982年提出的，M.Rathjen在假设经典逻辑的情况下提出了这个问题。
Abstract. We prove here that the intuitionistic theory T0↾ + UMIDN. or even EETJ↾ + UMIDN, of Explicit Mathematics has the strength of –CA0. In Section 1 we give a double-negation translation for the classical second-order μ-calculus, which was shown in [Mö02] to have the strength of –CA0. In Section 2 we interpret the intuitionistic μ-calculus in the theory EETJ↾ + UMIDN. The question about the strength of monotone inductive definitions in T0 was asked by S. Feferman in 1982, and — assuming classical logic — was addressed by M. Rathjen.