On the decomposition of WKL!!
On the decomposition of WKL!!
复制标题
DOI：
10.1098/rsta.2022.0010
复制
发表时间：
2023-05-29
期刊：
影响因子：
5
通讯作者：
Nemoto, Takako
中科院分区：
文献类型：
--
作者：
Fujiwara, Makoto;Nemoto, Takako
从概念的观点来看，许多数学命题至少隐含着两种原理。一个是逻辑原则，例如排除中间法则或德摩根法则。二是功能存在原则。出于概念和实践的原因，校准数学定理和公理中隐含的逻辑和函数存在原则的数量是一项有趣的事业。这是构造性逆向数学的主题，它指定了必要和充分的公理来构造性地证明每个数学命题。在本文中，我们分解弱Konig引理与唯一性假设WKL！！由Moschovakis，逻辑和功能存在原则，在最近的框架建设性的逆向数学。这篇文章的一部分，主题问题“现代观点的证明理论”。
From the conceptual viewpoint, many mathematical propositions implicitly contain at least two kinds of principle. One is a logical principle such as the law-of-excluded-middle or De Morgan's law. Another is a function-existence principle. For both conceptual and practical reasons, it is an interesting enterprise to calibrate how amount of logical and function-existence principles are implicit in mathematical theorems and axioms. This is the topic of constructive reverse mathematics, which specifies necessary and sufficient axioms to prove each mathematical proposition constructively. In this paper, we decompose weak Konig's lemma with a uniqueness hypothesis WKL!! by Moschovakis, into logical and function-existence principles in a recent framework of constructive reverse mathematics.This article is part of the theme issue 'Modern perspectives in Proof Theory'.