Effective topological spaces. I: A definability theory
This is the first episode of a three parts study intending to introduce an arithmetization and a first-order logic for the theory of topological spaces. The main subject of the work under review is the definition of satisfaction for formulas expressing topological properties. The main idea is that ''in computing practice one rarely has perfect information about a point but at best has an approximation in the form of a neighborhood''. Thus for each topological space X a first-order language without equality \(L_ X\) is associated such that the open subsets of the n-fold cartesian product \(X^ n\) under the product topology are designated by the n-ary predicate symbols of \(L_ X\). For such a predicate P, ''P(\(\alpha)\) is true'' means that \(\alpha\) is contained in the regular open set determined by P. This definition is adequately extended for the logical connectives and quantifiers of \(L_ X\). Some important logical rules of deduction, such as modus ponens and syllogism, are proved. It is clarified what it means for a formula to define a set and then there are found criteria for deciding whether a formula is a definition or not. In conclusion the present approach seems to be more adequate and general than the classical effective presentation through the rationals of the real line topology.
formulas expressing topological properties
scientific article; zbMATH DE number 3908421
scientific article