package coq-goedel
Coq proof of the Gödel-Rosser 1st incompleteness theorem
Install
Dune Dependency
Authors
Maintainers
Sources
v8.13.0.tar.gz
sha512=c3d44d64f3231f893f5bd806075adf3509b35d506bad6a24bff6ff75f4ebc0dbe97bbbc2eab513d881eccb4c74f59cdcd9b5928f5d45f0b3158c965eaf6aaa30
Description
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.
Tags
category:Mathematics/Logic/Foundations keyword:Goedel keyword:Rosser keyword:incompleteness keyword:logic keyword:Hilbert logpath:Goedel date:2021-08-10Published: 10 Aug 2021
Dependencies (3)
-
coq-pocklington
>= "8.12" -
coq-hydra-battles
>= "0.4" & <= "0.9" -
coq
>= "8.11" & < "8.17~"
Dev Dependencies
None
Used by
None
Conflicts
None
On This Page