The Second Incompleteness Theorem and Bounded Interpretations

In this paper we formulate a version of Second Incompleteness Theorem. The idea is that a sequential sentence has ‘consistency power’ over a theory if it enables us to construct a bounded interpretation of that theory. An interpretation of V in U is bounded if, for some n, all translations of V-sentences are U-provably equivalent to sentences of complexity less than n. We call a sequential sentence with consistency power over T a pro-consistency statement for T. We study pro-consistency statements. We provide an example of a pro-consistency statement for a sequential sentence A that is weaker than an ordinary consistency statement for A. We show that, if A is ${{sf S}^{1}_{2}}$ , this sentence has some further appealing properties, specifically that it is an Orey sentence for EA. The basic ideas of the paper essentially involve sequential theories. We have a brief look at the wider environment of the results, to wit the case of theories with pairing.