package coq-goedel

  1. Overview
  2. No Docs
Coq proof of the Gödel-Rosser 1st incompleteness theorem

Install

Dune Dependency

github.com Edit opam file Versions (8)

Authors

  1. R
    Russell O'Connor

Maintainers

  1. P
    palmskog@gmail.com

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-10

Published: 10 Aug 2021

Dependencies (3)

  1. coq-pocklington >= "8.12"
  2. coq-hydra-battles >= "0.4" & <= "0.9"
  3. coq >= "8.11" & < "8.17~"

Dev Dependencies

None

Used by

None

Conflicts

None