首页/论文/1609.01945

arXiv 1609.019452016-09-07math.LO

关于Loeb测度的计算内容

On the computational content of the Loeb measure

Sam Sanders

备注：: arXiv admin note: substantial text overlap with arXiv:1609.01919; text overlap with arXiv:1508.07434

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

摘要英文摘要相关论文

摘要：

Loeb测度是非标准分析的基石之一。Loeb测度的传统发展利用饱和度和外集。受文献[13]的启发，我们给出了文献[1]中Nelson内集合论的弱片段$\textsf{P}$中Loeb测度的特殊情形.也许令人惊讶的是，我们对Loeb测度的定义在[1]中的“项提取”框架的意义上具有计算内容。

英文摘要：

The Loeb measure is one of the cornerstones of Nonstandard Analysis. The traditional development of the Loeb measure makes use of saturation and external sets. Inspired by [13], we give meaning to special cases of the Loeb measure in the weak fragment $\textsf{P}$ of Nelson's internal set theory from [1]. Perhaps surprisingly, our definition of the Loeb measure has computational content in the sense of the `term extraction' framework from [1].

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

经典算术的计算内容

The computational content of classical arithmetic

几乎从希尔伯特的程序开始，证明论的基础和结构努力就一直指向澄清现代数学方法的计算内容的目标。本文综述了从经典一阶算术证明中提取计算信息的各种方法，并反思了它们之间的一些关系。哥德尔-根岑双重否定翻译的变体，有些不太为人所知，为该理论提供了规范和有效的计算解释。

2010-06-16math.LO

多维不连续性的计算内容

The computational content of multidimensional discontinuity

本文研究多维空间中函数不连续性的计算难度，扩展了先前工作，通过真值表丰富度在 Weihrauch 度中建立严格层级。

2024-07-18math.LO

非标准非标准分析与标准数学的计算内容

Non-standard Nonstandard Analysis and the computational content of standard mathematics

本文的目的是突出一个迄今未知的计算方面的非标准分析。最近，一些非标准版本的Goedel系统T已经被引入（[2，9，12]），并且在[26]中表明，[2]中的系统在从非标准分析的证明中提取计算信息方面起着关键作用。这是一个自然的问题，如果类似的技术可以用来提取计算信息，从证明不涉及非标准分析。本文利用文献[9]中的非标准系统对这个问题给出了肯定的回答。该系统验证了所谓的非标准一致有界性原则，这是Kohlenbach证明挖掘方法的核心（[14]）。特别是，我们表明，从经典和无效的存在证明（不涉及非标准分析，但使用弱柯尼希引理），可以“自动”提取近似声称存在的对象。

2015-09-10math.LO

本征密度的计算内容

The computational content of intrinsic density

在前一篇文章中，作者引入了内密度的概念--渐近密度对密度在可计算置换下不变的集合的限制。我们证明了具有良好定义的固有密度（特别是固有密度为0）的集合只存在于图灵度高（$\mathbf{a}'\ge_{\rm T}\emptyset"$）或计算对角不可计算函数中。相比之下，在每个不可计算度中免疫集的经典构造实际上产生了一个在每个不可计算度中具有内在低密度0的集合。我们还证明了前一个结果在逆向数学的意义下成立，因为（在$\mathsf{RCA}_0$上）存在一个控制或对角不可计算函数等价于存在一个固有密度为0的集合。

2017-09-04math.LO

关于Zorn引理的计算内容

On the computational content of Zorn's lemma

我们给出了一个计算的解释佐恩引理的一个抽象的例子制定为一个wellfoundedness原则的语言中的算术在所有有限类型。这是通过哥德尔的功能解释实现的，并且需要引入一种新的形式的递归在非良基偏序上，其存在于全连续泛函模型中使用域理论技术证明。我们表明，一个实现器的功能解释开放归纳的字典序序列如下作为一个简单的应用程序，我们的主要结果。

2020-04-28cs.LOmath.LO

扭转形式主义16

Reverse Formalism 16

在他著名的论文Formalism 64中，罗宾逊为他的哲学立场辩护如下：（1）任何提到无限总体的说法都是毫无意义的。(ii)我们应该表现得好像无限的整体真的存在。作为非标准分析的创始人，罗宾逊经常会面临这样一种对立的立场，即“一些无限的总体比其他的更有意义”，教科书上的例子就是无穷小（与争议较少的无限总体相比）。例如，毕晓普和康纳斯对无穷小和一般的非标准分析提出了这样的主张，甚至分别称后者为意义的贬低和虚的，同时接受其他无限总体和相关的数学框架为有意义的。我们将研究毕晓普和康纳斯对非标准分析的批评，并观察到这些作者将“意义”和“计算内容”等同起来，尽管他们对所说的内容的解释各不相同。正如我们将看到的，Bishop和Connes声称，非标准分析中理想对象（特别是无穷小）的存在导致了意义（即计算内容）的缺失。我们将通过建立相反的观点来揭穿Bishop-Connes的批判，即在非标准分析中理想对象（特别是无穷小）的存在产生了计算内容的普遍存在。特别是，无穷小提供了一个优雅的速记表示计算内容。为此，我们引入了一个直接的翻译之间的一大类定理的非标准分析和定理丰富的计算内容（不涉及非标准分析），类似于“逆转”的基础程序逆向数学。后者在衡量这一翻译的范围方面也起着重要作用。

2017-02-03math.LO

更多相关论文收起更多论文

论可计算性理论的统一计算内容

On the Uniform Computational Content of Computability Theory

我们证明，Weihrauch格可以用来分类的统一计算内容的可计算性理论的属性，以及计算内容的定理在一个共同的设置。我们研究的属性包括对角不可计算性，超免疫性，皮亚诺算法的完全一致扩展，1-genericity，Martin-Löf随机性和凝聚力。在我们的案例研究中，我们包括的定理是Jockusch和Soare的低基定理，Kleene-Post定理和Friedberg的跳跃反演定理。事实证明，所有上述性质和可计算性理论中的许多定理，包括所有声称存在某个图灵度的定理，几乎没有统一的计算内容：它们位于二元选择的上锥（也称为LLPO）之外;我们称具有此性质的问题为无差别的。由于几乎所有的经典分析定理的计算内容已被分类是歧视性的，我们的观察可以产生一个解释，为什么定理和结果在可计算性理论通常有很少的直接后果，在其他学科，如分析。在我们的案例研究中，一个值得注意的例外是低基定理，它是判别式的。这也许就是为什么它被认为是可计算性理论中最适用的定理之一。在某些情况下，经典数学的无差别世界和有差别世界之间的桥梁可以通过一个合适的剩余运算建立，我们证明了这一点的情况下的凝聚力问题和问题的一致性完全扩展的皮亚诺算术。两者都是两个判别问题的商。

2017-06-27cs.LOmath.LO

关于Ramsey定理的统一计算内容

On the Uniform Computational Content of Ramsey's Theorem

研究了Weihrauch格上Ramsey定理的一致计算内容。我们的中心结果提供信息如何拉姆齐定理下的产品，并行化和跳跃的行为。从这些结果中我们可以得到拉姆齐定理的一些重要性质。首先，Ramsey关于基数$n\geq1$和任意有限颜色数$k\geq2$的定理的并行化等价于弱König引理的第$n$跳.特别地，对于基数$n\geq1$的Ramsey定理是$Σ^0_{n+2}$ --在有效Borel层次中可测量，但不是$Σ^0_{n+1}$ --可测量。其次，我们得到了一些有趣的下界，例如弱Kynnig引理的$n$阶跳跃是Weihrauch可约化为（稳定版本的）Ramsey基数定理PDMATHAMR（对于$n\geq2$）.证明了在Weihrauch格上，随着颜色数的严格递增，Ramsey定理形成了一个严格递增的链.我们的研究跳跃还表明，某些统一的变种拉姆齐定理是不可区分的，从非统一的角度发挥了重要作用。例如，拉姆齐定理的着色版本明确地包含齐次集的颜色作为输出信息，并且这个问题的跳跃（但不是未着色的变体）等价于拉姆齐定理的下一个更大基数的稳定版本。最后，我们简要地讨论了特殊情况下的拉姆齐定理对，我们提供了一些新的分离技术的问题，涉及在这种情况下的跳跃。特别是，我们研究统一的结果，关于有界性和诱导问题的关系，拉姆齐定理，我们表明，有一些显着的差异，在逆向数学的非统一的情况。

2017-06-20math.LO

超强非扩张映射与一致单调算子的计算内容

The computational content of super strongly nonexpansive mappings and uniformly monotone operators

本文用证明挖掘方法定量研究超强非扩张映射与一致单调算子，构造超强非扩张性模量并关联一致单调性模量，在超强制情形下首次得到定性与定量兼新的不相容可行性结果及渐近正则性有效一致速率。

2023-08-11math.FAmath.LOmath.OC

逆向非标准数学的有效内容与有效逆向数学的非标准内容

The effective content of Reverse Nonstandard Mathematics and the nonstandard content of effective Reverse Mathematics

本文的目的是突出一个迄今为止未知的计算方面的非标准分析有关逆向数学（RM）。特别是，我们将建立RM-等价定理之间的非标准分析的一个片段纳尔逊的内部集合论。然后，我们提取原始的递归项从哥德尔的系统T（不涉及非标准分析）从上述非标准等价的证明。由此产生的条款原来是有效的证人1等价在Kohlenbach的高阶RM。换句话说，从非标准分析中的RM-等价，我们可以提取相关的有效高阶RM-等价，它不再涉及非标准分析。最后，我们表明，某些有效的等价反过来又引起原来的非标准定理，他们来自。

2015-11-15math.LO

关于Baire范畴定理的一致计算内容

On the Uniform Computational Content of the Baire Category Theorem

我们研究了Weihrauch格上Baire范畴定理不同版本的统一计算内容。Baire范畴定理可以被看作是一个鸽子洞原理，它指出一个完整的（即，“大”）度量空间不能被分解成可数个无处稠密（即，“小”）块。贝尔范畴定理是一个很有启发性的例子，它可以用来证明一个经典定理可以有几种不同的计算解释。首先，我们区分两个不同的逻辑版本的定理，其中一个可以被看作是另一个的对位形式。第一个版本的目标是在给定一个无处稠密的闭集序列的情况下，在空间中找到一个未覆盖的点。第二个版本的目标是找到一个闭集的指数，这是密集的地方，给定一个序列的闭集，覆盖空间。尽管这两个版本背后的陈述在经典逻辑中是等价的，但它们在直觉主义逻辑中并不等价，同样它们在Weihrauch格中表现出不同的计算行为。除了这种逻辑上的区别，我们还考虑了闭集序列如何被“给定”的不同方式。本质上，我们可以区分闭集上的正面和负面信息。我们讨论所有四个版本的Baire类别定理。有些令人惊讶的是，提供输入信息的差异也可以用跳转操作来表示。最后，我们还涉及到Baire范畴定理的一般性和可计算comeager集的概念。

2016-08-24cs.LOmath.LO

Weihrauch格上的Vitali覆盖定理

The Vitali Covering Theorem in the Weihrauch Lattice

利用Weihrauch约化方法研究了区间Vitali覆盖定理的统一计算内容。我们表明，一个更详细的图片出现比朱斯托，布朗和辛普森的相关研究揭示了在设置反向数学。特别是，维塔利覆盖定理的不同表述有不同的统一计算内容。这些版本要么是可计算的，要么与弱弱柯尼希引理的一致变体密切相关。

2016-07-26cs.LOmath.LO