SEARCH
検索詳細
倉橋 太志大学院システム情報学研究科 システム情報学専攻准教授
プロフィール
ゲーデルの不完全性定理を中心に,形式的算術の証明可能性に関する研究を行っています.
これまでには次のような研究を行ってきました.
・種々のパラドックスに基づく不完全性定理の証明の分析
・様々な性質をもつロッサーの証明可能性述語の構成
・算術の超準モデルにおける証明構造の分析
・不完全性定理の一般化と理論の証明可能性に関する諸概念の一般化
・述語証明可能性論理の限界の分析
・理論を表現する論理式とその命題証明可能性論理の対応の分析
・証明の論理の算術的完全性定理の拡張
・様相論理における補間定理や不動点定理の分析
不完全性定理に関連する話題については,内容もさることながら,論理式の不動点をとることよって様々な性質が導かれる,という技術的な点にも強く心惹かれています.
研究活動情報
■ 受賞■ 論文
- arXiv:2410.178952025年07月, Journal of Logic and Computation, 35(5) (5), 英語, 国内誌, 国際共著していない[査読有り]研究論文(学術雑誌)
- "不完全性定理の数学的発展" の英語翻訳版2025年06月, Sugaku Expositions, 38(1) (1), 1 - 32, 英語, 国際誌, 国際共著していない[査読有り][招待有り]研究論文(学術雑誌)
- arXiv:2306.072432025年03月, Journal of Logic and Computation, 35(2) (2), 英語, 国際誌, 国際共著していない[査読有り]研究論文(学術雑誌)
- arXiv:2407.005052025年, The Journal of Symbolic Logic (受理), 英語, 国際誌, 国際共著していない[査読有り]研究論文(学術雑誌)
- arXiv:2402.092552024年11月, Mathematical Logic Quarterly, 70(4) (4), 398 - 413, 英語, 国際誌, 国際共著していない[査読有り]研究論文(学術雑誌)
- 2024年09月, The Bulletin of Symbolic Logic, 30(3) (3), 362 - 397, 英語, 国際誌, 国際共著している[査読有り]研究論文(学術雑誌)
- arXiv:2208.035532024年09月, Journal of Logic and Computation, 34(6) (6), 1108 - 1135, 英語, 国際誌, 国際共著していない[査読有り]研究論文(学術雑誌)
- arXiv:2302.118082024年05月, Archive for Mathematical Logic, 63(3-4) (3-4), 391 - 403, 英語, 国際誌, 国際共著していない[査読有り]研究論文(学術雑誌)
- arXiv: 2110.025762024年03月, The Review of Symbolic Logic, 17(1) (1), 178 - 205, 英語, 国際誌, 国際共著していない[査読有り]研究論文(学術雑誌)
- arXiv:2203.021832024年02月, Mathematical Logic Quarterly, 70(1) (1), 37 - 63, 英語, 国際誌, 国際共著していない[査読有り]研究論文(学術雑誌)
- Abstract We study the fixed point property and the Craig interpolation property for sublogics of the interpretability logic $$\textbf{IL}$$. We provide a complete description of these sublogics concerning the uniqueness of fixed points, the fixed point property and the Craig interpolation property.Springer Science and Business Media LLC, 2024年02月, Archive for Mathematical Logic, 63(1-2) (1-2), 1 - 37, 英語, 国際誌, 国際共著していない[査読有り]研究論文(学術雑誌)
- 2024年, Studia Logica (受理), 英語, 国際誌, 国際共著していない[査読有り]研究論文(学術雑誌)
- 2024年, The Review of Symbolic Logic (受理), 英語, 国際誌, 国際共著していない[査読有り]研究論文(学術雑誌)
- arXiv:2306.130492024年, The Journal of Symbolic Logic (受理), 英語, 国際誌, 国際共著している[査読有り]研究論文(学術雑誌)
- arXiv:2305.147622024年, Studia Logica (受理), 英語, 国際誌, 国際共著していない[査読有り]研究論文(学術雑誌)
- arXiv:2107.11356Cambridge University Press (CUP), 2023年12月, The Journal of Symbolic Logic, 88(4) (4), 1469 - 1496, 英語, 国際誌, 国際共著していない[査読有り]研究論文(学術雑誌)
- arXiv:2110.148722023年10月, Studia Logica, 111(5) (5), 749 - 778, 英語, 国際誌, 国際共著していない[査読有り]研究論文(学術雑誌)
- arXiv:2208.035552023年07月, Annals of Pure and Applied Logic, 174(7) (7), 103271, 英語, 国際誌, 国際共著していない[査読有り]研究論文(学術雑誌)
- arXiv:2010.115272022年08月, Mathematical Logic Quarterly, 68(3) (3), 318 - 345, 英語, 国際誌[査読有り]研究論文(学術雑誌)
- arXiv:1909.02761Elsevier BV, 2022年05月, Annals of Pure and Applied Logic, 173(5) (5), 103087, 英語, 国際誌, 国際共著している[査読有り]研究論文(学術雑誌)
- 2022年02月, Studia Logica, 110(1) (1), 165 - 188, 英語, 国際誌, 国際共著していない[査読有り]研究論文(学術雑誌)
- arXiv:1811.12827Duke University Press, 2022年02月, Notre Dame Journal of Formal Logic, 63(1) (1), 35 - 49, 英語, 国際誌, 国際共著していない[査読有り]研究論文(学術雑誌)
- Oxford University Press (OUP), 2021年10月, Journal of Logic and Computation, 31(7) (7), 1716 - 1739, 英語, 国際誌, 国際共著していない
Abstract We introduce and develop a topological semantics of conservativity logics and interpretability logics. We prove the topological compactness theorem of consistent normal extensions of the conservativity logic $\textbf {CL}$ by extending Shehtman’s ultrabouquet construction method to our framework. As a consequence, we prove that several extensions of $\textbf {CL}$ such as $\textbf {IL}$, $\textbf {ILM}$, $\textbf {ILP}$ and $\textbf {ILW}$ are strongly complete with respect to our topological semantics.[査読有り]研究論文(学術雑誌) - Cambridge University Press (CUP), 2021年09月, The Journal of Symbolic Logic, 86(3) (3), 1124 - 1153, 英語, 国際誌, 国際共著していない
Abstract Akama et al. [1] systematically studied an arithmetical hierarchy of the law of excluded middle and related principles in the context of first-order arithmetic. In that paper, they first provide a prenex normal form theorem as a justification of their semi-classical principles restricted to prenex formulas. However, there are some errors in their proof. In this paper, we provide a simple counterexample of their prenex normal form theorem [1, Theorem 2.7], then modify it in an appropriate way which still serves to largely justify the arithmetical hierarchy. In addition, we characterize a variety of prenex normal form theorems by logical principles in the arithmetical hierarchy. The characterization results reveal that our prenex normal form theorems are optimal. For the characterization results, we establish a new conservation theorem on semi-classical arithmetic. The theorem generalizes a well-known fact that classical arithmetic is -conservative over intuitionistic arithmetic.$\Pi _2$ [査読有り]研究論文(学術雑誌) - Wiley, 2021年05月, Mathematical Logic Quarterly, 67(2) (2), 164 - 185, 英語, 国際誌, 国際共著していない[査読有り]研究論文(学術雑誌)
- Springer Proceedings in Mathematics & StatisticsSpringer Singapore, 2021年, Advances in Mathematical Logic: Dedicated to the Memory of Professor Gaisi Takeuti, SAML 2018, Kobe, Japan, September 2018, Selected, Revised Contributions, 77 - 97, 英語, 国際誌, 国際共著していない[査読有り]論文集(書籍)内論文
- arXiv:1907.00306v2The Japan Association for Philosophy of Science, 2020年11月, Annals of the Japan Association for Philosophy of Science, 29(0) (0), 1 - 25, 英語, 国際誌, 国際共著していない[査読有り]研究論文(学術雑誌)
- Cambridge University Press (CUP), 2020年09月, The Journal of Symbolic Logic, 85(3) (3), 1224 - 1253, 英語, 国際誌, 国際共著していない
Abstract We investigate relationships between versions of derivability conditions for provability predicates. We show several implications and non-implications between the conditions, and we discuss unprovability of consistency statements induced by derivability conditions. First, we classify already known versions of the second incompleteness theorem, and exhibit some new sets of conditions which are sufficient for unprovability of Hilbert–Bernays’ consistency statement. Secondly, we improve Buchholz’s schematic proof of provable -completeness. Then among other things, we show that Hilbert–Bernays’ conditions and Löb’s conditions are mutually incomparable. We also show that neither Hilbert–Bernays’ conditions nor Löb’s conditions accomplish Gödel’s original statement of the second incompleteness theorem.$\Sigma_1$ [査読有り]研究論文(学術雑誌) - arXiv:1809.00943Springer, 2020年08月, Archive for Mathematical Logic, 59(5-6) (5-6), 659 - 678, 英語, 国際誌, 国際共著していない[査読有り]研究論文(学術雑誌)
- arXiv:1812.097352020年06月, Studia Logica, 108(3) (3), 597 - 617, 英語, 国際誌[査読有り]研究論文(学術雑誌)
- ELSEVIER, 2019年02月, Annals of Pure and Applied Logic, 170(2) (2), 163 - 179, 英語, 国際誌[査読有り]研究論文(学術雑誌)
- 2018年09月, The Journal of Symbolic Logic, 83(3) (3), 1229 - 1246, 英語[査読有り]研究論文(学術雑誌)
- Springer Netherlands, 2018年04月, Studia Logica, 106(2) (2), 219 - 235, 英語[査読有り]研究論文(学術雑誌)
- Springer New York LLC, 2018年02月, Archive for Mathematical Logic, 57(7-8) (7-8), 1 - 28, 英語[査読有り]研究論文(学術雑誌)
- Springer Netherlands, 2018年02月, Studia Logica, 106(6) (6), 1 - 16, 英語[査読有り]研究論文(学術雑誌)
- Cambridge University Press, 2017年12月, Review of Symbolic Logic, 10(4) (4), 603 - 616, 英語[査読有り]研究論文(学術雑誌)
- 2017年03月, The Journal of Symbolic Logic, 82(1) (1), 292 - 302, 英語, 国際誌[査読有り]研究論文(学術雑誌)
- 2016年09月, The Journal of Symbolic Logic, 81(3) (3), 1163 - 1175, 英語, 国際誌[査読有り]研究論文(学術雑誌)
- 2016年08月, Journal of Philosophical Logic, 45(4) (4), 381 - 398, 英語, 国際誌[査読有り]研究論文(学術雑誌)
- 2016年02月, Annals of Pure and Applied Logic, 167(2) (2), 73 - 94, 英語, 国際誌[査読有り]研究論文(学術雑誌)
- 2014年10月, Journal of Philosophical Logic, 43(5) (5), 999 - 1017, 英語, 国際誌[査読有り]研究論文(学術雑誌)
- 出版社 HP http://www.sobunsha.co.jp/detail.html?id=Z121科学基礎論学会, 2014年03月, 科学基礎論研究, 41(2) (2), 13 - 21, 日本語[査読有り]研究論文(学術雑誌)
- 2013年11月, Archive for Mathematical Logic, 52(7-8) (7-8), 871 - 880, 英語[査読有り]研究論文(学術雑誌)
- 2013年03月, REVIEW OF SYMBOLIC LOGIC, 6(1) (1), 129 - 146, 英語[査読有り]研究論文(学術雑誌)
- 2012年08月, Mathematical Logic Quarterly, 58(4-5) (4-5), 307 - 316, 英語[査読有り]研究論文(学術雑誌)
- 出版社 HP http://www.sobunsha.co.jp/detail.html?id=Z115科学基礎論学会, 2011年05月, 科学基礎論研究, 38(2) (2), 27 - 32, 日本語[査読有り]研究論文(学術雑誌)
- arXiv: 2507.009552025年07月, 準備中, 英語
- arXiv:2506.223482025年06月, 投稿中, 英語
- arXiv:2506.135242025年06月, 準備中, 英語, 国際共著している
- 2025年, 投稿中, 英語, 国際共著していない
- arXiv:2412.082082025年, 投稿中, 英語, 国際共著していない
- 2024年10月, 京都大学数理解析研究所講究録, 2293, 日本語, 国際共著していない速報,短報,研究ノート等(大学,研究機関紀要)
- arXiv.2211.159192024年, 投稿中, 英語, 国際共著していない
- 2023年, 投稿中, 英語, 国際共著していない
- 2022年11月, 京都大学数理解析研究所講究録, 2233, 105 - 122, 日本語, 国内誌, 国際共著していない機関テクニカルレポート,技術報告書,プレプリント等
- 2017年10月, 京都大学数理解析研究所講究録, 2050, 24 - 40, 日本語機関テクニカルレポート,技術報告書,プレプリント等
- 共著, 第2部(証明可能性論理)担当, 共立出版, 2016年03月, 日本語, 本書は数理論理学の基礎的な知識を持つ読者を対象として,様相論理の構文論と意味論,ならびに,数学基礎論の専門家以外にも名前はよく知られているゲーデルの不完全性定理,コーエンの強制法,タルスキの真理論という三つの話題について,それらの基礎から最近の発展までを紹介するものである。様相論理を紹介する第1部は,その部分のみを取り出してコンパクトな様相論理の入門書または教科書として読むことができるように書かれている。三つの章からなる第2部から第4部では,いずれも最初の章で基礎的な話題の概要が丁寧に説明されており,これらの章のみを選んで数学基礎論の基本的な話題を紹介する入門書として読むこともできる。数学的な議論の詳細と最近の発展は各部の残りの二つの章で紹介されている。 数学基礎論は数学や哲学に興味を持つ専門家および非専門家から強い関心を持たれている分野であり,計算機科学や哲学,言語学の基礎でもあることから入門書,教科書,啓蒙書が数多く出版されている。しかし,それらの多くは数学基礎論の古典的な結果であるゲーデルの完全性定理,不完全性定理までの解説にとどまっており,数学基礎論の最近の展開には触れていない。本書はクリプキの可能世界意味論を軸に,証明可能性論理,集合論的多元宇宙論,真理の改定理論という想像力をかきたてる名前を持ち,古典的な数学観,真理観を覆す見方を具体的に提案する最新の理論を紹介することで,これまで専門家以外にはほとんど知られていなかった数学基礎論の新しく深い魅力を伝えるものである。, ISBN: 9784320111486数学における証明と真理―様相論理と数学基礎論―学術書
- 日本数学会 2025年度年会, 2025年03月, 日本語, 日本数学会, 早稲田大学 早稲田キャンパス, 日本国, 国内会議, 国際共著していないスマリヤンの Truth and Provability について口頭発表(一般)
- 日本数学会 2025年度年会, 2025年03月, 日本語, 日本数学会, 早稲田大学 早稲田キャンパス, 日本国, 国内会議, 国際共著していない様相論理と中間論理の Lyndon 補間性口頭発表(一般)
- 第59回MLG数理論理学研究集会, 2025年02月, 日本語, 東北大学, 日本国, 国内会議, 国際共著していない様相論理と中間論理における Lyndon 補間性口頭発表(一般)
- 数学基礎論サマースクール2024, 2024年09月, 日本語, 東北大学青葉山キャンパス, 日本国, 国内会議, 国際共著していない不完全性定理と反映原理公開講演,セミナー,チュートリアル,講習,講義等
- 日本数学会 2024年度秋季総合分科会, 2024年09月, 日本語, 日本数学会, 大阪大学豊中キャンパス, 日本国, 国内会議, 国際共著していない証明可能性の二重様相論理 GR に対する補間定理口頭発表(一般)
- 日本数学会 2024年度秋季総合分科会, 2024年09月, 日本語, 日本数学会, 大阪大学豊中キャンパス, 日本国, 国内会議, 国際共著している有限拡大に制限した本質的不完全性について口頭発表(一般)
- 日本数学会 2024年度秋季総合分科会, 2024年09月, 日本語, 日本数学会, 大阪大学豊中キャンパス, 日本国, 国内会議, 国際共著していないCollection 原理の特徴づけについて口頭発表(一般)
- 日本数学会 2024年度年会, 2024年03月, 日本語, 日本数学会, 大阪公立大学, 日本国, 国内会議, 国際共著している理論の不完全性,決定不能性,分離不能性口頭発表(一般)
- 日本数学会 2024年度年会, 2024年03月, 日本語, 日本数学会, 大阪公立大学, 日本国, 国内会議, 国際共著していない証明可能性-強制様相論理口頭発表(一般)
- 日本数学会 2024年度年会, 2024年03月, 日本語, 日本数学会, 大阪公立大学, 日本国, 国内会議, 国際共著していない必然化の論理 N の拡張論理の有限フレーム性口頭発表(一般)
- 日本数学会 2024年度年会, 2024年03月, 日本語, 日本数学会, 大阪公立大学, 日本国, 国内会議, 国際共著していない局所反映原理に関する保存性について口頭発表(一般)
- 第58回MLG数理論理学研究集会, 2024年02月, 日本語, 東北大学, 日本国, 国内会議, 国際共著していない証明可能性論理 GR の補間定理口頭発表(一般)
- 第58回MLG数理論理学研究集会, 2024年02月, 日本語, 東北大学, 日本国, 国内会議, 国際共著していない必然化の論理 N の拡張論理の有限フレーム性と補間定理口頭発表(一般)
- 第58回MLG数理論理学研究集会, 2024年02月, 日本語, 東北大学, 日本国, 国内会議, 国際共著していない証明可能性-強制様相論理 PF について口頭発表(一般)
- 第2回 ロジック・ウィンタースクール, 2023年12月, 日本語, 愛媛県松山市, 日本国, 国内会議, 国際共著していない理論の不完全性,決定不能性,分離不能性[招待有り]公開講演,セミナー,チュートリアル,講習,講義等
- 証明論研究集会2023 証明論と計算論の最前線, 2023年12月, 日本語, 京都大学数理解析研究所, 日本国, 国内会議, 国際共著していない局所反映原理における保存性口頭発表(一般)
- 日本数学会2023年度秋季総合分科会, 2023年09月, 日本語, 日本数学会, 東北大学, 国内会議, 国際共著していない証明可能性論理 D のカット無しシークエント計算口頭発表(一般)
- 日本数学会2023年度年会, 2023年03月, 日本語様相論理 $\mathbf{IL}^-(\mathbf{P})$ について口頭発表(一般)
- 日本数学会2023年度年会, 2023年03月, 日本語, 日本数学会, 中央大学, 国内会議, 国際共著していない単調性を満たす証明可能性述語の様相論理口頭発表(一般)
- 日本数学会2023年度年会, 2023年03月, 日本語, 日本数学会, 中央大学, 日本国, 国内会議, 国際共著していないFriedman--Goldfarb--Harrington の定理の拡張口頭発表(一般)
- 証明論シンポジウム 2022, 2022年12月, 日本語, 国内会議, 国際共著していない$\mathsf{R}$ と無矛盾な理論の不完全性と決定不可能性口頭発表(一般)
- SAML2022: Symposium on Advances in Mathematical Logic 2022, 2022年06月, 日本語, 京都大学数理解析研究所, 日本国, 国内会議, 国際共著していない証明可能性述語の様相論理[招待有り]口頭発表(招待・特別)
- 日本数学会2021年度秋季総合分科会, 2021年09月, 日本語, 日本数学会, 千葉大学(オンライン), 日本国, 国内会議, 国際共著していない様相算術における選言特性と存在特性口頭発表(一般)
- 日本数学会2021年度秋季総合分科会, 2021年09月, 日本語, 日本数学会, 千葉大学(オンライン), 日本国, 国内会議, 国際共著していない保存性の論理CL およびその拡大の位相的意味論について口頭発表(一般)
- 日本数学会2021年度秋季総合分科会, 2021年09月, 日本語, 日本数学会, 千葉大学(オンライン), 日本国, 国内会議, 国際共著していない述語証明可能性論理の包含関係について口頭発表(一般)
- International Workshop on Gödel's Incompleteness Theorems, 2021年08月, 英語, 武漢大学, 武漢, 中華人民共和国, 国際会議, 国際共著していないInclusions between quantified provability logics[招待有り]口頭発表(招待・特別)
- Celebrating 90 Years of Gödel’s Incompleteness Theorems, 2021年07月, 英語, University of Tübingen, University of Tübingen (Online), ドイツ連邦共和国, 国際会議, 国際共著していないOn the second incompleteness theorem and provability predicates[招待有り]口頭発表(招待・特別)
- 日本数学会2021年度年会, 2021年03月, 日本語, 日本数学会, 慶応義塾大学(オンライン), 日本国, 国内会議, 国際共著していない解釈可能性論理 IL の部分論理に対する Craig の補間定理及び不動点定理について口頭発表(一般)
- 証明論研究集会2020, 2020年12月, 日本語, 国内会議述語証明可能性論理の包含関係について口頭発表(一般)
- 日本数学会2020年度秋季総合分科会, 2020年09月, 日本語, 日本数学会, 日本国, 国内会議, 国際共著していない解釈可能性論理ILの部分論理口頭発表(一般)
- 日本数学会2020年度秋季総合分科会, 2020年09月, 日本語, 日本数学会, 国内会議, 国際共著していない部分保存的な文に対する Bennet の結果の一般化口頭発表(一般)
- 超準解析と数学基礎論のシンポジウム NSA 2017, 2017年12月, 日本語, 早稲田大学, 国内会議Rosser 証明可能性述語と超準的な証明[招待有り]口頭発表(招待・特別)
- Workshop ``Logic and Philosophy of Mathematics'', 2017年07月, 早稲田大学On partial disjunction properties of theories containing PA[招待有り]
- 日本数学会2016 年度秋季総合分科会, 2016年09月不完全性定理と証明可能性述語について(特別講演)[招待有り]
- 数学基礎論サマースクール 2015, 2015年08月, 中国語, 神戸大学, 国内会議証明可能性論理[招待有り]公開講演,セミナー,チュートリアル,講習,講義等
■ 共同研究・競争的資金等の研究課題
- 日本学術振興会, 科学研究費(基盤研究(C)), 2023年04月 - 2028年03月, 研究代表者形式的証明可能性の持つ諸性質の分析
- 日本学術振興会, 科学研究費(若手研究), 2019年04月 - 2023年03月, 研究代表者不完全性定理を通じた形式的証明可能性の研究競争的資金
- 日本学術振興会, 科学研究費(若手研究B), 2016年04月 - 2019年03月, 研究代表者超準モデルと理論における証明構造の分析競争的資金
- 日本学術振興会, 科学研究費(研究活動スタート支援), 2014年08月 - 2016年03月, 研究代表者可証性述語の解析に基づく形式的証明可能性の研究競争的資金
- 日本学術振興会, 科学研究費(特別研究員奨励費), 特別研究員奨励費, 神戸大学, 2012年04月 - 2014年03月, 研究代表者形式的算術の証明可能性について本研究の目的は、形式的体系の証明可能性を表現する論理式である可証性述語の形式的算術における振る舞いについて調べ, そのことを通じて不完全性定理や形式的算術の超準モデルなどの理解を深めることである. 1. ロッサーの可証性述語について ロッサー可証性述語に基づくヘンキン文および反映原理に関する研究を行った, まず, 独立なヘンキン文をもつかどうかが可証性述語の取り方に依存することを示し, Halbach and Visser (2013)による問題を解決した. また, Shavrukov (1991)による問題を解決することで, 反映原理が通常のものと同値でないようなロッサー可証性述語の存在を示し, Goryachev (1989)による結果と合わせて, それらの同値性がロッサー可証性述語の取り方に依存することを明らかにした. これらの結果により, ロッサー可証性述語の性質の理解だけでなく, 形式的証明そのものの構造の理解が深まることが期待される. 2. 算術の超準モデルにおける証明可能性ついて 本研究はこれまでほとんど行われていなかった, 算術の超準モデルにおける証明可能性について分析するものである. 本年度は(a)Con2のモデルでも証明可能的極大でもないようなペアノ算術の超準モデルの存在, (b)ペアノ算術の超準モデルである任意の始切片において証明可能なものが実際より増えているような超準モデルの存在, (c)ペアノ算術の各無矛盾な完全拡大を何らかの超準モデルにおいて定義するようなロッサー可証性述語の存在, を示した. 本結果により, 超準モデルにおける証明可能性や証明の構造に関する基本的な性質が明らかとなった.競争的資金
研究シーズ
■ 研究シーズ- 形式的数学における証明可能性シーズカテゴリ:自然科学一般研究キーワード:数理論理学, 数学基礎論, 不完全性定理, 様相論理, 証明可能性研究の背景と目的:1931年にゲーデルによって発表された不完全性定理によって、命題の真偽と証明可能性には本質的な違いがあり、また証明可能性は計算可能性の概念と密接に関わること、などが明らかになりました。不完全性定理を中心に、証明可能性や証明という概念を理解するための研究を行っております。研究内容:自然数論などの数学の理論を論理学を用いて形式化することで得られる、形式的数学における証明可能性の分析を行っています。特に様相論理などを用いることによって形式的数学とコード化された形式的数学の相互関係を分析し、そのことを通じて証明可能性の構造の理解を深めるという研究を行っています。期待される効果や応用分野:証明可能性関係を形式的体系内で弱表現する証明可能性述語の挙動の分析を通じて、数学における証明の構造への理解が深まることが期待されます。その分析の過程において得られる知見から、証明論・非古典論理・算術の超準モデル・計算理論などに関連する分野への応用も期待できます。