Logics of metric spaces

We investigate the expressive power and computational properties of two different types of languages intended for speaking about distances. First, we consider a first-order language ℱM the two-variable fragment of which turns out to be undecidable in the class of distance spaces validating the triangular inequality as well as in the class of all metric spaces. Yet, this two-variable fragment is decidable in various weaker classes of distance spaces. Second, we introduce a variable-free modal language ℳS that, when interpreted in metric spaces, has the same expressive power as the two-variable fragment of ℱM. We determine natural and expressive fragments of ℳS which are decidable in various classes of distance spaces validating the triangular inequality, in particular, the class of all metric spaces.