2012 Fiscal Year Annual Research Report
| Project/Area Number |
24840022
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
根元 多佳子 北陸先端科学技術大学院大学, 情報科学研究科, 助教 (20546155)
|
|---|
| Project Period (FY) |
2012-08-31 – 2014-03-31
|
| Keywords | 数理論理学 |
|---|
| Research Abstract |
平成２４年度は、当初の計画では演算適用の体系 APP の性質や、集合論を APP に翻訳するための手法の調査を行い APP と同じ証明能力をもつ CZF の自然な部分体系を調べる計画であった。しかし、研究を進める中で先に、より強い演算適用の体系の一種である Explicit Mathematics の体系 T_0 やその拡張と集合論の体系間の翻訳の関係を調べる方が本来の目的である APP と集合論間の翻訳の構築にも役に立つと判断されたため、前者を中心に行った。
具体的には、K. Sato （ベルン大学）により提案された集合論の体系 KP\beta の亜種との体系 T_0 への翻訳の手法の応用で、bisimilar interpretation、 double negation translation、forcing、realizability interpretation などを経て KP+\Pi_3 reflection の T_0+ 2-Uni への翻訳を構築しようというもので、現在も進行中である。また、この翻訳に関連する二階算術の体系においての順序数と、集合論において重要な性質である決定性との関係についても集合存在公理のひとつである arithmetical transfinite recursion の制限公理と \Delta02 決定性の部分命題との関係が明らかになり、現在雑誌投稿論文を準備中である。これらの研究は、クライストチャーチ大学（ニュージーランド）、リーズ大学（イギリス）、ベルン大学（スイス）への数週間の訪問で、関連する分野の研究者と集中的に議論を行うことで進められた
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
当初の計画と順番は異なるものの、２４年度に行った研究の結果により、これまで困難とされてきた Explicit Mathematics の体系への集合論の埋め込みの手法について明らかになりつつあり、これは本来の目的である APP と集合論間の翻訳の構築にも非常に重要な手法となると考えられる。また、この研究の発端はこれまでの算術の体系に基づいた逆数学で扱いにくかった順序数などの逆数学的挙動を調べるために集合論で同様の役割を果たすものを探そうという発想であったが、昨年度行った決定性と算術の体系の間の関係の研究でも順序数をと逆数学の関係を扱っており、本来の方針とはやや異なるものの、逆数学において順序数を扱う手法の開発という点では成果が得られ、おおむね順調に研究が進んでいると判断した。
|
| Strategy for Future Research Activity |
まずは、現在進めている Explicit Mathematics の体系 T_0+2-Uni への KP+\Pi_3 reflection の翻訳を完成させることが第一の課題である。
さらにその手法を応用して、本来の目的である、より演算適用の体系 APP と集合論との間の翻訳の手法の研究を次の順番で進める予定である。
１．構成的逆数学の算術の体系 EL と同程度の証明能力をもつ演算適用の体系 APP に対して P. Aczel により提案された集合論の型理論への翻訳の手法や、２４年度の研究で得られた集合論の Explicit Mathematics の体系のへの翻訳の手法を応用し、集合論の言語からの翻訳を構成する。
２．上記１で構成した手法を用い、 APP と集合論の体系 CZF に対して (1) APP と同程度の証明能力をもつ CZF の自然な部分体系を明らかにする (2) 逆に APP に自然な公理を加え、演算適用の体系として CZF と同程度の証明能力をもた体系を明らかにする、という順番で演算適用の体系と集合論の体系の間の翻訳を整備する。
３．上記２で得られた APP に対応する集合論の体系上で実際に順序数など算術の体系では扱いにくかった対象について、その挙動を逆数学的に調べる。
|
