「直観主義型理論（ITT, Intuitionistic Type Theory）」勉強会ノート其ノ壱「緒言」「命題と判断」（予習編）

　Per Martin-Löfの"Intuitionistic Type Theory"(1984)、通称ITT84*1の勉強会の記録でござる。今回はとりあえず、最初の2節で読んでもわからなかったところをメモっときます。

個人的な動機
緒言（Introductory remarks）
命題と判断（Proposition and judgements）

個人的な動機

　なにゆえITTに興味を持ったのかを書いといたほうがのちのち振り返ったときによいかもしれない。

　私は論理と計算の対応という現象に興味がある。なかでもITTは、めちゃくちゃ基礎的な理論でありながら、構成的プログラミングや定理証明支援系などわりとこうした話題のうち実用性が高い話とも繋がってくる。また近年注目(?)の証明論的意味論とも深い関わりがあり、哲学的にも興味深い。マーティン=レーフ先生は現象学に影響を受けているようで、思想面もおもしろそうなのである。

　ITTは直観主義論理をベースとしているが思想的には論理主義っぽいのではないかと思う。この数学の哲学の伝統的な論争もまた新たな観点から見られたりするでしょう。古の議論をずるずる引きずり続けるのは哲学のダメなところかもしれないが、私は哲学のそういうところが好きである。遊戯王OCGでシンクロ召喚が登場したときにレスキューキャットや召喚僧サモンプリーストの価値が高騰したように、哲学においても環境の変化と古典の復活みたいなことがしばしばあるのである。だから多面的な教養が必要で、哲学者はデュエリストなのである。

　あと遊戯王ついでにこれを

f:id:cut_elimination:20210414213220j:plain

ITTでは"judgement"という語が頻発されて、それを見るたびこのカードを思い出す。

緒言（Introductory remarks）

　ラッセル、可述性、プログラミングなど。

ロジックと数学の関係

　最初に。数学とロジックの関係は三通りの解釈があるという。

数学的記号法を使ったロジック、記号論理
数学の基礎（あるいは哲学）としてのロジック
数学的手法を使った、数学の一分野としてのロジック

なるほど、これはなるほどです。ITT84で扱うのは主に2で、1も少し入ってくるが3は違うという。なので難しい定理の証明は出てこない。

　対して3というのはそういった哲学論争に踏み込まずにメタ定理を証明したりとかする研究のことであろう。2節で「ヒルベルトによって創始されたメタ数学の流儀でやるようにロジックを他の数学の分野と同じように扱うとき、…」と書かれている*2。後期のヒルベルトやゲーデルやタルスキあたりから数学の基礎付けとして始まったロジックが数学の一分野になった感じがある。証明やモデルの構造の研究が始まったからである。具体的にはキューネン『数学基礎論講義*3』や新井敏康『数学基礎論 *4』*5で扱っているようなものだと思う。3ではないということは、そういう意味でのロジックではないということかと。

ラッセルの型理論

　続いて『プリンキピア・マテマティカ』（以下：『プリンキピア』）の批判(?)が書かれている。『プリンキピア』はラッセルとホワイトヘッドの共著だが、型理論を考案したのはラッセルのようなので以下ではホワイトヘッドのことはちょっと忘れる。

『プリンキピア』

　なので『プリンキピア・マテマティカ序論*6』の訳者*7解説を読んで勉強中。

　しかし、これを読めばラッセルの分岐型理論（ramified type theory）がどういうものなのかということと背景思想はわかるのだが、それがどれだけ使えてどんな限界があるのかは私にはあまりわからない。それが以下で露呈した。

可述性がわからん

　分岐型理論は可述的（predicative）な体系である。可述的というのは非可述的（impredicative）ではないということである。「非可述的ではない」というのは「非可述的な定義を含まない」ということでいいのでしょうか？

　ITT84も可述的な体系であるとマーティン=レーフ先生はいう。実はマーティン=レーフ先生は、これ以前に作った体系が矛盾しているということがのちにわかったという経験がある。これを受けて改良したのがITT84の体系らしい。矛盾を示したのは我らがジャン=イヴ・ジラール先生で、この矛盾はジラールのパラドクスというとか。ITT84は小さい型（small types）という概念を導入してこの矛盾を回避しているという話が途中で出てくる。これが非可述的な定義を逃れているらしい。

　ということは以前の体系は非可述性ゆえに矛盾したのか？分岐型理論で型の他に階（order）を導入しているのは非可述的定義によって生ずる悪循環を回避するためである。この悪循環はリシャールのパラドクスやベリーのパラドクスといった意味論的パラドクスを導く。しかしこれらが体系の矛盾といえるかどうかは微妙かと思う。それはさておき、ジラールのパラドクスはブラリ=フォルティのパラドクスと類似するらしい。ブラリ=フォルティのパラドクスはラッセルのパラドクスと類似した論理的パラドクスのはずで、これは深刻である。論理的パラドクスを回避するために導入されたのが型である。じゃあジラールのパラドクスはなぜ可述性で回避されるのだろう？というかITT84の可述性って結局どういうことなのだろう？私の理解が表面的すぎるのがいけないのだと思う。精進します。確か「すべての型の型」みたいなのがパラドクスと矛盾を導いて、これは非可述的だからやめればいいとかそういうことだと思う。

　ラムジーやウィトゲンシュタインの分岐型理論批判と真理値や真理関数の話、ラムジーの単純型理論（これは高階論理のことでいいという噂）のこともITT84でチラッと触れられている。これらの話題も『プリンキピア・マテマティカ序論』解説に出てくるので調べときます。

さらにITT84でわからんところ

It is free from the deficiency of Russell's ramified theory of types, as regards the possibility of developing elementary parts of mathematics, like the theory of real numbers, because of the presence of operation which allows us to form the cartesian product of any given family of sets, in particular, the set of all functions from one set to another*8.

これ（可述的な直観主義の型の理論）は、実数の理論のような数学の初等的な部分を展開しうるという点で、ラッセルの分岐的な型の理論の欠点を逃れている。何故なら、任意の与えられた集合族からデカルト積を作る操作が存在するからである。具体的には、あるひとつの集合から他の集合への関数すべての集合である。

やはり『プリンキピア』の知識が不足していて以下のことがわからない（3つ目は『プリンキピア』というより解析学の知識不足かも）。

分岐型理論では実数論を十分に展開できないのか？
分岐型理論では自由にデカルト積を作る操作がないのか？
デカルト積と実数の理論にはなんの関係があるのか？

ちょっと前のところで（還元公理を加える前の）分岐型理論について"... but it was not sufficient for deriving even elementary parts of analysis."と書いている*9。解析学（analysis）は実数論をベースにしたものなのでこれと上の"elementary parts of mathematics, like the theory of real numbers"は同じことのように思える。ただし解析学との関連で分岐型理論の欠点としてよく挙げられるのは最小上界をうまく定義できないということである。"... but it was not sufficient for deriving even elementary parts of analysis."が最小上界のことを言っているのだとしたら、これはデカルト積とは関係ないはずなのでデカルト積が作れることでは解決しないと思うのだけれど。もしかして関係なくないのだろうか。

　なおデカルト積を作る操作というのはそのうち出てくる $\Pi$ の依存型であろう。

プログラミング言語との親和性

　現行のロジックの記号法はプログラミング言語に適していない、故にコンピュータ科学者は自前の言語を作った、と述べている*10。しかしITTはプログラミング言語として使えるとのこと*11。のちにITTはこの予言どおりCoqやAgdaといった定理証明支援系の言語の基礎となっている。

　しかしここで気になるのは、ITTの何がこれらの言語に貢献しているのか、である。（このあと出てくる）判断とかはどう使われいているのだろう。どうも今のところ調べた感じでは依存型（dependent type）が重要らしいのだが、他の構成要素はどうだろう。また、依存型は"ITTの"特徴といえるのかどうか。ITT以前にも依存型はあったのではないかと。

命題と判断（Proposition and judgements）

　命題と判断の違い、判断の導入、BHK解釈

命題と判断の違い

　命題（英: proposition, 独: Satz）と主張（英: assertion）もしくは判断（英: judgement, 独: Urteil）との違いを強調している。言語哲学的には主張と判断の違いも微妙なはずで、これについてはマーティン=レーフ先生は別の論文で論じているはずだが、ITT84では特に何もない。これ以降では判断のほうを使っているのでそれでまあよい。

「Aは真である」と言ったとき、Aが命題で「」内が判断である。ITTはこれらの違いを体系内で明示的に扱う。この内容と判断の区別は後述するフレーゲの影響っぽいが、実はもっと遡ってボルツァーノに由来する、確か。

　さて、命題と判断の区別は何がそんなに重要なのだろう。いろいろ調べているとマーティン=レーフ先生の論文を読む人は彼の判断へのこだわりがよくわからなくてモヤッとらしい。私も例外ではない。これはどうも哲学的な動機があるようで、マーティン=レーフ先生は出自はゴリゴリに数学の人だが哲学史の論文も書いている。けどもしかしたら判断へのこだわりの補強するために哲学史を勉強したのかもしれない。このへんも徐々に調べるのである。

判断とは？

　判断の形式は4つある*12。マーティン=レーフ先生の記法は現代のスタンダードとは違うようなので、現代的なものも併せて書く。

$A$ は集合である（省略して $A \; set$ ）　これは現代では $A:Type$ じゃないかと。
$A$ と $B$ は等しい集合である（ $A = B$ ）　これは同じか。
$a$ は集合 $A$ の要素である（ $a \in A$ ）　これは $a:A$ 。
$a$ と $b$ は集合 $A$ の等しい要素である（ $a = b \in A$ ）　これは $a = b:A$

　マーティン=レーフ先生は $\in$ を文字どおりギリシア語の εστι として読むならば、ということを書いているが（ $\in$ 記号はギリシア語の繋辞 εστι の頭文字に由来するので）、まあ関係ないかと思う*13。どうもマーティン=レーフ先生は語学が得意なようで、こういう話題が好きなのかもしれない。

　重要な注意は、普通は $a \in b$ や $a = b$ は命題だがここではこれらは判断だということである。

BHK解釈

　ブラウワーとハイティングとコルモゴロフでちょっとずつ違うらしい。論理結合子の解釈は同じようなものだろうけど、命題と証明の関係というベースの部分でいろいろあるようだ。ITT84, 4ページの表によると、ハイティングの解釈は命題が予想？期待？（expectation）で証明がその実現である。

　コルモゴロフの「直観主義論理の解釈について」という論文はこのたび読んだ。元はドイツ語だが英訳（"On the Interpretation of Intuitionistic Logic"）がある。ここで直観主義論理は問題解決のための論理だということが述べられている。私は以前コルモゴロフが書いたグリヴェンコへの追悼文（これはロシア語）を読んだことがあるのだが、ここでも直観主義論理を問題解決の論理として紹介していた。コルモゴロフの論理・数学思想もまた別でまとめまっせ。

　マーティン=レーフ先生は若い頃モスクワに留学してコルモゴロフの指導を受けたらしい。この頃すでにコルモゴロフはロジックから離れていて、マーティン=レーフ先生はまだロジックを専門としていなかった。ランダムネスの研究をしていたらしい。コルモゴロフ複雑性とかマーティン=レーフランダムネスとかだと思う。ITT84, 4ページによれば、直観主義論理のコルモゴロフ解釈は証明をプログラムとみなす現代の考え方と親和的とのこと。

岡本賢吾先生の論文を読もう

　岡本先生の論文は過去にも二つ扱っている。

cut-elimination.hatenablog.com

この記事のなかでも述べたが、岡本先生は現代の計算機科学方面のロジックの知見を活かして古典を再解釈するという研究をされている。ITTを扱った論文も書いていてる。「「命題」•「構成」•「判断」の論理哲学－－フレーゲ／ウィトゲンシュタインの「概念記法」をどう見るか」という論文で『分析哲学の誕生－フレーゲ・ラッセル*14』という本に入っている。この論文の前半ではITTの知見を活かしてフレーゲの「概念記法」の判断論を再解釈している。

　というわけなのでマーティン=レーフ先生がフレーゲの判断論からどのような影響を受けたのかはこの論文ではわからないのだが（話が逆なので）、しかしおもしろい論文なのでここでメモっておく。

　概念記法には二つの重要な記号が出てくる。内容線と判断線である。これらは以下のようなもの：

　内容線： $\vcenter{\rule{1.0cm}{0.4pt}}\;\Phi$

　内容線＋判断論： $|\vcenter{\rule{1.0cm}{0.4pt}}\;\Phi$

岡本先生によれば内容線というのはそれ（上ならば $\Phi$ ）が適正な文であることを表し、判断線が加わるとそれがその体系の公理または導出されていることを表すという。内容線＋判断線は現代でも証明可能であることを表すターンスタイル記号 $\vdash$ として残っているが、それと同じようなことである。しかし決定的に違うのが、『概念記法』では内容線＋判断線は「公理または定理であることが現に証明されているような文に付されるだけである」が、ターンスタイルは「原理的に…導出可能であるようなすべての文に付される」*15。

　しかしこれは岡本先生の解釈であってフレーゲがそう書いているわけではないらしい。というわけで『概念記法*16』（藤村龍雄訳）を見てみた。いわく「内容を表す記号の前に $|\vcenter{\rule{0.5cm}{0.4pt}}$ を書けば、それで、あらゆる内容が判断になる訳ではない。例えば、「家」という表象は判断にはなり得ない。それゆえ、われわれは判断可能な内容と判断不可能な内容を区別する。…内容線の後に続くものは、常に、判断可能な内容をもたなければならない*17」。これを見ると内容線に関しては確かに岡本論文の解釈は当っているように思える。ただし判断についてはもうちょっとフレーゲの哲学を調べてから判断したい。岡本論文はフレーゲの判断論において証明という概念が重要であると述べているが、その正否は私にはまだ判断できない。今後の課題である。

　さてITTである。岡本論文によるとITTの判断のうち二つは概念記法の内容線と判断線と対応しているという。

　ITTの内容線： $\Phi$ : proposition

　ITTの判断線： $\Phi$ : true

そしてこれらはITTの規則を使ってちゃんと証明できることなので、その点で概念記法よりいい感じである。 $\Phi$ : proposition は上述の四つの判断を使うと $\Phi \; set$ に当たる。 $\Phi$ : true は例えば $p \in \Phi$ みたいにする。命題を集合（あるいは型）と同一視し、証明をその要素と同一視するカリー=ハワード対応である。命題が証明を持っていることが、その命題が真であるという判断になる。つまりフレーゲのいう判断はITTでは常に証明を伴って現れるので、フレーゲにおいて証明が重要だとする岡本先生の解釈が正しいのだとすれば、概念記法とITTはすごく相性がいいことになる。

そういえば証明ってなんなのだろうか

　命題と判断だけでなく、証明と判断の違いにも注意が必要であろう。

　自然演繹や推件計算でよく書くあの樹状の図は判断の証明で、命題の証明は要素であるから別である。自分なりの言葉で書くと、命題の証明はモノで、判断の証明は認識のプロセスである。しかしこういうことを書くと形而上学にコミットしてしまうので危険かもしれぬ。マーティン=レーフ先生は判断の証明と命題の証明の混同を避けるためにしばしば後者を構成（construction）と呼ぶとしている*18。そういえば「証明図」や「証明可能」の定義はよく見るが、「証明」の定義って一般的にあるのだろうか？あと推件計算ってあれは「証明」をやっているのだろうか？なんか変なことが気になってきて怖い。

　さて、例えば「自然数は無限にある」という命題の証明はどういうモノか。うまく記号化するとこの命題はこんな感じになるかと思う。

　 $\forall n \in {\mathbb N} \exists m \in {\mathbb N}(n ＜ m)$

　この命題の証明を、自然数（例えば n）が与えられたときにそれよりも大きい自然数（例えば n+1）を返す関数、およびその自然数が確かにもとの自然数よりも大きいという別の証明のペア、というように解釈するのがITTであろうかと。ただしこれだと不等式の定義がまた必要になってややこしい例かもしれない。まあでも「命題の証明はモノ」というのは、こうやって関数やデータとして構成できるということによる。

　モノと認識プロセスの違いなどと書いたが、マーティン=レーフ先生はボルツァーノ・ブレンターノ・フッサールといった初期の現象学者を参照して判断に関する哲学的な議論も行っている*19。これはダメットの『分析哲学の起源*20』の影響ではないかな〜という気もする。ダメットも直観主義論者の大御所で、同書では現象学と分析哲学は同根であると主張している。

*1:いま私が思いついた略称です。

*2:ITT84, 2ページ。

*3: