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Σ₁.