JAIST Repository
https://dspace.jaist.ac.jp/

Title

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

Author(s)横山, 啓太Citation

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

Issue Date

2020‑06‑01

Type

Research Paper

Text version

publisher

URL

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

RightsDescription

若手研究(B), 研究期間：2016〜2019, 課題番号
：16K17640, 研究者番号：10534430, 研究分野：数理論理学

Japan Advanced Institute of Science and Technology

２版

様

式

Ｃ−１９、Ｆ−１９−１、Ｚ−１９ （共通）

科学研究費助成事業

研究成果報告書
令和

２ 年

６ 月

１ 日現在

機関番号： １３３０２
研究種目： 若手研究(B)
研究期間： 2016 〜 2019
課題番号： １６Ｋ１７６４０
研究課題名（和文）多重視点の証明解析による逆数学の汎用化・深化とその応用研究課題名（英文）Expanding reverse mathematics with multiple viewpoints

研究代表者
横山

啓太（Yokoyama, Keita）

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

研究者番号：１０５３４４３０
交付決定額（研究期間全体）：（直接経費）

3,100,000 円

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

研究成果の学術的意義や社会的意義
2次元ラムゼイの定理の証明論的強さにおける長年の問題の解決とそのための手法の導入は逆数学研究におけるマイルストーンとなり、逆数学や証明論分野の国際会議で関連する多くの話題が取り上げられたほか、ウエブジャーナル Quanta Magazine でも取り上げられた。また、上の結果により、2次元ラムゼイの定理の強さがヒルベ
ルトの還元主義プログラムの視点で十分弱いということが解明されたため、この結果の哲学的意味についても議論がなされた。

研究成果の概要（英文）：In this project, we investigated the complexity and difficulty ofmathematical theorems from the view point of reverse mathematics. Especially, we developed some newtechniques 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 tothe 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.

研究分野： 数理論理学
キーワード： 数理論理学

証明論

逆数学

算術

数学基礎論

ラムゼイの定理

組み合わせ論

計算可能性理論※科研費による研究は、研究者の自覚と責任において実施するものです。そのため、研究の実施や研究成果の公表等については、国の要請等に基づくものではなく、その研究成果に関する見解や責任は、研究者個人に帰属されます。

様式 Ｃ−１９、Ｆ−１９−１、Ｚ−１９（共通）１．研究開始当初の背景
数学で扱われる諸定理・諸命題の強さ・複雑さの論理学的尺度による評価分析は、数学基礎論の主要テーマとして様々な形で研究されてきた。本課題では特に次の 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)であげた停止性検証の理論面への応用があり、加えてヒルベルトの還元主義プログラムと関連
して哲学視点で結果をとらえることもできる。この結果については一般科学雑誌 QuantaMagazine からも取材を受け、記事[QM]として紹介された。さらに[2]において 2 次元多色のラムゼイの定理の強さを決定する問題をより一般的な形で解決した。具体的には 2 次元多色ラムゼ
イの定理の数論的帰結を特徴付ける数学的帰納法公理を完全に特定し、ラムゼイの定理を利用した証明を数学的帰納法のみを用いた証明に書き換える一般的な手続きを与えた。これらの研究で用いた手法をさらに改良、洗練することでポーランドのグループなどと共同でより精密な
証明論的分析を進めている。
(2): [3]をはじめとした一連の論文において、逆数学の視点を用いた理論計算機科学における停止性検証の証明論的側面からの分析手法を提案した。具体的には、システムの停止性を証明するのに必要な公理系の強さを証明論的に評価することで、停止性検証能力の限界が与えられることをふまえ、停止性検証に使われる組み合わせ命題の証明論的強さの評価を行った。ここで提案した手法により(1)の一連の研究を計算機科学分野に応用していく道筋が開けたと言える。
また[4]では証明論の計算量理論への新しい応用の可能性を示した。ディオファントス方程式の非決定性を示した MRDP 定理の弱い公理系における証明可能性が線形時間計算可能階層の分離問題を肯定的に解決することを示した。弱い公理系における証明可能性と計算量階層の関係は
これまでにも調べられてきたが、その多くは非常に強い仮定の下に計算量階層の崩壊を導く結果であった。それに対し本研究では実現可能にも見える比較的弱い証明可能性を仮定して、分離問題を肯定的に導いており、証明論と計算量理論の新たな関係性を示した結果であると言える。
(3):[5]において変分問題を解く際の基本的な定理の一つである Ekeland の定理の証明にΠ11 内
包公理と呼ばれる非可述的な強い公理が必要となることを示した。これまで解析学、特に連続的な現象を扱う微分方程式の解法には、たとえ非常に複雑な計算が必要であっても証明論の意味での強い公理は必要ないと考えられてきた。この論文はそうした予想に反例を与えるものである。これにより、これまで困難と考えられていた解析学、特に微分方程式論の複雑な定理や未解決問題に証明論の視点からのアプローチを行う足掛かりが得られたと考えている。この論文の発展として、関数解析学における不動点定理の強さに階層を与える研究を現在進めている。
以上の他、逆数学研究に関連した新しいフレームワーク研究として、算術における証明の長さの新しい解析手法を与える研究や、算術の超準モデルとクリプキモデルの理論を組み合わせた直観主義算術体系のクリプキモデルの新しい構成手法の研究等についても一定の成果が得られ、現在も継続して研究を行っている。
また、以上を通じて、現在では米国、英国、シンガポール、ポーランド、フランスの研究グル
ープと継続して研究を行っており、この枠組みを通じて異なる分野の手法の融合を日本を拠点として進めていきたいと考えている。

参考文献[1] L. Patey and K. Yokoyama, The proof‑theoretic strength of Ramsey s theorem forpairs 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 andarbitrarily 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 Symposiumon Logic in Computer Science (LICS), 2018, 235‑‑244.
[5] D. Ferná
ndez‑Duque, P. Shafer and K. Yokoyama, Ekeland's variational principle inweak 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 inintuitionistic arithmetic, TYPES 2013, 64‑‑83.
[QM] Natalie Wolchover, Mathematicians Bridge Finite‑Infinite Divide,
https://www.quantamagazine.org/20160524‑mathematicians‑bridge‑finite‑infinite‑divide/５．主な発表論文等〔雑誌論文〕 計9件（うち査読付論文 8件／うち国際共著
１．著者名
Yijia Chen, Moritz Muller and Keita Yokoyama

7件／うちオープンアクセス

0件）
４．巻
‑

２．論文標題A parameterized halting problem, the linear time hierarchy, and the MRDP theorem

５．発行年
2018年

３．雑誌名
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science

６．最初と最後の頁
235‑244

掲載論文のDOI（デジタルオブジェクト識別子）
10.1145/3209108.3209155

査読の有無

オープンアクセス

国際共著

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

該当する

１．著者名
Ludovic Patey and Keita Yokoyama

４．巻

２．論文標題The proof‑theoretic strength of Ramsey's theorem for pairs and two colors

５．発行年
2018年

３．雑誌名
Advances in Mathematics

６．最初と最後の頁
1034‑1070

掲載論文のDOI（デジタルオブジェクト識別子）
10.1016/j.aim.2018.03.035

査読の有無

オープンアクセス

国際共著

330

有

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

該当する

１．著者名
Theodore A. Slaman and Keita Yokoyama

４．巻

２．論文標題The strength of Ramsey's theorem for pairs and arbitrarily many colors

５．発行年
2018年

３．雑誌名
Journal of Symbolic Logic

６．最初と最後の頁
1610‑1617

掲載論文のDOI（デジタルオブジェクト識別子）
10.1017/jsl.2018.19

査読の有無

オープンアクセス

国際共著

83

有

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

該当する

１．著者名
Emanuele Frittaion, Florian Pelupessy, Silvia Steila and Keita Yokoyama

４．巻

２．論文標題The strength of SCT soundness

５．発行年
2018年

３．雑誌名
Journal of Logic and Computation

６．最初と最後の頁
1217‑1242

掲載論文のDOI（デジタルオブジェクト識別子）
10.1093/logcom/exy003

査読の有無

オープンアクセス

国際共著
オープンアクセスではない、又はオープンアクセスが困難

28

有

該当する

１．著者名Keita Yokoyama

４．巻

２．論文標題Recent studies on the proof‑theoretic strength of Ramsey's theorem for pairs

５．発行年
2017年

３．雑誌名
RIMS Kokyuroku

６．最初と最後の頁
67‑76

掲載論文のDOI（デジタルオブジェクト識別子）
なし

査読の有無

オープンアクセス

国際共著

2050

無

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

−

１．著者名
Silvia Steila and Keita Yokoyama

４．巻

２．論文標題
Reverse mathematical bounds for the Termination Theorem

５．発行年
2016年

３．雑誌名
Annals of Pure and Applied Logic

６．最初と最後の頁
1213‑‑1241

掲載論文のDOI（デジタルオブジェクト識別子）
10.1016/j.apal.2016.06.001

査読の有無

オープンアクセス

国際共著

167

有

オープンアクセスではない、又はオープンアクセスが困難
１．著者名
Alexander P. Kreuzer and Keita Yokoyama
２．論文標題On principles between Σ1‑ and Σ2‑induction,

該当する
４．巻
16

and monotone enumerations

５．発行年
2016年

３．雑誌名
Journal of Mathematical Logic

６．最初と最後の頁
21 pages

掲載論文のDOI（デジタルオブジェクト識別子）
10.1142/S0219061316500045

査読の有無

オープンアクセス

国際共著

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

該当する

１．著者名
Emanuele Frittaion, Silvia Steila and Keita Yokoyama

４．巻

２．論文標題The strength of the SCT criterion

５．発行年
2017年

３．雑誌名
Lecture Notes in Computer Science

６．最初と最後の頁
260‑‑273

掲載論文のDOI（デジタルオブジェクト識別子）
なし

査読の有無

オープンアクセス

国際共著
オープンアクセスではない、又はオープンアクセスが困難

10185

有

該当する

１．著者名Keita Yokoyama

４．巻

２．論文標題Notes on various versions of Friedman's self‑embedding theorem

５．発行年
2016年

３．雑誌名
in;Patrick Cegielski, Ali Enayat, and Roman Kossak (eds.): Studies in Weak Arithmetics

６．最初と最後の頁
231‑‑241

掲載論文のDOI（デジタルオブジェクト識別子）
なし

査読の有無

オープンアクセス

国際共著

3

有

オープンアクセスではない、又はオープンアクセスが困難〔学会発表〕 計19件（うち招待講演
１．発表者名Keita Yokoyama

8件／うち国際学会17件）

２．発表標題Ramsey s theorem and sizes of proofs

３．学会等名Workshop on Ramsey Theory and Computability（招待講演）（国際学会）
４．発表年
2018年
１．発表者名Keita Yokoyama

２．発表標題Weihrauch degrees of numerical problems

３．学会等名Computability Theory and Foundations of Mathematics 2019（招待講演）（国際学会）
４．発表年
2019年
１．発表者名Keita Yokoyama

２．発表標題Approaching the first‑order strength of Hindman's theorem

３．学会等名Workshop on Computability Theory and Foundations of Mathematics 2018（国際学会）
４．発表年
2018年

−

１．発表者名
Keita Yokoyama

２．発表標題Ekeland s variational principle in reverse mathematics

３．学会等名Symposium on Advances in Mathematical Logic 2018（国際学会）
４．発表年
2018年
１．発表者名Keita Yokoyama

２．発表標題First‑order parts of Weihrauch degrees

３．学会等名Third Workshop on Mathematical Logic and its Applications,（国際学会）
４．発表年
2019年
１．発表者名Keita Yokoyama

２．発表標題Ramsey's theorem in arithmetic

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

２．発表標題On the first‑order part of Ramsey's theorem for pairs

３．学会等名Computability Theory and Foundations of Mathematics 2017（招待講演）（国際学会）
４．発表年
2017年

１．発表者名
Keita Yokoyama

２．発表標題On the first‑order strength of Ramsey's theorem in reverse mathematics

３．学会等名
Logic Colloquium 2017（招待講演）（国際学会）
４．発表年
2017年
１．発表者名Keita Yokoyama

２．発表標題Caristi's fixed point theorem in reverse mathematic

３．学会等名Twelfth International Conference on Computability, Complexity and Randomness (CCR 2017)（招待講演）（国際学会）
４．発表年
2017年
１．発表者名Keita Yokoyama

２．発表標題Generalized indicator and forcing

３．学会等名Oberwolfach Workshop: Mathematical Logic: Proof Theory, Constructive Mathematics（国際学会）
４．発表年
2017年
１．発表者名Keita Yokoyama

２．発表標題On the Proof‑Theoretic Strength of Ramsey's Theorem for Pairs

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

１．発表者名
Keita Yokoyama

２．発表標題Nonstandard methods in combinatorics

３．学会等名The 11th AIMS Conference on Dynamical Systems（招待講演）（国際学会）
４．発表年
2016年
１．発表者名Keita Yokoyama

２．発表標題Computable analysis and reverse mathematics

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

２．発表標題Proof‑theoretic strength and indicator arguments

３．学会等名Workshop on Mathematical Logic and its Applications（国際学会）
４．発表年
2016年
１．発表者名Keita Yokoyama

２．発表標題On the first‑order strength of Ramsey's theorem for pairs and finitely many colors

３．学会等名Association for Symbolic Logic 2016 Annual North American Meeting（国際学会）
４．発表年
2016年

１．発表者名
Keita Yokoyama

２．発表標題The proof‑theoretic strength of Ramsey's theorem for pairs

３．学会等名Mathematics for Computation（国際学会）
４．発表年
2016年
１．発表者名横山啓太

２．発表標題Konig's lemma for a tree which has at most finitely many paths in reverse mathematics

３．学会等名
日本数学会
４．発表年
2017年
１．発表者名横山啓太

２．発表標題On the proof‑theoretic strength of Ramsey's theorem for pairs

３．学会等名
日本数学会
４．発表年
2016年
１．発表者名Keita Yokoyama

２．発表標題On the Proof‑Theoretic Strength of Ramsey's Theorem for Pairs

３．学会等名2016 NFSC‑JSPS computer science/joint research workshop（国際学会）
４．発表年
2016年

〔図書〕

計0件

〔産業財産権〕〔その他〕
横山啓太 ‑ 研究者 ‑ Research map
http://researchmap.jp/read0145758/

６．研究組織氏名（ローマ字氏名）（研究者番号）

所属研究機関・部局・職（機関番号）

備考