Gödel’s second incompleteness theorem states that for a sufficiently strong and consistent theory there exists a formula which expresses the consistency of the theory and is not provable inside that theory. Here the notions of “sufficiently strong theory” and “expressing the consistency” should be carefully analyzed, as this theorem is sensitive to these concepts. For example, Rosser’s consistency is provable in a sufficiently strong theory (and so Gödel’s theorem does not hold for this consistency statement); also it is known that weak theories, in which Löb’s rule is not valid, might be able to prove their own consistency: adding a fixed point \(F\) of \(x\mapsto \neg{\mathtt pr}_T(\neg x)\) to a very weak theory \(T\) will result in a theory \(T+F\) which is consistent since Löb’s rule cannot be applied to \(T\vdash \neg F\rightarrow{\mathtt pr}_T(\neg F)\) to conclude \(T\vdash\neg F\), and the consistent theory \(T+F\) implies its own consistency, i.e., \(T+F\vdash {\mathtt con}(T+F)\).
The author postpones the discussion of the crucial question as to what do we mean by “expressing the consistency of the theory”, and in fact never comes back to it. Instead the other question, when a theory is “sufficiently strong”, catches the author’s attention. Usually “sufficiently strong” means containing Robinson’s arithmetic Q, but as the author argues a theory like Zermelo-Frankel set theory ZF does not contain Q in the strict sense; but it does by a translation, or more generally by an interpretation. The interpretations considered in this paper are “one-dimensional, many-sorted, relative interpretations without parameters, where identity is not necessarily translated as identity”. So a beautiful reading of Gödel’s second theorem is that no recursively enumerable theory \(T\) can interpret \({\mathbf Q}+{\mathtt con}(T)\), where \({\mathtt con}(T)\) is a canonical consistency statement of \(T\).
In this paper the author provides some characterizations for the statements of cut-free consistency and standard consistency (with the cut rule) for certain theories. For a theory \(T\) he defines the theory \({\mathtt SEQ}(T)\) and shows that for a finitely axiomatized theory \(A\), the cut-free consistency statement of \(A\) is the unique \(\Pi_1\)-sentence \(P\) such that \({\mathtt SEQ}(A)\) is mutually interpretable in \({\mathbf Q}+P\). This cut-free consistency can be characterized as follows for a finitely axiomatizable and sequential theory \(A\): it is the unique \(\Pi_1\)-sentence \(P\) such that \(\mathbf{EA}+P\) is mutually interpretable in \({\mathbf Q}+P\), where EA is elementary arithmetic (\(\mathrm{I}\Delta_0 + \mathrm{Exp}\)). Finally, the consistency statement of a finitely axiomatizable and sequential theory \(A\) is the unique \(\Pi_1\)-sentence \(P\) such that \({\mathbf Q}+P\) is mutually interpretable in \(A\). The paper contains also some other interesting results.