非标准分析的不合理有效性

正如标题所示，本文旨在揭示经典非标准分析中蕴含的丰富计算内容。为此，我们构建了一个模板 $\mathfrak{CI}$，它将一个“纯”非标准分析定理（即仅用非标准定义（如连续性、积分、可微性、收敛性、紧致性等）表述的定理）转化为相应的有效定理。后者构成一个不再涉及非标准分析的可计算数学定理。为了确立 $\mathfrak{CI}$ 的广泛适用范围，我们将此模板应用于逆数学中“五大类”分类的代表性定理。逆数学这一基础性研究计划将“普通”（即非集合论）数学中的大多数定理归入上述五大类。逆数学动物园收集了这一分类的例外情况，并在文献[70,71]中使用 $\mathfrak{CI}$ 进行了研究。因此，得益于逆数学的五大类分类（及相关的动物园），模板 $\mathfrak{CI}$ 被认为适用于几乎所有普通数学。最后，我们证明某些被称为 Herbrand 化（Herbrandisations）的“高度构造性”定理，蕴含了通过 $\mathfrak{CI}$ 从它们导出的原始非标准分析定理。