Abstract
A constructive proof of the Gödel-Rosser incompleteness theorem [9] has been completed using 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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Burris, S.N.: Logic for mathematics and computer science: Supplementary text (1997), http://www.math.uwaterloo.ca/~snburris/htdocs/LOGIC/stext.html
Caprotti, O., Oostdijk, M.: Formal and efficient primality proofs by use of computer algebra oracles. J. Symb. Comput. 32(1/2), 55–70 (2001)
Despeyroux, J., Hirschowitz, A.: Higher-order abstract syntax with induction in coq. In: Pfenning, F. (ed.) LPAR 1994. LNCS, vol. 822, pp. 159–173. Springer, Heidelberg (1994)
Gödel, K.: Ueber Formal Unentscheidbare sätze der Principia Mathematica und Verwandter Systeme I. Monatshefte für Mathematik und Physik 38, 173–198 (1931); english translation: On Formally Undecidable Propositions of Principia Mathematica and Related Systems I. Oliver & Boyd, London (1962)
Harrison, J.: Formalizing basic first order model theory. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998, vol. 1479, pp. 153–170. Springer, Heidelberg (1998)
Harrison, J.: The HOL-Light manual (2000)
Marche, C.: Fwd: Question about fixpoint. Coq club mailing list correspondence [cited 2005-02-07] (February 2005), http://pauillac.inria.fr/pipermail/coq-club/2005/001641.html
McBride, C.: Dependently Typed Functional Programs and their Proofs. PhD thesis, University of Edinburgh (1999), Available from http://www.lfcs.informatics.ed.ac.uk/reports/00/ECS-LFCS-00-419/
O’Connor, R.: The Gödel-Rosser 1st incompleteness theorem (March 2005), http://r6.ca/Goedel20050512.tar.gz
Hodel, R.E.: An Introduction to Mathematical Logic. PWS Pub. Co. (1995)
Shankar, N.: Metamathematics, Machines, and Gödel’s Proof. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (1994)
Shoenfield, J.R.: Mathematical Logic. Addison-Wesley, Reading (1967)
Stoughton, A.: Substitution revisited 59(3), 317–325 (August 1988)
The Coq Development Team. The Coq Proof Assistant Reference Manual – Version V8.0 (April 2004), http://coq.inria.fr
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
O’Connor, R. (2005). Essential Incompleteness of Arithmetic Verified by Coq. In: Hurd, J., Melham, T. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2005. Lecture Notes in Computer Science, vol 3603. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11541868_16
Download citation
DOI: https://doi.org/10.1007/11541868_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28372-0
Online ISBN: 978-3-540-31820-0
eBook Packages: Computer ScienceComputer Science (R0)