ワシって自分が専門的にやってる分野はごく狭い範囲しか読んでいなくて関係ない哲学分野の事ばかり書いているなあと思い、自分の専門*1である線形論理（を中心とした証明論と計算の理論）に近い所の読書をする事にした。
↑この本には有名な数学の哲学論文の翻訳と解説が載っている。本当は英語の↓この本の方が充実しているのだけどまあまあまあ。この↓内いくつかが↑と被っている。
で、本の中程のダグ・プラウィッツ「証明論の哲学的立場」加地大介訳という論文から読んだ。これは私の専門とも近い話題なので読める！ 1972年の論文らしい。以下思ったことをつらつらと。
プラウィッツ先生は(分析)哲学のノーベル賞であるショック賞(論理学・哲学部門)を受賞している大論理学者である。自然演繹の正規化定理を証明した事で有名（ゲンツェンによって既にそこそこ示されていたという話も聴いた事あるが）。ゲンツェンが自然演繹を導入したのは1930年代だが、プラウィッツ先生の『自然演繹』という本は1965年に出ている。この本から自然演繹の研究は活発化したと思うのだけどその間の30年くらいはどんな扱いだったのだろう。カリー=ハワード同型は最初はヒルベルト式公理とコンビネータの同型性から見つかって、自然演繹と型付ラムダ計算の同型性が言われ出したのはプラウィッツ先生の本の後らしい。
で、この論文について。当時は証明論がモデル論に比べて盛んでなかったようで、証明論も重要だという事を啓発する論文である（今でも証明論てそんなに盛んではないかもしれないけれど…）。
プラウィッツ先生は還元的証明論と一般的証明論という二つがあると述べる。還元的証明論とは、数学をもっと確固たる基礎のある部分に還元しようという目的のもと、証明を分析する研究である。対して一般的証明論は、証明そのものの理解が目指される。照井一成先生の『コンピュータは数学者になれるのか？』では還元的証明論と「構造的証明論」という言葉で区別されていたと思う。
ヒルベルト・プログラムなんかは数学をいわゆる有限的な部分に還元しようとする還元的証明論の試みである。プラウィッツ先生はこのヒルベルト・プログラムと不完全性定理の関係を詳しく解説している。
しかし、プラウィッツ先生ご自身の関心は一般的証明論の方にあった筈である。こちらの方の紹介は短めだが。プラウィッツ先生が発見した自然演繹の規則の反転原理が少し解説されている。これは証明論的意味論の基礎になるものである。これによって、論理結合子の意味が証明の構造的な性質によって説明できるようになる。
ところで還元的証明論を大きく前進させたのはゲンツェンの（カット除去定理による）無矛盾性証明の研究だが、しかし一般的証明論もゲンツェンの研究がなければ生れなかった訳だからゲンツェンは凄いなあ。
私が読んでいるジラール先生なんかも線形論理以降は明らかに一般的証明論の研究者である（それ以前は還元的証明論の研究をして教科書も書いていたが）。なので私もこちらに興味がある。ただしジラール先生は、証明の構造だけでなく、証明から証明への変換(ダイナミクス、インタラクション)、即ちカット除去を更なる研究対象としているが。あと注にGirard, Martn-Löf, Prawitzの共著論文が出る予定とあるのだけれどこれは出たのだろうか？
ジラール先生がダイナミクスに興味を持つのは、証明と計算のカリー=ハワード対応があるからである。ダイナミクスとは計算の実行のダイナミクスでもある。証明を計算と関連させて意味付ける発想はまだ(?)このプラウィッツ先生の論文には現れていない。
あと、ヒルベルトの「形式主義」というのは誤解が多いが、プラウィッツ先生はヒルベルト・プログラムと形式主義を分けて論じてこれを回避しているようだった。
訳者の加地先生の↓この本は最近新装版が出た所で、興味があります。「穴」について形而上学的に論じたユニークな本みたい。
*1:と言える程ではないけど…。なんか他に良い言い方ないんすかね？
