証明論 (1): 証明論とは何か。 [証明論]

先日の月曜、証明論の授業に出てきました。

ぼくは聴講生なので成績等を気にする必要がまったくなく、ゆえに、ノートも取らずにぼけーっと話を聞いているだけだったのですが、それだと聞いたことが右から左となってしまいもったいないので、授業の内容をかんたんにまとめておくことにします。

• 証明論ってそもそも何？
  数学における証明を数学的に研究する学問。

• 何でそんなことしようと思ったの？
  直接的には、ブラウワーの「古典数学のやり方だと矛盾が導出されるかもしれない」という危惧に応えるため。（「数学の証明ってのはこうこうこういうふうに形式化できて、そういう形式化された証明体系を分析すれば『この体系からは矛盾は証明されないよ』ってことが分かる」ということを言おうとした）

• で、そのために具体的に何するの？
  まず、数学における言葉づかいをきちんと定義する。そのうえで、そうした定義をつかって「これはまあ議論の余地なく正しいよね」ってことを記述して、ある言明（数学では通常「定理」と呼ばれる）を「これはまあ議論の余地なく正しいよね」ってことに推論規則（たとえば、「人はみんな死ぬ」「ソクラテスは人である」という前提から「ソクラテスは死ぬ」という結論を導き出すときにつかうようなやつ）をつかって導き出す。そのときの導き出しのあれこれ（証明の複雑さ、とか）を検証する。

• それと「この体系からは矛盾は証明されない」ってことはどう関係するの？
  そういう「導き出しのあれこれ」の検証を通じて、数学の「核」となる部分（具体的には算術）にかんする命題の証明は何であれある一定の複雑さに収まることを示し、そして、その程度の複雑さの証明内では矛盾は証明され得ないということを示す、というのが基本戦略。

• でも、この講義はいちおう哲学科の講義でしょ？　証明論と哲学のかかわりは？
  まず「数学の無矛盾性」というテーマ自体、哲学的なもの。また、「言葉の意味とはそもそも何か」を探求する方法のひとつに「言葉の意味とはその推論における働きにある」とする証明論的意味論というものがあり、それを理解するには言うまでもなく証明論の知識が必須。そして、証明論的意味論にかぎらず意味論一般と哲学は深いかかわりがある。（そもそも、「……とはそもそも何か」という問いの裏には、「……」に何が代入されようとほぼかならず哲学の影があることが多い）

……ってことが、証明論のパイオニアであるゲンツェンの原論文読解を軸に掘り下げられるようです。

（じっさいの授業ではこうした「証明論とは何か」にかんする説明のあと、基本概念（「シーケント計算とは何か」など）の解説と、シーケント計算における論理演算子の導入と除去規則が説明されました）