JAIST Repository: 多重視点の証明解析による逆数学の汎用化・深化とその応用

Japan Advanced Institute of Science and Technology

JAIST Repository

Title

多重視点の証明解析による逆数学の汎用化・深化とそ

の応用

Author(s)

横山, 啓太

Citation

科学研究費助成事業研究成果報告書: 1-12

Issue Date

2020-06-01

Type

Research Paper

Text version

publisher

URL

http://hdl.handle.net/10119/16734

Rights

Description

若手研究(B), 研究期間：2016∼2019, 課題番号

：16K17640, 研究者番号：10534430, 研究分野：数理

論理学

北陸先端科学技術大学院大学・先端科学技術研究科・講師

科学研究費助成事業  研究成果報告書

Expanding reverse mathematics with multiple viewpoints

１０５３４４３０ 研究者番号： 横山 啓太（Yokoyama, Keita） 研究期間： １６Ｋ１７６４０ 年 月 日現在 ２ ６ １ 円 3,100,000 研究成果の概要（和文）：本課題では、数学の定理やその証明の難しさ・複雑さを数理論理学の視点から評価・ 分析する、逆数学と呼ばれる研究を複数の視点から推し進めた。特に、組み合わせ命題ラムゼイの定理の評価分 析において長年の未解決問題であった２次元無限ラムゼイの定理の「証明論的強さ」すなわち無矛盾性証明の困 難さを確定する問題を解決し、さらにそれを理論計算機科学における停止性検証に応用する手法を考案した。 さらに有限組み合わせ命題の順序数を用いた解析手法を証明論における証明の長さの分析に応用や解析学におけ る新たな逆数学現象の発見等、関連研究を推し進め、逆数学研究の基盤を拡張した。

研究成果の概要（英文）：In this project, we investigated the complexity and difficulty of

mathematical theorems from the view point of reverse mathematics. Especially, we developed some new techniques to analyze the strength of combinatorial principles such as Ramsey's theorem, and solved a long-standing open problem on the proof-theoretic strength of Ramsey's theorem for pairs.

Besides the above, we introduced some arguments to apply the above result and related techniques to the termination analysis, the study of sizes of proofs, found a new phenomenon on the reverse mathematical study of functional analysis, and expanded the field of reverse mathematics with those new points of view.

研究分野： 数理論理学 キーワード： 数理論理学 証明論 逆数学 算術 数学基礎論 ラムゼイの定理 組み合わせ論 計算可能性理論 ２版 令和 研究成果の学術的意義や社会的意義 2次元ラムゼイの定理の証明論的強さにおける長年の問題の解決とそのための手法の導入は逆数学研究における マイルストーンとなり、逆数学や証明論分野の国際会議で関連する多くの話題が取り上げられたほか、ウエブジ ャーナル Quanta Magazine でも取り上げられた。また、上の結果により、2次元ラムゼイの定理の強さがヒルベ ルトの還元主義プログラムの視点で十分弱いということが解明されたため、この結果の哲学的意味についても議 論がなされた。 ※科研費による研究は、研究者の自覚と責任において実施するものです。そのため、研究の実施や研究成果の公表等に ついては、国の要請等に基づくものではなく、その研究成果に関する見解や責任は、研究者個人に帰属されます。

様 式 Ｃ−１９、Ｆ−１９−１、Ｚ−１９（共通） １．研究開始当初の背景 数学で扱われる諸定理・諸命題の強さ・複雑さの論理学的尺度による評価分析は、数学基礎論 の主要テーマとして様々な形で研究されてきた。本課題では特に次の 3 つの尺度に着目した研 究を構想した。 (1) 計算的: 集合の計算不可能度合いを評価する「扱う集合の複雑さ」 (2) 証明論的: 無矛盾性や帰納法の強さに対応する評価である「導出される関数の増加速度」 (3) 構成的: 直観主義論理に基づき論理公理の複雑さを評価する「必要な排中律命題の強さ」 各尺度による諸定理の評価はそれぞれ独立した分野をなし発展してきた。特に(1)に視点を置い て数学の定理の分類を目指す研究は「逆数学」の名で米国やシンガポールの研究グループをはじ めとした多くの計算可能性理論の専門家により幅広く進められ、研究代表者もこの分野の発展 に寄与してきた。一方、(2),(3)の視点では欧州を中心とした複数の研究グループが専門的な手 法を発展させてきた。 しかし近年、特にラムゼイの定理等の組み合わせ論の分析において(1),(2) の視点を複合的に 扱った[CJS]や、これにさらに(iii)の視点を加えた [BS] など、複数の尺度を用いる研究が徐々 に行われ始めている。そこで本課題では、これらの視点を複合的に用いた証明分析の新手法を構 築し、また各尺度の相互関連性を調べるなど、こうした多重視点での評価分析の枠組みの整備に 取り組み、さらに実際に具体的な数学命題の評価分析をこうした視点から進めていくことを目 指した。 ２．研究の目的 上記の状況を背景に、本課題では特に数学の定理の分類をより多角的・多数の尺度により行う こと、そのための分野をまたいだ手法の集積、さらにこうした横断的な手法による関連未解決問 題へのアプローチを目標とし、特に次の 3 つのテーマを主軸において研究を行うこととした。 (a) 多重視点に対応した証明解析手法の融合を進め、それを基にした組み合わせ論の諸命題、特 にラムゼイの定理、及び擬順序構造理論の諸命題の強さを評価 (b) 計算機科学におけるプログラムや項書き換え系の停止性検証アルゴリズムにおいて、停止性 検証が可能なプログラム/項書き換え系の限界を、組み合わせ命題の評価から統一的に導出 する方法を確立 (c) 各尺度の評価をより汎用的な手法で行うためのフレームワークの拡充 また、副次的な研究目的として、米国・欧州・シンガポール等の中で個別に洗練されてきた手 法を融合する中で、研究代表者の所属する国内の研究拠点と各国の研究グループを結ぶ国際共 同研究のネットワークの構築も目指した。 ３．研究の方法 2 であげた研究テーマについて、主として各テーマに関連の深い分野の専門家と共同により研 究を行った。特にテーマ (a) については、計算可能性理論の洗練されたテクニックを用いて数々 の組み合わせ論の逆数学研究を行っているカリフォルニア大学バークレー校に長期間の研究滞 在を行い、同研究グループとの共同を軸に研究を進展させた。研究代表者の得意とする算術の超 準モデルを応用する手法に計算可能性理論の様々な手法を取り入れ、さらに順序数解析と呼ば れる証明論のアイデアも用いることで、多様な視点を融合し難問解決へのブレークスルーを得 た。 テーマ (b) においてはトリノ大学の研究グループと共同で研究を開始し、各段階で得られた部 分的な成果を数学関連・計算機科学関連の両方の国際会議の場で公表することを通じてさらに 色々な視点からのアイデアを集め、結果としてベルギー・英国のグループを結んだ幅広いネット ワークで研究を行うこととなった。 さらに (a) の研究を拡充する中で、米国を中心とした逆数学研究の国際連携のネットワークに 加わり、さらにポーランドとシンガポールの共同研究グループの枠組みにも参画したことで、逆 数学研究の枠組みを多様な視点から拡充する機運に恵まれた。テーマ (c) はそのような環境の 中で固定の研究グループによる共同体制に留まらず、関連国際会議の様々な議論の場で共有さ れた問題意識を発展させる形で研究を進めた。

以上に加えて、研究代表者の所属する北陸先端科学技術大学院大学を研究拠点としたJSPS 拠 点形成事業「数理論理学とその応用の国際研究拠点形成」(研究代表:石原哉)が開始され、同事業 に参加する機会に恵まれたため、本課題の研究テーマとこの拠点形成事業の研究テーマを有機 的に結びつけることも目指した。これを通じて解析学の新しい逆数学現象の発見につながるリ ーズ大学(英国)との共同研究や、北陸先端大のグループを中心とした構成主義数学の分離問題に 算術の超準モデル理論を融合する共同研究を行った。 ４．研究成果 本研究課題の主たる成果は以下の通りである。いずれの成果についても国際学術論文誌及び国 際会議において成果の公表を行っている。 (1) ２次元無限ラムゼイの定理の証明論的強さに関する二つの未解決問題の解決、およびそのた めの算術の超準モデル理論と計算可能性理論の融合手法の確立 (2) 組み合わせ論の逆数学研究を理論計算機科学に応用する手法の考案 (3) 解析学における新しい逆数学現象の発見 (1):[1]において算術の超準モデル理論における指標関数と呼ばれる手法を汎用化し、これに 計算可能性理論の強制法を組み合わせることで、グラフ理論における中心定理である 2 次元ラ ムゼイの定理が弱い公理系の下で導出する急増加関数の種類を特定し、それにより逆数学分野 における重要な未解決問題であったラムゼイの定理の無矛盾性の強さ、証明論的強さを決定す る問題を解決した。結果および導入した手法は逆数学分野に留まらず、算術のモデル論分野、(2) であげた停止性検証の理論面への応用があり、加えてヒルベルトの還元主義プログラムと関連 して哲学視点で結果をとらえることもできる。この結果については一般科学雑誌 Quanta Magazine からも取材を受け、記事[QM]として紹介された。さらに[2]において 2 次元多色のラム ゼイの定理の強さを決定する問題をより一般的な形で解決した。具体的には 2 次元多色ラムゼ イの定理の数論的帰結を特徴付ける数学的帰納法公理を完全に特定し、ラムゼイの定理を利用 した証明を数学的帰納法のみを用いた証明に書き換える一般的な手続きを与えた。これらの研 究で用いた手法をさらに改良、洗練することでポーランドのグループなどと共同でより精密な 証明論的分析を進めている。 (2):[3]をはじめとした一連の論文において、逆数学の視点を用いた理論計算機科学における停 止性検証の証明論的側面からの分析手法を提案した。具体的には、システムの停止性を証明する のに必要な公理系の強さを証明論的に評価することで、停止性検証能力の限界が与えられるこ とをふまえ、停止性検証に使われる組み合わせ命題の証明論的強さの評価を行った。ここで提案 した手法により(1)の一連の研究を計算機科学分野に応用していく道筋が開けたと言える。 また[4]では証明論の計算量理論への新しい応用の可能性を示した。ディオファントス方程式 の非決定性を示した MRDP 定理の弱い公理系における証明可能性が線形時間計算可能階層の分離 問題を肯定的に解決することを示した。弱い公理系における証明可能性と計算量階層の関係は これまでにも調べられてきたが、その多くは非常に強い仮定の下に計算量階層の崩壊を導く結 果であった。それに対し本研究では実現可能にも見える比較的弱い証明可能性を仮定して、分離 問題を肯定的に導いており、証明論と計算量理論の新たな関係性を示した結果であると言える。 (3):[5]において変分問題を解く際の基本的な定理の一つである Ekeland の定理の証明にΠ1 1内 包公理と呼ばれる非可述的な強い公理が必要となることを示した。これまで解析学、特に連続的 な現象を扱う微分方程式の解法には、たとえ非常に複雑な計算が必要であっても証明論の意味 での強い公理は必要ないと考えられてきた。この論文はそうした予想に反例を与えるものであ る。これにより、これまで困難と考えられていた解析学、特に微分方程式論の複雑な定理や未解 決問題に証明論の視点からのアプローチを行う足掛かりが得られたと考えている。この論文の 発展として、関数解析学における不動点定理の強さに階層を与える研究を現在進めている。 以上の他、逆数学研究に関連した新しいフレームワーク研究として、算術における証明の長さ の新しい解析手法を与える研究や、算術の超準モデルとクリプキモデルの理論を組み合わせた 直観主義算術体系のクリプキモデルの新しい構成手法の研究等についても一定の成果が得られ、 現在も継続して研究を行っている。 また、以上を通じて、現在では米国、英国、シンガポール、ポーランド、フランスの研究グル ープと継続して研究を行っており、この枠組みを通じて異なる分野の手法の融合を日本を拠点 として進めていきたいと考えている。

参考文献

[1] L. Patey and K. Yokoyama, The proof-theoretic strength of Ramsey’s theorem for pairs and two colors, Advances in Mathematics 330, 1034--1070, 2018.

[2] T.A. Slaman and K. Yokoyama, The strength of Ramsey's theorem for pairs and arbitrarily many colors, Journal of Symbolic Logic 83, 1610--1617, 2018.

[3] S. Steila and K. Yokoyama, Reverse mathematical bounds for the Termination Theorem, Annals of Pure and Applied Logic 167, 1213--1241, 2016.

[4] Y. Chen, M. Müller and K. Yokoyama, A parameterized halting problem, the linear time hierarchy, and the MRDP theorem, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2018, 235--244.

[5] D. Fernández-Duque, P. Shafer and K. Yokoyama, Ekeland's variational principle in weak and strong systems of arithmetic, submitted.

[CJS] P. A. Cholak, C. G. Jockusch, T. A. Slaman, On the strength of Ramsey’s theorem for pairs, J. Symbolic Logic 66, 1–-55, 2001.

[BS] S. Berardi, S. Steila, Ramsey theorem for pairs as a classical principle in intuitionistic arithmetic, TYPES 2013, 64--83.

[QM] Natalie Wolchover, Mathematicians Bridge Finite-Infinite Divide,

５．主な発表論文等 〔雑誌論文〕 計9件（うち査読付論文 8件／うち国際共著 7件／うちオープンアクセス 0件） 2018年 2018年 2018年 2018年 オープンアクセスではない、又はオープンアクセスが困難 該当する 10.1093/logcom/exy003 ３．雑誌名 ６．最初と最後の頁 有 オープンアクセス 国際共著 ２．論文標題 ５．発行年

The strength of SCT soundness

Journal of Logic and Computation 1217-1242

掲載論文のDOI（デジタルオブジェクト識別子） 査読の有無

オープンアクセスではない、又はオープンアクセスが困難 該当する

４．巻 Emanuele Frittaion, Florian Pelupessy, Silvia Steila and Keita Yokoyama 28

１．著者名 10.1017/jsl.2018.19 ３．雑誌名 ６．最初と最後の頁 有 オープンアクセス 国際共著 ２．論文標題 ５．発行年

The strength of Ramsey's theorem for pairs and arbitrarily many colors

Journal of Symbolic Logic 1610-1617

掲載論文のDOI（デジタルオブジェクト識別子） 査読の有無

オープンアクセスではない、又はオープンアクセスが困難 該当する

４．巻 Theodore A. Slaman and Keita Yokoyama 83

１．著者名 10.1016/j.aim.2018.03.035 ３．雑誌名 ６．最初と最後の頁 有 オープンアクセス 国際共著 ２．論文標題 ５．発行年

The proof-theoretic strength of Ramsey's theorem for pairs and two colors

Advances in Mathematics 1034-1070

掲載論文のDOI（デジタルオブジェクト識別子） 査読の有無

オープンアクセス 国際共著

オープンアクセスではない、又はオープンアクセスが困難 該当する

４．巻

Ludovic Patey and Keita Yokoyama 330

１．著者名

A parameterized halting problem, the linear time hierarchy, and the MRDP theorem

Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science 235-244

掲載論文のDOI（デジタルオブジェクト識別子） 査読の有無

10.1145/3209108.3209155

３．雑誌名 ６．最初と最後の頁

有 ４．巻

Yijia Chen, Moritz Muller and Keita Yokoyama

１．著者名

2017年 2016年 2016年 2017年 オープンアクセスではない、又はオープンアクセスが困難 該当する なし ３．雑誌名 ６．最初と最後の頁 有 オープンアクセス 国際共著 ２．論文標題 ５．発行年

The strength of the SCT criterion

Lecture Notes in Computer Science 260--273

掲載論文のDOI（デジタルオブジェクト識別子） 査読の有無

オープンアクセスではない、又はオープンアクセスが困難 該当する

４．巻 Emanuele Frittaion, Silvia Steila and Keita Yokoyama 10185

１．著者名 10.1142/S0219061316500045 ３．雑誌名 ６．最初と最後の頁 有 オープンアクセス 国際共著 ２．論文標題 ５．発行年

On principles between Σ1- and Σ2-induction, and monotone enumerations

Journal of Mathematical Logic 21 pages

掲載論文のDOI（デジタルオブジェクト識別子） 査読の有無

オープンアクセスではない、又はオープンアクセスが困難 該当する

４．巻 Alexander P. Kreuzer and Keita Yokoyama 16

１．著者名 10.1016/j.apal.2016.06.001 ３．雑誌名 ６．最初と最後の頁 有 オープンアクセス 国際共著 ２．論文標題 ５．発行年

Reverse mathematical bounds for the Termination Theorem

Annals of Pure and Applied Logic 1213--1241

掲載論文のDOI（デジタルオブジェクト識別子） 査読の有無

オープンアクセスではない、又はオープンアクセスが困難 −

４．巻

Silvia Steila and Keita Yokoyama 167

１．著者名 なし ３．雑誌名 ６．最初と最後の頁 無 オープンアクセス 国際共著 ２．論文標題 ５．発行年

Recent studies on the proof-theoretic strength of Ramsey's theorem for pairs

RIMS Kokyuroku 67-76

掲載論文のDOI（デジタルオブジェクト識別子） 査読の有無

４．巻

Keita Yokoyama 2050

2016年 〔学会発表〕 計19件（うち招待講演 8件／うち国際学会 17件） 2018年 2019年 2018年 ２．発表標題 ２．発表標題 ２．発表標題

Workshop on Ramsey Theory and Computability（招待講演）（国際学会）

Computability Theory and Foundations of Mathematics 2019（招待講演）（国際学会）

Workshop on Computability Theory and Foundations of Mathematics 2018（国際学会） ３．学会等名 ３．学会等名 ３．学会等名 Keita Yokoyama Keita Yokoyama Keita Yokoyama １．発表者名 １．発表者名 １．発表者名 ４．発表年 ４．発表年 ４．発表年 オープンアクセスではない、又はオープンアクセスが困難 −

Ramsey’s theorem and sizes of proofs

Weihrauch degrees of numerical problems

Approaching the first-order strength of Hindman's theorem なし

３．雑誌名 ６．最初と最後の頁

有

オープンアクセス 国際共著

２．論文標題 ５．発行年

Notes on various versions of Friedman's self-embedding theorem

in;Patrick Cegielski, Ali Enayat, and Roman Kossak (eds.): Studies in Weak Arithmetics 231--241

掲載論文のDOI（デジタルオブジェクト識別子） 査読の有無

４．巻

Keita Yokoyama 3

2018年 2019年 2018年 2017年 ２．発表標題 ２．発表標題 ２．発表標題 ２．発表標題

Computability Theory and Foundations of Mathematics 2017（招待講演）（国際学会） Symposium on Advances in Mathematical Logic 2018（国際学会）

Third Workshop on Mathematical Logic and its Applications,（国際学会）

2018 Winter Meeting of the Association of Symbolic Logic（招待講演）（国際学会） ３．学会等名 ３．学会等名 ３．学会等名 ３．学会等名 Keita Yokoyama Keita Yokoyama Keita Yokoyama Keita Yokoyama １．発表者名 １．発表者名 １．発表者名 ４．発表年 ４．発表年 ４．発表年 ４．発表年

First-order parts of Weihrauch degrees

Ramsey's theorem in arithmetic

On the first-order part of Ramsey's theorem for pairs １．発表者名

2017年 2017年 2017年 2016年 ２．発表標題 ２．発表標題 ２．発表標題 ２．発表標題 Logic Colloquium 2017（招待講演）（国際学会）

Twelfth International Conference on Computability, Complexity and Randomness (CCR 2017)（招待講演）（国際学会）

Oberwolfach Workshop: Mathematical Logic: Proof Theory, Constructive Mathematics（国際学会）

Mathematical Logic and Its Applications（招待講演）（国際学会） Keita Yokoyama Keita Yokoyama Keita Yokoyama Keita Yokoyama ３．学会等名 ３．学会等名 ３．学会等名 ３．学会等名 １．発表者名 １．発表者名 １．発表者名 ４．発表年 ４．発表年

On the Proof-Theoretic Strength of Ramsey's Theorem for Pairs

On the first-order strength of Ramsey's theorem in reverse mathematics

Caristi's fixed point theorem in reverse mathematic

Generalized indicator and forcing ４．発表年

４．発表年 １．発表者名

2016年 2016年 2016年 2016年 ２．発表標題 ２．発表標題

Association for Symbolic Logic 2016 Annual North American Meeting（国際学会） The 11th AIMS Conference on Dynamical Systems（招待講演）（国際学会） ２．発表標題 Keita Yokoyama Keita Yokoyama １．発表者名 １．発表者名 １．発表者名 ３．学会等名 ３．学会等名

Algorithmic Randomness Interacts with Analysis and Ergodic Theory（国際学会） ２．発表標題 ４．発表年 ４．発表年 ４．発表年 ４．発表年 １．発表者名 Keita Yokoyama Keita Yokoyama ３．学会等名

Nonstandard methods in combinatorics

Computable analysis and reverse mathematics

Proof-theoretic strength and indicator arguments

On the first-order strength of Ramsey's theorem for pairs and finitely many colors

３．学会等名

2016年 2017年 2016年 2016年 ２．発表標題 ２．発表標題 ２．発表標題 ２．発表標題

Mathematics for Computation（国際学会）

日本数学会

日本数学会

2016 NFSC-JSPS computer science/joint research workshop（国際学会） ３．学会等名 ３．学会等名 ３．学会等名 ３．学会等名 横山啓太 横山啓太 Keita Yokoyama １．発表者名 １．発表者名 １．発表者名 ４．発表年 ４．発表年 ４．発表年 ４．発表年

Konig's lemma for a tree which has at most finitely many paths in reverse mathematics

On the proof-theoretic strength of Ramsey's theorem for pairs

On the Proof-Theoretic Strength of Ramsey's Theorem for Pairs The proof-theoretic strength of Ramsey's theorem for pairs １．発表者名

〔図書〕 計0件 〔産業財産権〕 〔その他〕 ６．研究組織 横山啓太 - 研究者 - Research map http://researchmap.jp/read0145758/ 所属研究機関・部局・職 （機関番号） 氏名 （ローマ字氏名） （研究者番号） 備考