On Constructivity and the Rosser Property: a closer look at some G\"odelean proofs

TL;DR

This paper examines the constructivity and Rosser property of various proofs of G"odel's Incompleteness Theorem, revealing which proofs explicitly construct independent sentences and which only prove their existence.

Contribution

It provides a detailed analysis of the constructivity and Rosser property in proofs by G"odel, Rosser, Kleene, Chaitin, and Boolos, highlighting the differences and a variant with the Rosser property.

Findings

G"odel's original proof lacks the Rosser property.

Kleene's and Boolos' proofs are non-constructive.

A variant of Chaitin's proof can have the Rosser property.

Abstract

The proofs of Kleene, Chaitin and Boolos for G\"odel's First Incompleteness Theorem are studied from the perspectives of constructivity and the Rosser property. A proof of the incompleteness theorem has the Rosser property when the independence of the true but unprovable sentence can be shown by assuming only the (simple) consistency of the theory. It is known that G\"odel's own proof for his incompleteness theorem does not have the Rosser property, and we show that neither do Kleene's or Boolos' proofs. However, we show that a variant of Chaitin's proof can have the Rosser property. The proofs of G\"odel, 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.