Abstract
We present an analogue of Godel's second incompleteness theorem for systems of second-order arithmetic. Whereas Godel showed that sufficiently strong theories that are Pi(0)(1)-sound and sigma(0)(1)-definable do not prove their own Pi(0)(1)-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.

This publication has 15 references indexed in Scilit: