一句话:利用非标准分析中的标准外延性技巧,从非标准不连续泛函导出图灵跳跃泛函的有效蕴含。
本文研究如何从非标准分析中提取有效内容。Grilliot 技巧可将图灵跳跃泛函 (∃²) 由给定的有效不连续二型泛函显式定义;作者提出与之类似的标准外延性技巧:从某些非标准不连续泛函的存在性推出限制在 Π₁⁰ 公式上的 Transfer 原理,再由这个一般非有效的蕴含消去非标准分析,得到用不连续泛函表达图灵跳跃泛函的有效蕴含。其优点是无需刻意关注有效内容即可获得有效内容。文章还讨论了一类直接来自标准部分公理的新泛函,它们似乎超出已有分类。
The technique known as Grilliot's trick constitutes a template for explicitly defining the Turing jump functional $(\exists^2)$ in terms of a given effectively discontinuous type two functional. In this paper, we discuss the standard extensionality trick: a technique similar to Grilliot's trick in Nonstandard Analysis. This nonstandard trick proceeds by deriving from the existence of certain nonstandard discontinuous functionals, the Transfer principle from Nonstandard analysis limited to $\Pi_1^0$-formulas; from this (generally ineffective) implication, we obtain an effective implication expressing the Turing jump functional in terms of a discontinuous functional (and no longer involving Nonstandard Analysis). The advantage of our nonstandard approach is that one obtains effective content without paying attention to effective content. We also discuss a new class of functionals which all seem to fall outside the established categories. These functionals directly derive from the Standard Part axiom of Nonstandard Analysis.Comment: 21 pages