日記（2021/8/1）:読書要約をやっていたら今日が終わってしまった。マジかよ（注:論理と集合と数の専門的な話）

1.集合論と論理学のループ（に見えるもの）

とある事情で論理学の本の要約をしていました。

昔から疑問があって、

「通常、数学基礎論の核心である集合論は、やはり数学基礎論の核心である論理学を使う。

しかし、論理学の中に、集合っぽい何かや数っぽい何かが使われているように見える。

平たく言うと、集合論と論理学がループしているように見える。

こういう循環定義はおかしい。

フローチャートめいた、ループのない完全な有向グラフが描けてなければならない」

というところで、これを解決するためにものすごく頑張っていたのでした。

（たかが脳のかゆみのために、どんだけコストをかけて、どんな顔でこんなことしてやがんだコイツ…）

（そいつはこんな顔でしたかね）

（ウワーッ！　のっぺらぼう！）

（太って肉が垂れているからいるからぬっぺふほふですよ）

（来るな！　何だよこのテンションの差！　そこが却って怖いよ！）

（夏の怪談ですねえ）

2.「論理学に集合論は必要ないのではないか？」というアドバイス

ある善良な方々のアドバイスで、

「論理学に出て来る『集合っぽい何か』や『数っぽい何か』は、本物のZFC公理系由来の集合や自然数がなくても出来るから、別に循環はない」

という示唆がありました。

「本当かよ」ということで、まあ頑張って調べてたんですよ。

3.戸次大介『数理論理学』

3.1.戸次大介『数理論理学』

今回読んでいたのは、言語学系論理学の先生である戸次大介『数理論理学』。

（その前に前原昭二『記号論理入門』も読んでたけど、これは終わったから今回は説明しません）

3.2.論理学の部門3つ

この本の趣旨はこうです。

＊＊＊

専門的な話をすると、論理学にはざっくり三つジャンルがあると考えます。

論理学の全ての根本としての「記号」や、それを練り上げて作る、論理学の主たる対象となる「論理式」を扱う「統語論/構文論」。

論理式の「真偽」を扱う「意味論」。

そして、ある論理式から別の論理式を作るルール、そしてそのプロセス全体である「証明」を扱う「証明論」。

3.3.意味論は集合を使っており、循環定義回避の役に立ってくれない疑いがある

意味論について、アツイ話と、限界が見えてきます。

＊＊＊

要するに、「真偽とは何か」という、しばしば哲学的に言われる問いは、論理学の意味論においては

「真偽という区別できる2個の元/要素（中身）の入ったなんか集合（箱）があり、論理式の集合と真偽の集合の間に写像（元同士の一方通行の矢印）があるとき、「ある論理式は真か偽である」という意味になる」

という形に定式化されます。

＊＊＊

ここで、集合、あるいは譲歩しても、写像を作れる程度には公理の入った集まりが使われています。

「論理学を使って集合を定義したいのに、その集合を使って論理学を構築している」

というのは、循環定義であり、インチキでしょう。

最初に書いた問題意識について、論理学の、少なくとも意味論の部門は、力にならなさそうだ。ということです。

3.4.統語論は集合と数を使っており、循環定義回避の役に立ってくれない疑いがある

統語論について、同じ話が出てきます。

＊＊＊

論理学の土台である記号として、2項真理関数というものが出てきます。

これは、2つの記号を入れたら1つの論理式が出て来る写像であり、たとえば「ならば」という2項真理関数に「A」という記号と「B」という記号を入れると「AならばB」という論理式が出てきます。

そうです。写像を使っている訳です。

「論理学を使って集合を定義したいのに、その集合を使って論理学を構築している」

というのは、循環定義であり、インチキでしょう。

＊＊＊

さらには、ここでは「2」という元数/アリティ（この写像は何個の入力を要請する、といった時の個数のようなもの）が使われています。

数は通常、ZFC公理系という、論理学よりさらに高度な体系で、構築して初めて出来るものなんです。

というか、ZFC公理系は、

「公理（出発点となるルールを表す論理式）のキッチリ入った集合は、写像や自然数を作れる」

という触れ込みで有名なものです。

じゃあ、そもそも論理学を構築する時点で、0とか1とか2とかが出て来ていることは、どうやったら正当化できるんだ？

最初に書いた問題意識について、論理学の、少なくとも統語論の部門も、力にならなさそうだ。ということです。

さて、困ったな…なんかおかしいぞこれは…

＊＊＊

3.5.「集合や数を（核心的には）使わない（かもしれない）証明論で行こう」という戦略

論理学は妥当な証明を行うためのものです。

だから、妥当な証明が出来ていなければならない。そういう要請がある。

「真である論理式だけから真である論理式だけを導出出来ていて欲しい」

これは論理学に求められる、当然の要求でしょう。

前提が全部正しいのに帰結が間違っていたら、まーキレもしようものです。

＊＊＊

ここで、奇妙な話が出てきます。

真であるかどうかは無視して、ある論理式から別の論理式を導出するためには、証明論を使います。

本書が示唆するところでは、論理学の体系の中には、

「意味論で言い表せることは、証明論でほぼ同じように言い表せる」

ものがあります。

マジかよ。

＊＊＊

ここで、証明論で集合や数を（少なくとも統語論や意味論のようにかなり初期の段階で）使わないとしたら、集合や数をあらかじめ持ち込んでいない証明論の一部を使って、集合や数を構築できるのではないか。

だとしたら、循環定義は避けられる。イケるか？

というのが、本書の（第7章以降の）動機である。ということが示されています。

3.6.無理では？

いやいやいや。

証明論といえども、統語論で扱う記号を使わなければ、何も定義できない訳です。

じゃあ「ならば」を使った時点で、数が2個入ってくるから、作戦失敗じゃん。

それとも、これを回避する手段が、さらに別にあるのか…？

3.7.証明論もやはり集合と数を使っており、循環定義回避の役に立ってくれない疑いがある

3.7.1.証明論の手法いろいろ（特にゲンツェン流シーケント計算）

あと、証明論そのものを読み進めると、どうにもマズイところが出てきました。

＊＊＊

証明論の手法には「ヒルベルト流証明論」「自然演繹」「タブロー」などがあります。（内容については説明しません）

＊＊＊

これらをもう少し一般化した、「シーケント計算」という手法があります。

論理式ではなく、「前提となる論理式から帰結としての論理式を導出する一連の推論」、「推件式/シーケント」を基本単位とするのが、「シーケント計算」の特徴です。

これを「ヒルベルト流証明論」「自然演繹」「タブロー」に適用すると、一見丸っきり違うこの3つの証明体系が、統合的に扱える、という有難みがあります。

＊＊＊

「シーケント計算」の方言である、より網羅的な事柄を扱える強まった手法、「ゲンツェン流シーケント計算」というのがあります。

これは「推件式/シーケント」の定義が「前提となる論理式「の列」から帰結としての論理式「の列」を導出する一連の推論」になっています。

しかもこれは列の長さは0でも1でも2以上でも構いません。この一般化により、扱える論理式や推件式の在り方のバリエーションが、大幅に柔軟になります。

しかし、これは、「0や1や2以上を使っている」と言うことです。

また数が生えてきた。これは避けられない形で使っているのか？　そうではないのか？

3.7.2.（専門的な話）ゲンツェン流シーケント計算で二重否定除去律を導出する過程で2個の論理式が出て来てしまう

で、ここで問題が発生しました。「避けられない形で使っている」ケースが存在したのです。

広く使われている高等な論理学の体系「一階述語古典論理」において、必須である論理式または推件式があります。「二重否定除去律」というものです。

（馴染みやすく言うと、「否定の否定は、元々の話に何も手を加えていない、肯定と同じ」というやつです。

なお、世の中には、これを採用したら扱えない、「否定の否定と、元々の話が、微妙にズレている」ような話もしばしばありますね。

こちらは一階述語古典論理よりさらに原始的な論理学「直観主義論理」で扱うことになります。

直観主義論理は二重否定除去律を導出できませんので、一階述語古典論理を作りたいなら、それは直観主義論理で自前でどうこうしようとせず、ちゃんと追加しなければなりません。

ここについては後で簡単に説明します）

＊＊＊

ゲンツェン流シーケント計算で二重否定除去律を作る時の操作で、

「無から「肯定的な論理式」と「否定的な論理式」を生じせしめることができる」

という操作を行います。

＊＊＊

さて、これが何を意味するかと言うと、

「この場合、帰結となる論理式は、つまりは「肯定的な論理式」と「否定的な論理式」で2個ありますよね」

ということなんです。

＊＊＊

ちなみに、ゲンツェン流シーケント計算において、直観主義論理にはある制約があるのです。

「推件式の中で、論理式は高々1個しか出て来てはならない。要は、0個か1個かだ」

ということです。（だから直観主義論理では二重否定除去律は作れないのですね。つまりこれは数のせいなのです。ますます困るな…）

＊＊＊

えーと。

そうなんですよ。

「直観主義論理と二重否定除去律の独立性（お互い関係ないということ）」という状況下で、0と1と2という数っぽいもの、出て来てるやんけ。

さっき言った、数を作れるZFC公理系は、一階述語古典論理の上で構築されているものです。

つまり、一階述語古典論理の要である二重否定除去律に、数が持ち込まれているのは、これはどう見ても、マズイ。

＊＊＊

うおー…やはり、最初の問題の解決という観点からは、証明論の部門も、やはりダメなのでは？

どうすんのコレ？

4.論理学の中の「集合っぽいもの」と「数っぽいもの」の無害化の試み

4.1.数を無害化する手段として、戸田山和久『論理学をつくる』に書いてあった、等号の同一性による疑似的な個数を使うのはどうだ？

以前読んだ、戸田山和久『論理学をつくる』の方式、イケるかもしれない。

「一階述語古典論理」の「古典論理」を弱めると「直観主義論理」になる。

が、「一階述語論理」の方を弱めると、記号の中に等号が採用されており、これによって同一性が表せる「同一性のある述語論理」（「等号付き述語論理」と呼ぶ向きもある）になる。

「「等号で表せる「このもの」を、1個という数を持つとみなす」という方法で、「同一性のある述語論理」はある種の疑似的な個数を表せる」

というのが戸田山本の趣旨だから、この場合の0や1や2も、等式で表せば、問題なくイケる。

つまり、非常に原始的な数を定義する場合は、高度過ぎるZFC公理系など、要らん、ということです。

「入力すべき記号が2個要請されている」場合も、「論理式の数が2個ある」場合も、これで扱う分には問題ない。

エウレカ！

4.2.記号列の長さは気になるが、記号列はいわゆる（自然数を使う）列ではないと見なしても問題ないので、無視してよい

また、記号を記号列だと思った時、つい

「列は、自然数の集合または自然数全体の集合と、集合の、写像であるから、自然数の集合か自然数全体の集合という形で自然数を利用している」

と思ってしまいますが、記号を羅列するだけなら「いくつあるか」ということには基本的に頓着しなくてもよい、ということが分かってきました。

4.3.「集合」から公理を抜き切った純粋な「集まり」を使ってどこまで行けるか

数は無害化出来そうだ。じゃあ、集合は？

「集合」から公理を抜き切った純粋な「集まり」を使ってどこまで行けるか？

（今やってる最中です。終わってません）

（こいつ…）

5.おれのいちにち、ぼうにふろう

そんなこんなで、今日一日棒に振っていたんですね。

おれのいちにち、ぼうにふろう。

（何だお前。ちょっとおかしいぞ）

まあ、続きはまた来週にしましょう。あー超疲れた…