On constructivity and the Rosser property: a closer look at some Gödelean proofs

DOI10.1016/J.APAL.2018.04.009MaRDI QIDQ1653263zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Saeed Salehi, Payam Seraji

Publication date 17 July 2018

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1612.02549

zbMATH Keywords

incompletenessconstructive proofBoolos' proofChaitin's proofKleene's proofRosser property

Mathematics Subject Classification ID

Algorithmic randomness and dimension (03D32) Algorithmic information theory (Kolmogorov complexity, etc.) (68Q30) First-order arithmetic and fragments (03F30) Gödel numberings and issues of incompleteness (03F40)

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.

Recommendations

• On the Constructive Dedekind Reals: Extended Abstract
• On Rosser's Provability Predicate
• On the constructive Dedekind reals
• Generalisations of Gödel's universe of constructible sets
• scientific article; zbMATH DE number 4030318
• Compactness in constructive analysis revisited
• On the Cauchy completeness of the constructive Cauchy reals
• On the Cauchy completeness of the constructive Cauchy reals
• A constructive proof of Kirszbraun's theorem

Cites work

• scientific article; zbMATH DE number 5776111 (Why is no real title available?)
• scientific article; zbMATH DE number 4066875 (Why is no real title available?)
• scientific article; zbMATH DE number 1144041 (Why is no real title available?)
• scientific article; zbMATH DE number 1550362 (Why is no real title available?)
• scientific article; zbMATH DE number 3057484 (Why is no real title available?)
• scientific article; zbMATH DE number 3073037 (Why is no real title available?)
• A Note on Boolos' Proof of the Incompleteness Theorem
• Algorithmic information theory
• An introduction to Gödel's theorems
• Boolos-style proofs of limitative theorems
• General recursive functions of natural numbers
• Gödel incompleteness theorems and the limits of their applicability. I
• Gödel's incompleteness phenomenon -- computationally
• Necessary and Sufficient Conditions for Undecidability of the Gödel Sentence and its Truth
• On formalization of model-theoretic proofs of Gödel's theorems
• On proofs of the incompleteness theorems based on Berry's paradox by Vopěnka, Chaitin, and Boolos
• On the scheme of induction for bounded arithmetic formulas
• The incompleteness theorems after 70 years
• The shortest definition of a number in Peano arithmetic
• Undecidable theories

Cited in

(6)

• On the foundations of mathematical economics
• Theorem Proving in Higher Order Logics
• Current research on Gödel's incompleteness theorems
• On the diagonal lemma of Gödel and Carnap
• Gödel's second incompleteness theorem: how it is derived and what it delivers
• Gödel-Rosser's incompleteness theorem, generalized and optimized for definable theories

This page was built for publication: On constructivity and the Rosser property: a closer look at some Gödelean proofs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1653263)