Goedel

A proof in Coq of the Gödel-Rosser 1st incompleteness theorem, which says that any first order theory extending NN (which is PA without induction) that is complete is inconsistent.

Meta

• Author(s):
  • Russell O'Connor (initial)
• Coq-community maintainer(s):
  • Pierre Castéran (@Casteran)
• License: MIT License
• Compatible Coq versions: 8.13 or later
• Additional dependencies:
  • Hydra Battles
  • CoqPrime
• Coq namespace: Goedel
• Related publication(s):
  • Essential Incompleteness of Arithmetic Verified by Coq doi:10.1007/11541868_16

Building and installation instructions

The easiest way to install the latest released version of Goedel is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-goedel

To instead build and install manually, do:

git clone https://github.com/coq-community/goedel.git
cd goedel
make   # or make -j <number-of-cores-on-your-machine> 
make install

Documentation

More information about the project can be found at this website.