Systems of Explicit Mathematics with Non-Constructive µ-Operator, Part II
Systems of Explicit Mathematics with Non-Constructive µ-Operator, Part II
复制标题
具有非构造性 µ 运算符的显式数学系统，第二部分
DOI：
10.1016/0168-0072(95)00028-3
复制
发表时间：
1996
期刊：
影响因子：
--
通讯作者：
Gerhard Jäger
中科院分区：
文献类型：
--
作者：
S. Feferman;Gerhard Jäger
本文主要讨论一些具有非构造性极小算子的二阶显式数学系统的证明论分析。通过引入变量类型公理，我们将一阶理论BON推广到初等显式类型理论EET，并增加了归纳法的几种形式以及μ的公理。主要结果表明：EET(μ)+集合归纳法(类型归纳法，公式归纳法)在证明理论上等价于Peano算术PA(二阶系统(Π0∞-CA<；ε0，二阶系统(Π0∞-CA)<；εε0))。
This paper is mainly concerned with proof-theoretic analysis of some second-order systems of explicit mathematics with a non-constructive minimum operator. By introducing axioms for variable types we extend our first-order theory BON to the elementary explicit type theory EET and add several forms of induction as well as axioms for μ. The principal results then state: EET(μ) plus set induction (type induction, formula induction) is proof-theoretically equivalent to Peano arithmetic PA (the second-order system (Π0∞-CA<ε0, the second-order system (Π0∞-CA)<εε0).