以下の要領でCAPEレクチャーが開催されます。奮ってご参加ください。
日時:11月26日(木)18:00-19:30
場所: 京都大学文学部校舎1階会議室( 8番の建物)
スピーカー: 秋吉亮太 博士(早稲田大学 高等研究所)
タイトル: 形式主義の新展開に向けてー竹内外史を手がかりにー
アブストラクト:数学の哲学の文脈における形式主義はヒルベルトによって1920年代に導入され,その目的は有限的な対象に関する有限的な操作のみを許す「有限の立場」において,形式化された数学の無矛盾性を証明することにあった.ゲーデルの不完全性定理(1931年)によってこのプログラムが実行不可能であると受容された後,ゲンツェンが有限の立場を拡張することでペアノ算術の無矛盾性を証明した(1935, 36, 38年)ことはよく知られている.
戦後の混乱期の中で,金沢出身の論理学者である竹内外史(1926-2017)はこのプログラムを高階へと拡張することを構想し,高階論理の式計算体系を定式化してそこでカット消去定理が成り立つことを予想した(GLC予想,1953年).竹内は1950年代にGLC予想の部分解を何度も出版しており,1958年には解析学が展開できる程度の体系の無矛盾性証明を出版している.なお,この時期に竹内は『科学基礎論研究』などに哲学的な論文を発表している.特に,無矛盾性証明に必要な順序数とその身分に関して,竹内は様々な考えを述べている.
1960年代以後,スタンフォードのクライゼルやフェファーマン,ミュンヘンのシュッテをその源流として,竹内の結果をよりわかりやすく証明してさらに拡張しようとする試みが盛んに行われた.(発表者が専門としているブフホルツのΩ規則は,この流れの中で登場した無限個の前提をもつ推論規則である.)この流れにおいては,証明論の目的は「形式体系の無矛盾性を証明するのに必要な最小限の順序数」と専ら数学的に定義されることが多く,現在では「順序数解析」の名前で知られている.
これまで竹内の証明論はその数学的な側面に注目が集まってきたと言ってよいが,上で述べたように(主に日本語で)哲学的著作が残されている.本発表ではこれらの著作を分析し,その背景を探ってみたい.より具体的には,竹内が「有限的」であると主張する順序数の整列性の証明を取り上げる.そして,京都学派の哲学との繋がりを指摘することで,竹内の証明論に対するヴィジョンをスケッチしてみたい.
本研究はパリ第一大学哲学科アラナ氏との共同研究に基づいている.
関連