驯服逆向数学动物园

逆向数学是数学基础中的一个研究纲领。其结果基于可计算性对普通数学的定理给出了一种优雅的分类。特别地，这些定理中的绝大多数仅落入五个范畴，其相关的逻辑系统被称为“五大类”。近期，大量努力被投入到寻找例外定理，即落在“五大类”范畴之外的定理。所谓的逆向数学动物园即是此类例外定理（及其关系）的集合。在本文中，我们证明了动物园定理的一致版本，即由一个泛函计算出被断言存在的对象，在 Kohlenbach 的高阶逆向数学中均落入第三大范畴——算术理解。换言之，动物园似乎在一致层面上消失了。我们的分类适用于所有其对象表现出极少结构的定理，我们猜想这一概念与 Montalbán 的鲁棒性概念相关。令人惊讶的是，我们的方法揭示了非标准分析一个此前未知的“计算”层面：我们将构建一个算法 $\mathfrak{RS}$，它以 Nelson 内部集合论中一个特定等价性的证明作为输入，并输出一致动物园原则与算术理解之间所期望的（不涉及非标准分析的）等价性证明。此外，由此证明的等价性甚至是显式的，即该语言中的一个项可将一个一致原则中的泛函转换为另一个原则中的泛函，反之亦然。