非标准非标准分析与标准数学的计算内容
Non-standard Nonstandard Analysis and the computational content of standard mathematics
摘要：
本文的目的是突出一个迄今未知的计算方面的非标准分析。最近，一些非标准版本的Goedel系统T已经被引入（[2，9，12]），并且在[26]中表明，[2]中的系统在从非标准分析的证明中提取计算信息方面起着关键作用。这是一个自然的问题，如果类似的技术可以用来提取计算信息，从证明不涉及非标准分析。本文利用文献[9]中的非标准系统对这个问题给出了肯定的回答。该系统验证了所谓的非标准一致有界性原则，这是Kohlenbach证明挖掘方法的核心（[14]）。特别是，我们表明，从经典和无效的存在证明（不涉及非标准分析，但使用弱柯尼希引理），可以“自动”提取近似声称存在的对象。
英文摘要：
The aim of this paper is to highlight a hitherto unknown computational aspect of Nonstandard Analysis. Recently, a number of nonstandard versions of Goedel's system T have been introduced ([2,9,12]), and it was shown in [26] that the systems from [2] play a pivotal role in extracting computational information from proofs in Nonstandard Analysis. It is a natural question if similar techniques may be used to extract computational information from proofs not involving Nonstandard Analysis. In this paper, we provide a positive answer to this question using the nonstandard system from [9]. This system validates so-called non-standard uniform boundedness principles which are central to Kohlenbach's approach to proof mining ([14]). In particular, we show that from classical and ineffective existence proofs (not involving Nonstandard Analysis but using weak Koenig's lemma), one can `automatically' extract approximations to the objects claimed to exist.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
