| Research Abstract |
今年度は,第一に,ゲンツェンの無矛盾性証明に関する研究を行った.従来,ゲンツェンの三つの無矛盾性証明(1935～1938年)は異なるものであると考えられてきたが,実は統一的動機を持ったものとして解釈できることを提言した.このために,論理学・数学的アプローチと,歴史的,哲学的アプローチの両方を用いた.論理学・数学的手法としては,現代証明論の手法であるミンツ=ブフホルツの『無限的証明図のための有限的記法』を用い,三つの無矛盾性証明が統一的に再構成・解釈できることを数学的に根拠づけた.また,ゲンツェンのこれまでに注目されてこなかった講演も読解するなど,論理哲学史的な側面に関する根拠づけも試みた.これらの根拠を元に哲学的分析を行い,ゲンツェンの三つの証明が統一的に解釈できることは決して偶然的ではなく,ミンツ=ブフホルツの手法の背後にある「無限的な証明図のコード(プログラム)としての有限的な証明図」というアイディアに基づいていることを指摘した.そして,無矛盾性証明とは,コード(プログラム)としての有限的な証明図を実行するという試みとして解釈できるのではないか,という提言も行った.これらの結果をまとめた論文を,慶應大学の高橋優太氏と作成・投稿し『科学基礎論研究』に受理された.
第二に,直観主義者の創始者であるブラウワーのバー定理の証明(1927年)は,数学的ではない仮定(以下,「根本仮定」)に依存しているとしてこれまで扱われてきたが,実は数学的な仮定として解釈できるのではないか,ということに気づき,この点に関して研究を行った.なお,バー帰納法とは,整礎な木の上の帰納法であり,直観主義数学を展開するにあたっての根本原理の一つである.実は,この原理は,直観主義数学において,ブラウワーの証明が数学的ではないとされてきたために,単に公理として仮定される.研究の具体的内容としては,ブラウワーのバー帰納法の証明を,現代的証明論のΩ規則で解釈できるのではないか,という提言を行った.特に,ブラウワーが根本仮定を置かざるを得なかった理由は,Ω規則における非可述性の問題と同じであることを指摘した.また,この成果をいくつかの国際ワークショップで発表し,哲学者,論理学者,数学者のいずれの側からも好評を博し,活発な議論を行うことができた.さらに,この成果のスケッチを来年度ギリシャで開催される国際会議「世界哲学者会議」に投稿した.Ω規則は,本来直観主義と対立すると考えられてきた形式主義の伝統に属し,さらには1970年代後半になって導入された手法であるため,このような洞察は哲学的,数学的にだけではなく,歴史的にも興味深いと思われる.Ω規則がブラウワーの証明論の数学的モデルになっていることを完全に厳密に示すには,まだ数学的細部を詰める必要があり,それは来年度の課題であると考えられる.そして,数学的細部を詰めることができた際には,直観主義解析の順序解析が達成できると考えられ,数学的な結果にもつながると思われる.
|
| Current Status of Research Progress |
Current Status of Research Progress
1: Research has progressed more than it was originally planned.
Reason
今年度は初年度にも関わらず,一本の論文(上記のゲンツェンに関するもの)を査読付きの学会誌における受理までもっていくことができ,さらに,ブラウワーのバー帰納法に関して再解釈のアイディアを得て,発信することができた.両者ともに,数学的・論理学的な道具立てを用いるのみならず,論理哲学史上非常に重要な成果の再解釈という哲学・歴史的な含みを持つ結果を出すことができた.また,これらの結果を,国内学会のみならず,国際的な学会で発表し,高評価であったことも意外であった.
|
| Strategy for Future Research Activity |
来年度は,まず,ブラウワーに関する論文を査読付きの国際学会誌から出版することを目指す.また,スタンフォード大学ミンツ教授との共同研究の成果も,なるべく早くに査読を通過させ,査読付きの国際学会誌から出版することを目標としたい.研究の方策としてはこれまでと同様であるが,来年度は,2013年2月に申請者を訪ねてきたベルギーのゲント大学の若手研究者とのディスカッションを元に,より数学的な課題にも取り組むことを予定している.特に,帰納法を制限した場合の,非可述な体系の順序解析,および,ブラウワーのアイディアをブフホルツのΩ規則を用いて厳密に再構成することを達成したい.そして,必要に応じて,順序解析の世界的な専門家を訪問することを予定している.
|
