Essential Incompleteness of Arithmetic Verified by Coq

Details Essential Incompleteness of Arithmetic Verified by Coq Essential Incompleteness of Arithmetic Verified by Coq

2005-05-12

arxiv.org/abs/cs/0505034v2

Russell O'Connor, Essential Incompleteness of Arithmetic Verified by Coq, Lecture Notes in Computer Science, Volume 3603, Aug

Computer Science

Logic in Computer Science

This paper is part of the proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2

Scientific paper

10.1007/11541868_16

A 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.

Affiliated with

Also associated with

No associations

Rating

Essential Incompleteness of Arithmetic Verified by Coq does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Essential Incompleteness of Arithmetic Verified by Coq, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Essential Incompleteness of Arithmetic Verified by Coq will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-162841