package coq-goedel

  1. Overview
  2. Homepage
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.

Dependencies (2)

  1. coq-pocklington >= "8.12" & < "8.13~"
  2. coq >= "8.7" & < "8.14~"

Dev Dependencies

None

Used by

None

Conflicts

None

Rocq

Interactive Theorem Prover