秋吉 亮太

元々の専門は数学・論理学の哲学および数理論理学、哲学的論理学、理論計算機科学（タイプ理論）で、「証明とは何か」という哲学的問いが私の研究の基礎にあります。近年ではスマートシティ、ロボット倫理、自然言語処理（日本語の談話理論）といった分野にも関心が広がってきました。

現代の数学の哲学は20世紀初頭に勃興した数学基礎論論争をきっかけとして始まり、当初は哲学的議論と数学的発展が並行していました。現在では専門化が進んだこともありそれぞれ比較的独立に研究されていますが、私は数理論理学（証明論、スタンフォード大学のグリゴリー・ミンツ氏との共同研究）や理論計算機科学（型理論、京都大学数理解析研究所の照井一成氏との共同研究）への寄与をすると同時に数学の哲学をより現代的文脈で研究してきました。特に、ヒルベルトの形式主義やブラウワーの直観主義、そしてフレーゲの論理主義といった20世紀初頭の論理哲学に強い興味を持っており、「証明とは何か」という観点からこれらの学派の共通基盤を探ることを目標としています。ここ数年は、数学の証明論的意味論を展開するプロジェクトを進めています（パリ大学アルベルト・ナイーボ氏との共同研究）。

数学の証明の形式化(IsabelleやCoq、Minlogなど)にも強い興味を持ち、計算機科学的／自然言語処理的な観点からも証明とは何かという問いを探求しています（慶應大学の峯島宏次氏との共同研究）。こうした研究の哲学的な背景としては、フッサールの論理哲学（特に『論理学研究』周辺）にそもそも興味があり、判断論や記号による知識の拡張という問題を研究してきました（岡山大学の植村玄輝氏との共同研究）。

 最近は日本を代表する論理学者である竹内外史の論理哲学に関するプロジェクトを進めており、その哲学的な背景（特に西田幾多郎の哲学）を掘り下げつつ全体像を描くことを目指しています（ロレーヌ大学アンドリュー・アラナ氏との共同研究）。さらに、関連する研究として東洋で展開されてきた自己の哲学をデジタルツインやVRへ応用する研究や、東洋哲学を背景としたロボット倫理の研究も進めてきました（京都大学の出口グループとの共同研究）。そして、こうした哲学の実社会へ応用にも強く興味を持っていて、 「よりよいスマートWEを目指して：東アジア人文社会知から価値多層社会へ」（日本学術振興会 課題設定による先導的人文学・社会科学研究推進事業、学術知共創プログラム）の人的交流グループのリーダーを務めています。

より具体的には

(I) ゲーデルの不完全性定理とヒルベルト・プログラムの関係　　　　　　　　　　　　　　　　　　　　　　　　
(II) ゲンツェンの複数の無矛盾性証明の再解釈
(III) ブラウワーのバー帰納法の証明の証明論的再解釈
(IV) 初期フッサールの論理哲学（記号による知識の拡張、判断論）
(V) フレーゲの論理体系の証明論的分析（判断論）
(VI) 直観主義論理の論理定項の意味、証明論的意味論
(VII) 高階算術の非可述な部分体系、並びに高階型理論の証明論（カット消去定理、順序数解析）
(VIII) 構成主義数学（点を仮定しない位相空間論）
(IX) 竹内外史の論理思想（無矛盾性証明の意義、形式主義の哲学）
(X) デジタルツインやVR（志向性）の論理
(XI) ロボット倫理における主人-奴隷モデルのオルタナティブ　
(XII) スマートシティについての産学官連携プロジェクト　　
(XIII) 推論的観点からみた日本語の談話関係　　　　　　　　　　　　　　　　　　　　　　　　　

などを中心に哲学・数理論理学・計算機科学の三方向から研究しています。