非标准非标准分析及标准数学的计算内容
逻辑
2015-09-11 v2
摘要
本文旨在强调非标准分析中迄今未知的一个计算方面。近期，Goedel 系统 T 的若干非标准版本被提出（[2,9,12]），并且在 [26] 中证明了来自 [2] 的系统在从非标准分析的证明中提取计算信息方面发挥了关键作用。一个自然的问题是，类似的技术是否可用于从不涉及非标准分析的证明中提取计算信息。本文使用 [9] 中的非标准系统对这一问题给出了肯定回答。该系统验证了所谓的非标准一致有界性原理，这些原理是 Kohlenbach 证明挖掘方法的核心（[14]）。特别地，我们证明了从经典且非有效构造的存在性证明（不涉及非标准分析，但使用了弱 Koenig 引理）中，可以“自动”提取出所宣称存在对象的近似。
引用
@article{arxiv.1509.00282,
title = {Non-standard Nonstandard Analysis and the computational content of standard mathematics},
author = {Sam Sanders},
journal= {arXiv preprint arXiv:1509.00282},
year = {2015}
}
备注
arXiv admin note: text overlap with arXiv:1508.07434