-
Gödel-Rosser第一不完全性定理在Coq中由维护者@Casteran实现
资源介绍
戈德尔
Gödel-Rosser一阶不完备定理的Coq证明，即任何扩展NN（即无归纳的PA）的完备的一阶理论都是不一致的。
元
作者： 拉塞尔·奥康纳（初始）
Coq社区维护者： 皮埃尔·卡斯特兰（ ）
执照：
兼容的Coq版本：8.11或更高版本
其他依赖项：
Coq名称空间： Goedel
相关出版物： doi：
建造和安装说明
安装最新版本的Goedel的最简单方法是通过 ：
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-goedel
要改为手动构建和安装，请执行以下操作：
git clone https://github.com/coq-community/goedel.git
cd goedel
make # or make -j <number