A Foundation for Metareasoning Part I: The Proof Theory

We propose a framework, called OM pairs, for the formalization of metareasoning. OM pairs allow us to generate deductively pairs composed of an object theory and a metatheory related via a so called reflection principle. This is done by imposing, via appropriate reflection rules, the relation we want to hold between the object theory and the metatheory. In this paper we concentrate on the proof theory of OM pairs. We study them from various points of view: we compare the strength of the object theory and the metatheories generated by different combination of reflection rules; for each combination we characterize the object theory and metatheory, both axiomatically (when possible), and by means of fix-point equations. Finally we present four important case studies.