构造性多型理论与二阶算术子系统的比较
Comparison of constructive multi-typed theory with subsystems of second order arithmetic
摘要：
本文描述了构造性数学的一个公理化理论BT。BT有一个谓词性的概括公理，适用于可数个集合类型和通常的组合运算。BT具有直觉主义逻辑，与经典逻辑一致，具有与形式丘奇命题一致、存在性与析取性等构造性特征。BT可以与所谓的算术真值理论PATr和包含无穷多种自然数集合的二阶算术SA相互解释。我们比较BT与一些标准的二阶算法，并调查证明理论的BT，PATr和SA片段的强度。
英文摘要：
This paper describes an axiomatic theory BT for constructive mathematics. BT has a predicative comprehension axiom for a countable number of set types and usual combinatorial operations. BT has intuitionistic logic, is consistent with classical logic and has such constructive features as consistency with formal Church thesis, and existence and disjunction properties. BT is mutually interpretable with a so called theory of arithmetical truth PATr and with a second-order arithmetic SA that contains infinitely many sorts of sets of natural numbers. We compare BT with some standard second-order arithmetics and investigate the proof-theoretical strengths of fragments of BT, PATr and SA.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
