タブローは如何にして構文論か
この記事は、2021年ごろに書いたもので、ずっと公開するか迷っていたら忘れていたものです。少しだけ手直しして、今更ですが公開します。今見ると色々拙い部分があって、文章的な部分はもちろん、内容的にも、特にcut除去まわりに全く言及していないのが結構まずいと思っています。あと、構造射だけでいいみたいなこと言ってますけど普通にmeetの普遍性も要る気がします。話半分に読んでください。
少し前に、哲学者で学部生向けに論理学を教えている山口尚先生がこんなことをつぶやいていた。
《タブローは本質的に何を行なっているのか》は、私はまだよく分かっていない。
— 山口尚 (@yamaguchi__sho) December 30, 2021
例えばジェフリーの教科書はタブローを構文論のひとつとして紹介するが《タブローがいかなる意味で構文論なのか》を私はまだ理解していない。何か案があるひとには聞いてみたい。
twitterで「タブロー 構文論」みたいに調べてみると、同様の疑問を抱いている方がちらほらいるようなので、自分なりに考えたことを書いてみようと思う。念の為注記しておくと、僕の専門と数理論理学との間には、遠いとは言えないぐらいの距離感がある。一応圏論の知識を使うが、圏の定義ぐらいがわかれば読めるようにした、と思う。基本的な普遍性（積、余積など）については理解している必要があるかもしれない。
線形論理の専門家であるHyland氏はかつて"Abstract is Concrete"*1という標語を掲げていたらしい。その意味するところは次のようにまとめることができると思う。
構文論とは、自由生成された意味論的構造である。
もちろんこれは（理想的には）みたいなカッコ書きが必要な主張ではあるのだが、どうやら簡単な論理たちに制限すれば基本的にうまくいく指針らしいので、この標語に従ってタブローを解釈してみようと思う。
さて、古典命題論理の「意味論的構造」とはBoole代数だ、ということはとりあえず認める*2。Boole代数には同値な定義が複数あるので、ここでの定義を固定しておこう。
Boole代数とは5つの演算（引数の数は左から2, 2, 1, 0, 0）をもつ代数
$$
B:=(B, \land, \lor, \lnot, \bot, \top)
$$
であって、次を満たすものである。
$$
(a\land b)\land c=a\land (b\land c),\ (a\lor b)\lor c=a\lor (b\lor c)
$$
$$
a\land b = b\land a,\ \ a\lor b = b\lor a
$$
$$
(a\land b)\lor c=(a\lor b)\land (a \lor c)
$$
$$
(a\land b)\lor a = a, \ \ (a\lor b)\land a= a
$$
$$
a\land \lnot a = \bot,\ a\lor\lnot a =\top
$$
（このように代数的に定義されれば、Boole代数の間の射（準同型）も自明に定義できる。つまり関数であって、これらの演算を保つものである。）
演算子の組み合わせからなる項とそのあいだのイコールだけでかけるこのような代数（等式理論と呼ばれる）に対しては、自由代数と呼ばれるものを構成することができる。ここでは「自由生成された」をこの意味でとる。数学の分野では自由群や自由ベクトル空間などがこの例だが、Boole代数に対しては、命題論理式のなす集合を同値関係で割って得られるBoole代数（Lと書くことにする）が自由Boole代数となっている。このとき要素命題は生成元に対応している。
Hyland氏のアイデアは、そもそもこの自由Boole代数L内での計算*3を（古典命題論理の）構文論と呼んでしまおう、というものだ。
この時点で感のいい方は気づかれると思うが、このような構文論の定義は同値関係で割る、という操作の時点でそもそも証明=構文論を使ってしまっているのである意味循環している。しかし、上述したHyland氏の標語の意図していることは、構文論の定義というよりは、様々に考えられる「構文論」全体を数学的対象として取りまとめることにある。別の言い方をすれば、彼の提示しているものは、ある体系がその論理の「構文論」に属すかを判定するメタ基準であり、自然演繹やシーケント計算のようなものとは次元の異なるものである。
（なんでわざわざこんなことをするのかといえば、古典的でない種々の論理、とくに彼にとっては線形論理の、（歴史的に成熟していないがゆえに境界がより漠然としがちな）「構文論/意味論」を理解することにある、のだと思う。）
これは私見だが（というか全部私見なのだが）、"Abstract is Concrete"とは構文(=意味論的構造のAbstract)をConcreteな意味論的構造たちの一種とみなすことの謂であるとともに、Concreteな証明計算=構文論を数学的構造=Abstractとみなすことの謂でもあるのだろう。
さて、Boole代数は半順序集合であり、特に圏である。今、Boole代数 Bを一つ固定しよう。Bを圏とみなしたとき、その対象は単にBの台集合の元であり、２つの元の間の射は存在すれば一意なものであって、
$$
a\to b\ \ \mathrm{in}\ B
$$
は
$$
a=a\land b
$$
と同値である。
初めに戻ろう。山口先生のツイートで提起されている問題、「タブローは本質的には何を行っているのか」に対する僕の提案は以下のように書ける。あとで説明するので、とりあえず主張を連続して述べる。
タブローとは、上述の自由Boole代数Lにおいて、生成元とその補元からmeetとjoinのみを使って生成される元から、ボトム(=始対象)への射をjoinの普遍性と"構造射"のみから構成する操作のことであり、この意味でタブローは構文論だといえる。
さらに、タブローによる充足可能性証明を正当化する次の定理aは本質的にはグリベンコの定理から従う。
定理a: Lにおいて、ボトムへの射が上述の構成で得られないなら、そのような射は存在しない。
（山口先生のツイートには「タブローにかんする健全性定理および完全性定理（ジェフリーの教科書はその証明を行なう）を、いわば「わざわざ示すまでもない自明な真理」にしかねない。」とあるが、これに対する一つの説明？というか分析？として、タブローではグリベンコの定理が隠されていることをいえるのではないだろうか。グリベンコの定理が特に完全性の証明にとって本質的であることは、現代的な数理論理学の入門書にもしばしば書かれている。例えば『現代数理論理学序説』(小野寛晰 古森雄一)など。）
未定義語が大量に出てきたので解説が必要である。まず、ボトムとは上のBoole代数の定義で出てきたボトム記号で表現されるLの元であり、始対象というのはその圏論的な特徴づけである。当然、論理学的には矛盾を表現する。
始対象と記したのはそれが純粋にL内部の特徴づけで得られることを明示するためである。つまり、始対象の存在は構文論的な主張である。論理学的には爆発律と対応するだろう。
次にjoinとその普遍性について。日本語だと例えば結びとか呼ばれるのだがあまり一般的でない気がするのでjoinのままにしている。ここでは選言記号で表現されるLの二項演算のことで、一般には前順序集合における余積coproductの別名である。圏論的な概念であり、したがってその定義と普遍性は全く同じものである。具体的には、
$$
a\lor b \to c \mathrm{\ \ \ in\ }B
$$
と
$$
a\to c\mathrm{\ \ in\ }B\ \ \&\ \ b\to c\mathrm{\ \ in\ }B
$$
との同値性で定義される唯一の元がjoinである。普遍性から得られる射、はこの同値性から導出される射、と言い換えて良い。そして、これは選言を特徴づける規則と同一視できる。
"構造射"はここでの定義であるが、単にmeet(joinの双対)の射影
$$
a\land b\to a, \ \ a\land b\to b
$$
及び、補元とmeetの関係から得られる射
$$
a\land\lnot a \to \bot
$$
のことである。
ここまで書けばすでに気づいていると思うが、これら一連の射たちは命題論理の直観主義的な構文規則たちを圏論的に言い換えただけである。
なぜ言い換えたのか、それは僕の主張の核心が タブローとはLにおける特殊な図式追跡を簡略化したものである という点にあるためである。*4
この非常に重要な点は具体例を提示して説明するべきものだが、あいにくnoteは図を書くのには向いていないし、なにより残念ながら手書きのノートを書く僕の気力がわいてこないので、本当に申し訳ないのだが興味のある方には手を動かしてもらいたい。タブローには様々な流儀があるが、ここに書いてあるグラフ図式のタブローが最も整合すると思う。他の流儀の場合でも、グリベンコの定理を考慮した直観主義的な構文論と考えればうまくいくのではないか。
最後にグリベンコの定理を説明しておく。この定理は古典論理と直観主義論理の関係を記述する定理であり、その帰結の一つは、論理式の(有限)集合が古典論理において矛盾的であることと、直観主義論理において矛盾的であることが同値になる、というものである。
明らかに、矛盾的になる、と、ボトムへの射が存在する、は同値である。上述の通り構造射とjoinの普遍性による射の構成は直観主義論理の証明と対応しており、上で書いた定理aは、これらの射がLでの射（=古典論理の証明）を尽くす、といっているので、ほとんどグリベンコの定理と同じものである事がわかるだろう。
*1: リンク先の6ページ目。
*2: Boole代数より"Pre" Boole代数と呼べるような構造（前順序集合であって、有限双完備かつ補元をもつもの）を選んだほうが正確かもしれない。
*3: L内での計算とは、Lを圏とみなしたときの図式追跡と考えて差し支えないと思う。
*4: 線形論理や証明網にはあまり詳しくないのだが、タブローは証明網の亜種なのではないか、という提案に言い換えられるかもしれない。(2024追記: 少しだけ勉強した結果、こっちで見た方が普通に良さそうに思えてきました。というか、証明網がそもそもタブローっぽいアイデアを線形論理に使おうとしている側面があると思います。とはいえ、証明網がいかにして構文論か、という問題に答えるにはHylandの見方が有用、というかHylandのそもそもの目的はそちらに近いと思います。相変わらず証明網には詳しくないままですが…）