package coq-goedel
Coq proof of the Gödel-Rosser 1st incompleteness theorem
Install
Dune Dependency
Authors
Maintainers
Sources
v8.12.0.tar.gz
sha512=778b7eacbb13574428cd6f1349d724c27b2859159a32316b19f3460d5a5495216fd24fe1ce2b6159b2d6322396cae6c27d8f3447e43bde1877e4cd2e1f523282
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-01-01Published: 02 Jan 2021
Dependencies (2)
-
coq-pocklington
>= "8.12" & < "8.13~" -
coq
>= "8.7" & < "8.14~"
Dev Dependencies
None
Used by
None
Conflicts
None
On This Page