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

DOI10.1016/J.APAL.2018.04.009zbMATH Open1434.03135DBLPjournals/apal/SalehiS18arXiv1612.02549OpenAlexW2787237760WikidataQ57533018 ScholiaQ57533018MaRDI QIDQ1653263FDOQ1653263

Authors: Saeed Salehi, Payam Seraji 

Publication date: 17 July 2018

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

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.

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

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

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)

Cites Work

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

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)