岡本賢吾先生は東京都立大学の哲学の教授で、専門は論理学・数学の哲学と情報の哲学とある（https://www.comp.tmu.ac.jp/philosophy/contents/staff/okamoto.html）。中央公論新社『哲学の歴史』の分析哲学編である第11巻で、ヒルベルトやブラウワーを中心としたいわゆる数学基礎論論争の歴史の章の執筆を担当しておられ、それは読んだことがある。 しかし「情報の哲学」というのを掲げておられるとおり、過去の歴史だけでなく、コンピュータ科学と一体化した現代論理学の知見をもとにそうした論争を見直すという研究もされているようだ。そのようなテーマの論文を二つ読んだので、その記録。
その論文というのは「命題を集合と同一視すること－－包括原理からカリー＝ハワード対応へ」というものと「なぜ意味論はプロセスを含むか－－表示意味論・領域理論をめぐって」というものである（文献情報は先程のリンクにある）。
まず「命題を集合と同一視すること」について。
大まかな内容は、副題にあるとおり包括原理とカリー＝ハワード対応を比較するというものである。岡本先生の主張は、包括原理を使った素朴集合論が公理的集合論へと発展した際に失われたものがカリー＝ハワード対応を通してみたタイプ理論では復活している、ということのようだ。その復活したものというのは、純粋な言語による数学的構造の構成である。「純粋な言語」というのは岡本先生によれば「論理的・数学的な諸構造に対する原始的な定項も存在公理も一切含まないような言語」であるという。これはフレーゲが目指したようなことである。ZF集合論は存在公理で成り立っているので、純粋な言語ではない。ここでいう「言語」とは、ロジックでいう意味、すなわち数学的構造を構成するうえで必要な記号の集合（プラス古典一階述語論理の言語）のことだが、一般的な意味での言語もニュアンスとして含んでいる感じである。
素朴な集合論を使った構成では古典一階述語論理に以下のようなものを加えて拡張する。
まずはクラス演算子。集合を定義するのに開放文を用いて以下のようにすることがよくあると思う。
これを、開放文に自由出現する
を束縛する演算子と見たのがクラス演算子である。このとき、任意の
について上記のような集合の存在を保証するのが包括原理である*1。
続いて集合のメンバー関係の記号 であるが、これは以下の述定原理というのを満たすものである。
これらを使えばいろいろな数学的構造を言語によって素朴に構成することができる。自然数の構成も空集合を0としたり後者関数や数学的帰納法を集合として定義すればいい。しかし、周知のとおりこれはラッセルのパラドクスによって矛盾する。ラッセルは矛盾を回避するためにタイプを導入し、公理的集合論では包括原理を制限した。型付ラムダ計算はラッセルのタイプ理論を継承したものなので矛盾を回避できる*2*3。
ラムダ計算ではチャーチ数項を使って自然数が定義できる。ラムダ計算の抽象と適用を使えばけっこういろいろな構造が構成できるし、岡本論文ではさらに System F という高階のラムダ計算を紹介している。しかし、実は素朴集合論でも同じようなことをしている。クラス演算子はラムダ抽象、述定原理の左辺は関数適用、右辺は簡約と実は同じなのである。歴史を遡っても、フレーゲはそもそもいろいろな概念や対象を関数で定義しようとしたわけだから、そうなるのもうなずける。
では型付ラムダ計算を集合論とみなせば満足かというとそうではない。型付ラムダ計算を別のルートで純粋な言語とみなすのが岡本論文の後半である。その別のルートというのがカリー＝ハワード対応である。カリー＝ハワード対応では、型は命題、型付ラムダ項は命題の証明と対応づけられる。となると、型付ラムダ計算で構成される数学的構造は命題論理の命題や証明と対応する。より細かくいうと、N: という型付ラムダ計算の判断文は、数学的には N が 数学的構造
のメンバーということを表し、論理学的には N が命題
の証明ということを表す。豊かな数学的構造を構成できる型付ラムダ計算は、カリー＝ハワード対応を通して、命題論理という純粋に言語的なものとなる。包括原理による集合論や、分出公理を用いた公理的集合論もそうなのだが、言語と抽象と適用によって数学的構造を構成することは、型付ラムダ計算にも受け継がれている、しかし、その言語は命題論理というさらにシンプルなものになっている、これは興味深い。
と、けっこう難しい論文なのだが、だいたいこんな感じかと思う。
読んでいて思ったことを書いておく。数学的構造と命題論理の命題との対応は、具体的にはどのような形となって現れるのだろうか。というのも、カリー＝ハワード対応に現れる命題はあまり言語っぽくない。クラス演算子に登場する開放文は、内容というか意味を持つものである。対して型付ラムダ計算と対応する命題論理にはそのような性格はない。照井先生の本や論文なんかを読んでいると、カリー＝ハワード対応というのは、プログラムの検証に証明論を使い、証明からプログラムを抽出するという相互関係があるという。たしか構成的型理論なんかでは論理学の証明と数学の証明とプログラムの対応はもっと実践的なものになってくる*4。岡本論文では、命題論理の証明をすることで対応する数学的構造に「アクセス」できると書いてあるのだが、この「アクセス」の意味がよくわからなかった。そのあたりをちょっと考えてみたいなあ*5。
もう一つの論文「なぜ意味論はプロセスを含むか」についても。
一つ目の論文は型付ラムダ計算やカリー＝ハワード対応からフレーゲやラッセルのプログラムを再考する感じだったが*6、こちらはデイナ・スコット先生の領域理論からブラウワーの連続性概念を再考するという内容である。
領域理論というのはプログラムの表示的意味論というやつである。表示的意味論というのはプログラムを何らかの数学的構造に対応させる手法だが、スコット先生の領域理論は、プログラムを連続写像に対応させることで再帰的プログラムを最小不動点として構成する。岡本論文では照井先生の「線形論理の誕生」という論文も参照されていて私も見たことがあったのだが、スコット連続は有限呼び出し性と同値になる*7。これがブラウワーの始切片から連続性を定義するという手法と似ているという話である。
領域理論とブラウワーの数学が似ているのは、どちらも生成やプロセスというものに重きを置いているからであろうというのが岡本先生の主張である。これはおもしろい。
後半は、もっと一般的な数学的構造もスコット流の領域として構成するという試みが紹介されているが、私には難しくてわからなかった。
私としてはタイトルの「プロセス」という言葉が気になっている。これはコンピュータ科学でいうプロセスとどう違うのだろうか。調べてみたい。
また、ブラウワーの数学をそういえばよく知らないなあと思った。20世紀後半の構成主義はプログラミングの理論でもあるので普通にロジックや計算機の勉強をしていると出会うのだが、ブラウワーのオリジナルの直観主義はボーッと生きていると見逃してしまうのね。
*1:包括原理は内包公理ともいうやつである。英語でいうと Comprihension Principle なのだが、Comprihension が「包括」とも「内包」とも訳されるっぽい。しかし内包は intention の訳でもあるので、包括のほうが良いと思わます。公理は英語で axiom だが、包括原理は公理として採用されない場合もあるわけで、一般には包括原理と言っておけばよさそうですね。
*2: (単純)型付ラムダ計算がラッセルのパラドクスを回避できる理由は岡本論文では明記されていないけど、まあこういうことでしょう。これは常識なのかな。
*3:それ以外にも包括原理を維持して論理を弱めるという方法もある。具体的には縮約規則を除くことで、これはグリシン論理と言って、同じ号の「科学哲学」に載っている照井先生の論文に解説があると岡本論文に書かれている。
*4:論理学の証明と数学の証明が別物であることを前提するのはなんか可笑しいですね。
*5:「考えてみたい」とか言っておいてけっきょく考えないのが人生ではありますが。
*6:私のまとめだとそんな感じがしないかもしれませんが。
*7:いろいろ前提条件があって。
