Gödel–Rosser's Incompleteness Theorem, generalized and optimized for definable theories
Saeed Salehi, Payam Seraji · Journal of Logic and Computation · 2016
Gödel–Rosser's Incompleteness Theorem is generalized by showing Πn+1-incompleteness of any Σn+1-definable extension of Peano Arithmetic which is either Σn-sound or n-consistent. The optimality of this result is proved by presenting a complete, Σn+1-definable, Σn−1-sound, and (n−1)-consistent theory for any n>0. Though the proof of the incompleteness theorem for Σn+1-definable theories using the Σn-soundness assumption is constructive, it is shown that there is no constructive proof for the Incompleteness Theorem for Σn+1-definable theories using the n-consistency assumption, when n>2.