Awesome
<!--- This file was generated from `meta.yml`, please do not edit manually. Follow the instructions on https://github.com/coq-community/templates to regenerate. --->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:
- Coq namespace:
Goedel - Related publication(s):
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.