Apartness and formal topology
Apartness and formal topology
复制标题
分离性和形式拓扑
DOI：
--
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
P. Schuster
中科院分区：
文献类型：
--
作者：
Erik Palmgren;P. Schuster
形式空间的理论和最近的分离空间理论有一个先验的共同点，即它们都是作为一般拓扑学的一种构造性方法而提出的。尽管如此，我们还是试图做第一步，把这些相互竞争的理论联系起来。形式拓扑是在1980年代中期由Sambin [11]提出的，目的是为了使Martin-Löf的类型理论[9]可以使用经典拓扑的概念，这些概念值得保留在这样一个构造性和谓词性的框架中。形式拓扑学的发展受到Fourman和Grayson [8]提出的形式空间理论的启发。从早期开始，形式拓扑就被证明是一种以无点方式进行拓扑的相当通用的设置。我们参考[12]中关于形式拓扑的最近的详尽的调查。分离空间的理论是由Bridges和Vaughan [4]在将近20年后开始的，将集合论拓扑重新表述为Bishop的构造性分析的扩展[2，3]。随后的发展理论的apartness空间也揭示了一些光在其经典的对应，理论的接近或接近空间。很快就会有一个全面的概述[5]。在形式拓扑学中，“基本邻域”是一个原始概念，而“点”是一个派生概念;作为基本邻域的集合，点必须特别小心地处理，以满足像马丁-洛夫类型理论这样的谓词框架的需要。在分离空间理论中，情况正好相反：在经典拓扑学中，点是这样给出的，而（基本）邻域是点的集合。由于，但是，这是很难发现任何真正的impredicative动议的做法主教的建设性数学一般，我们敢于进行以下尝试联系正式拓扑和理论的apartness空间彼此。1.基本定义我们回顾与形式拓扑和它们之间的态射（可逼近映射）相关的标准定义。定义1.1.设A是一个集合，设A的元素与A的子集之间的关系，即<$A× P（A）。通过设置U V扩展到A的子集之间的关系，当且仅当对所有a ∈ U都有V。对于一个预序（A，≤）和一个子集U <$A，它的下闭包U≤由那些a ∈ A使得a ≤ B对某些B ∈ U组成。1991年数学科目分类小学03 F65、中学03 F60、06 D22、54 A05、54 E17、54 E05。
The theory of formal spaces and the more recent theory of apartness spaces have a priori not much more in common than that each of them was initiated as a constructive approach to general topology. We nonetheless try to do the first steps in relating these competing theories to each other. Formal topology was put forward in the mid 1980s by Sambin [11] in order to make available to Martin–Löf’s type theory [9] the concepts of classical topology that are worth keeping to such a constructive and predicative framework. The development of formal topology was inspired by, among other things, the theory of formal spaces worked out by Fourman and Grayson [8]. Since its early days formal topology has proved a fairly universal setting for doing topology in a point–free way. We refer to [12] for a recent and exhaustive survey of formal topology. The theory of apartness spaces was started by Bridges and Vı̂ţă [4] nearly twenty years later to reformulate set–theoretic topology as an extension of Bishop’s constructive analysis [2, 3]. The subsequent development of the theory of apartness spaces has also shed some light on its classical counterpart, the theory of proximity or nearness spaces. A comprehensive overview will be available soon [5]. In formal topology ‘basic neighbourhood’ is a primitive concept, whereas ‘point’ is a derived notion; as sets of basic neighbourhoods, points have to be handled with particular care to meet the needs of a predicative framework like Martin–Löf type theory. In the theory of apartness spaces, it is the other way round: as in classical topology, points are given as such, and (basic) neighbourhoods are sets of points. Since, however, it is hard to detect any truly impredicative move in the practice of Bishop’s constructive mathematics in general, we dare to undertake the following attempt to link formal topology and the theory of apartness spaces to each other. 1. Basic Definitions We recall the standard definitions associated with formal topologies and morphisms between them (approximable mappings). Definition 1.1. Let A be a set, and let be a relation between elements of A and subsets of A, i.e. ⊆ A× P(A). Extend to a relation between subsets of A by setting U V if and only if a V for all a ∈ U . For a preorder (A,≤) and a subset U ⊆ A, its downwards closure U≤ consists of those a ∈ A such that a ≤ b for some b ∈ U . 1991 Mathematics Subject Classification Primary 03F65, Secondary 03F60, 06D22, 54A05, 54E17, 54E05.