JAIST Repository
https://dspace.jaist.ac.jp/Title「3次元的逆数学」のための基盤構築

Author(s)横山, 啓太Citation

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

Issue Date

2015‑06‑01

TypeResearch Paper

Text version

publisher

URL

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

RightsDescription

研究種目：研究活動スタート支援, 研究期間
：2013〜2014, 課題番号：25887026, 研究者番号：10534430, 研究分野：数学基礎論, 数理論理学

Japan Advanced Institute of Science and Technology

１版

様式

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

科学研究費助成事業

研究成果報告書
平成 ２７ 年

６ 月

１ 日現在

機関番号： １３３０２
研究種目： 研究活動スタート支援
研究期間： 2013 〜 2014
課題番号： ２５８８７０２６
研究課題名（和文）「3次元的逆数学」のための基盤構築

研究課題名（英文）The start‑up for reverse mathematics from various angles

研究代表者
横山啓太（YOKOYAMA, Keita）

北陸先端科学技術大学院大学・情報科学研究科・助教
研究者番号：１０５３４４３０
交付決定額（研究期間全体）：（直接経費）

2,100,000 円

研究成果の概要（和文）：数学の諸命題の強さを論理学の視点から分析する逆数学研究の基盤を広げ、より多様な視点から数学の諸命題の評価を行うことを目指して研究を行った。特に、これまで計算可能性理論の視点からの命題の強さの評価に偏りがちだった組み合わせ命題の強さについて、帰納法の強さ等の証明論的強さの視点からの評価を行うための諸種の手法の導入を行った。さらに、これらの成果を構成的数学の視点を踏まえて計算機科学、特にプログラム検証の分野と結びつけるための道筋を得た。

研究成果の概要（英文）：The purpose of this research is to develop several new approaches for the studyof reverse mathematics, whose goal is to determine the strength of ordinary mathematical theorems fromvarious angles. In this research, I investigated the proof‑theoretic strength of several combinatorial
principles and introduced several new methods to determine the proof‑theoretic strength. I also found a
new way to apply these results into the study of termination analysis.

研究分野： 数学基礎論、数理論理学
キーワード： 逆数学

２階算術

組み合わせ論

証明論

計算可能性理論数学基礎論

様 式 Ｃ−１９、Ｆ−１９、Ｚ−１９（共通）１．研究開始当初の背景
数学の定理の論理学の手法による評価は論理学の主要なテーマの一つであり、様々な形で大きな成功を遂げてきている．その一つが逆数学と呼ばれる手法である。逆数学研究
は H. Friedman により 1970 年代に始められ、S. Simpson らによって多くの数学の定理の強さの評価がなされてきた。表においてRCA0 が計算可能な手法に対応した基準となる公理系であり、WWKL0, WKL0, ACA0 はそれぞれ計算可能性理論における諸種の概念にも対応した集合存在公理で特徴付けられる公理系である。(逆数学の主要な結果については[Sim]を参照。)
逆数学によ る 定理分類 ( 逆数学現象) の例
公理系
同値にな る 定理群
RCA 0
代数学の基本定理 ( 代) *陰関数定理 ( 解)*正則関数の解析性 ( 解)W W K L0
ルベーグ測度の可算加法性 ( 解)*デルタ 関数の存在 ( 解)W K L0*ジ ョ ルダン ＝シ ェ ーン フ リ ースの定理 ( 幾)*コ ーシ ーの積分定理 ( 解) 不動点定理 ( 幾)ACA 0*リ ーマ ン の写像定理 ( 解)
無限次元ベク ト ル空間の基底の存在定理 ( 代)(代)は代数，(解)は解析，(幾)は幾何の定理の分類, {*} は自身による結果

私はこれまでに主に自然数とその部分集合を扱う 2 階算術と呼ばれる公理体系を基盤とした逆数学研究を行ってきた。より具体的には，「効率的に逆数学による定理の評価・分類を進め、逆数学の枠組みを拡大すること」を目指して研究を行ってきた。このため、数学の具体的な定理の評価を直接行うだけでなく、2 階算術の枠組みそのものを拡張する研究も並行して行い基礎的な解析学等の分類で成果を上げてきた。
しかし、近年の研究である種の命題、特に弱い組み合わせ命題の強さの評価は既存の方法ではなかなか上手く行えないことが分かってきた。一方で、逆数学以外にも数学の命題の論理学の手法による評価方法は様々有り、特に計算機科学(計算可能性理論や計算量理論)や直観主義論理を用いた構成的数学を用いた手法は多くの成功を収めている。(これらの一部の研究まで含めて、広く逆数学と呼ばれることもある。)この 3 種の異なる数学の命題の評価方法については、相互に深い関わりがありながら、相互に他の手法では測ることの出来ない独立した尺度を備えている。
そこで、今後こうした手法をさらに発展させていくためには、この 3 種類、あるいはより多くの独立した尺度を統一的に扱い、単純に命題が「強い弱い」というだけの一次元的な評価から、多次元的な物の見方に引き上げていく必要があると考えた。
[Sim] S. G. Simpson, Subsystems of Second
Order
Arithmetic,
SecondEdition,
Association for Symbolic Logic. Cambridge
University Press, 2009.

２．研究の目的
本研究の先に広がる長期的な目標は、上述の数学的命題の多次元的な評価・分類の枠組みを作り上げ、数学、論理学、計算機科学の専門家が同じ枠組みで多様な数学の命題の評価を進め、さらにそれを各分野に応用していけるような広範なフィールドを築くことである。ただしこの研究の完成には長期的な取り組みが必要と考えられる。そこで本研究ではこうした長期目標のための基盤構築として、特にこれまで自身の研究の基盤としていた算術領域の公理系を再整備し、一定の比較的弱い範囲の数学の命題に多元的な視点からの評価基盤を与える。さらにその公理系を利用して、特に弱い組み合わせ命題の 3 次元的評価を与え、重要なサンプルケースを与える。

３．研究の方法
平成２５年度は主に逆数学をより証明論的な立場から拡張することを念頭に研究を行った。特に、逆数学の枠組みで帰納法の強さを評価する新たな手法の確立に力を注いだ。まず、これまでの研究で自身が構想していたモデル論的手法を逆数学に応用する方法をワルシャワ大学の Kolodziejczyk 氏も構想していることを知ったため、email 等でのやりとりを通じて議論を深めた。
また、組み合わせ論の諸命題の強さを包括的に調べる研究の一環として、東北大学の村上氏、山崎氏の提唱するオートマトンの停止性と関連の深いラムゼイの定理の弱いバリエーションについてその強さを調べる研究を進めた。その中で最近発表された Lermanら[LST]により扱われている ADS や CAC と呼ばれる組み合わせ命題と上述の組み合わせ命題の深い関連性が得られたため、これら周辺の組み合わせ命題との比較を特に重視して強さの評価を進めた。
加えて、より研究の幅を広げ周辺の分野との研究交流を深める目的で、逆数学と計算可能性理論の国際会議 Computability Theoryand Foundations of Mathematics のプログラム委員を務め、プログラムの編成等に貢献した。この会議を通じ、コネチカット大学のDzhafarov 氏 や ペ ン シ ル バ ニ ア 大 学 のTowsner 氏らとの研究交流を深め、特に逆数学の新たな発展の方向性を議論し合う等、将来的な見通しについての展望の構想につなげた。
平成２６年度は、前年度からの研究を継続するとともに、新たな逆数学基盤の拡大を目指すべく各国の研究者との研究交流を深めた。５月には超準解析学及び計算機科学に関する集会を主催し、また６月以降にComputability,ComplexityandRandomness( シ ン ガ ポ ー ル ) 、 Workshop onweak arithmetic( ス ウ ェ ー デ ン ) 、 Logic
Colloquium(オーストリア)等に参加し、研究成果を公表するとともに計算可能性理論、ランダムネス、算術の証明論およびモデル理論、計算機科学等の諸分野の情報収集を進め、また関連分野の研究者との交流を深めた。特にそれらの研究交流の中で、トリノ大学のBerardi 氏、Steila 氏らが提唱するラムゼイの定理の構成的証明からのプログラム抽出の手法と自身の進める有限ラムゼイの定理の証明論的分析の関わりが深いことが分かり、共同研究を開始した。この研究は計算機科学、特にプログラム検証分野との関連性が強く期待されるため、そちらの分野の関連研究、特に Podelski/Rybalchenko[PR]によるプログラム検証にラムゼイの定理を応用する手法との関連性を軸に研究を展開した。
また１月にはインドで開催された AsianLogic Conference で講演を行うとともに情報を収集し、この中でシンガポール国立大学のKreuzer 氏の最新の成果と自身の関連研究を組み合わせることで、近年注目されているChong ら[CYS]の論文で鍵として用いられた組み合わせ命題 BME の強さの評価が確定できることが分かった。この結果をさらに一般的な形に発展させるため、Krouzer 氏との共同研究を行った。
２、３月にはカリフォルニア大学バークレー校とコネチカット大学を訪問し、自身の研究で得られた結果をセミナーで説明するとともに研究の総括を行った。
[LST] Manuel Lerman, Reed Solomon andHenry Towsner, Separating principles
below Ramsey s Theorem for Pairs, Journalof Mathematical Logic 13(2), 44 pages,
2013.
DOI: 10.1142/S0219061313500074[PR] Andereas Podelski and Andrey
Rybalchenko, Transition invariants, In
LICS 2004: Logic in Computer Science,
32–41, IEEE, 2004.
[CSY] C. T. Chong, Theodore A. Slaman, andYue Yang, The inductive strength ofRamsey s theorem for pairs, 2014,
Preprint.

４．研究成果本研究では、特に証明論的な視点から逆数学研究を拡張する成果が多く得られた。まず得られたのが、shortening cut と呼ばれる算術のモデル理論の手法の逆数学への応用である。この手法にその他の手法を組み合わせることで、シグマ 1 帰納法を成り立たせないような算術のモデルの内側に自分自身とは同型にならないより複雑な内部モデルを擬似的に構成できることを示した。これを応用して、自然数の構造の自然な二階公理化から得られる範疇性は必ずシグマ 1 帰納法を導くことを示し、J. Vaananen により提示されていた自然数の二階範疇性の強さの問題をより一般的な形で解決した。この成果はKolodziejczyk 氏との共著論文[1]としてまとめられている。この結果は、個別の命題の強さでは無く、一定の性質を持つ数学命題の強さを包括的に評価するもので、これは今までの逆数学研究には無いタイプの成果である。今後この手法を一般にモデル論におけるcut の構成と逆数学の包括手法を結びつける一般的な方法論に拡張することも考えていきたい。
また、ラムゼイの定理型の組み合わせ命題の証明論的強さをより詳しく評価するため、有限ラムゼイ定理の様々なバリエーションを考案し、それらを導くような自然な無限組み合わせ命題が何であるかを探った。特に、ラムゼイの定理を変形して多重化させ、単独の適用とどのように強さが変化するかに着目した。結果として得られた無限組み合わせ命題は、計算可能性の立場からはラムゼイの定理をわずかに強めた自然な拡張で多重化によって強さが変化せず、一方証明論的な視点からは繰り返す毎に強さが増す、という性質を有することが分かった。さらに、ここで導入したラムゼイの定理の多重版がラムゼイの定理の無矛盾性を主張する命題と同値であることをつきとめた。ラムゼイの定理には有限版と無限版の 2 種類があり、これまで有限ラムゼイの定理は無限ラムゼイの定理の弱い帰結であると考えられてきたが、上記の結果は実は無限版のラムゼイの定理がある種の有限版のラムゼイの定理と見なせることを示している。
また、Kreuzer 氏との共同研究により、近年新たに組み合わせ名だの強さの研究で課題としてあがっていた組み合わせ命題 BME の強さの検証を進め、BME が特定の順序構造の整序性と完全に同値になることが分かった。
このことは今後のラムゼイの定理の証明論的強さの検証に大いに役立つ。
計算機科学との関連性についての研究では、オートマトンの停止性と関連の深いラムゼイの定理の弱いバリエーションの計算可能性・証明論双方の立場からの強さを、東北大学の村上氏、山崎氏と共同研究で確定する
こ と が 出 来 た [2] 。 さ ら に こ の 成 果 が 、Berardi 氏、Steila 氏によるラムゼイの定理の証明論的分析によりプログラムの停止性を検証するプロジェクトに応用できることが分かった。この手法について両氏とさらに詳細に研究を進めたところ、上記のラムゼイの定理の弱いバリエーションに限らず、ラムゼイの定理の有限・無限の諸種のバリエーシ
ョンがプログラムの停止性(特に計算時間の上界)と密接に関わり合うことが分かった。
この成果は、組み合わせ論の逆数学研究が計算機科学に重要な応用を持つことを示している。

５．主な発表論文等〔雑誌論文〕（計 5 件）[1] Leszek Aleksander Kołodziejczyk andKeita
Yokoyama,
Categoricalcharacterizations of the natural numbers
require primitive recursion, Annals ofPure and Applied Logic 166, 219‑231, 2015.
(査読有)
DOI: 10.1016/j.apal.2014.10.003[2] Shota Murakami, Takeshi Yamazaki andKeitaYokoyama,On
theRamseyan
factorization theorem, in the proceedingsof Computability in Europe 2014, Language,Life, Limits, Lecture Notes in Computer
Science 8493, 2014, 324‑332. (査読有)DOI: 10.1007/978‑3‑319‑08019‑2̲33[3] Kojiro Higuchi, Phil Hudelson, Stephen
G. Simpson and Keita Yokoyama, Propagationof partial randomness, Annals of Pure andApplied Logic 165, 742‑758, 2014. (査読有)DOI: 10.1016/j.apal.2013.10.006[4] Yoshihiro Horihata and Keita Yokoyama,Nonstandard second‑order arithmetic andRiemann's mapping theorem, Annals of Pureand Applied Logic 165, 520‑551, 2014. (査読有)DOI: 10.1016/j.apal.2013.06.022[5] Stephen G. Simpson and Keita Yokoyama,Reversemathematics
andPeano
categoricity, Annals of Pure and AppliedLogic 164(3), 284‑293, 2013. (査読有)DOI: 10.1016/j.apal.2012.10.014〔学会発表〕（計 8 件）[1] Keita Yokoyama, Reverse mathematics
and program termination, Berkeley Logic
Colloquium, University of California,
Berkeley, USA, March 20, 2015.
[2] Keita Yokoyama, What is needed tocharacterize the natural number system?
Shiinoki Complex, Kanazawa, Ishikawa,Japan, March 6, 2015.
[3] Keita Yokoyama, Reverse mathematics
and termination analysis, 14th Asian Logic
Conference, IIT Bombay, India, January 5‑8,2015 (招待講演).
[4] Keita Yokoyama, Termination theorem
and Ramsey's theorem, IMS‑JSPS Joint
Workshop in Mathematical Logic andFoundations of Mathematics, National
University of Singapore, September 1‑5,
2014 (招待講演).
[5] Keita Yokoyama, Proof transformations
for nonstandard analysis, The 10th AIMS
Conferenceon
DynamicalSystems,Differential Equations and Applications,
Special session 114: Nonstandard Analysis,
Quantizations and Singular Perturbations,Madrid, Spain, July 10, 2014 (招待講演).

[6] Keita Yokoyama, Use of nonstandard
models in reverse mathematics, Journé
essur les Arithmétiques Faibles 33,
University of Gothenburg, Sweden, June 17,
2014.
[7] Keita Yokoyama, The strength ofRamsey's theorem from several different
view points, CORCON 2014 Workshop, Genoa,Italy, March 25, 2014.
[8] Keita Yokoyama, Finite iterations ofinfinite and finite Ramsey's theorem,
Computability Theory and Foundations ofMathematics 2014, Tokyo Institute ofTechnology, February 18, 2014.
〔図書〕（計 0 件）〔産業財産権〕○出願状況（計 0 件）
○取得状況（計 0 件）
〔その他〕
ホームページ(Research map)
http://researchmap.jp/read0145758/?lang=japanese
６．研究組織(1)研究代表者
横山 啓太（YOKOYAMA, Keita）
北陸先端科学技術大学院大学・情報科学研
究科・助教
研究者番号：１０５３４４３０