ゲーデルの不完全性定理








ゲーデルの不完全性定理（ゲーデルのふかんぜんせいていり、英: Gödel's incompleteness theorems、独: Gödelscher Unvollständigkeitssatz）又は単に不完全性定理とは、数学基礎論における重要な定理で、クルト・ゲーデルが1930年に証明した[1]ものである。


「完全性」および「ゲーデルの完全性定理」も参照



目次






  • 1 概要


  • 2 詳細


    • 2.1 ゲーデル文の構成


    • 2.2 第一不完全性定理の証明


      • 2.2.1 否定命題の証明不能性


      • 2.2.2 肯定命題の証明不能性




    • 2.3 第二不完全性定理の証明




  • 3 決定不能命題の例


  • 4 ゲーデルの定理に関する制限


  • 5 不完全性定理の成立しない体系


  • 6 その影響・応用


  • 7 ゲーデル以後の展開


  • 8 不完全性定理の代数化


  • 9 誤解（哲学等による誤解・誤用）


    • 9.1 誤用例


      • 9.1.1 一般社会・インターネット


      • 9.1.2 数学者以外の学者


      • 9.1.3 宗教


      • 9.1.4 神学


      • 9.1.5 誤用の分類






  • 10 脚注


    • 10.1 注釈


    • 10.2 出典




  • 11 関連文献


    • 11.1 原論文


    • 11.2 原論文の日本語訳


    • 11.3 原論文の英訳


    • 11.4 教科書


    • 11.5 講義ノート


    • 11.6 誤用と誤解について




  • 12 関連項目


  • 13 外部リンク





概要



第1不完全性定理 

自然数論を含む帰納的公理化可能な理論が、ω無矛盾であれば、証明も反証もできない命題が存在する。

第2不完全性定理 

自然数論を含む帰納的公理化可能な理論が、無矛盾であれば、自身の無矛盾性を証明できない[2]。


ゲーデルの定理でいう証明不能命題Gは、「Gは証明できない」という命題と同値である。Gはゲーデル文と呼ばれる。


Gが証明可能であれば、Σ1完全性により命題「Gは証明できる」もまた証明可能である。一方Gは命題「Gは証明できない」と同値であることが証明可能であるので、両者から矛盾が導かれる。つまり


「Gは証明できる」ならば「矛盾が証明できる」…(A)


したがって、対偶を取れば


「矛盾が証明できない」ならば「Gは証明できない」…(B)


となる。
また、￢Gが証明可能であれば、Gの性質から命題


「Gは証明できる」


も証明可能である。この際、もしGそのものが証明不能だとすると、ω矛盾ということになる。ω無矛盾であればGも証明可能である。しかしGが証明可能であれば


「Gは証明できない」


も証明可能であるので、やはり両者から矛盾が導かれる。したがってω無矛盾であれば￢Gも証明できないのである。よってω無矛盾であれば、Gも￢Gも証明できない（第一不完全性定理）。


なお、証明可能性の代わりに真理性を用いるならば、パラドックスが導かれる。このことから、自然数論における真理性は自然数論の中では表現できないことが示される（タルスキの定理）。


ゲーデル文を構成するためには自然数論の式を自然数に変換するゲーデル数および自己言及で用いられる対角化の技法（を形式化したもの）が必要である。後者は対角化補題と呼ばれる。



自然数を変数とする述語


「xは…である」


の対角化は、左記の述語のxに


「xは…である」


のゲーデル数を代入した命題である。その意味は


「「xは…である」は…である」


となる。
ゲーデル文Gは


「「xで表される述語の対角化は証明できない」


で表される述語の対角化は証明できない」と表される。


「xで表される述語の対角化は証明できない」


の対角化は、G自身と同値になる。
さて、自然数論の無矛盾性とは、


「自然数論において矛盾を証明できない」


ということである。そして、自然数論による自然数論の無矛盾性証明とは、「」内が、自然数論で証明できるということである。


「自然数論で矛盾が証明できない」


と自然数論で証明できれば、第一不完全定理での議論中の(B)より


「Gは証明できない」


と証明できる。
しかし、


「Gは証明できない」


とはGと同値であるから、Gも証明されることとなり、そこから第一不完全定理での議論中の(A)により、矛盾が証明される。


したがって自然数論が無矛盾、すなわち自然数論で矛盾が証明されないならば、そのこと自体も自然数論では証明できない（第二不完全性定理）。



詳細



ゲーデルの定理は


「自然数論を含む帰納的公理化可能な無矛盾理論」


に対して示されているが、ここでは簡単の為、自然数論のみを扱う。一般の場合も同様。



ゲーデル文の構成


概要でも説明したように、ゲーデル数というテクニックを使って間接的に自己言及を可能とし、ゲーデル文を構成する。


コンピュータでは全てのデータを一意な数値で表しており、特に文字列や論理式そして論理式の列も数値で表す。このように、論理式を数値で表す行為を論理式のゲーデル数化といい、命題P{displaystyle P}Pに対応する数値をP{displaystyle P}Pのゲーデル数という[注釈 1]。


ゲーデル数化により、論理式に関する様々な性質を論理式として表すことができる。たとえば、




  • Axiom(x){displaystyle Axiom(x)}{displaystyle Axiom(x)}： x{displaystyle x}xは公理のゲーデル数である。


  • MP(x,y,z){displaystyle MP(x,y,z)}{displaystyle MP(x,y,z)}： x{displaystyle x}xをゲーデル数に持つ論理式とy{displaystyle y}yをゲーデル数に持つ論理式から三段論法によりz{displaystyle z}zをゲーデル数に持つ論理式が導ける。



といった論理式を作ることができる。ここで、Axiom{displaystyle Axiom}{displaystyle Axiom}やMP{displaystyle MP}{displaystyle MP}の引数が論理式自身ではなく自然数であることが重要である。前述のように自然数論は


「命題に言及する命題」


を取り扱うことはできないが、


「命題のゲーデル数に言及する命題」


なら取り扱うことができるのである。


Axiom(x){displaystyle Axiom(x)}{displaystyle Axiom(x)}やMP(x,y,z){displaystyle MP(x,y,z)}{displaystyle MP(x,y,z)}などを組み合わせれば、



  • Proof(y,z){displaystyle Proof(y,z)}{displaystyle Proof(y,z)} : z{displaystyle z}zをゲーデル数に持つ論理式をP{displaystyle P}Pとするとき、y{displaystyle y}yをゲーデル数に持つ論理式の列が論理式P{displaystyle P}Pの証明になっている。

という論理式も作ることができる。


さらにProof{displaystyle Proof}{displaystyle Proof}を「∃{displaystyle exists }exists 」と組み合わせることで、




  • Provable(z){displaystyle Provable(z)}{displaystyle Provable(z)} : 「∃y:Proof(y,z){displaystyle exists y:Proof(y,z)}{displaystyle exists y:Proof(y,z)}」である。すなわち、z{displaystyle z}zをゲーデル数に持つ論理式をP{displaystyle P}Pとするとき論理式Pは証明可能である。


  • ProvableARG(z,x){displaystyle ProvableARG(z,x)}{displaystyle ProvableARG(z,x)} : 「∃y:Proof(y,z,x){displaystyle exists y:Proof(y,z,x)}{displaystyle exists y:Proof(y,z,x)}」である。すなわち、z{displaystyle z}zをゲーデル数に持つ論理式をQ{displaystyle Q}Qとするとき、Q{displaystyle Q}Q中の変数に自然数x{displaystyle x}xを代入した論理式Q(x){displaystyle Q(x)}Q(x)は証明可能である。


という論理式も作ることができる（上ではP{displaystyle P}Pは引数を持たず、Q{displaystyle Q}Qの引数は1つである）。


論理式¬ProvableARG(x,x){displaystyle lnot ProvableARG(x,x)}{displaystyle lnot ProvableARG(x,x)}のゲーデル数をm{displaystyle m}mとすると、x{displaystyle x}xにm{displaystyle m}mを代入した論理式¬ProvableARG(m,m){displaystyle lnot ProvableARG(m,m)}{displaystyle lnot ProvableARG(m,m)}がゲーデル文となる（対角化）。



第一不完全性定理の証明


ゲーデル文¬ProvableARG(m,m){displaystyle lnot ProvableARG(m,m)}{displaystyle lnot ProvableARG(m,m)}のゲーデル数をnpmm{displaystyle npmm}{displaystyle npmm}とする。



否定命題の証明不能性


否定命題¬ProvableARG(m,m){displaystyle lnot ProvableARG(m,m)}{displaystyle lnot ProvableARG(m,m)}が証明可能とすると、Provable(npmm){displaystyle Provable(npmm)}{displaystyle Provable(npmm)}は真である。このときΣ1{displaystyle Sigma _{1}}Sigma _{1}完全性よりProvable(npmm){displaystyle Provable(npmm)}{displaystyle Provable(npmm)}は証明可能である。



一方¬ProvableARG(m,m){displaystyle lnot ProvableARG(m,m)}{displaystyle lnot ProvableARG(m,m)}は


「m{displaystyle m}mをゲーデル数に持つ論理式にm{displaystyle m}mを代入したものは証明不能」


という意味である。
m{displaystyle m}mをゲーデル数に持つ論理式にm{displaystyle m}mを代入したものはnpmm{displaystyle npmm}{displaystyle npmm}であるから


¬ProvableARG(m,m)⇔¬Provable(npmm){displaystyle lnot ProvableARG(m,m)Leftrightarrow lnot Provable(npmm)}{displaystyle lnot ProvableARG(m,m)Leftrightarrow lnot Provable(npmm)}


が証明可能である。したがって、


¬Provable(npmm){displaystyle lnot Provable(npmm)}{displaystyle lnot Provable(npmm)}


は証明可能である。


したがってProvable(npmm){displaystyle Provable(npmm)}{displaystyle Provable(npmm)}および¬Provable(npmm){displaystyle lnot Provable(npmm)}{displaystyle lnot Provable(npmm)}が証明され、これは矛盾である[注釈 2]が、これは自然数論が無矛盾であるという仮定に反する。



肯定命題の証明不能性



肯定命題ProvableARG(m,m){displaystyle ProvableARG(m,m)}{displaystyle ProvableARG(m,m)}が証明可能だとすると、


ProvableARG(m,m)⇔Provable(npmm){displaystyle ProvableARG(m,m)Leftrightarrow Provable(npmm)}{displaystyle ProvableARG(m,m)Leftrightarrow Provable(npmm)}


により


Provable(npmm){displaystyle Provable(npmm)}{displaystyle Provable(npmm)}


が証明可能である。


このときω無矛盾性を前提すると、npmm{displaystyle npmm}{displaystyle npmm}をゲーデル数とする論理式¬ProvableARG(m,m){displaystyle lnot ProvableARG(m,m)}{displaystyle lnot ProvableARG(m,m)}が証明可能である。[注釈 3]


それ故、矛盾が証明されるが、これは自然数論が無矛盾であるという仮定に反する。



第二不完全性定理の証明


矛盾を「⊥{displaystyle bot }bot」で表し、「⊥{displaystyle bot }bot」のゲーデル数をb{displaystyle b}bとする。すると、「自然数論の体系内で自然数論の無矛盾性を証明できる」という言説を


自然数論の体系内で「¬Provable(b){displaystyle lnot Provable(b)}{displaystyle lnot Provable(b)}」を証明できる


の意味に解することができる。



まず


¬Provable(b){displaystyle lnot Provable(b)}{displaystyle lnot Provable(b)}


が自然数論の体系内で証明可能であると仮定する。
第一不完全性定理のところで示したように、¬ProvableARG(m,m){displaystyle lnot ProvableARG(m,m)}{displaystyle lnot ProvableARG(m,m)}が証明できれば矛盾が証明できる。この議論を自然数論の体系内で行うことで、


Provable(npmm)⇒Provable(b){displaystyle Provable(npmm)Rightarrow Provable(b)}{displaystyle Provable(npmm)Rightarrow Provable(b)}


が自然数論の体系内で証明可能なことがわかる。故に対偶を取ることで


¬Provable(b)⇒¬Provable(npmm){displaystyle lnot Provable(b)Rightarrow lnot Provable(npmm)}{displaystyle lnot Provable(b)Rightarrow lnot Provable(npmm)}


が自然数論の体系内で証明可能なことがわかる。したがって、仮定および¬ProvableARG(m,m)⇔¬Provable(npmm){displaystyle lnot ProvableARG(m,m)Leftrightarrow lnot Provable(npmm)}{displaystyle lnot ProvableARG(m,m)Leftrightarrow lnot Provable(npmm)}から


¬ProvableARG(m,m){displaystyle lnot ProvableARG(m,m)}{displaystyle lnot ProvableARG(m,m)}


が自然数論の体系内で証明可能なことがわかる。第一不完全性定理の所で示したように、¬ProvableARG(m,m){displaystyle lnot ProvableARG(m,m)}{displaystyle lnot ProvableARG(m,m)}が証明可能だと、矛盾が証明される。したがって矛盾が証明されないならば、¬Provable(b){displaystyle lnot Provable(b)}{displaystyle lnot Provable(b)}は証明されない。



決定不能命題の例


数学と計算機科学（コンピュータ科学）において、「決定不能」という言葉には二つの異なった意味がある。一つ目は証明論の文脈でゲーデルの定理に関連して使われる意味であり、特定の形式的体系の下で或る命題を証明も否定の証明もできないことを言う。二つ目は（本項では詳述しないが）計算可能性理論に関連した用法であり、命題ではなく決定問題に適用される。決定問題とは入力に対して答が真か偽のいずれかになるような問題である。ある問題を全ての入力に対して正しく解答するような計算可能関数が存在しないとき、そうした問題は決定不能であると言う。


このように決定不能という言葉には二つの意味があるので、代わりに独立（英語版）という用語をもって「証明も否定の証明もできない」という意味にあてる場合がある。ところが「独立」という用語にしても依然曖昧な部分がある。単に「証明できない」という意味を表し、「否定の証明もできない」かどうかについてはあえて含意していない場合があるからである。


以下、本節では一つ目の意味で「決定不能」と書く。特定の形式的体系の下である命題が決定不能であることは、その命題の真理値がwell-definedであるかどうかや他の手段で決定可能かどうかについては明らかにしない。決定不能ということが意味するのは、あくまで使用されている特定の形式的体系の下ではその命題の真偽をいずれも証明できないということにすぎない。真理値を決して知ることができないか、または真理値の定義自体が無効となるような、いわゆる「絶対的決定不能」命題が存在するのかどうかは数理哲学における論争の的となっている。


ゲーデルとポール・コーエンの仕事を合わせて、決定不能命題の確かな実例が得られた。連続体仮説はZFC（集合論における標準的な公理系）の下では証明も否定の証明もできない。また、選択公理もZF（ZFCに含まれる公理から選択公理を除いたもの）では証明も否定の証明もできない。これらの結果は不完全性定理を必要としない。1940年、ゲーデルはこれらの命題が何れも ZF または ZFC 集合論では否定を証明できないことを証明した。1960年代、コーエンはこれらがいずれも ZF から証明できず、また連続体仮説が ZFC から証明できないことを証明した。


マチャセビッチによるヒルベルトの第10問題によって決定不能な命題の例が得られる。そのような例はディオファントス方程式の外側に存在量化子を幾つか並べた形として得られる。すなわち不完全性定理の前提条件を満たす形式的体系において、解の存在が証明も反証もできないようなディオファントス方程式が存在する。


1973年、群論におけるホワイトヘッドの問題（英語版）が標準的な集合論では決定不能であることが示された。


1977年、パリスとハーリントンは、ラムゼーの定理の一種であるパリス・ハーリントンの定理（英語版）が、一階算術の公理体系であるペアノ算術の下では決定不能だが、より大きな二階算術の体系では真であることを証明できることを証明した。カービーとパリスは後にグッドスタインの定理（自然数の数列に関する命題であり、パリス・ハーリントンの原理よりもいくらか易しい）がペアノ算術では決定不能であることを示した。


計算機科学で応用される Kruskal の木定理（英語版）はペアノ算術では決定不能だが集合論では証明できる。実際、Kruskalの木定理（またはその有限版）は、可述主義（英語版）[注釈 4]と呼ばれる数学的哲学に基づいて構築されたもっと強い体系の下でも決定不能である。これに関連し、更に一般的な graph minors 定理（英語版）（2003年）は計算複雑性理論に影響する。


グレゴリー・チャイティンはアルゴリズム情報理論における決定不能命題を発見し、その状況下で新たな不完全性定理を得た。チャイティンの定理によると、十分な算術を表現可能ないかなる理論においても、どのような数であっても c{displaystyle c}c よりも大きなコルモゴロフ複雑性を有することがその理論上では証明できないような、上限 c{displaystyle c}c が存在する。ゲーデルの定理が嘘つきのパラドックスと関係しているのに対し、チャイティンの結果はベリーのパラドックスに関係している。



ゲーデルの定理に関する制限


第1不完全性定理はロビンソン算術を含んでいれば十分である。またω無矛盾性の仮定は単なる無矛盾性の仮定に弱められる（後述）。第2不完全性定理はロビンソン算術にΣ1論理式に対する数学的帰納法の公理図式を追加した体系（IΣ1{displaystyle ISigma _{1}}{displaystyle ISigma _{1}}）を含んでいれば十分である。ペアノ算術はこれを含むから、ペアノ算術を含む理論は第2不完全性定理の適用範囲である。


ゲーデルの定理は無矛盾な理論についてのみ適用できる。一階論理では、ex falso quodlibet (en) により、矛盾した理論 T{displaystyle T}T はその言語上の如何なる式であれ証明できてしまい、その中には「T{displaystyle T}T は無矛盾である」と主張する式も含まれる。


ゲーデルの定理が成り立つのは、あくまで定理が必要としている仮定を満足するような形式的体系に限られる。全ての公理系がこれらの仮定を満たす訳ではなく、中には自然数論の標準モデルを部分構造として持つようなモデルを持っていてもなお仮定を満たさないような公理系もある。例えば、ユークリッド幾何学の一階公理化理論、実閉体の理論、乗算が全域で可能なことを証明できないような算術理論、これらは何れもゲーデルの定理に必要な仮定を満たさない。要点は、これらの公理系では自然数の集合を定義することや自然数の基本的な性質を証明することができないことにある。三つ目の例に関して Dan E. Willard は第二不完全性定理に必要な仮定を満たさないような様々な弱い算術理論を調べた（例えば Willard 2001）。


ゲーデルの定理は実効的に生成された（即ち帰納的可算な）理論についてのみ適用できる。自然数に関する真である文を全て公理とするような理論を考えれば、この理論は無矛盾かつ完全であり、かつペアノ算術を含んでいる。これはゲーデルの定理と矛盾しない。何故ならこの理論は帰納的可算ではないからである[注釈 5]。


第二不完全性定理が示すのは、ある公理系の無矛盾性はその公理系自身では証明できないということであって、他の無矛盾な公理系からも証明できないとは言っていない。例えば、ペアノ算術の無矛盾性はZFCから証明できるし、算術の理論にε0までの超限帰納法を加えて得られたゲンツェンによる無矛盾性の証明（英語版）もある。



不完全性定理の成立しない体系


不完全性定理は「『自然数論を含む帰納的公理化可能な理論が、無矛盾（ω無矛盾）であれば』～」という形の定理である。したがって、自然数論を含まない公理系や、帰納的公理化可能でない理論が完全であっても、不完全性定理とは矛盾しない。


真の算術やペアノ算術の無矛盾完全拡大などは無矛盾かつ完全であるが、帰納的公理化可能でない。とくに真の算術は算術的に定義不能である。この結果はタルスキの真理定義不可能性として知られる。


プレスバーガー算術は帰納的公理化可能、無矛盾かつ完全である。プレスバーガー算術は加法しか含まない公理系であり、ゲーデル数によるコード化のテクニックを扱えない。そのため、不完全性定理は適用できない。また、実閉体の理論やユークリッド幾何学も完全であり、（直観に反して）算術を含まないため、不完全性定理は適用できない。したがって実閉体の理論は決定可能である。もっと精密にいうと実閉体の理論では量化記号消去が可能である。この事実は数式処理系の実装などに応用されている。


なお、群や環の公理などは、「自然数論を含まない帰納的公理化可能かつ無矛盾な公理系」であり、不完全性定理は適用できないが、不完全である。例えば、可換群と非可換群がともに存在することから、健全性定理より、群の公理からは積の可換性は証明も反証もできない。



その影響・応用


詳細は「数学基礎論」および「ゲーデル」を参照

ゲーデルの定理は、数学基礎論のうち、数学の無矛盾性の証明を目標としていたヒルベルト・プログラムには、深刻な影響を与えた。ヒルベルトは公理の適切な設定によって完全かつ無矛盾な体系を達成できると楽観視していたが、第二不完全性定理により、ヒルベルトの計画は頓挫した。


上記のような述語論理式を自然数論の体系内に構成し、証明を形式的に進めるために、ゲーデルはゲーデル数化という操作を導入した。自由変数、論理式、証明図などを自然数でコード化し証明可能、反証可能などの概念を数論的関数として表現する。このように、論理式や証明を数学的に表現して数学内に埋め込む上記の手法は、数学そのものを分析する「メタ数学」を、分析すべきの数学の中に写像する技法の先駆けであり、その後数学基礎論や理論計算機科学でよく用いられるようになる。



ゲーデル以後の展開


第一不完全性定理の拡張として、証明の定義に、命題の証明より小さな、否定命題の証明が存在しないという性質を追加した上で、前提のω無矛盾性を無矛盾性に弱めた定理がジョン・バークリー・ロッサー (1936年) によって示された。この事実はω矛盾した算術理論を考える場合などにおいて重要となる。なお算術を内包する真である体系（自然数の標準モデルで真である公理に基づく体系）はω無矛盾なので、第1不完全性定理は原型のままでも適用できる。今日ではこちらの無矛盾性のみを仮定する強い定理もゲーデルの不完全性定理と呼ばれるが、単にロッサーの定理、ゲーデル・ロッサーの定理などと呼ばれることもある。


第二不完全性定理に関しては、ゲーデルによる証明の定義に代えて、ロッサーによる上記の証明の定義を用いれば、体系自身の無矛盾性が証明できることが、クライゼル (1960) によって指摘されている。2つの証明の定義の同値性は体系内では証明できないため、第2不完全性定理とは矛盾しない。


レオン・ヘンキンは、対角化により「Hは証明できる」と同値となる命題H（ヘンキン文）を構成し、その証明可能性に関する問題を1952年に提起した。この問題は3年後の1955年に、マーティン・レーブによって解かれた。彼は、「Hの証明が存在すればHである」が証明可能であれば、Hもまた証明可能であることを示した（レーブの定理）。Hに矛盾を代入すれば、レーブの定理から第二不完全性定理が示せる。



不完全性定理の代数化


不完全性定理は他の論理構造と同じく抽象代数による簡易な表現が可能である。リンデンバウム代数（英語版）を次のように定義する。



  • 理論 T{displaystyle T}T のリンデンバウム代数 TL{displaystyle T_{L}}T_{L} は，文に順序構造を入れたものである。

  • 順序は、もし理論 T{displaystyle T}T で A⇒B{displaystyle ARightarrow B}{displaystyle ARightarrow B} を証明できるならば A≥B{displaystyle Ageq B}{displaystyle Ageq B} と定義される。


  • A{displaystyle A}A と B{displaystyle B}B の順序が等しいなら、A{displaystyle A}A と B{displaystyle B}B を同一視する。


T{displaystyle T}T で無条件に証明可能な文 A{displaystyle A}A は，この順序で最小元となり、T{displaystyle T}T で ¬A{displaystyle lnot A}lnot A を証明できるとき、A{displaystyle A}A はこの順序の最大元となる。よって最大元でも最小元でもないものは独立命題のみ。つまり不完全であるためにはリンデンバウム代数の位数は3以上であることが要請される。一方 B{displaystyle B}B を，一階述語論理のリンデンバウム代数とすると、どんな理論のリンデンバウム代数 L{displaystyle L}L についても，あるイデアル I⊆B{displaystyle Isubseteq B}{displaystyle Isubseteq B} が存在して、L=B/I{displaystyle L=B/I}{displaystyle L=B/I} と表される。よって T{displaystyle T}T が生成するイデアル (T){displaystyle (T)}{displaystyle (T)} が T{displaystyle T}T が生み出す定理全体となる。このとき、理論 T{displaystyle T}T のリンデンバウム代数は、剰余代数 B/(T){displaystyle B/(T)}{displaystyle B/(T)} である。ここでロビンソン算術に対応する B{displaystyle B}B の部分集合を Q{displaystyle Q}Q とする。このとき、ゲーデルの第一不完全性定理は次のようにして表現される。



  • (Q){displaystyle (Q)}{displaystyle (Q)} を含む再帰的可算素イデアル p⊂B{displaystyle psubset B}{displaystyle psubset B} は存在しない。

他に、ザリスキ位相や素スペクトルによる表現が知られている。



誤解（哲学等による誤解・誤用）


計算機科学者（コンピュータ科学者）・電子工学者のトルケル・フランセーンによれば、不完全性定理のインパクトと重要性について、しばしば大げさな主張が繰り返されてきた[3]。たとえば


「数学の思考に変革をもたらした」「数学ばかりでなく、科学全体も一新した」

「数学だけではなく、哲学、言語学、計算機科学と宇宙論にまで革命を起こした」



という言があるが、これらは乱暴な誇張とされる[3]。不完全性定理が一番大きな衝撃を与えたと思われる数学においてさえ、「革命」らしきものは何も起きていない[3]。


この定理は、数理論理学（数学の比較的小さな領域）で常に使われているが、普通の数学者の仕事にはほとんど何の役にも立っていない[3]（そもそも計算機科学は、不完全性定理の証明後に、アラン・チューリング主導で成立した。不完全性定理が計算機科学に革命を発生させたと述べるのは、時系列が誤っている）[4]。


ゲーデルの完全性定理と不完全性定理は、革命的出来事ではなく時代の流れの産物だった[4]。ゲーデル以外の誰かがこれらの定理を発見するのは時間の問題だったとされており、ゲーデル自身もそう見ていた[4]。



誤用例


フランセーンは『ゲーデルの定理：利用と誤用の不完全ガイド』において、ゲーデルの定理が広範に誤用されていることについて論じている[5]。



一般社会・インターネット


数学者の田中一之によれば、ゲーデルの名や定理は「知的会話」に頻出している[6]。フランセーンが述べたように、インターネットのどんなニュースグループでも、遅かれ早かれ誰かがゲーデルの定理を持ち出す[6]。そういった一般的な引用における間違いを正すことが、フランセーンの著書の目的となっている[6]。


1931年にゲーデルが示したのは、「特定の形式体系P{displaystyle P}Pにおいて決定不能な命題の存在」であり、一般的な意味での不完全性についての定理ではない[7]。


フランセーンによれば、ゲーデルの不完全性定理と結び付けられるテーマはロジック、数学、計算、哲学、物理学、進化論、政治、宗教、無神論、神学、文学、詩歌、写真、建築、音楽、ヒップホップ、デートなど多岐にわたる[8]。


形式論理学のような専門領域の外では、不完全性定理についての言及の多くは、誤解や自由連想に基いており、馬鹿げているとさえ言える[5]。たとえば、


ゲーデルの不完全性定理は、客観的現実の存在は証明できないことを示している

ゲーデルの不完全性定理によって、すべての情報は本質的に不完全で、自己言及的である


存在と意識を同等に考えることによって、私たちはゲーデルの不完全性定理を進化論に応用できる

などが見られる[5]。


アラン・ソーカルとジャン・ブリクモンは、ポストモダニズムに対する論評『「知」の欺瞞』の中で、「ゲーデルの定理こそ汲めども尽きぬ知的濫用の泉である」と述べ、レジス・ドブレ、ミシェル・セールらの文章を批判している[9][5]。ゲーデルの理論の誤解は、さらに一般的な人々の間でも起こっている[5]。たとえば


ある種の事実は、論理や数学でうまく証明できない

何ものも確実に知り尽くすことはできない

人間の心は計算機（コンピュータ）ができないこともできる

などである[5]。



数学者以外の学者


田中によれば、ゲーデル自身が不完全性定理について明言しているのは、1963年8月28日の次の文言である[7]。


.mw-parser-output .templatequote{overflow:hidden;margin:1em 0;padding:0 40px}.mw-parser-output .templatequote .templatequotecite{line-height:1.5em;text-align:left;padding-left:1.6em;margin-top:0}

ある程度の有限的算術を含むどんな無矛盾な形式体系にも決定不能な算術命題が存在し、さらにそのような体系の無矛盾性はその体系においては証明できない。[7]



ゲーデルは慎重を重ねて言葉を選んでいるため、この表現を安易に変えようとすると、不具合を生じる[7]。実際、この定理のいずれかの条件が落とされることで、多数の誤解が生じている（特に「有限的算術を含む」という条件が落とされていることが多い）[7]。


「ある程度の有限的算術を含む」という条件を、「十分大きな」「十分複雑な」「十分表現力のある」などといった曖昧な条件に置き換えることは誤りだが、一般向けの解説などには横行している（実際には、大きな理論で完全なものもあれば、小さな理論で不完全なものもある）[7]。


さらに見落とされやすい点は、不完全性定理の前提および結論部に「算術の条件」があることである[10]。要するに不完全性定理は、「算術を含む体系がその算術部分で不完全である」という主張であり、その算術の外側が完全か不完全かについては、この定理は何も語っていない[11]。


高名な物理学者でさえ、間違いを冒すことがある[11]。フリーマン・ダイソンとスティーヴン・ホーキングの論説は、万物理論の可能性を否定するのにゲーデルの定理を持ち出した[11]。しかし仮に物理理論に不完全性定理が適用できたとしても、不完全性はその算術部分に見つかるだけで、その理論が完全か不完全かは別の問題である[11]。


また、哲学者によるゲーデル関係の本が、フランセーンの本と同じ頃に書店販売されていたが、哲学者の本は専門誌によって酷評された[12]。その本は全体として読みやすく一般読者からの評判は高かったが、ゲーデルの証明の核（不動点定理）について、根本的な勘違いをしたまま説明していた[12]。同様の間違いは他の入門書などにもあり、田中は「一般の哲学者は、論理の専門家ではない」と述べている[12]。



宗教


フランセーンによれば、次のような講釈さえ存在する[13]。


ゲーデルの不完全性定理は、数学的なアプローチや証明なしにも直観的に理解しうるものである。実際、禅仏教思想のなかにも明瞭にそれとわかる形で不完全性の概念が出現しているからだ。[13]

実際には不完全性定理は、「形式体系の無矛盾性と完全性についての定理」である[13]。確かに「矛盾」「無矛盾」「完全」「不完全」「体系（システム）」という語は、専門用語でない言語とも結びつきがあるが、およそこのような結びつきは不完全性定理と関係が無い[13]。



神学


神学にも不完全性定理は持ち込まれ濫用されており、たとえば『キリスト教と数学の書誌学』（1983年）がある[14]。


ゲーデルの不完全性定理は … 神の自由への道を示す。[14]

〔この論文では〕ゲーデルの定理を用いて、物理学者が物質的実在の最終的理論を決して定式化できないことを示す。 … 人間の心がたんなる論理機械以上のものであるという適切な見方を発展させる[14]

数学者も彼らのシステムで数学的真理のすべてを把握できないのだから、神学者が、すでに明らかになった真理をうまく体系化できなくても気に病むには及ばない。[14]

科学の方法、技法、仮定が、完全に科学に基礎づけられるはずはないことは、ゲーデルの定理からの類推によって説明される。それらの妥当性を判定するためには、科学の外のリソースを使わなくてはならない。[15]

ダニエル・グレーブスは次の通り「考察」をしている。[14]



ユダヤ・キリスト教は、真理はたんなる理性で推し量れる域を越えていると長い間考えてきた。霊的な真理は、霊魂によってのみ理解される、と私たちは教えられている。それも、そうあるべくしてそのようにある。ゲーデル流の構図は、キリスト教徒が宇宙について信じていることに適っている。[16]

ナジャムディン・モハメッドも、神学的に「応用」している[17]。


あなたが世界をどのように（論理的規則で）記述しても、あなたに真か偽か判定できない「何ものか」がつねにあるであろうことが指摘されている。 … これは、ゲーデルの不完全性定理の基本である。

もし私たちが論理や推論だけに頼るなら、互いに矛盾しているが論理的に自己無矛盾な推論・論理システムが多数生じ、完全な混乱状態で終わることもありうる。どっちが正しいか？　すべての事柄は、何がよいか悪いかのように現在の心理的な傾向に依存するものなのか？　こういう場合には「正しさ」は意味をもたず、まさにこのことが不可知論的無神論の立場を招きうるのだ。[17]



これらの考察と、「ポストモダン的状況」という考え方には類似性がある[18]。そうした理屈では、不完全性は無数の様々な無矛盾理論を導き、どこで「真理」が手に入るかは誰も知らない（したがって、理性だけで正しい道を歩むことはできず、信仰が進むべき道となる[19]）。


しかし実際の数学では、そのような枝分かれは無く、「決定不能性の海」の中でもがくようなことも無いため、そのような「混乱」は神学的幻想に過ぎないとされている[19]。



誤用の分類


田中はゲーデルの定理の様々な誤用を分類している[20]。その一つは、人間の悟性が陥りやすい間違った傾向である[20]。たとえば、自分が思いつく有意義そうな体系がどれも不完全であるので、「有意義な体系はすべて不完全である」と思い込み、さらにその原因を定理か何かに帰着させようとする傾向である[21]。


別の誤用は、言語の誤用である[20]。不完全性定理に含まれる「矛盾」「完全」「体系（システム）」などの語は、日常では多様に使われている[20]。そこを混同すれば、ゲーデルの定理までがインフォーマル（非公式・非正式）な意味と結び付けられる[20]。



脚注



注釈





  1. ^ 歴史的には論理式のゲーデル数化の概念が先に生まれ、後にコンピュータがデータを数値で表すようになった。なお、ゲーデル自身は、素因数分解の一意性を利用して論理式のゲーデル数化を実現している。


  2. ^ 実際、¬ProvableARG(m,m){displaystyle lnot ProvableARG(m,m)}{displaystyle lnot ProvableARG(m,m)}が証明可能ならP̸rovableARG(m,m){displaystyle not ProvableARG(m,m)}{displaystyle not ProvableARG(m,m)}の証明系列P1,…,Pn0{displaystyle P_{1},ldots ,P_{n_{0}}}P_{1},ldots ,P_{{n_{0}}}が存在するので、論理式の列P1,…,Pn0{displaystyle P_{1},ldots ,P_{n_{0}}}P_{1},ldots ,P_{{n_{0}}}のゲーデル数をa{displaystyle a}aとすると、「Proof(a,m,m){displaystyle (a,m,m)}(a,m,m)」が証明可能、したがって特に「∃y:Proof(y,m,m){displaystyle exists y:Proof(y,m,m)}{displaystyle exists y:Proof(y,m,m)}」=「ProvableARG(m,m){displaystyle ProvableARG(m,m)}{displaystyle ProvableARG(m,m)}」が証明可能。一方我々は「¬ProvableARG(x,x){displaystyle lnot ProvableARG(x,x)}{displaystyle lnot ProvableARG(x,x)}」が証明可能な事を仮定していたので、これは矛盾である。


  3. ^ ω無矛盾とは∃yP(y){displaystyle exists yP(y)}{displaystyle exists yP(y)}が証明できれば、P(u){displaystyle P(u)}{displaystyle P(u)}を満たす自然数u{displaystyle u}uが実際に存在することを指す。定義より「ProvableARG(m,m){displaystyle ProvableARG(m,m)}{displaystyle ProvableARG(m,m)}」は「∃y:Proof(y,m,m){displaystyle exists y:Proof(y,m,m)}{displaystyle exists y:Proof(y,m,m)}」であった。ω無矛盾性より、「Proof(u,m,m){displaystyle Proof(u,m,m)}{displaystyle Proof(u,m,m)}」を満たす自然数u{displaystyle u}uが実際に存在し、u{displaystyle u}uをゲーデル数に持つ論理式の列がP̸rovableARG(m,m){displaystyle not ProvableARG(m,m)}{displaystyle not ProvableARG(m,m)}の証明系列になる。


  4. ^ 訳注：自己言及的でないこと。


  5. ^ 訳注：この場合の「帰納的可算」とは、すべての定理のゲーデル数を枚挙する計算可能関数が存在する（実効的に枚挙可能）ことを意味する。クレイグのトリックによれば、このことは定理集合が帰納的な公理系から生成される（演繹閉包である）ことと同値である。




出典





  1. ^ Gödels Unvollständigkeitssatz 2018年7月15日閲覧。


  2. ^ webcache.googleusercontent.com 2018年7月15日閲覧。

  3. ^ abcdフランセーン 2011, p. 9.

  4. ^ abcフランセーン 2011, p. 10.

  5. ^ abcdefフランセーン 2011, p. 4.

  6. ^ abcフランセーン 2011, p. 229.

  7. ^ abcdefフランセーン 2011, p. 230.


  8. ^ フランセーン 2011, pp. 3-4.


  9. ^ ソーカル & ブリクモン 2012, p. 262.


  10. ^ フランセーン 2011, pp. 230-231.

  11. ^ abcdフランセーン 2011, p. 231.

  12. ^ abcフランセーン 2011, p. 233.

  13. ^ abcdフランセーン 2011, p. 7.

  14. ^ abcdeフランセーン 2011, p. 126.


  15. ^ フランセーン 2011, p. 127.


  16. ^ フランセーン 2011, p. 128.

  17. ^ abフランセーン 2011, p. 131.


  18. ^ フランセーン 2011, pp. 131-132.

  19. ^ abフランセーン 2011, p. 132.

  20. ^ abcdeフランセーン 2011, p. 234.


  21. ^ フランセーン 2011, pp. 234-235.




関連文献



原論文




  • Gödel, Kurt (1931), “Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I.”, Monatshefte für Mathematik und Physik 38: 173–198, doi:10.1007/BF01700692, http://www.zentralblatt-math.org/zbmath/search/?q=an:57.0054.02 .


  • Rosser, John Barkley (1936), “Extensions of some theorems of Gödel and Church”, Journal of Symbolic Logic 1 (3): 87–91, doi:10.2307/2269028, https://www.jstor.org/stable/2269028 .



原論文の日本語訳




  • 廣瀬健、横田一正 『ゲーデルの世界　完全性定理と不完全性定理』 海鳴社、1985年5月10日。.mw-parser-output cite.citation{font-style:inherit}.mw-parser-output .citation q{quotes:"""""""'""'"}.mw-parser-output .citation .cs1-lock-free a{background:url("//upload.wikimedia.org/wikipedia/commons/thumb/6/65/Lock-green.svg/9px-Lock-green.svg.png")no-repeat;background-position:right .1em center}.mw-parser-output .citation .cs1-lock-limited a,.mw-parser-output .citation .cs1-lock-registration a{background:url("//upload.wikimedia.org/wikipedia/commons/thumb/d/d6/Lock-gray-alt-2.svg/9px-Lock-gray-alt-2.svg.png")no-repeat;background-position:right .1em center}.mw-parser-output .citation .cs1-lock-subscription a{background:url("//upload.wikimedia.org/wikipedia/commons/thumb/a/aa/Lock-red-alt-2.svg/9px-Lock-red-alt-2.svg.png")no-repeat;background-position:right .1em center}.mw-parser-output .cs1-subscription,.mw-parser-output .cs1-registration{color:#555}.mw-parser-output .cs1-subscription span,.mw-parser-output .cs1-registration span{border-bottom:1px dotted;cursor:help}.mw-parser-output .cs1-ws-icon a{background:url("//upload.wikimedia.org/wikipedia/commons/thumb/4/4c/Wikisource-logo.svg/12px-Wikisource-logo.svg.png")no-repeat;background-position:right .1em center}.mw-parser-output code.cs1-code{color:inherit;background:inherit;border:inherit;padding:inherit}.mw-parser-output .cs1-hidden-error{display:none;font-size:100%}.mw-parser-output .cs1-visible-error{font-size:100%}.mw-parser-output .cs1-maint{display:none;color:#33aa33;margin-left:0.3em}.mw-parser-output .cs1-subscription,.mw-parser-output .cs1-registration,.mw-parser-output .cs1-format{font-size:95%}.mw-parser-output .cs1-kern-left,.mw-parser-output .cs1-kern-wl-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right,.mw-parser-output .cs1-kern-wl-right{padding-right:0.2em}
    ISBN 4-87525-106-8。
    （ゲーデルの完全性定理と不完全性定理の解説書。両方の原論文の邦訳が収録されている）



  • ゲーデル 『ゲーデル　不完全性定理』 林晋・八杉満利子訳、岩波書店〈岩波文庫 青944-1〉、2006年9月15日。
    ISBN 4-00-339441-0。
    （前半の58頁が原論文の邦訳、残りの233頁が歴史的な背景を中心とした解説、という構成）



  • 田中一之 『ゲーデルに挑む　証明不可能なことの証明』 藤村まりこ イラストレーション、東京大学出版会、2012年4月26日。
    ISBN 978-4-13-063900-2。
    （原論文の邦訳と解説）




原論文の英訳




  • Gödel, Kurt (1986), Feferman, Solomon, ed., Kurt Gödel: Collected Works: Volume I: Publications 1929-1936, Oxford University Press, pp. 144-195, ISBN 978-0-19-503964-1, https://books.google.com/books?id=5ya4A0w62skC&pg=PA144 


  • Gödel, Kurt Meltzer, B.訳 (1992), On Formally Undecidable Propositions of Principia Mathematica and Related Systems, Dover Books on Mathematics, Dover Publications, ISBN 978-0-486-66980-9, https://books.google.com/books?id=R7cHCYzIdWYC&pg=PA1 


  • Gödel, Kurt; Hirzel, Martin (2000-11-27), “On formally undecidable propositions of Principia Mathematica and related systems I” (PDF), Boulder: 173-196, http://hirzels.com/martin/papers/canon00-goedel.pdf 


  • Gödel, Kurt (2002), “Some metamathematical results on completeness and consistency, On formally undecidable propositions of Principia mathematica and related systems I, and On completeness and consistency”, in van Heijenoort, Jean, From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931, Source Books in the History of the Sciences (Fourth Printing ed.), Harvard University Press, pp. 592-617, ISBN 978-0-674-32449-7, https://books.google.com/books?id=v4tBTBlU05sC&pg=PA592 


  • Gödel, Kurt (2004), “On Formally Undecidable Propositions of the Principia Mathematica and Related Systems. I.”, in Davis, Martin, The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions, Dover Books on Mathematics, Courier Corporation, pp. 4-38, ISBN 978-0-486-43228-1, https://books.google.com/books?id=qW8x7sQ4JXgC&pg=PA4 



教科書



  • 前原昭二 『数学基礎論入門（復刊）』 朝倉書店〈基礎数学シリーズ 23〉、2006年3月20日（原著1977年6月1日）。
    ISBN 978-4-254-11723-3。

  • 新井敏康 『数学基礎論』 岩波書店、2016年8月16日（原著2011年5月18日）。ISBN 978-4-00-005536-9 ISBN 978-4-00-730459-0。

  • 田中一之 編著 『数学基礎論講義　不完全性定理とその発展』 日本評論社、1997年3月。
    ISBN 4-535-78241-5。

  • 『ゲーデルと20世紀の.mw-parser-output ruby>rt,.mw-parser-output ruby>rtc{font-feature-settings:"ruby"1}.mw-parser-output ruby.large{font-size:250%}.mw-parser-output ruby.large>rt,.mw-parser-output ruby.large>rtc{font-size:.3em}
    論理学(ロジック) 1 ゲーデルの20世紀』 田中一之 (編)、東京大学出版会、2006年7月。
    ISBN 978-4-13-064095-4。

  • 『ゲーデルと20世紀の
    論理学(ロジック) 2 完全性定理とモデル理論』 田中一之 (編)、東京大学出版会、2006年10月。
    ISBN 978-4-13-064096-1。

  • 『ゲーデルと20世紀の
    論理学(ロジック) 3 不完全性定理と算術の体系』 田中一之 (編)、東京大学出版会、2007年3月。
    ISBN 978-4-13-064097-8。

  • 『ゲーデルと20世紀の
    論理学(ロジック) 4 集合論とプラトニズム』 田中一之 (編)、東京大学出版会、2007年7月。
    ISBN 978-4-13-064098-5。


  • Lindstrom, Per (1997), Aspects of Incompleteness, Lecture Notes in Logic 10, Springer-Verlag, ISBN 3-540-63213-1 


  • Hajek, Petr; Pudlak, Pavel (2013-10-04) [1993], Metamathematics of First-Order Arithmetic, Perspectives in Mathematical Logic (Softcover reprint ed.), Springer-Verlag, ISBN 978-3-540-63648-9 



講義ノート


  • 照井一成. “再帰的関数論（2005年度、慶應義塾大学文学部） (PDF)”. 京都大学数理解析研究所. 2018年12月24日閲覧。


誤用と誤解について



  • トルケル・フランセーン 『ゲーデルの定理：利用と誤用の不完全ガイド』 田中一之訳、みすず書房、2011年3月25日。
    ISBN 978-4-622-07569-1。

  • アラン・ソーカル、ジャン・ブリクモン 「11 ゲーデルの定理と集合論――濫用のいくつかの例」『「知」の欺瞞――ポストモダン思想における科学の濫用』 田崎晴明・大野克嗣・堀茂樹訳、岩波書店〈岩波現代文庫 学術 261〉、2012年2月16日、262-269頁。
    ISBN 978-4-00-600261-9。



関連項目




  • グッドスタインの定理

  • ゲーデルの完全性定理

  • 算術的階層

  • 自己言及

  • 自己言及のパラドックス


  • 対角線論法 - ゲーデルによる不完全性定理の証明は対角線論法を用いている。

  • タルスキの定理

  • チューリングマシン

  • チューリングマシンの停止問題

  • パリス＝ハーリントンの定理

  • プリンキピア・マテマティカ

  • ライスの定理

  • ZFCから独立な命題の一覧




外部リンク



  • 西村敏男. “ゲーデルの不完全性定理 - Yahoo!百科事典”. Yahoo! JAPAN. 2013年8月2日時点のオリジナル[リンク切れ]よりアーカイブ。2013年8月2日閲覧。

  • 西村敏男『ゲーデルの不完全性定理』 - コトバンク

  • ゲーデルの不完全性定理について : MATHEMATICS.PDF

  • Weisstein, Eric W. "Gödel's First Incompleteness Theorem". MathWorld（英語）.

  • Weisstein, Eric W. "Gödel's Second Incompleteness Theorem". MathWorld（英語）.







  • 表

  • 話

  • 編

  • 歴


.mw-parser-output .hlist ul,.mw-parser-output .hlist ol{padding-left:0}.mw-parser-output .hlist li,.mw-parser-output .hlist dd,.mw-parser-output .hlist dt{margin-right:0;display:inline-block}.mw-parser-output .hlist dt:after,.mw-parser-output .hlist dd:after,.mw-parser-output .hlist li:after{white-space:normal}.mw-parser-output .hlist li:after,.mw-parser-output .hlist dd:after{content:" · ";font-weight:bold}.mw-parser-output .hlist dt:after{content:": "}.mw-parser-output .hlist-pipe dd:after,.mw-parser-output .hlist-pipe li:after{content:" | ";font-weight:normal}.mw-parser-output .hlist-hyphen dd:after,.mw-parser-output .hlist-hyphen li:after{content:" - ";font-weight:normal}.mw-parser-output .hlist-comma dd:after,.mw-parser-output .hlist-comma li:after{content:"、 ";font-weight:normal}.mw-parser-output .hlist dd:last-child:after,.mw-parser-output .hlist dt:last-child:after,.mw-parser-output .hlist li:last-child:after{content:none}.mw-parser-output .hlist dd dd:first-child:before,.mw-parser-output .hlist dd dt:first-child:before,.mw-parser-output .hlist dd li:first-child:before,.mw-parser-output .hlist dt dd:first-child:before,.mw-parser-output .hlist dt dt:first-child:before,.mw-parser-output .hlist dt li:first-child:before,.mw-parser-output .hlist li dd:first-child:before,.mw-parser-output .hlist li dt:first-child:before,.mw-parser-output .hlist li li:first-child:before{content:" (";font-weight:normal}.mw-parser-output .hlist dd dd:last-child:after,.mw-parser-output .hlist dd dt:last-child:after,.mw-parser-output .hlist dd li:last-child:after,.mw-parser-output .hlist dt dd:last-child:after,.mw-parser-output .hlist dt dt:last-child:after,.mw-parser-output .hlist dt li:last-child:after,.mw-parser-output .hlist li dd:last-child:after,.mw-parser-output .hlist li dt:last-child:after,.mw-parser-output .hlist li li:last-child:after{content:") ";font-weight:normal}.mw-parser-output .hlist ol{counter-reset:listitem}.mw-parser-output .hlist ol>li{counter-increment:listitem}.mw-parser-output .hlist ol>li:before{content:" "counter(listitem)" ";white-space:nowrap}.mw-parser-output .hlist dd ol>li:first-child:before,.mw-parser-output .hlist dt ol>li:first-child:before,.mw-parser-output .hlist li ol>li:first-child:before{content:" ("counter(listitem)" "}

  • メタ論理（英語版）

  • 数学




  • カントールの定理

  • Entscheidungsproblem（英語版）

  • チャーチ＝チューリングのテーゼ

  • Consistency（英語版）

  • Effective method（英語版）

  • 数学基礎論

  • （幾何学）

  • ゲーデルの完全性定理

  • ゲーデルの不完全性定理

  • 健全性

  • 完全性

  • 決定可能性

  • Interpretation（英語版）

  • レーヴェンハイム–スコーレムの定理

  • メタ定理（英語版）

  • Satisfiability（英語版）

  • Independence（英語版）

  • タイプとトークンの区別

  • Use–mention distinction（英語版）





Popular posts from this blog

MongoDB - Not Authorized To Execute Command

Image
.everyoneloves__top-leaderboard:empty,.everyoneloves__mid-leaderboard:empty,.everyoneloves__bot-mid-leaderboard:empty{ height:90px;width:728px;box-sizing:border-box; } 0 I have successfully enabled authorization on MongoDB and I have created an account on the admin database and then I created an account for my database called test. The following connection string to connect to my test database works successfully: mongo --host 192.168.17.52 --port 27017 -u user1 -p password --authenticationDatabase test Only problem I have now is, I cannot execute commands such as: show dbs. I get the following error when I try to do so: "errmsg" : "not authorized on admin to execute command { listDatabases: 1.0, lsid: { id: UUID("a1d5bc0d-bc58-485e-b232-270758a89455") }, $db: "admin...
Read more

How to fix TextFormField cause rebuild widget in Flutter

Image
.everyoneloves__top-leaderboard:empty,.everyoneloves__mid-leaderboard:empty,.everyoneloves__bot-mid-leaderboard:empty{ height:90px;width:728px;box-sizing:border-box; } 0 I've got the same issue at #9280. I tried all solutions from that topic with/without GlobalKey for Scaffold and Form but the problem wasn't fixed. I tried to build a authentication form with login and signup. But the keyboard doesn't show when I tap the TextFormField at the first time. Then I try to input some letter from physical keyboard, the widget is rebuilt. Like this: login screen Nothing to be log when I run flutter run --verbose, so I logged manually. Every tapping on field, the widget called dispose -> init -> build. [√] Flutter (Channel beta, v1.0.0, on Microsoft Windows [Version 10.0.17763.195], ...
Read more

in spring boot 2.1 many test slices are not allowed anymore due to multiple @BootstrapWith

Image
1 I tried to upgrade a yummy sandwich made of two test slices (@JsonTest and @JdbcTest in my case, crunchy test code in between) adding spring boot 2.1 flavour to it. But it seems it was not much of a success. I cannot annotate my tests with many @...Test since they are now each bringing their own XxxTestContextBootstrapper. It used to work when they all used same SpringBootTestContextBootstrapper. @RunWith(SpringRunner.class) @JdbcTest @JsonTest public class Test { @Test public void test() { System.out.printn("Hello, World !"); } } The error I get from BootstrapUtils is illegalStateException : Configuration error: found multiple declarations of @BootstrapWith for test class I understand I might be doing something wrong here but is there an easy way I could load both Json and Jdbc contex...
Read more