Essential Incompleteness of Arithmetic Verified by Coq

Simple item page
dc.creatorO'Connor, Russell
dc.date2005-05-12
dc.date2006-05-11
dc.date.accessioned2026-07-07T09:39:27Z
dc.date.available2026-07-07T09:39:27Z
dc.descriptionA constructive proof of the Goedel-Rosser incompleteness theorem has been completed using the Coq proof assistant. Some theory of classical first-order logic over an arbitrary language is formalized. A development of primitive recursive functions is given, and all primitive recursive functions are proved to be representable in a weak axiom system. Formulas and proofs are encoded as natural numbers, and functions operating on these codes are proved to be primitive recursive. The weak axiom system is proved to be essentially incomplete. In particular, Peano arithmetic is proved to be consistent in Coq's type theory and therefore is incomplete.
dc.descriptionThis paper is part of the proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2005). For the associated Coq source files see the TeX sources, or see <http://r6.ca/Goedel20050512.tar.gz>
dc.identifierhttps://arxiv.org/abs/cs/0505034
dc.identifierhttp://arxiv.org/abs/cs/0505034
dc.identifierRussell O'Connor, Essential Incompleteness of Arithmetic Verified by Coq, Lecture Notes in Computer Science, Volume 3603, Aug 2005, Pages 245 - 260
dc.identifierdoi:10.1007/11541868_16
dc.identifier.urihttp://salesiana.dossiersoluciones.com/handle/123456789/161177
dc.subjectLogic in Computer Science
dc.titleEssential Incompleteness of Arithmetic Verified by Coq
dc.typetext

Files

Collections

arXiv