Godel's Second Incompleteness Theorem for Definable Theories

TL;DR

This paper extends Godel's Second Incompleteness Theorem to definable theories, showing limitations on their ability to prove their own soundness, with optimality demonstrated through specific theory constructions.

Contribution

It generalizes Godel's Second Incompleteness Theorem to $ ext{Sigma}_{n+1}$-definable theories and establishes the limits of self-proof of soundness for various classes of theories.

Findings

$ ext{Sigma}_{n+1}$-definable, $ ext{Sigma}_n$-sound theories extending PA cannot prove their $ ext{Sigma}_n$-soundness.

Constructed theories show the optimality of the main result.

No recursively enumerable theory, even very weak ones, can prove their own $ ext{Sigma}_1$-soundness.

Abstract

It is proved that if $T$ is a $\Sigma_{n+1}$ Definable theory which is $\Sigma_n$-sound and extends $PA$, then $T$ can not prove the sentence $\Sigma_n-sound(T)$ that expresses the $\Sigma_n$-soundness of $T$. Optimality of this result is showed by constructing a $\Sigma_{n+1}$-definable and $\Sigma_{n-1}$-sound theory extending $PA$ such that $\Sigma_n-sound(T)$ is $T$-provable. It is also proved that no R.E. arithmetical theory, evevn very weak theories which are not $\Sigma_1$-complete, can prove $\Sigma_1$-soundness of itself.