In this paper we devise some technical tools for dealing with
problems connected with the philosophical view usually called
mathematical instrumentalism. These tools are interesting in
their own right, independently of their philosophical
consequences. For example, we show that even though the fragment
of Peano's Arithmetic known as IΣ₁ is a conservative
extension of the equational theory of Primitive Recursive
Arithmetic (PRA), IΣ₁ has a super-exponential
speed-up over PRA. On the other hand, theories studied in
the Program of Reverse Mathematics that formalize powerful
mathematical principles have only polynomial speed-up over
IΣ₁.
¶
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.