An incompleteness theorem via ordinal analysis

Abstract

We present an analogue of Gödel's second incompleteness theorem for systems of second-order arithmetic. Whereas Gödel showed that sufficiently strong theories that are ${\Pi }_1^0$-sound and ${\Sigma }_1^0$-definable do not prove their own ${\Pi }_1^0$-soundness, we prove that sufficiently strong theories that are ${\Pi }_1^1$-sound and ${\Sigma }_1^1$-definable do not prove their own ${\Pi }_1^1$-soundness. Our proof does not involve the construction of a self-referential sentence but rather relies on ordinal analysis.