北田 発見への道4章

4章 命題計算の完全性

拡張命題論理と称するモノから完全性に迫る。すなわち命題式の論理式に対して、命題変数の閉包をとる操作を行うと、（自然数論では変数記号に関する閉包をとる限りこのような事情は発生しない）、任意の式は真理値1か0のみをとるようになる。この議論をつぶさに見ると、「真理値1の閉包命題式は拡張命題論理の定理であり、真理値0の閉包命題式の否定は拡張命題論理の定理である」という予測が得られ、ここから「閉包命題式が真理値1をとることと拡張命題論理の定理であることは同値である」、すなわち「命題論理の命題式Aが恒真式であることと、Aが命題論理の定理であることは同値である」ことが予想される。

実際、「命題論理の恒真式は命題論理の定理式である」ことは数学的帰納法を利用することによって確かめられる（メタでは数学的帰納法は有用な道具立てとされる）。また、命題論理において証明可能でない式を公理に加えると体系が矛盾することを示すことができる。

上記をモデルの言葉でいえば、「命題論理の命題式Aが定理式であることは、Aが自然数論Sの任意の構造Mをモデルとすることと同値である」、または「命題論理の命題式Aが定理式であることは、それが恒真式であることと同値である」

以上、命題論理を自然数論の影とする立場からだとこのように拡張された命題論理を持ち出す必要がある（野矢先生の言葉でいえば、自然数論における命題は、変数の閉包をとる限り---すなわち閉じた式-- である限り、自然数論が真偽を決定することに責任を持つべき数論的命題であることに対応する）。証明とか、ヒューリスティックに関しては納得がいくがもう少しやりようはないのだろうか？命題論理をそれ自体として扱うのではなく、自然数論の影として扱うからこのようになるのだろう。まぁ本の主題がゲーデルの定理であるから仕方ないのかもしれないが、命題論理の枠内だけで完全性定理を証明してほしかった。野矢論理学でも完全性の証明ははしょられているわけだし・・・べつのテキストブックを用意する必要がありそうだ。

北田 発見への道 3章

3章 命題計算の無矛盾性

いったん命題理論から始める。しかし本書では一貫して自然数論Sを前提に置いているため、命題変数は自然数論における命題と同一視する。命題論理自身もSの影としてみる立場のようだ。

統語論、推論規則（MP１つ）、公理系(11こ）を提示。意味論として真理値表を導入する。全ての公理がトートロジーであることが示せる。また、唯一の推論規則MP の前件が真と仮定した際に、後件が真になる、すなわち真理性が保存されることが示せる。トートロジーたる公理からはじめ、MPを有限回用いて定理を導いていくので、全ての定理がトートロジーであることが示せる。したがって矛盾式が定理でないことが示されるので、無矛盾性・整合性が確かめられる。

真理値表を与える代わりに、モデルという概念を導入して、「命題論理の定理式がトートロジーである」の現代版「命題論理の定理式は、自然数論における任意の構造Mにおいて真である」ことを示す。

全体の議論は非常に明快。うまく公理系、推論規則を選んだから、かな。あと、命題論理だとモデルの概念が簡単になりすぎて逆にわかりづらい・・

北田 発見への道 1-2章

発見への道

1章 不完全性定理とはなにか

・自然数論を含む理論Sを考える

・Sには反証できない命題Gが存在する＝ゲーデルの第一不完全性定理

・これは統語論的不完全性と呼ばれる

・Gは「私は証明できない」という意味の命題

・Gはメタレベルの命題であり、自身をS自身に「写さない限り」いけないはず

・したがって、ゲーデルの不完全性定理は、統語論的な形式的な演算のみによっておこる不完全性でなく、意味論的な仕掛けが存在することが示唆される

極めてまっとうなことを短い文章にまとめている。惜しむらくは、わかる人にしかわからない文章であるように見える。わかる人には知ってることだし、わからない人にはわからないという・・・・

2章 形式的自然数論

・第一不完全性定理は、「Sは矛盾するか不完全かである」ともいえる

・第二不完全性定理は「Sが無矛盾ならばその無矛盾性はSにおいて形式化される方法によっては証明できない」

・ヒルベルトプログラムを打ち砕いたのは、第一ではなく、第二の不完全性定理

・ラッセル「プリンキア・マティマティカ」＝論理主義はもはやオワコン

・とは言え直観主義や形式主義に大きな影響を与えた

・直観主義のブラウアーは痛烈に批判

・ヒルベルトは、それに対して理論の取り扱いを直観主義の方法（有限の取り扱い）で回避しようと考えた

・第二不完全性定理がそれを不可能と指摘した

・Sの説明。統語論、推論規則（MP, GEN, SPEC）、公理の紹介

・推論 |- 、定理についての説明

この辺りはまぁ常識なので特に疑問はない

北田 発見への道の勉強開始

今日からしばらく以下のテキストブックでゲーデル不完全性定理を勉強する

「理系への数学」に連載していたものをまとめたもののようだ。ぱっと見たところ、メタな議論をすることに特化している模様。日本語が多いので読みやすい。ゲーデルナンバリングの振り方に特徴がある。初学者向けではなさそう。短くて読みやすそう。

ブログタイトルでは、「発見への道」と称することにする。

野矢論理学 5章

ゲーデルの不完全性定理の概観。なぞっても面白くないので自分なりに再構成。

自然数論を含む公理系Nは、矛盾しているか、不完全である（ゲーデルの第一の不完全性定理）。そして、Nの無矛盾性は、有限の立場では証明することができない（ゲーデルの第二の不完全性定理）。

そもそも、理論の無矛盾性などのメタな問題の議論は、理論内部で行うような式変形ではなく、他の何らかの手段で検証されるべき性質のものである。とはいえ、我々はヒルベルト的な考え方、すなわち有限の立場で（すなわち数学的帰納法などを使った構成的立場で）メタな議論を行うことを常としている。命題論理や述語論理の完全性や無矛盾性はその方法で示される。一方、自然数論は、その方法では完全性や無矛盾性を示せないとゲーデルが指摘した。なおゲンツェンは、別の立場（超限帰納法）で議論すれば、無矛盾性が示せると指摘した。我々は、理論に対するメタな議論をする際にどのような方法に訴えるべきかについて、再考するべきかもしれない。

第一不完全性定理は、実際に「私は証明できない」という意味の命題が存在することで示される。「・は証明できる」という述語はメタな述語であり、1階述語論理における述語ではないが、ヒルベルト流メタ議論は、自然数論と同一の道具立てを使っているため、「・は証明できる」という述語を自然数論Nにおける述語にすることができる。そして、対角化定理を利用することで、「私が証明できない」という意味の命題の存在を示すことができる。第二不完全性定理は、第一不完全性定理をちょろっと使うとすぐに出てくる。

一応ゲーデルの不完全性定理に関してその定理の意味とそれを取り巻く議論は俯瞰できるようになった。定理の証明はざっと読んだ感じなのでもう少し時間をかけてゆっくり見ていきたい。

野矢先生の本は、対話形式ということもあり、素朴に思うような疑問にきちんと答えてくれるのがありがたい。この本によって不完全性定理の意味を、過大評価せずに見つめなおすことができ、また理論に関するメタ的な理解が深まったように思う。

以上で野矢論理学読了。

野矢論理学 4章

直観論理についての概説。排中律が否定されるとともに、古典論理では妥当であったいくつかの定理が成り立たないことを示す。例えば、次のものは直観論理では成立しない：否定除去型の背理法（￢Aを仮定して矛盾を示せば、Aが示せる）、二重否定除去（￢￢AからAを示す）。直観論理とは観念論であり、証明は構成可能性によってしめされるものだという言及。

上記の概説の元、直観命題論理である公理系LIPを紹介。意味論として、クリプキによる意味論を採用し、認識史・知識状態・「 ||- 」を使って意味論を与える。古典論理の真理値分析に対して、認識史分析がある、すなわち決定手続きがあることを示す（具体的に書いてあるが、煩雑なので読むのをあきらめた）。

また、古典論理に関して再度意味論を検討する。すなわち、モデルという概念によって意味論を再解釈した。

直観命題論理は、古典命題論理の部分系であるが、完全である。直観命題論理の妥当式は、古典命題論理の妥当式であるが、その逆は必ずしも成り立たない。

ここで「 ||- 」が出てきた。なるほど、確かに直観論理から借りてきた記号なのか・・・と腹落ちしたのであった

野矢論理学 3章

ラッセルのパラドクスが生まれる歴史を振り返る。パラドクスが起きるのは二階論理に相当することをしていることを示し、論理学と数学は異なることを強調。パラドクスに対して、３つの反応があることを示す。つまり、論理主義・直観主義・形式主義。

直観主義の背後には、無限に対する構成主義的見方があり、それは存在論的見方と異なることを証明。一方排中律等が成り立たないことを提示。片や形式主義はこのような姿勢を批判、形式的体系と、メタに対して構成的な手法を取り入れる立場であること、ヒルベルトがそれを主導したことを示す。しかし、ゲーデルにより、メタ数学にこのような構成方法では完全性および無矛盾性を示すことができないことが示されてしまったことが示された。一方この方針で公理的集合論が整備されたことを指摘。

以上、論理学を超えた（二階論理等に踏み込んだ）際には矛盾らしきものが発生するが、論理学にとどまる限り、完全性や無矛盾性が示される。

というわけで、命題論理の無矛盾性を示す。一般の形式的推論をつぶさに調べ、各行の導出式はすべてトートロージーであることを数学的帰納法で示す。したがって、推論の最後の行である定理式がトートロジーであること、すなわち、「すべての定理はトートロジーである」という健全性が示される。健全性が示されれば、トートロジーでない矛盾式は定理でないことが示されるので、無矛盾性が示される。

述語論理の無矛盾性は、述語論理を命題論理に還元する方法（影を作る）という形で、述語論理に矛盾式が存在すると仮定すると、命題論理が矛盾することを利用した背理法を用いることで示される。

なお、完全性に関しては、命題論理・述語論理のいずれも省略されている。

補足に、「＝」を（数学ではなく）述語論理の公理であることを示す。

メタ論理での完全性や無矛盾性はテキストによって少しずつ説明が違うので読んでいてなかなか楽しいものがある。

公理的集合論は、一階述語論理で記述できており、かつ、自然数を含む体系でありまた数学を包含しているので、本文で触れられているように、数学には二階の論理が必要という説明はほんとか？？？と思う。

とはいえ、数というものが論理のたまものなのか、経験的に体得される自然科学的性質を持ったものなのかははっきりしない。ZFCで仮定される各種公理がア・プリオリなものかどうか？というのに還元されると思うのだが、私は答えがだせない。