In the topological semantics for modal logic, S4 is well-known to be complete for the rational line, for the real line, and for Cantor space: these are special cases of S4’s completeness for any dense-in-itself metric space. The construction used to prove completeness can be slightly amended to show that S4 is not only complete, but also strongly complete, for the rational line. But no similarly easy amendment is available for the real line or for Cantor space and the (...) question of strong completeness for these spaces has remained open, together with the more general question of strong completeness for any dense-in-itself metric space. In this paper, we prove that S4 is strongly complete for any dense-in-itself metric space. (shrink)

We prove strong completeness results for some modal logics with the universal modality, with respect to their topological semantics over 0-dimensional dense-in-themselves metric spaces. We also use failure of compactness to show that, for some languages and spaces, no standard modal deductive system is strongly complete.

In [14], we studied the computational behaviour of various first-order and modal languages interpreted in metric or weaker distance spaces. [13] gave an axiomatisation of an expressive and decidable metric logic. The main result of this paper is in showing that the technique of representing metric spaces by means of Kripke frames can be extended to cover the modal (hybrid) language that is expressively complete over metric spaces for the (undecidable) two-variable fragment of (...) first-order logic with binary pred-icates interpreting the metric. The frame conditions needed correspond rather directly with a Boolean modal logic that is, again, of the same expressivity as the two-variable fragment. We use this representation to derive an axiomatisation of the modal hybrid variant of the two-variable fragment, discuss the compactness property in distance logics, and derive some results on (the failure of) interpolation in distance logics of various expressive power. (shrink)

Dynamic Topological Logic ( $\mathcal{DTL}$ ) is a modal framework for reasoning about dynamical systems, that is, pairs 〈X, f〉 where X is a topological space and f: X → X a continuous function. In this paper we consider the case where X is a metric space. We first show that any formula which can be satisfied on an arbitrary dynamic topological system can be satisfied on one based on a metric space; in fact, this space can be (...) taken to be countable and have no isolated points. Since any metric space with these properties is homeomorphic to the set of rational numbers, it follows that any satisfiable formula can be satisfied on a system based on $\mathbb{Q}$ . We then show that the situation changes when considering complete metric spaces, by exhibiting a formula which is not valid in general but is valid on the class of systems based on a complete metric space. While we do not attempt to give a full characterization of the set of valid formulas on this class we do give a relative completeness result; any formula which is satisfiable on a dynamical system based on a complete metric space is also satisfied on one based on the Cantor space. (shrink)

We introduce a new approach to the model theory of metric structures by defining the notion of a metric abstract elementary class (MAEC) closely resembling the notion of an abstract elementary class. Further we define the framework of a homogeneous MAEC were we additionally assume the existence of arbitrarily large models, joint embedding, amalgamation, homogeneity and a property which we call the perturbation property. We also assume that the Löwenheim-Skolem number, which in this setting refers to the density (...) character of the set instead of the cardinality, is ${\aleph_0}$ . In these settings we prove an analogue of Morley’s categoricity transfer theorem. We also give concrete examples of homogeneous MAECs. (shrink)

§ 1. Introduction. In this communication we present some recent results on the classification of Polish metric spaces up to isometry and on the isometry groups of Polish metric spaces. A Polish metric space is a complete separable metric space.Our first goal is to determine the exact complexity of the classification problem of general Polish metric spaces up to isometry. This work was motivated by a paper of Vershik [1998], where he remarks (...) : “The classification of Polish spaces up to isometry is an enormous task. More precisely, this classification is not ‘smooth’ in the modern terminology.” Our Theorem 2.1 below quantifies precisely the enormity of this task.After doing this, we turn to special classes of Polish metric spaces and investigate the classification problems associated with them. Note that these classification problems are in principle no more complicated than the general one above. However, the determination of their exact complexity is not necessarily easier.The investigation of the classification problems naturally leads to some interesting results on the groups of isometries of Polish metric spaces. We shall also present these results below.The rest of this section is devoted to an introduction of some basic ideas of a theory of complexity for classification problems, which will help to put our results in perspective. Detailed expositions of this general theory can be found, e.g., in Hjorth [2000], Kechris [1999], [2001]. (shrink)

We study Polish spaces for which a set of possible distances $A \subseteq R^+$ is fixed in advance. We determine, depending on the properties of A, the complexity of the collection of all Polish metric spaces with distances in A, obtaining also example of sets in some Wadge classes where not many natural examples are known. Moreover we describe the properties that A must have in order that all Polish spaces with distances in that set belong (...) to a given class, such as zero-dimensional, locally compact, etc. These results lead us to give a fairly complete description of the complexity, with respect to Borel reducibility and again depending on the properties of A, of the relations of isometry and isometric embeddability between these Polish spaces. (shrink)

In this paper we will consider two possible definitions of projective subsets of a separable metric space X. A set A subset of or equal to X is Σ11 iff there exists a complete separable metric space Y and Borel set B subset of or equal to X × Y such that A = {x ε X : there existsy ε Y ε B}. Except for the fact that X may not be completely metrizable, this is the classical (...) definition of analytic set and hence has many equivalent definitions, for example, A is Σ11 iff A is relatively analytic in X, i.e., A is the restriction to X of an analytic set in the completion of X. Another definition of projective we denote by ΣX1 or abstract projective subset of X. A set of A subset of or equal to X is ΣX1 iff there exists an n ε ω and a Borel set B subset of or equal to X × Xn such that A = {x ε X:there existsy ε Xn ε B}. These sets ca n be far more pathological. While the family of sets Σ11 is closed under countable intersections and countable unions, there is a consistent example of a separable metric space X where ΣX1 is not closed under countable intersections or countable unions. This takes place in the Cohen real model. Assuming CH, there exists a separable metric space X such that every Σ11 set is Borel in X but there exists a Σ11 set which is not Borel in X2. The space X2 has Borel subsets of arbitrarily large rank while X has bounded Borel rank. This space is a Luzin set and the technique used here is Steel forcing with tagged trees. We give examples of spaces X illustrating the relationship between Σ11 and ΣX1 and give some consistent examples partially answering an abstract projective hierarchy problem of Ulam. (shrink)

Fix an integer $r \ge 3$. We consider metric spaces on n points such that the distance between any two points lies in $\left\{ {1, \ldots,r} \right\}$. Our main result describes their approximate structure for large n. As a consequence, we show that the number of these metric spaces is $\left\lceil {{{r + 1} \over 2}} \right\rceil ^{\left + o\left}.$Related results in the continuous setting have recently been proved by Kozma, Meyerovitch, Peled, and Samotij [34]. When (...) r is even, our structural characterization is more precise and implies that almost all such metric spaces have all distances at least $r/2$. As an easy consequence, when r is even, we improve the error term above from $o\left$ to $o\left$, and also show a labeled first-order 0-1 law in the language ${\cal L}_r $, consisting of r binary relations, one for each element of $[r]$. In particular, we show the almost sure theory T is the theory of the Fraïssé limit of the class of all finite simple complete edge-colored graphs with edge colors in $\left\{ {r/2, \ldots,r} \right\}$.Our work can be viewed as an extension of a long line of research in extremal combinatorics to the colored setting, as well as an addition to the collection of known structures that admit logical 0-1 laws. (shrink)

§1. Introduction. Asymptotic cones of metric spaces were first invented by Gromov. They are metric spaces which capture the ‘large-scale structure’ of the underlying metric space. Later, van den Dries and Wilkie gave a more general construction of asymptotic cones using ultrapowers. Certain facts about asymptotic cones, like the completeness of the metric space, now follow rather easily from saturation properties of ultrapowers, and in this survey, we want to present two applications of the (...) van den Dries-Wilkie approach. Using ultrapowers we obtain an explicit description of the asymptotic cone of a semisimple Lie group. From this description, using semi-algebraic groups and non-standard methods, we can give a short proof of the Margulis Conjecture. In a second application, we use set theory to answer a question of Gromov.§2. Definitions. The intuitive idea behind Gromov's concept of an asymptotic cone was to look at a given metric space from an ‘infinite distance’, so that large-scale patterns should become visible. In his original definition this was done by gradually scaling down the metric by factors 1/nfornϵ ℕ. In the approach by van den Dries and Wilkie, this idea was captured by ultrapowers. Their construction is more general in the sense that the asymptotic cone exists for any metric space, whereas in Gromov's original definition, the asymptotic cone existed only for a rather restricted class of spaces. (shrink)

This paper gives a formalization of general topology in second-order arithmetic using countably based MF spaces. This formalization is used to study the reverse mathematics of general topology. For each poset P we let MF denote the set of maximal filters on P endowed with the topology generated by {Np | p ∈ P}, where Np = {F ∈ MF | p ∈ F}. We define a countably based MF space to be a space of the form MF for (...) some countable poset P. The class of countably based MF spaces includes all complete separable metric spaces as well as many nonmetrizable spaces. The following reverse mathematics results are obtained. The proposition that every nonempty Gδ subset of a countably based MF space is homeomorphic to a countably based MF space is equivalent to [Formula: see text] over ACA0. The proposition that every uncountable closed subset of a countably based MF space contains a perfect set is equivalent over [Formula: see text] to the proposition that [Formula: see text] is countable for all A ⊆ ℕ. The proposition that every regular countably based MF space is homeomorphic to a complete separable metric space is equivalent to [Formula: see text] over [Formula: see text]. (shrink)

The localic completion of a metric space induces a canonical notion of continuous map between metric spaces. It is shown that these maps are continuous in the sense of Bishop constructive mathematics, i.e., uniformly continuous near every compact image.

This manuscript investigates fixed point of single-valued Hardy-Roger’s type F -contraction globally as well as locally in a convex b -metric space. The paper, using generalized Mann’s iteration, iterates fixed point of the abovementioned contraction; however, the third axiom of the F -contraction is removed, and thus the mapping F is relaxed. An important approach used in the article is, though a subset closed ball of a complete convex b -metric space is not necessarily complete, the convergence of (...) the Cauchy sequence is confirmed in the subset closed ball. The results further lead us to some important corollaries, and examples are produced in support of our main theorems. The paper most importantly presents application of our results in finding solution to the integral equations. (shrink)

In the topological semantics for modal logic, S4 is well known to be complete for the rational line and for the real line: these are special cases of S4’s completeness for any dense-in-itself metric space. The construction used to prove completeness can be slightly amended to show that S4 is not only complete but strongly complete, for the rational line. But no similarly easy amendment is available for the real line. In an earlier paper, we proved a general theorem: (...) S4 is strongly complete for any dense-in-itself metric space. Strong completeness for the real line is a special case. In the current paper, we give a proof of strong completeness tailored to the special case of the real line: the current proof is simpler and more accessible than the proof of the more general result and involves slightly different techniques. We proceed in two steps: first, we show that S4 is strongly complete for the space of finite and infinite binary sequences, equipped with a natural topology; and then we show that there is an interior map from the real line onto this space. (shrink)

We show how to encode, by classical structures, both the objects and the morphisms of the category of complete metric spaces and uniformly continuous maps. The result is a category of, what we call, cognate metric spaces and cognate maps. We show this category relativizes to all models of set theory. We extend this encoding to an encoding of complete metric structures by classical structures. This provide us with a general technique for translating results about (...) infinitary logic on classical structures to the setting of infinitary continuous logic on continuous structures. Our encoding will also allow us to talk about not only the relations between complete metric structures, but also the potential relations between complete metric structures, i.e. those which are satisfied in some larger model of set theory. For example we will show that given any two complete metric structures we can determine if they are potentially isomorphic by looking at any admissible set which contains them both. (shrink)

The axiom of multiple choice implies that metric spaces are paracompact but the reverse implication cannot be proved in set theory without the axiom of choice.

We show that metric spaces and continuous functions between them are domain representable using the category of Scott-Ershov domains. A notion of effectivity for metric spaces is thereby inherited from effective domain theory. It is shown that a separable metric space with an effective metric can be represented by an effective domain. For a class of spaces, including the Euclidean spaces, the usual notions of effectivity are obtained. The Banach fixed point theorem (...) is a consequence of the least fixed point theorem for domains. A notion of semieffective domains is introduced and used to give a new proof of Ceitin's theorem. (shrink)

If is a Polish metric space of dimension 0, then by Wadge’s lemma, no more than two Borel subsets of X are incomparable with respect to continuous reducibility. In contrast, our main result shows that for any metric space of positive dimension, there are uncountably many Borel subsets of that are pairwise incomparable with respect to continuous reducibility. In general, the reducibility that is given by the collection of continuous functions on a topological space \\) is called the (...) Wadge quasi-order for \\). As an application of the main result, we show that this quasi-order, restricted to the Borel subsets of a Polish space \\), is a well-quasiorder if and only if \\) has dimension 0. Moreover, we give further examples of applications of the construction of graph colorings that is used in the proofs. (shrink)

The most majestic scientific achievement, of this century in mathematical beauty, axiomatic consistency, and experimental verifications has been special relativity with its unitary structure at the operator level, and canonical structure at the classical levels, which has turned out to be exactly valid for point particles moving in the homogenenous and isotropic vacuum (exterior dynamical problems). In recent decades a number of authors have studied nonunitary and noncanonical theories, here generally calleddeformations for the representation of broader conditions, such as extended (...) and deformable particles moving within inhomogeneous and anisotrophic physical media (interior dynamical problems). In this paper we show that nonunitary deformations, including, q-, k-, quatum-, Lie-isotopic, Lie-admissible, and other deformations, even thoughmathematically correct, have a number of problematic aspects ofphysical character when formulated on conventional spaces over conditional fields, such as lack of invariance of the basic space-time units, ambiguous applicability to measurements, loss of Hermiticity-observability in time, lack of invariant numerical predictions, loss of the axions of special relativity, and others. We then show that the classical noncanonical counterparts of the above nonunitary deformations are equally afflicted by corresponding problems of physical consistency. We also show that the contemporary formulation of gravity is afflicted by similar problematic aspects because Riemannian spaces are noncanonical deformations of Minkowskian spaces, thus having noninvariant space-time units. We then point out that new mathematical methods, calledisotopies, genotopies, hyperstructures and their isoduals, offer the possibilities of constructing a nonunitary theory, known asrelativistic hadronic mechanics which: (1) is as axiomatically consistent as relativistic quantum mechanics, (2) preserves the abstract axioms of special relativity, and (3) results in a completion of the conventional mechanics much along the celebrated Einstein-Podolski-Rosen argument. A number of novel applications are indicated, such as a geometric unification of the special and general relativity via the isominkowskian geometry in which the two relativities are differentiated via the invariant basic unit, while preserving conventional Riemannian metrics, Einstein's field equations, and related experimental verifications; a novel operator form of gravity verifying the axioms of relativistic quantum mechanics under the universal isopoincaré symmetry; a new structure model of hadrons with conventional massive particles as physical constituents which is compatile with composite quarks and with established unitary classifications; and other novels applications in nuclear physics, astrophysics, theoretical biology, and other fields. The paper ends with the proposal of a number of new experiments, some of which may imply new practical applications, such as conceivable new forms of recycling nuclear waste. The achievement of axiomatic consistency in the study of the above physical problems has been possible for the first time in this paper thanks to mathematical advances that recently appeared in a special issue of theRendiconti Circolo Matematico Palermo, and in other journals identified in the Acknowledgements. (shrink)

Using the category of metric spaces as a template, we develop a metric analogue of the categorical semantics of classical/intuitionistic logic, and show that the natural notion of predicate in this “continuous semantics” is equivalent to the a priori separate notion of predicate in continuous logic, a logic which is independently well-studied by model theorists and which finds various applications. We show this equivalence by exhibiting the real interval $[0,1]$ in the category of metric spaces (...) as a “continuous subobject classifier” giving a correspondence not only between the two notions of predicate, but also between the natural notion of quantification in the continuous semantics and the existing notion of quantification in continuous logic.Along the way, we formulate what it means for a given category to behave like the category of metric spaces, and afterwards show that any such category supports the aforementioned continuous semantics. As an application, we show that categories of presheaves of metric spaces are examples of such, and in fact even possess continuous subobject classifiers. (shrink)

Strengthening a theorem of Hjorth this paper gives a new characterization of which Polish groups admit compatible complete left invariant metrics. As a corollary it is proved that any Polish group without a complete left invariant metric has a continuous action on a Polish space whose associated orbit equivalence relation is not essentially countable.

We study conditions for a topological space to be metrizable, properties of metrizable spaces, and the role the axiom of choice plays in these matters.

We show that the set of points of an overt closed subspace of a metric completion of a Bishop-locally compact metric space is located. Consequently, if the subspace is, moreover, compact, then its collection of points is Bishop-compact. © 2011 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim.

Two real-valued deduction schemes are introduced, which agree on $\vdash \triangle$ but not on $\Gamma \vdash \triangle$ , where Δ and ▵ are finite sets of formulae. Using the first scheme we axiomatize real-valued equality so that it induces metrics on the domains of appropriate structures. We use the second scheme to reduce substitutivity of equals to uniform continuity, with respect to the metric equality, of interpretations of predicates in structures. This continuity extends from predicates to arbitrary formulae and (...) the appropriate models have completions resembling analytic completions of metric spaces. We provide inference rules for the two deductions and discuss definability of each of them by means of the other. (shrink)

We prove in the framework of Bishop's constructive mathematics that the sequential completion equation image of the space [MATHEMATICAL SCRIPT CAPITAL D] is filter-complete. Then it follows as a corollary that the filter-completeness of [MATHEMATICAL SCRIPT CAPITAL D] is equivalent to the principle BD-ℕ, which can be proved in classical mathematics, Brouwer's intuitionistic mathematics and constructive recursive mathematics of Markov's school, but does not in Bishop's constructive mathematics. We also show that equation image is identical with the filter-completion (...) which was provided by Bishop. (shrink)

Under the axiom of choice, every first countable space is a Fréchet-Urysohn space. Although, in its absence even ℝ may fail to be a sequential space.Our goal in this paper is to discuss under which set-theoretic conditions some topological classes, such as the first countable spaces, the metric spaces, or the subspaces of ℝ, are classes of Fréchet-Urysohn or sequential spaces.In this context, it is seen that there are metric spaces which are not sequential (...) spaces. This fact raises the question of knowing if the completion of a metric space exists and it is unique. The answer depends on the definition of completion.Among other results it is shown that: every first countable space is a sequential space if and only if the axiom of countable choice holds, the sequential closure is idempotent in ℝ if and only if the axiom of countable choice holds for families of subsets of ℝ, and every metric space has a unique equation image-completion. (shrink)

It is shown that for compact metric spaces the following statements are pairwise equivalent: “X is Loeb”, “X is separable”, “X has a we ordered dense subset”, “X is second countable”, and “X has a dense set G = ∪{Gn : n ∈ ω}, ∣Gn∣ < ω, with limn→∞ diam = 0”. Further, it is shown that the statement: “Compact metric spaces are weakly Loeb” is not provable in ZF0 , the Zermelo-Fraenkel set theory without the (...) axiom of regularity, and that the countable axiom of choice for families of finite sets CACfin does not imply the statement “Compact metric spaces are separable”. (shrink)

: In the first edition of his book on the completeness of Kant’s table of judgments, Klaus Reich shortly indicates that the B-version of the metaphysical exposition of space in the Critique of pure reason is structured following the inverse order of the table of categories. In this paper, I develop Reich’s claim and provide further evidence for it. My argumentation is as follows: Through analysis of our actually given representation of space as some kind of object, the metaphysical exposition (...) will show that this representation is secondary to space considered as an original, undetermined and as such unrepresentable intuitive manifold. Now, following Kant, the representation of any kind of object involves diversity, synthesis and unity. In the case of our representation of space as formal intuition, this involves, firstly, a manifold a priori, i.e. space as pure form, delivered by the transcendental Aesthetic, secondly, a figurative, productive synthesis of that manifold, and, thirdly, the unity provided by the categories. Analysing our given representation of space – the task of the metaphysical exposition – amounts to dismantling its unity and determine its characteristics with respect to the categories. (shrink)

It has been known for long time that the cosmic sound wave was there since the early epoch of the Universe. Signatures of its existence are abound. However, such an acoustic model of cosmology is rarely developed fully into a complete framework from the notion of space, cancer therapy up to the sky. This paper may be the first attempt towards such a complete description of the Universe based on classical wave equation of sound. It is argued that one can (...) arrive at a consistent description of space, elementary particles, Sachs-Wolfe acoustic theorem, up to a novel approach for cancer therapy, starting from this simple classical wave equation of sound. We also discuss a plausible extension of Acoustic Sachs-Wolfe theorem based on its analogue with Klein-Gordon equation to become Acoustic Sachs-Wolfe-Christianto-Smarandache-Umniyati (ASWoCSU) equation. It is our hope that the new proposed equation can be verified with observation data. But we admit that our model is still in its infancy, more researches are needed to fill all the missing details. (shrink)

This paper studies the metric structure of the space Hr of absolutely summable sequences of real numbers with at most r nonzero terms. Hr is complete, and is located and nowhere dense in the space of all absolutely summable sequences. Totally bounded and compact subspaces of Hr are characterized, and large classes of located, totally bounded, compact, and locally compact subspaces are constructed. The methods used are constructive in the strict sense. MSC: 03F65, 54E50.

The size of animal exhibits has important effects on their lives and welfare. However, most references to exhibit size only consider floor space and height dimensions, without considering the space afforded by usable features within the exhibit. In this paper, we develop two possible methods for measuring the usable space of zoo exhibits and apply these to a sample exhibit. Having a metric for usable space in place will provide a better reflection of the quality of different exhibits, and (...) enhance comparisons between exhibits. (shrink)

This work concerns constructive aspects of measure theory. By considering metric completions of Boolean algebras – an approach first suggested by Kolmogorov – one can give a very simple construction of e.g. the Lebesgue measure on the unit interval. The integration spaces of Bishop and Cheng turn out to give examples of such Boolean algebras. We analyse next the notion of Borel subsets. We show that the algebra of such subsets can be characterised in a pointfree and constructive (...) way by an initiality condition. We then use our work to define in a purely inductive way the measure of Borel subsets. (shrink)

We examine, from a constructive perspective, the relation between the complements of S, T, and S ∩ T in X, where X is either a metric space or a normed linear space. The fundamental question addressed is: If x is distinct from each element of S ∩ T, if s ϵ S, and if t ϵ T, is x distinct from s or from t? Although the classical answer to this question is trivially affirmative, constructive answers involve Markov's principle (...) and the completeness of metric spaces. (shrink)

We prove that the set of all Polish groups admitting a compatible complete left-invariant metric (called CLI) is coanalytic non-Borel as a subset of a standard Borel space of all Polish groups. As an application of this result, we show that there does not exist a weakly universal CLI group. This, in particular, answers in the negative a question of H.Becker.

We show, within the framework of Bishop's constructive mathematics, that (sequential) completeness of the locally convex space $\mathcal{D} (\mathbb{R})$ of test functions is equivalent to the principle BD-N which holds in classical mathemtatics, Brouwer's intuitionism and Markov's constructive recursive mathematics, but does not hold in Bishop's constructivism.

We show, within the framework of Bishop's constructive mathematics, that (sequential) completeness of the locally convex space $\mathcal{D} (\mathbb{R})$ of test functions is equivalent to the principle BD-N which holds in classical mathemtatics, Brouwer's intuitionism and Markov's constructive recursive mathematics, but does not hold in Bishop's constructivism.

Subset Spaces were introduced by L. Moss and R. Parikh in [8]. These spaces model the reasoning about knowledge of changing states.In [2] a kind of subset space called intersection space was considered and the question about the existence of a set of axioms that is complete for the logic of intersection spaces was addressed. In [9] the first author introduced the class of directed spaces and proved that any set of axioms for directed frames also (...) characterizes intersection spaces.We give here a complete axiomatization for directed spaces. We also show that it is not possible to reduce this set of axioms to a finite set. (shrink)

We develop the general theory of topometric spaces, i.e., topological spaces equipped with a well-behaved lower semi-continuous metric. Spaces of global and local types in continuous logic are the motivating examples for the study of such spaces. In particular, we develop Cantor-Bendixson analysis of topometric spaces, which can serve as a basis for the study of local stability (extending the ad hoc development in Ben Yaacov I and Usvyatsov A, Continuous first order logic and (...) local stability. Trans Am Math Soc, in press), as well as of global ${\aleph_0}$ -stability. We conclude with a study of perturbation systems (see Ben Yaacov I, On perturbations of continuous structures, submitted) in the formalism of topometric spaces. In particular, we show how the abstract development applies to ${\aleph_0}$ -stability up to perturbation. (shrink)

The Dedekind cuts in an ordered set form a set in the sense of constructive Zermelo—Fraenkel set theory. We deduce this statement from the principle of refinement, which we distill before from the axiom of fullness. Together with exponentiation, refinement is equivalent to fullness. None of the defining properties of an ordering is needed, and only refinement for two—element coverings is used. In particular, the Dedekind reals form a set; whence we have also refined an earlier result by Aczel and (...) Rathjen, who invoked the full form of fullness. To further generalise this, we look at Richman's method to complete an arbitrary metric space without sequences, which he designed to avoid countable choice. The completion of a separable metric space turns out to be a set even if the original space is a proper class; in particular, every complete separable metric space automatically is a set. (shrink)

-/- Continuous first-order logic has found interest among model theorists who wish to extend the classical analysis of “algebraic” structures (such as fields, group, and graphs) to various natural classes of complete metric structures (such as probability algebras, Hilbert spaces, and Banach spaces). With research in continuous first-order logic preoccupied with studying the model theory of this framework, we find a natural question calls for attention. Is there an interesting set of axioms yielding a completeness result? -/- (...) The primary purpose of this article is to show that a certain, interesting set of axioms does indeed yield a completeness result for continuous first-order logic. In particular, we show that in continuous first-order logic a set of formulae is (completely) satisfiable if (and only if) it is consistent. From this result it follows that continuous first-order logic also satisfies an approximated form of strong completeness, whereby Σ⊧φ (if and) only if Σ⊢φ ∸2−n for all n < ω. This approximated form of strong completeness asserts that if Σ⊧φ, then proofs from Σ, being finite, can provide arbitrarily better approximations of the truth of φ. -/- Additionally, we consider a different kind of question traditionally arising in model theory—that of decidability. When is the set of all consequences of a theory (in a countable, recursive language) recursive? Say that a complete theory T is decidable if for every sentence φ, the value φ T is a recursive real, and moreover, uniformly computable from φ. If T is incomplete, we say it is decidable if for every sentence φ the real number φ T o is uniformly recursive from φ, where φ T o is the maximal value of φ consistent with T. As in classical first-order logic, it follows from the completeness theorem of continuous first-order logic that if a complete theory admits a recursive (or even recursively enumerable) axiomatization then it is decidable. (shrink)

We propose a logic for reasoning about metric spaces with the induced topologies. It combines the 'qualitative' interior and closure operators with 'quantitative' operators 'somewhere in the sphere of radius r.' including or excluding the boundary. We supply the logic with both the intended metric space semantics and a natural relational semantics, and show that the latter (i) provides finite partial representations of (in general) infinite metric models and (ii) reduces the standard '∈-definitions' of closure and (...) interior to simple constraints on relations. These features of the relational semantics suggest a finite axiomatisation of the logic and provide means to prove its EXPTIME-completeness (even if the rational numerical parameters are coded in binary). An extension with metric variables satisfying linear rational (in)equalities is proved to be decidable as well. Our logic can be regarded as a 'well-behaved' common denominator of logical systems constructed in temporal, spatial, and similarity-based quantitative and qualitative representation and reasoning. Interpreted on the real line (with its Euclidean metric), it is a natural fragment of decidable temporal logics for specification and verification of real-time systems. On the real plane, it is closely related to quantitative and qualitative formalisms for spatial representation and reasoning, but this time the logic becomes undecidable. (shrink)

We propose a logic for reasoning about metric spaces with the induced topologies. It combines the ‘qualitative’ interior and closure operators with ‘quantitative’ operators ‘somewhere in the sphere of radiusr’ including or excluding the boundary. We supply the logic with both the intended metric space semantics and a natural relational semantics, and show that the latter (i) provides finite partial representations of (in general) infinite metric models and (ii) reduces the standard ‘ε-definitions’ of closure and interior (...) to simple constraints on relations. These features of the relational semantics suggest a finite axiomatisation of the logic and provide means to prove its EXPTIME-completeness (even if the rational numerical parameters are coded in binary). An extension with metric variables satisfying linear rational (in)equalities is proved to be decidable as well. Our logic can be regarded as a ‘well-behaved’ common denominator of logical systems constructed in temporal, spatial, and similarity-based quantitative and qualitative representation and reasoning. Interpreted on the real line (with its Euclidean metric), it is a natural fragment of decidable temporal logics for specification and verification of real-time systems. On the real plane, it is closely related to quantitative and qualitative formalisms for spatial representation and reasoning, but this time the logic becomes undecidable. (shrink)

We show that the countable axiom of choice CAC strictly implies the statements “Lindelöf metric spaces are second countable” “Lindelöf metric spaces are separable”. We also show that CAC is equivalent to the statement: “If is a Lindelöf topological space with respect to the base ℬ, then is Lindelöf”.