Higher order reversemathematics
Higher order reversemathematics
复制标题
高阶逆数学
DOI：
10.1017/9781316755846.018
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
S. G. Simpson
中科院分区：
文献类型：
--
作者：
U. Kohlenbach;S. G. Simpson
§1。介绍。由H. Friedman， S. Simpson等人发展的逆向数学（参见[16]的综合处理）侧重于二阶算术语言，“因为这种语言是最弱的，它足够丰富，可以表达和发展大部分核心数学”（[16]，第viii页）。然而，正如我们在[13]中所讨论的，在波兰空间X， Y之间处理连续函数f: X-> Y不仅需要相当复杂的编码。更重要的是，受限制的语言使得有必要（已经为X= Nn， Y= N）使用一个建设性的稍微丰富的连续函数定义，其与通常定义的等价性无法证明，例如在有限类型扩展E-PAW+ qf - ac1,0（一个函数变量而不是集合变量的变体）的二阶或二阶系统RCA（即RCAo加完全归纳，其中RCAo是反向数学中使用的著名基系统，见[16]）。这里QF-AC1, 0表示
§ 1. Introduction. Reverse mathematics as developed by H. Friedman, S. Simpson and others (see [16] for a comprehensive treatment) focuses on the language of second order arithmetic “because that language is the weakest one that is rich enough to express and develop the bulk of core mathematics”([16], p. viii).However, as we have argued in [13], already the treatment of continuous functions f: X-> Y between Polish spaces X, Y not only requires a quite complicated encoding. Even more importantly, the restricted language makes it necessary (already for X= Nn, Y= N) to use a constructively slightly enriched definition of continuous functions whose equivalence with the usual definition cannot be proved eg in the finite type extension E-PAW+ QF-AC1, 0 of (a variant with function variables instead of set variables of) the second or der system RCA (ie RCAo plus full induction, where RCAo is the well-known base system used in reverse mathematics, see [16]). Here QF-AC1, 0 denotes