2013 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 | applicative theory / proof theory / set theory / interpretation |
|---|
| Research Abstract |
今年度は行った研究は１.算術体系に翻訳可能な演算適用の体系 APP に対応する集合論について２．演算適用の体系にクラスの概念を付け加えた体系である Explicit Mathematics の体系と集合論の間の翻訳の関係について３．そのような体系に関係する順序数構造と決定性命題の関係についての研究を行った。
１．APP に翻訳可能な演算適用の体系としては、P. Aczel によって提案された直観主義上の集合論の型理論の体系への翻訳と類似した手法をどこまで集合論から演算適用の体系で用いることができるかを調べた。結果としては、正楚性を持たない集合論で、とくに「宇宙」と呼ばれる「集合全体からなる集合」の存在を許す集合論の翻訳が部分的に可能であることがわかり、APP を無矛盾性等価な断片を求めることができた。いくつかの結果は3月にイタリア・ジェノヴァで行われた国際研究集会 Correctness by Costruction にて発表した。
２．Explicit Mathematics の体系と集合論の間の翻訳の関係については、強制法やrealizablitey interpretation、その他いくつかの手法の組み合わせで行える翻訳の可能性について調べた。
３．決定性命題については超限再帰法を許す順序数を制限することで APP と同程度の無矛盾性の強さを持つことができる二階算術の体系について、そこで証明可能な数学的命題である決定性の強さについての研究を行った。この結果は9月にスイス･ベルンで行われた国際研究集会 Proof で発表した。
|
| Current Status of Research Progress |
Reason
25年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
25年度が最終年度であるため、記入しない。
|
