  We present a new manifestation of G\"odel's second incompleteness theorem and
discuss its foundational significance, in particular with respect to Hilbert's
program. Specifically, we consider a proper extension of Peano arithmetic
($\mathbf{PA}$) by a mathematically meaningful axiom scheme that consists of
$\Sigma^0_2$-sentences. These sentences assert that each computably enumerable
($\Sigma^0_1$-definable without parameters) property of finite binary trees has
a finite basis. Since this fact entails the existence of polynomial time
algorithms, it is important for computer science. On a technical level, our
axiom scheme is a variant of an independence result due to Harvey Friedman. At
the same time, the meta-mathematical properties of our axiom scheme distinguish
it from most known independence results: Due to its logical complexity, our
axiom scheme does not add computational strength. The only known method to
establish its independence relies on G\"odel's second incompleteness theorem.
In contrast, G\"odel's theorem is not needed for typical examples of
$\Pi^0_2$-independence (such as the Paris-Harrington principle), since
computational strength provides an extensional invariant on the level of
$\Pi^0_2$-sentences.
