Godel’s Incompleteness Theorem in coq(4) 壁いくつ、今壁4つ

1. Godel’s Incompleteness Theorem
   https://madiot.fr/coq100/

Essential Incompleteness of Arithmetic Verified by Coq
Russell O’Connor
1 Institute for Computing and Information Science Faculty of Science Radboud University Nijmegen
2 The Group in Logic and the Methodology of Science University of California, Berkeley
[e-mail]

内容を確かめるため、ソースをダウンロードして、論文中のソースを表示。
http://r6.ca/Goedel/Goedel20050512.tar.gz

このほか、
coq-contribs/goedel
https://github.com/coq-contribs/goedel

順に作業して手順がわかれば追記予定。
助言、編集リクエスト、コメント歓迎。

0 License

nl
http://creativecommons.org/licenses/by/2.0/nl/
壁１
coqideで
goedel1.v
を実行すると

Unable locate library folprop

と出る。これは、folprop.vのpathがきれていないため。goedel1.vの先頭に、pathをたす。

$ cd Goedel20050512
$ cd Goedel
$ pwd
/Users/ogawakiyoshi/Downloads/Goedel20050512/Geedel

この内容をgoedel1.vの先頭に、
Add LoadPath の後に""で囲んで記述する。上記のpwdの内容だったら、下記。

goedel1.v

Add LoadPath "/Users/ogawakiyoshi/Downloads/Goedel20050512/Goedel".

の行をたす。

壁２　pathを足すだけじゃだめ。コンパイルしないと。

pathを足すだけではだめ。コンパイルしないといけない。上記、ダウンロードファイルにはコンパイル済みのファイルもあるが、版が違うというエラーがでている。
今の版ですべてコンパイルし直す。

folproof.vの８行目の
Require Import folProp.
がだめって。

folprop.vを開いて実行してみる。

folprop.v

Require Import ListExt.

で止まっている。

壁３　ListExt.vファイルがないのだろうか。

該当するファイルはフォルダにないのだろうか。
あった。コンパイルしてみる、
順に、ないものは開いてコンパイル

ようやくcoqのファイル以外のエラーだろうか。

壁４　エラー

上記エラー、まだとれていません。

2.1 Definition of Language

Record Language : Type := language
{Relations : Set;
Functions : Set;
arity : Relations + Functions -> nat}.

2.2 Definition of Term

Variable L : Language.
(* Invalid definition *)
Inductive Term0 : Set :=
| var0 : nat -> Term0
| apply0 : forall (f : Functions L) (l : List Term0),
(arity L (inr _ f))=(length l) -> Term0.

Inductive Vector (A : Set) : nat -> Set :=
| Vnil : Vector A 0
| Vcons : forall (a : A) (n : nat),
Vector A n -> Vector A (S n).

Variable L : Language.
Inductive Term1 : Set :=
| var1 : nat -> Term1
| apply1 : forall f : Functions L,
(Vector Term1 (arity L (inr _ f))) -> Term1.

Variable L : Language.
Inductive Term : Set :=
| var : nat -> Term
| apply : forall f : Functions L,
Terms (arity L (inr _ f)) -> Term
with Terms : nat -> Set :=
| Tnil : Terms 0
| Tcons : forall n : nat,
Term -> Terms n -> Terms (S n).

2.3 Definition of Formula

Inductive Formula : Set :=
| equal : Term -> Term -> Formula
| atomic : forall r : Relations L, Terms (arity L (inl _ r)) ->
Formula
| impH : Formula -> Formula -> Formula
| notH : Formula -> Formula
| forallH : nat -> Formula -> Formula.

2.4 Definition of Prf

Inductive Prf : Formulas -> Formula -> Set :=
| AXM : forall A : Formula, Prf (A :: nil) A
| MP : forall (Axm1 Axm2 : Formulas) (A B : Formula),
Prf Axm1 (impH A B) -> Prf Axm2 A ->
Prf (Axm1 ++ Axm2) B
| GEN : forall (Axm : Formulas) (A : Formula) (v : nat),
~ In v (freeVarListFormula L Axm) -> Prf Axm A ->
Prf Axm (forallH v A)
| IMP1 : forall A B : Formula, Prf nil (impH A (impH B A))
| IMP2 : forall A B C : Formula,
Prf nil (impH (impH A (impH B C))
(impH (impH A B) (impH A C)))
| CP : forall A B : Formula,
Prf nil (impH (impH (notH A) (notH B)) (impH B A))
| FA1 : forall (A : Formula) (v : nat) (t : Term),
Prf nil (impH (forallH v A) (substituteFormula L A v t))
| FA2 : forall (A : Formula) (v : nat),
~ In v (freeVarFormula L A) ->
Prf nil (impH A (forallH v A))
| FA3 : forall (A B : Formula) (v : nat),
Prf nil
(impH (forallH v (impH A B))
(impH (forallH v A) (forallH v B)))
| EQ1 : Prf nil (equal (var 0) (var 0))
| EQ2 : Prf nil (impH (equal (var 0) (var 1))
(equal (var 1) (var 0)))
| EQ3 : Prf nil
(impH (equal (var 0) (var 1))
(impH (equal (var 1) (var 2)) (equal (var 0) (var 2))))
| EQ4 : forall R : Relations L, Prf nil (AxmEq4 R)
| EQ5 : forall f : Functions L, Prf nil (AxmEq5 f).

2.5 Definition of SysPrf

Definition System := Ensemble Formula.
Definition mem := Ensembles.In.
Definition SysPrf (T : System) (f : Formula) :=
exists Axm : Formulas,
(exists prf : Prf Axm f,
(forall g : Formula, In g Axm -> mem _ T g)).

3 Coding

Fixpoint codeFormula (f : Formula) : nat :=
match f with
| fol.equal t1 t2 => cPair 0 (cPair (codeTerm t1) (codeTerm t2))
| fol.impH f1 f2 =>
cPair 1 (cPair (codeFormula f1) (codeFormula f2))
| fol.notH f1 => cPair 2 (codeFormula f1)
| fol.forallH n f1 => cPair 3 (cPair n (codeFormula f1))
| fol.atomic R ts => cPair (4+(codeR R)) (codeTerms _ ts)
end.

4 The Statement of Incompleteness

Theorem Incompleteness
: forall T : System,
Included Formula NN T ->
RepresentsInSelf T ->
DecidableSet Formula T ->
exists f : Formula,
Sentence f /\
(SysPrf T f \/ SysPrf T (notH f) -> Inconsistent LNN T).

Definition RepresentsInSelf (T : System) :=
exists rep : Formula, exists v : nat,
(forall x : nat, In x (freeVarFormula LNN rep) -> x = v) /\
(forall f : Formula,
mem Formula T f ->
SysPrf T (substituteFormula LNN rep v
(natToTerm (codeFormula f)))) /\
(forall f : Formula,
~ mem Formula T f ->
SysPrf T (notH (substituteFormula LNN rep v
(natToTerm (codeFormula f))))).

5 Primitive Recursive Functions

Inductive PrimRec : nat -> Set :=
| succFunc : PrimRec 1
| zeroFunc : PrimRec 0
| projFunc : forall n m : nat, m < n -> PrimRec n
| composeFunc :
forall (n m : nat) (g : PrimRecs n m) (h : PrimRec m),
PrimRec n
| primRecFunc :
forall (n : nat) (g : PrimRec n) (h : PrimRec (S (S n))),
PrimRec (S n)
with PrimRecs : nat -> nat -> Set :=
| PRnil : forall n : nat, PrimRecs n 0
| PRcons : forall n m : nat,
PrimRec n -> PrimRecs n m -> PrimRecs n (S m).

6.1 Incompleteness of PA

Theorem PAIncomplete :
exists f : Formula,
(forall v : nat, ~ In v (freeVarFormula LNT f)) /\
~ (SysPrf PA f \/ SysPrf PA (notH f)).

References

1. Stanley N. Burris. Logic for mathematics and computer science: Supplementary
   text. http://www.math.uwaterloo.ca/~snburris/htdocs/LOGIC/stext.
   html, 1997.
2. Olga Caprotti and Martijn Oostdijk. Formal and efficient primality proofs by use
   of computer algebra oracles. J. Symb. Comput., 32(1/2):55–70, 2001.
3. Jo¨elle Despeyroux and Andr´e Hirschowitz. Higher-order abstract syntax with induction
   in coq. In LPAR ’94: Proceedings of the 5th International Conference on
   Logic Programming and Automated Reasoning, pages 159–173, London, UK, 1994.
   Springer-Verlag.
4. K. G¨odel. Ueber Formal Unentscheidbare s¨atze der Principia Mathematica und
   Verwandter Systeme I. Monatshefte f¨ur Mathematik und Physik, 38:173–198, 1931.
   english translation: On Formally Undecidable Propositions of Principia Mathematica
   and Related Systems I, Oliver & Boyd, London, 1962.
5. John Harrison. Formalizing basic first order model theory. In Jim Grundy and Malcolm
   Newey, editors, Theorem Proving in Higher Order Logics: 11th International
   Conference, TPHOLs’98, volume 1497 of Lecture Notes in Computer Science, pages
   153–170, Canberra, Australia, 1998. Springer-Verlag
6. John Harrison. The HOL-Light manual, 2000.
7. Claude Marche. Fwd: Question about fixpoint. Coq club mailing
   list correspondence, http://pauillac.inria.fr/pipermail/coq-club/2005/001641.html, [cited 2005-02-07], February 2005.
8. Conor McBride. Dependently Typed Functional Programs and their Proofs.
   PhD thesis, University of Edinburgh, 1999. Available from http://www.lfcs.informatics.ed.ac.uk/reports/00/ECS-LFCS-00-419/.
9. Russell O’Connor. The G¨odel-Rosser 1st incompleteness theorem. http://r6.ca/Goedel20050512.tar.gz, March 2005.
10. Richard E. Hodel. An Introduction to Mathematical Logic. PWS Pub. Co., 1995.
11. N. Shankar. Metamathematics, Machines, and G¨odel’s Proof. Cambridge Tracts
    in Theoretical Computer Science. Cambridge University Press, Cambridge, UK,
13. J. R. Shoenfield. Mathematical Logic. Addison-Wesley, 1967.
14. Allen Stoughton. Substitution revisited. 59(3):317–325, August 1988.
15. The Coq Development Team. The Coq Proof Assistant Reference Manual – Version
    V8.0, April 2004. http://coq.inria.fr.

物理記事　上位100
https://qiita.com/kaizen_nagoya/items/66e90fe31fbe3facc6ff

数学関連記事１００
https://qiita.com/kaizen_nagoya/items/d8dadb49a6397e854c6d

言語・文学記事　１００
https://qiita.com/kaizen_nagoya/items/42d58d5ef7fb53c407d6

医工連携関連記事一覧
https://qiita.com/kaizen_nagoya/items/6ab51c12ba51bc260a82

通信記事１００
https://qiita.com/kaizen_nagoya/items/1d67de5e1cd207b05ef7

自動車　記事　１００
https://qiita.com/kaizen_nagoya/items/f7f0b9ab36569ad409c5

OSEK 記事で views 100,000を目指して　OSEK(8)
https://qiita.com/kaizen_nagoya/items/ff45ee55566eeff5f62e

無線網（Wi-Fi）空中線(antenna)(0) 記事一覧(209/300目標) https://qiita.com/kaizen_nagoya/items/5e5464ac2b24bd4cd001

なぜdockerで機械学習するか 書籍・ソース一覧作成中 (目標100)
https://qiita.com/kaizen_nagoya/items/ddd12477544bf5ba85e2

仮説（0）一覧（目標100現在40）
https://qiita.com/kaizen_nagoya/items/f000506fe1837b3590df

安全（0）安全工学シンポジウムに向けて: 21
https://qiita.com/kaizen_nagoya/items/c5d78f3def8195cb2409

日本語（０）一欄
https://qiita.com/kaizen_nagoya/items/7498dcfa3a9ba7fd1e68

英語(0) 一覧
https://qiita.com/kaizen_nagoya/items/680e3f5cbf9430486c7d

転職(0)一覧
https://qiita.com/kaizen_nagoya/items/f77520d378d33451d6fe

一覧の一覧( The directory of directories of mine.) Qiita(100)
https://qiita.com/kaizen_nagoya/items/7eb0e006543886138f39

プログラマが知っていると良い「公序良俗」
https://qiita.com/kaizen_nagoya/items/9fe7c0dfac2fbd77a945

LaTeX(0) 一覧　
https://qiita.com/kaizen_nagoya/items/e3f7dafacab58c499792

自動制御、制御工学一覧（０）
https://qiita.com/kaizen_nagoya/items/7767a4e19a6ae1479e6b

Rust(0) 一覧　
https://qiita.com/kaizen_nagoya/items/5e8bb080ba6ca0281927

小川清最終講義、小川清最終講義（再）計画, Ethernet(100) 英語(100) 安全(100)
https://qiita.com/kaizen_nagoya/items/e2df642e3951e35e6a53

＜この記事は個人の過去の経験に基づく個人の感想です。現在所属する組織、業務とは関係がありません。＞
This article is an individual impression based on the individual's experience. It has nothing to do with the organization or business to which I currently belong.

文書履歴

ver. 0.10 20180803 初稿
ver. 0.11 20180819 壁４つ

最後までおよみいただきありがとうございました。

いいね　💚、フォローをお願いします。

Thank you very much for reading to the last sentence.

Please press the like icon 💚　and follow me for your happy life.