论文标题
关于$ \ mathbb {r} $的不可支配性
On the uncountability of $\mathbb{R}$
论文作者
论文摘要
Cantor的第一盘理论论文（1874）确定了$ \ Mathbb {r} $的不可数。我们研究了以高阶算术语言提出的最基本的数学事实。特别是，我们研究了NIN（NBI分别）的逻辑和计算属性，即第三阶语句：没有$ [0,1] $到$ \ MATHBB {n} $的注射（分别进行射击）。在Kohlenbach的高阶反向数学中工作，我们表明NIN和NBI很难证明（常规）理解公理，而许多基本定理（如Arzela的Riemann collement the Riemann Integrals（1885））都暗示了NIN的融合定理（1885），这意味着NIN nin and and and and/或nbi。在Kleene的高阶可计算性理论基于S1-S9的工作中，我们表明，基于NIN的以下四阶过程很难计算：对于给定的$ [0,1] \ RightArrow \ MathBb {N} $ - 函数，在单位间隔中找到与相同自然数量的单位间隔中的真实词。
Cantor's first set theory paper (1874) establishes the uncountability of $\mathbb{R}$. We study this most basic mathematical fact formulated in the language of higher-order arithmetic. In particular, we investigate the logical and computational properties of NIN (resp. NBI), i.e. the third-order statement: there is no injection (resp. bijection) from $[0,1]$ to $\mathbb{N}$. Working in Kohlenbach's higher-order Reverse Mathematics, we show that NIN and NBI are hard to prove in terms of (conventional) comprehension axioms, while many basic theorems, like Arzela's convergence theorem for the Riemann integral (1885), are shown to imply NIN and/or NBI. Working in Kleene's higher-order computability theory based on S1-S9, we show that the following fourth-order process based on NIN is similarly hard to compute: for a given $[0,1]\rightarrow \mathbb{N}$-function, find reals in the unit interval that map to the same natural number.
