【論理学用語の私的メモ】
【論理学の基本略語】
自然演繹 推件計算
古典論理 NK LK
直観主義論理 NJ LJ
【略語の導入】
論理学においてまず覚えたほうがいいのは、ゲンツェンの業績と用語法である。ゲンツェンの主要な業績は、自然演繹であるNK, NJとシークエント計算であるLK, LJ と呼ばれる証明論の体系の確立である。NK,LK は古典論理を扱い、NJ, LJ は直観主義論理を扱う。アルファベットの順番でNK,LK(古典論理)よりも排中律がないせいでミニマルなのがNJ,LJ(直観主義論理)だという説明は覚えやすいが、実際には、LK(Logistischer Klassischer Kalkül)、NK (Natürlicher Klassischer Kalkül)、LJ (Logistischer Intuitionistischer Kalkül)、NJ (Natürlicher Intuitionistischer Kalkül)というのが正式名称であり、なぜ直観主義をJと表現するかといえば、ドイツ文字ではJとIの区別がつかないのである。シークエント計算に登場する頭文字(acronym)のLK（エルケー、エルカー） のLは、ドイツ語の Logischer Kalkül（論理計算）に由来する。
【自然演繹と推件計算】
自然演繹の体系は、「自然」の名の通り実際の人間の推論過程に近い見やすくて分かりやすい体系である。一方、シークエント計算(推件計算)は、最小限の公理 A→A と、構造規則および論理結合子に関する推論規則からなる。ゲンツェンはこのLK(古典論理のシークエント計算)において「カット除去定理 」という基本定理を証明した。 この定理は、ある定理を導く論理の道筋には、その定理自身と公理より複雑なものは現れないようにできることを示し、 LK の完全性の証明に使われた。 ゲンツェンには他に純粋算術の無矛盾性証明などの業績がある。 「すべての」を意味する記号∀(ターンエー)を使い始めたのもゲンツェンである。ざっくりいうと、自然演繹は人間が書いた証明であり推件計算のほうはコンピュータがそれを処理するコードのようだといわれる。閉じた証明しか許さないのが自然演繹で開いた証明もかけるのが推件計算。
【LK】
LKというシークエント計算は1934年、ゲルハルト・ゲンツェンが自然演繹を研究する道具として生み出した。その後、論理導出を行うのに非常に有効であることから普及した。LK（エルケー、エルカー） という名称はドイツ語の Logischer Kalkül（論理計算）に由来する。
【直観主義論理】
無限に関する直観が無いような世界が直観主義論理の世界である。そしてそれに従って展開される数学の世界が構成的・建設的数学の世界である。直観主義論理には否認がない。直観主義論理にはただ主張とその根拠しかない。だから直観主義論理は計算機とやっていることが同じだと言える。
【継続(continuation)の概念】
ジングル・スレッド(single thread)でスタンド・アローンなコンピューテイションに特徴を持つ直観主義論理に定位したまま、「継続continuation」概念を使うことによって古典論理の複雑さをそのままに直観主義論理に翻訳できることが知られているが、非常に難しい手続きがある。
【言語哲学の2派】
言語哲学にはふたつの派閥がある。イギリスのマイケル・ダメットは、全ての主張を1から構成して独りで作り上げていくボトムアップ型の直観主義論理重視派であり、アメリカのクワインとデイヴィッドソンとパースは、探求の共同体における議論やコミュニケーション、世界像づくりといったものを重視する古典論理派である。古典論理派は、一般にクリプキ・セマンティクスをはじめとする様相概念と相性がとても悪い。人間はあらかじめたくさんの信念を持っていて、それを適宜修正しながら生きていくのであって、自明なものから積み上げて行き、1から主張を構成しようなどという直観主義は夢物語だというのが古典論理の立場である。直観主義論理のシークエント計算に登場するのは、自明な推論規則と体系全体を整える構造規則くらいしかないので「主張assertion」だけなわけだが、古典論理には、「主張」のほかに「否認denial」を持っている。
【カリー=ハワード同型対応】
カリー＝ハワード同型対応をみつけたハスケル・カリーの名前を取ったハスケルというプログラミング言語がある。これは、直観主義論理がやっていう証明とコンピューターがやっているλ計算が証明の集まりとしての命題観を取ると対応するという考え方である。
【推件計算という訳語】
推件計算はシークエント・カルキュラスにあてられた訳語である。
【図式的整理】
最小述語論理+矛盾律=直観主義論理。直観主義論理+排中律=古典論理。直観主義論理+排中律より弱いルール(=排中律を使ってその命題を証明できるけどその命題から排中律を証明できないようなもの、具体的には「前提なしでA→BまたはB→Aが常に成り立つ」を足す)=ゲーデル論理。ゲーデル論理+幾つかのルール=古典論理。
【ゲーデル論理】
ゲーデル論理は「A→BまたはB→A」(プレ・リニアリティ(前線型性))を直観主義論理にプラスしたもの。前線形性の別名が「アミダアクシオム」。直観主義論理の推件計算に対応するゲーデル論理の推件計算のことをハイパー推件計算という。
【意味論とモデル】
ファジー論理の一種であるゲーデル論理では排中律が証明できないわけだが、それはどうやって証明するのかというと意味論でモデルを使う。数学の絶対値記号みたいなやつを論理式に使うのが意味論の「モデル」である。排中律が全てのモデルで真理値1になるわけではないことが示せればいい。そうすればゲーデル論理では排中律が証明できないということを証明できる。つまり、排中律があればプレリニアリティが証明できるけど、プレリニアリティがある世界で排中律が正しくないことはあるのだ。それが直観主義論理よりも強く古典論理よりも弱いようなゲーデル論理の世界である。
【論理体系】
論理のシステムは論理結合子の導入規則と除去規則と矛盾律と、その他の略記法などをまとめた構造規則から出来ている。
【いろいろな論理】
古典論理と直観主義論理のほかに、「オペレーター」を足して古典論理を拡張した様相論理やファジー論理(ウカシェヴィッチの無限値述語論理)や線型論理(リニアロジック)や古典論理の部分論理であるゲーデル論理や、矛盾許容論理がある。
【最小論理】
最小述語論理の統語論は簡単だが、意味論は難解であることが知られている。
【三値論理】
ヤン・ウカシェヴィッチの三値論理。真偽がまだ決まっていないという値がある。ブラウアーは最初、自らが考案した直観主義論理は三値論理なのではないかと思っていたが、ゲーデルがゲーデル論理の3値版を使ってそうではないことを証明した。
【無限値論理】
無限値論理はダメットが提唱したもので、今ではファジー論理の一種とされている。普通命題は真か偽かの2つの値しか取れないが0から1の無限個の実数の値を取れるのである。ファジー論理の中で一番有名なのがウカシェヴィッチの無限値述語論理である。
【ボトム】
最小述語論理において矛盾命題はボトムという。ボトムは矛盾を表す特殊な命題である。
【否定は略記】
最小述語論理においてはnotは「Aならばボトム」の略記として導入される。たとえば、Aかつnot Aというのは、Aかつ「Aならばボトム」のことであり、Aかつ「Aならばボトム」はボトムである。よって、notはボトムがあればAならばボトムの略記として定義できる。
【矛盾律とはなにか。】
矛盾という前提からは任意の命題を勝手に導出していい(なんでもあり)というのが矛盾律。(法律の世界ではプライバシーの権利と知る権利が矛盾したからといってなんでもありにはならないが、数学の世界では矛盾を前提になんでも導出できる。)
【ト記号】
ト記号の右導入規則と左導入規則。ト記号の右導入規則は自然演繹の導入規則。ト記号の左導入規則は自然演繹の除去規則。
【結論は基本的にはひとつ】
直観主義論理の推件計算のト記号の右側の論理式の数は基本ひとつ。古典論理の場合には２つとかになる。
【略記法ガンマ】
Γ(ガンマ)を推件計算の中で使う場合、その意味は、「全部書くわけには行かないとにかく他にもたくさんの前提がある」という意味になる。
【排中律の異様さ】
直観主義に排中律が足されて古典論理と化したとき、何が足されてしまったことになるのか。それは3つのものの関係である。①orの新しい導入方法。そしてnotすなわち「Aならば②ボトム③」。この①と②と③の新しい関係を強制的に前提なしで結論してしまえるということが排中律の意味である。排中律は非構成的な原理のひとつである。選択公理も非構成的である。
【proposition as data types】
命題があってその証明があるのだけれども、命題とはその命題の証明の集まりであるという強烈な主張がある。つまり命題というのは証明の集まりであるという考え方の導入。直観主義論理の計算機科学的な意味は、proposition as data typesつまり、「データ型としての命題」観を導入すれば明らかにすることができて、それはすなわち「証明の集まりとしての命題」観を導入することである。命題Aは、証明a1と証明a2と証明a3らの集合であるという考え方。
【ラッセルのパラドクス】
素朴集合論や古典論理や縮約規則のある論理では、「ある性質を満たすものを集めてきたものは集合として存在を認める」ので、「自分自身をメンバーとして含まないような集合」というものについての集合を認めてしまうと古典論理には矛盾が導かれることが知られている(ラッセルのパラドックス)。縮約規則のない論理では、包括原理という集合の存在保証原理は矛盾を導かない。
【ラムダ記法】
この変数には後で何らかの入力が入りますよということを予告するために作られたのがλ記法である。たとえば、恒等写像(identity mapping, identity function)の場合にはλx.xと表記する。xに何らかの入力がこれからあり、その結果がそのまま出力されることをこれは表現している。ラムダを使ってならばを定義することができそれをラムダ抽象という。
【ターミネシーションする】
ずっと計算して行きそれ以上計算できないところまでいくことをターミネシーションするという。
【ラムダ記法の凄さ】
ラムダ記法を使って関数の代入を表現すると、自然数の全ての計算規則をカバーできることが知られている。
【直観主義論理の歴史的ねじれ】
もともと「人間的な証明」とか「有限な人間の認識の限界内での数学」というモチベーションがあって、それが非属人的なコンピュータと直観主義論理を生み出したというのが皮肉である。古典論理は直観主義論理に比べて強い仮定を置いているのだ。
【ルベーグ積分】
量子力学の基礎になっている積分。無限集合の有限和(と有限の共通部分)を取るのを無限回繰り返して作る実数の無限集合の集合族をつくるとルベーグ積分できる。無限集合を無限個和集合とって、その共通部分を無限個取るのを無限回繰り返すのだ。それは完全に有限な人間の認識を超えているが、量子力学の数学的基礎のひとつなのだ。これを認めたくなかったのがフランスの19世期末の直観主義論理の数学者たちだったのだ。
【ZFC】
ツェルメロ–フレンケルの公理系(ZF) に選択公理 (C) を加えた公理系をZFCと呼ぶ。
【有限の立場】
ヒルベルトの数学的立場は有限の立場で、それはゲーデルの不完全性定理の証明において岩波文庫のように延々と再帰関数を定義しながら進めるもの。それに対してモデル論をつかってゲーデルの不完全性定理の証明をする場合には証明はとても短くなるのだが、それは有限の立場で数学をやろうという立場ではない。しかも、ヒルベルトの有限の立場とブラウアーの直観主義は異なりヒルベルトとブラウアーは排中律を認めるかどうかをめぐって論争もしている。ヒルベルトの立場は今の言葉でいうプリミティブ・リカーシヴ・アリスメティック(PRA:原始再帰関数しか証明で認めない立場)に相当すると言われている。ゲンツェンはヒルベルトの有限の立場の発展系である。
【ゲーデル論理】
古典論理の推件計算の部分体系のことをゲーデル論理という。
【デュエム＝クワインテーゼ】
ピエール・デュエムは物理学理論について研究する中で、物理学的観察には実験装置についての理論などさまざまな補助仮説が必要であるため、物理学理論のみから何らかの観察予測が導き出されることはなく、したがってそうした理論が文字通りに反証されることはないことに気づいた(例:マコーネルのプラナリア実験)。一見反証されたように見える仮説も、補助仮説のアド・ホックな修正で救うことができる。そうした反証が存在しないというのがデュエムのテーゼである。たとえば、周転円を増やすだけで天動説は延命できた。つまり、当時の科学者たちは、自前の理論の微調整をするだけで計算結果が合うのであれば、根本的な仮定を撤回するのは嫌だったのである。つまり、ローカルな変化で済むならばそのほうが良くて、ドラスティックな変化を当時の科学者は嫌ったのである。ただ、その周転円を増やしていけばいくほど、天動説のパラダイムには「ひずみ」というかボロが蓄積してしまったのだが。
【パースの法則:((A→B)→A)→A】
パースの法則は哲学者であり論理学者であるチャールズ・サンダース・パースにちなむ論理学における法則である。彼の最初の命題論理の公理化において、この法則を公理に採用した。この公理は、「含意」と呼ばれるただひとつの結合子を持つ体系における排中律であると考えることもできる。パースの法則の証明においては排中律と矛盾律をどちらもアクロバットに使って証明するため非常に異様な証明図をつくることになる。
【難しい問題】
「Aを主張すること」と「Aを否認できないこと」の違いはなにか。また、「Aの否定を証明すること」と「Aを否認すること」の違いはなにか。
【古典論理では同値だが直観主義論理では同値ではないこと】
「AならばB」と「not AまたはB」は、古典論理では同値だが直観主義論理では同値ではない。
【三大構造規則】
代表的な構造規則は、①エクスチェンジ、②ウィークニング、③コントラクションの3つである。直観主義論理には結論がひとつなのでシークエント計算においてト記号の右に導入するような構造規則はないが、古典論理では結論が複数ありうるので、シークエント計算においてト記号の右に導入するような構造規則がある。
【ウィークニングの意味】
ウィークニングというのは、推論において前提を強化したり結論を弱化させても推論の妥当性自体は変わらないということをいう。例えば、「この書類は君が書いたのだろう」と言われて本当は全部自分が書いているのに「この部分は私が書きました」と答える場合には前提を強化している。それに対して、本当は自分が全部書いたのに「私か先輩のどちらかが書きました」と答える場合には結論を弱化させていることになる。
【グリベンコの定理】
古典論理における「否認」の否定を「主張」として扱うとか、直観主義論理で二重否定をプラスしたりなどして直観主義論理において古典論理の真似事をできるようにする定理があり、そのひとつがグリベンコの定理である。
【論理学全体をざっくり概観】
証明とは公理から推論規則(モーダスポネンス、背理法など)をつかって定理を導くことである。数学者の仕事は定理の証明である。ではその証明について考えているのが数理論理学である。あたりまえだからこそ公理なのであり、あたりまえでなかったら証明しないといけない。あたりまえすぎて証明できないこと、たとえば、【ペアノ算術】の公理は、「どんな自然数にも次の自然数が存在する」である。
※ラッセルは、『数学は論理学に帰着する』と主張していた人だ。なぜなら、数学を公理化できると考えていたからである。つまり、公理と推論規則から数学全体を導けると考えていたということであり、ラッセルはなにが数学全体の公理かを考えていたひとだ。
数理論理学の世界には大きく2つの方法がある。ひとつは、真理関数によってその命題が正しいか間違っているかを判定していく方法であり、もう１つは公理から出発して推論規則によって式を変形し、証明をしていく方法である。
前者の真理関数の方法は意味論(セマンティクス)といい、後者の形式証明の方法は構文論(シンタクス)という。日常的には、文法が間違っていても意味が通じることはあるし、文法的にはオーケーでも意味が通らないこともある。しかし数学の世界ではそんなことないと思われる。しかし、意味が通っても文法的には正しくないみたいなことは数学の世界でも起こる。どういうことか。
そもそもラッセルとホワイトヘッドはペアノの公理化を忠実に実行しようとした。
彼らの立場では、数学基礎論とは数理論理学と集合論のことで、数は集合によって定義され、集合は論理学で定義されなければならない。
しかし数学全体を論理学に帰着させようという野望はゲーデルによって挫折したとされている。自然数の範囲の算数ができるようなペアノ算術というシステムにおいては、正しいのに証明できないことがあるのである。つまり、【正しいという概念と証明できるという概念がちょっとだけズレている】のである。
真であることと証明できることは微妙にちがうらしい。ゲーデルの第一不完全性定理は、真でも証明できないことがある。ゲーデルの第二不完全性定理は、システム内で自らの整合性は証明できないと主張している。真偽の範囲と、証明可能か否かの範囲は微妙にずれている。
計算機科学では、証明できない文とは計算がいつまでも終わらないプログラムのこと、とも言える。「プログラムがバグっていないかどうかを判定するようなプログラムが作れない」と言い換えてもいいらしい。
公理から始めて推論規則を使って定義を紡ぎ出していくことを【証明】と言って、なにを公理(証明がいらないほどあたりまえなこと)として、何を推論規則(仮言三段論法やモーダスポネンスや背理法など)とするかは流儀の問題であるとされる。
例えば、公理を増やして推論規則を少なくするのが【ヒルベルト流】で、公理を最小限にして推論規則を多くするのが【ゲンツェン流】である。この流儀は、具体的に証明をやるときにはゲンツェン流がよくて、理論全体の枠組みを論ずるときにはヒルベルト流がいいとされる。
※ヒルベルトの23の未解決問題のひとつ「算術が矛盾しないこと」について、ゲーデルが「算術を含むシステムは、自ら矛盾しないことを証明できない」ことを証明した。しかし1936年にゲンツェンが「システム外からだったら算術が矛盾しないこと」を証明している。(ただし問題を設定したヒルベルト本人は、自然数ではなく実数も扱えるような算術を念頭に置いていたらしい。)
※ヒルベルトの1問目は連続体仮説であり、2問目が算術(ペアノの公理系)の無矛盾性の証明で、6問目が物理学の公理化で、8問目はリーマン予想である。全23問中、6問目と8問目と12問目と16問目と23問目を除いた18問は何らかの形で既に解決している。
※連続体仮説とは可算無限のすぐ次が実数無限であるという仮説である。つまり、可算無限と実数無限の間の濃度は存在しないということ。つまり、「アレフ・ノート＝アレフ」という仮説である。
現在のツェルメロ＝フレンケル(ZF)の公理系では、1940年にゲーデルが連続体仮説の否定は証明できないことを証明し、1963年にポール・コーエンが連続体仮説はそもそも証明できないことを証明した。つまり、連続体仮説は証明することも反証することも現在の標準的な公理化された集合論においてはできない。
※ペアノの公理系とはなにか。自然数の範囲では足し算や掛け算が含まれるが、負の数は考えていないので自由に引き算ができない。さらに、有理数＝分数を考えていないので、自由に割り算もできない。自然数における算数というのがペアノの公理系である。
※ダフィット・ヒルベルトの【無限ホテル】は物理学的・建築学的・経営学的には不可能だが、数学的には可能な思考実験であり、非常に有名。
※ちなみに、「プレスバーガー算術」は、足し算だけしかできない弱いシステムだが、ゲーデルの不完全性定理の適用を受けつけないので、完全な算術であることが知られている。
※様相論理学というのは、「いま横浜では雨が降っている」という文に対して、並行宇宙をたくさん考え、全ての並行宇宙における横浜で雨が降っているなら【必然的に】真だけれど、たくさんある並行宇宙の中に、横浜でいま雨が降っているような宇宙が１つ以上存在するというだけなら【可能的に】真であるということが言えるような論理学。様相論理学はゲーデルの不完全性定理の証明と非常に相性がいいらしく、これは1970年代に判明したことである。
そもそも、ゲーデルの不完全性定理はメタ数学である。メタという言葉の意味は、メタフィクションなどのメタと同じである。「メタフィクション」というのは、本の中に著者本人が登場したりするフィクションのことで、ひとことで言えば、フィクションについてのフィクションのこと。例えばセルバンテスの『ドン・キホーテ』や、カート・ヴォネガットの『チャンピオンたちの朝食』、ポール・オースターの『シティー・オブ・グラス』、筒井康隆の『朝のガスパール』などがそれにあたる。
「算数ではあらゆることが証明できる」という文は真ではない。しかしこの文は超数学的(メタ数学的)な文である。数学について数学するのが超数学で、数学者の方法である公理と推論規則を使って、数学自身について語るのがメタ数学である。メタ数学の真骨頂は嘘つきのパラドクスに代表されるような意図的なレベルの混同であるとされる。
ゲーデルが多大な影響を受けているのがカントールである。哲学者のヴィトゲンシュタインはカントールの数学をナンセンスで間違っていると笑っていたらしい。クロネッカーはカントールに嫌がらせをしたし、ポワンカレもカントールを攻撃したことが知られている。でも、【デデキント切断】で有名なデデキントはカントールを援護していた。このカントールの対角線論法をゲーデルやチューリングが不完全性定理の証明に利用したのである。
※そもそもカントールは順序数と濃度を区別した。【オーディナルナンバー】(背番号)と【カーディナルナンバー】(濃度)があるというのである。オーディナルナンバーは自然数の概念を拡張したもので、順序がつけられる数という意味で、カーディナルナンバーは集合どうしの大きさを比較する概念である。
カントール的に考えると、奇数の無限と偶数の無限と自然数の無限はみんな同じであると考えてよいらしい。つまり可能無限の濃度はみな同じであると考えてよい。なぜなら一対一対応がつくからだ。濃度(もしくは基数)が同じだからである。(ちなみに自然数と一対一対応がつくのが可算無限。)
※濃度の記号が「アレフ」である。可算無限の濃度を「アレフノート」という。可算無限「アレフノート」の次に大きな無限を「アレフワン」という。実数無限は何番目に大きい無限か分からないので単に「アレフ」という。
自然数の集合の大きさを「アレフノート」という。自然数の集合の全ての部分集合の集合の大きさを「アレフワン」という。たとえば、要素が2個の有限集合の部分集合は空集合を含めて4つである。無限と【無限プラス1】は濃度がアレフノートで同じで、順序数が違う。
実数も無限にたくさんあるが、その濃度は可算無限より大きい。というか、濃い。実数のほうが自然数よりたくさんある。なぜなら、自然数は可算無限であり、実数は実数無限だからである。これこそが、カントールの対角線論法(背理法)によって証明されたことだった。
「この文は嘘である」という文が本当だとしたら、この文は嘘である。同文が嘘だとしたらこの文は本当である。意味論にとどまる限り、この循環は無限に続く。だからゲーデルは意味論から構文論へと舞台を変えて、証明できることと真であることは別であると示そうとした。だから、「この命題は証明できません」という命題を証明することにした。
文字や記号に数字の【背番号】を割り当ててコード化(命題を番号で表記してやること)するアイデアが元になっているゲーデル数は、「どんな自然数も素因数分解ができて、しかもそれがただ一通りに決まる」という自然数の性質を利用している。
このアイデアの面白さは、あらゆる命題だけでなくあらゆる証明を背番号＝ゲーデル数で呼ぶことが可能になるという点である。命題が無限個あったら証明は終わらないので、証明は必ず有限個の命題の集まりなのだが、素数は無限個あるので、ゲーデル数に置き換えると全ての命題、つまり過去に証明された全ての命題から、これから未来永劫にわたって証明されるであろうすべての命題も、それぞれ固有のゲーデル数で表現することが可能になるらしい。しかもすべての証明が素数の素数乗の積(素因数分解のかたち)で表されていて、しかもそれがただ一通りに決まるので、同じゲーデル数をもつ証明は２つとなく、ゲーデル数から元の証明を復元できるという。このゲーデル数を活躍させて不完全性定理は証明されている。
