Essential Incompleteness of Arithmetic Verified by Coq

TL;DR

This paper provides a constructive proof of the Gödel-Rosser incompleteness theorem within Coq, formalizing classical logic, primitive recursive functions, and demonstrating the essential incompleteness of Peano arithmetic.

Contribution

It offers a formal, machine-verified proof of incompleteness using Coq, including formalizations of logic, primitive recursive functions, and consistency of Peano arithmetic.

Findings

Peano arithmetic is consistent in Coq's type theory.

All primitive recursive functions are representable in a weak axiom system.

The weak axiom system is essentially incomplete.

Abstract

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.