From intuitionistic mathematics to point-free topology
From intuitionistic mathematics to point-free topology
复制标题
从直觉数学到无点拓扑
DOI：
10.1142/9789811236488_0003
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Tatsuji Kawai
中科院分区：
文献类型：
--
作者：
Yoshikazu Giga;Fumihiko Onoue;Keisuke Takasao;梶原直人;Tatsuji Kawai
本文从无点拓扑的角度重新审视直觉实数。我们对三元分布对实数的直观表示的分析导致了实数的独特表示，称为正则理想。正则理想的概念是几何的，因此存在相关的正则理想的形式空间。这为我们提供了无点实数的新颖概念。作为无点概念的应用，我们给出了中间值定理和布劳威尔不动点定理的无点证明。这些证明使这些定理的有限方面比通常诉诸某些选择原则的点集对应物更加明确。
This paper takes another look at the intuitionistic real numbers from the viewpoint of point-free topology. Our analysis of the intuitionistic presentation of real numbers by the ternary spread leads to a unique representation of a real number called regular ideal. The notion of regular ideal is geometric, and hence there is an associated formal space of regular ideals. This provides us with a novel notion of point-free real numbers. As applications of this point-free notion, we give point-free proofs of the intermediate value theorem and Brouwer’s fixed-point theorem. These proofs make the finitary aspect of these theorems more explicit than their point-set counterparts that typically appeal to some choice principles.