前書き

概要: 直観主義論理といえば、「排中律が不成立」「構成主義」「カリーハワード対応」「定理証明の前提」「様相論理S4に埋め込める」などなど面白そうな話を聞くのだけれど、どこがどうつながっているのかわからなかったので整理してみた。

表記: 言語は1階言語を想定。古典論理をCL、直観主義論理をILとも略記。自然演繹の証明系は古典論理の場合NK、直観主義論理の場合NJと略記。シーケント計算は古典論理の場合LK、直観主義論理の場合LJと略記。論理式、特に妥当式を<と>で括って表記（例：<排中律>）

1. 証明能力はどれくらい強いのか？

証明系という側面から見ると、直観主義論理はNJであれLJであれ「古典論理（の公理ないし推論規則）に制限を加えて証明能力を弱めた体系」にすぎない。なので必然的に**直観主義論理はどこまで古典論理の証明能力に迫れるか？**が気になってくる。

よく知られているように直観主義論理では<排中律>や<二重否定除去>が定理でない（逆に排中律を公理にすればor背理法を推論規則にすれば証明能力が同等となる）。しかし直観主義論理の証明能力は一般に思われている以上に強い。

例えば否定翻訳という操作によって「直観主義論理は古典論理を包含する」といった一種パラドキシカルな言明が成立する。ざっくり言うと古典論理での任意の理論Tでの任意の定理φに対して（古典論理で）同値変形をしたφNという文が存在する。直観主義論理ではTのサブ理論TNにおいてφNが証明できる。

ペアノ算術(ILではハイティング算術と呼ぶ)のようにある種の「性質の良い」理論においてはもう少し両者の近さが言える。A翻訳という操作を通じて「ペアノ算術の理論における∀∃文ひいてはパイ0-2言明の形の定理は直観論理でも（つまりハイティング算術でも）定理である」ことがいえる。

参考:

2. 証明系は構成主義を含意するか？

直観主義論理はよく構成主義であるといわれるが、証明系は前述のとおり古典論理の証明系を弱めただけで構成的な部分は見当たらない。つまり証明能力を弱めたことと構成的であることは一瞥しただけでは無関係に見える。この二つはどうつながる？

一つの方法は（後述するが）意味論で応えるものだ。しかし意味論に訴えなくても以下のメタメタな言明で一部応えることができる:

文P⋁Qが証明可能ならば文Pと文Qの少なくとも一方は証明可能

この言明（選言特性と呼ぶ）は一般には古典的な理論では成り立たない。よって古典論理と直観主義論理の違いとして際立っているだけでなく、その内容が直観主義の構成的な性質を反映している。

参考:
- PDF: 直観主義論理への招待 - RIMS, Kyoto university - 京都大学, 特に3章
- 書籍: 小野『情報科学における論理』 5章
- Disjunction and existence properties - Wikipedia

3. どの意味論を採用すべきか？

以下ざっと意味論の復習をしてから直観主義の意味論に話を移す:

証明系においては論理式は単なる記号列だし、導出/証明は単なる記号変形ゲームである。「論理式をどう読むか？その時推論規則と公理はどう読めるか？」は読者に委ねられている。うまい読み（＝モデル）が存在すれば現実世界で役立つし、そのモデルで証明系がちゃんとしているか（＝完全性）も決まる。つまり完全性はモデルと証明系のペアで定義される性質となる。

さて、意味論では原子命題記号Pや論理語(例えば⋀)ですら意味付けされるのを待っている。例えば電気回路の意味付けでは A,B ⊢ A⋀B は「AND素子の二つの入力の電圧がHighのとき出力の電圧はHighになる」と読むので、このモデルでは、命題や論理語といった当初論理学を創始した際に想定した概念は消え失せているし、実際それでもうまく回る。

直観主義論理においても、論理式の読み方が複数あり、それぞれ別の意味論につながる。逆に言うとどのように読みたいかで採用すべき意味論が変わる。BHK解釈は構成主義的な意味付けを前面に押し出すので構成主義的な立場を取る人には相性がよく（その分真理概念がわかりにくくなる）、カリーハワード対応にも関係がある（後述）。フレーム解釈は、様相論理の意味論として成功を収めたものを輸入したものであり、真理概念の認識的な側面を明らかにする。

参考

4. 排中律の反例は？

フレーム解釈についての話。古典論理では議論領域 U と各種記号の解釈I の二つ組(U,I)をモデルとして与えると文の真偽値が定まる。フレーム解釈では可能世界の集合M とその到達可能性関係 ≦ を加えた四つ組 (M,≦,U,I)をモデルとして与えると文の真偽値が定まる。

特に、論理語の解釈の違いが直観論理と古典論理を明確に分ける。例えば「¬Aが真である」と「Aは真でない」は明確に区別される。前者は他の到達可能な世界に依存して決まり、後者は単にその世界での付値のみで決まる（注：Aが原子式の時）。

古典の時と真理概念が大きく変わらない（というか真理概念の拡張な）ので古典論理と直観論理の違いを比較できる。<排中律>の反例を挙げることさえできる（二つの世界 w1 ≦ w2 を考え w1 では p が真でなく w2 では p が真であるとき w1 において p⋁¬p は成立しない）。証明不可能性を示すより反例を挙げる方がインパクトが大きい（と私は思う）。

様相論理的な観点でフレーム解釈を見る。フレームに対して反射性・推移性を課すのでS4っぽい。加えて付値は遺伝的なものしか許さないという制約を課している。これにより「真だった文が、後になって真でなくなった」ということが避けられる。また議論領域は単調性を満たす（後ろの世界には前の世界の対象が必ず存在する）ので量化に伴う哲学的な議論（固定指示等）は少なくてすむ。

最後にいくつかの補足：フレーム解釈とLJ で完全性定理が成立する。命題論理でのフレーム解釈とハイティング代数は密接に関連する。

参考:
- 書籍: 小野『情報科学における論理』 5章

5. なぜ直観主義は構成主義なのか？

BHK解釈についての話。3章で述べたように意味論としてBHK解釈を採用すると直観主義論理の構成的な側面が強調される。BHK解釈では論理式φに対して「φは真である（もしくは偽である）」という意味付けをするのではなく「φには証拠がある（もしくはない）」という意味付けをする。このことは、表面上（つまり日本語として）言い換えただけではないことが、論理語の解釈をいくつか見ればわかる:

A⋀Bに証拠があるとは、(a,b)という対を証拠として構成できることだ
- ここで a, bとはそれぞれ A, Bの証拠
A→Bに証拠があるとは、a を入力として b を出力する関数 f を証拠として構成できることだ
- ここで a, bとはそれぞれ A, Bの証拠

つまり、古典論的解釈では A, B(の真偽値)の 2bit の情報さえあれば A⋀BもA→Bも意味付けできることになるが、BHK解釈では (a,b)やfを実際に「作って提示」しなければいけないので構成的であるといえるし、より強い条件を課しているといえる（尤も前者を作るのは簡単なので後者の関数をどう作るか？というのが主要な課題になる）。

任意の論理式φに対して上記の解釈を再帰的に行うことにより φの証拠の有無という概念を定義できる。一方、そこで登場する 「原子式＝基本述語の証拠とは具体的にどのような存在物か？」や「関数という言葉で示されている存在物は何か？」に対して何も答えていないことがわかる。古典命題論理の論理式を電気回路としての意味付けをしたときに「電圧」という語の意味付けをしていないのと同じことが起きている（3章の例）。これは欠陥ではなくて、むしろ現実に沿った意味付けができることを意味している。通常は以下のような対応付けをする（Kleene's realizability theory）:

「原子式の証拠」に「（基本述語が等号の場合）項同士が一致するかのアルゴリズム」
「関数」に「計算可能関数」
- チューリングマシン or 型無しラムダ計算 or 帰納的関数で定義可能な関数

一方、別の意味付けをしてもよい（カリーハワード対応）

「原子式の証拠」に「原子式の型」（例: int型）
- ついでに原子式に任意の外延を対応付ける(例: 整数全体）
「関数」にラムダ抽象

こうすることで直観論理の意味論とラムダ計算の計算規則が結びつく（意味論＝読み方だけでなく、形式体系＝計算規則もNJとぴったり一致する）

Brouwer–Heyting–Kolmogorov interpretation - Wikipedia
Realizability - Wikipedia
PDF: 亀山『計算論理学講義資料』筑波大学

6. その他色々

定理証明との絡みをまとめたい
コメント・つっこみ歓迎です
様相論理に埋め込む話（）もまとめたい