北田 発見への道 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で仮定される各種公理がア・プリオリなものかどうか？というのに還元されると思うのだが、私は答えがだせない。
野矢論理学 2章
アリストテレスのオルガノンの概説。256通りの三段論法のうち、24の正しいものを、4の正しいと思われる論法から証明したとのこと。一方、多重量子化や固有名、関係文を扱う上で問題があることを提示し、フレーゲの開発した述語論理へと話をつなげていく。述語論理は、オルガノンを包含し、また命題論理を包含するものであるという説明。実際に1～4格を述語論理で記述できることを示している。
述語論の意味論の説明。トートロジー→妥当式。解釈という意味付け（述語記号、個体定項の割り当て、議論領域）及び ∀、∃の意味を決定づける。
気になる記述
- ∧の解釈。命題関数をつなぐ∧はどのように解釈するのか？そのためにテクニカルな処置がとられるとのことだが、、、、
- 妥当式の全てがトートロジーというわけではもちろんありません
- 述語論理の機械的決定手続きは存在しない
述語論理の構文論。定項および自由変項を一括して項と呼ぶ。また、述語論理の公理系Lを提示。ドモルガンの法則の存在量化版の提示。完全性に関しては先送り。
まぁこの辺も初歩中の初歩。とはいえ、アリストテレスの三段論法をある程度ちゃんとした形で記載しているのは初めてみた。面白い。
