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
r.oconnor@cs.ru.nl

内容を確かめるため、ソースをダウンロードして、論文中のソースを表示。
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
を実行すると
👁 goe1.png

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の内容だったら、下記。

AddLoadPath"/Users/ogawakiyoshi/Downloads/Goedel20050512/Goedel".

の行をたす。

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

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

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

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

RequireImportListExt.

で止まっている。

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

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

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

壁４　エラー

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

2.1 Definition of Language

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

2.2 Definition of Term

VariableL:Language.(* Invalid definition *)InductiveTerm0:Set:=|var0:nat->Term0|apply0:forall(f:FunctionsL)(l:ListTerm0),(arityL(inr_f))=(lengthl)->Term0.

InductiveVector(A:Set):nat->Set:=|Vnil:VectorA0|Vcons:forall(a:A)(n:nat),VectorAn->VectorA(Sn).

VariableL:Language.InductiveTerm1:Set:=|var1:nat->Term1|apply1:forallf:FunctionsL,(VectorTerm1(arityL(inr_f)))->Term1.

VariableL:Language.InductiveTerm:Set:=|var:nat->Term|apply:forallf:FunctionsL,Terms(arityL(inr_f))->TermwithTerms:nat->Set:=|Tnil:Terms0|Tcons:foralln:nat,Term->Termsn->Terms(Sn).

2.3 Definition of Formula

InductiveFormula:Set:=|equal:Term->Term->Formula|atomic:forallr:RelationsL,Terms(arityL(inl_r))->Formula|impH:Formula->Formula->Formula|notH:Formula->Formula|forallH:nat->Formula->Formula.

2.4 Definition of Prf

InductivePrf:Formulas->Formula->Set:=|AXM:forallA:Formula,Prf(A::nil)A|MP:forall(Axm1Axm2:Formulas)(AB:Formula),PrfAxm1(impHAB)->PrfAxm2A->Prf(Axm1++Axm2)B|GEN:forall(Axm:Formulas)(A:Formula)(v:nat),~Inv(freeVarListFormulaLAxm)->PrfAxmA->PrfAxm(forallHvA)|IMP1:forallAB:Formula,Prfnil(impHA(impHBA))|IMP2:forallABC:Formula,Prfnil(impH(impHA(impHBC))(impH(impHAB)(impHAC)))|CP:forallAB:Formula,Prfnil(impH(impH(notHA)(notHB))(impHBA))|FA1:forall(A:Formula)(v:nat)(t:Term),Prfnil(impH(forallHvA)(substituteFormulaLAvt))|FA2:forall(A:Formula)(v:nat),~Inv(freeVarFormulaLA)->Prfnil(impHA(forallHvA))|FA3:forall(AB:Formula)(v:nat),Prfnil(impH(forallHv(impHAB))(impH(forallHvA)(forallHvB)))|EQ1:Prfnil(equal(var0)(var0))|EQ2:Prfnil(impH(equal(var0)(var1))(equal(var1)(var0)))|EQ3:Prfnil(impH(equal(var0)(var1))(impH(equal(var1)(var2))(equal(var0)(var2))))|EQ4:forallR:RelationsL,Prfnil(AxmEq4R)|EQ5:forallf:FunctionsL,Prfnil(AxmEq5f).

2.5 Definition of SysPrf

DefinitionSystem:=EnsembleFormula.Definitionmem:=Ensembles.In.DefinitionSysPrf(T:System)(f:Formula):=existsAxm:Formulas,(existsprf:PrfAxmf,(forallg:Formula,IngAxm->mem_Tg)).

3 Coding

FixpointcodeFormula(f:Formula):nat:=matchfwith|fol.equalt1t2=>cPair0(cPair(codeTermt1)(codeTermt2))|fol.impHf1f2=>cPair1(cPair(codeFormulaf1)(codeFormulaf2))|fol.notHf1=>cPair2(codeFormulaf1)|fol.forallHnf1=>cPair3(cPairn(codeFormulaf1))|fol.atomicRts=>cPair(4+(codeRR))(codeTerms_ts)end.

4 The Statement of Incompleteness

TheoremIncompleteness:forallT:System,IncludedFormulaNNT->RepresentsInSelfT->DecidableSetFormulaT->existsf:Formula,Sentencef/\(SysPrfTf\/SysPrfT(notHf)->InconsistentLNNT).

DefinitionRepresentsInSelf(T:System):=existsrep:Formula,existsv:nat,(forallx:nat,Inx(freeVarFormulaLNNrep)->x=v)/\(forallf:Formula,memFormulaTf->SysPrfT(substituteFormulaLNNrepv(natToTerm(codeFormulaf))))/\(forallf:Formula,~memFormulaTf->SysPrfT(notH(substituteFormulaLNNrepv(natToTerm(codeFormulaf))))).

5 Primitive Recursive Functions

InductivePrimRec:nat->Set:=|succFunc:PrimRec1|zeroFunc:PrimRec0|projFunc:forallnm:nat,m<n->PrimRecn|composeFunc:forall(nm:nat)(g:PrimRecsnm)(h:PrimRecm),PrimRecn|primRecFunc:forall(n:nat)(g:PrimRecn)(h:PrimRec(S(Sn))),PrimRec(Sn)withPrimRecs:nat->nat->Set:=|PRnil:foralln:nat,PrimRecsn0|PRcons:forallnm:nat,PrimRecn->PrimRecsnm->PrimRecsn(Sm).

6.1 Incompleteness of PA

TheoremPAIncomplete:existsf:Formula,(forallv:nat,~Inv(freeVarFormulaLNTf))/\~(SysPrfPAf\/SysPrfPA(notHf)).

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,
12. J. R. Shoenfield. Mathematical Logic. Addison-Wesley, 1967.
13. Allen Stoughton. Substitution revisited. 59(3):317–325, August 1988.
14. 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.