Constructibility and Rosserizability of the Proofs of Boolos and Chaitin for Godel's Incompleteness Theorem.
Saeed Salehi, Payam Seraji · arXiv (Cornell University) · 2016
The proofs of Chaitin and Boolos for Godel's Incompleteness Theorem are studied from the perspectives of constructibility and Rosserizability. By Rosserization of a proof we mean that the independence of the true but unprovable sentence can be shown by assuming only the (simple) consistency of the theory. It is known that Godel's own proof for his incompleteness theorem is not Rosserizable, and we show that neither are Kleene's or Boolos' proofs. However, we prove a Rosserized version of Chaitin's (incompleteness) theorem. The proofs of Godel, Rosser and Kleene are constructive in the sense that they explicitly construct, by algorithmic ways, the independent sentence(s) from the theory. We show that the proofs of Chaitin and Boolos are not constructive, and they prove only the mere existence of the independent sentences.