存在定理の一様証明可能性及び直観主義証明可能性に関する逆数学的解析

存在定理的一致可证明性和直觉可证明性的逆向数学分析

• 批准号: 14J04387
• 负责人: 藤原 誠
• 金额: $ 1.09万
• 依托单位: Japan Advanced Institute of Science and Technology (2015)Tohoku University (2014)
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for JSPS Fellows
• 财政年份: 2014
• 资助国家: 日本
• 起止时间: 2014-04-25 至 2016-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-14J04387/
• 关键词: 構成的数学; 直観主義論理; 逆数学; 数学基礎論; 存在定理

今年度は本研究課題に関して大きく二つの成果が得られた．まず，直観主義高階算術における論理原理の織り成す構造の解析において，重要な研究成果が得られた．特に，古典的逆数学における観点から自然に考えられる12種類の論理原理を検討し，それらの論理原理とマルコフ原理等これまで構成的逆数学で扱われてきた3種類の論理原理との逆数学的関係性を完全に解明した．マルコフ原理よりも弱い論理原理はこれまでにほとんど発見されておらず，本研究成果は構成的逆数学に一つの新たなる階層をもたらすものとなった．なお，本研究成果は北陸先端科学技術大学院大学の石原哉教授，根元多佳子助教との共同研究の成果である．この研究の延長として，自然に考えられる他の論理原理についても現在調査を進めている．一方で，存在定理の一様証明可能性及び直観主義証明可能性に関する新たなるメタ定理が得られた．自身の先行結果のさらなる拡張として，比較的単純な形のΠ12論理式として形式化される全ての存在定理Sに対して，「Sが弱ケーニヒの補題WKLを含む古典的逆数学の体系で一様証明可能であること」と「Sが構成的数学の体系で証明可能であること」が同値であることを示した．この証明にはmonotone functional interpretationと呼ばれるProof mining研究で用いられている証明論の手法を使った．

This year's research topic is related to the achievements of the two major issues. In the analysis of the structure of logic principles in higher order arithmetic, important research results have been obtained. In particular, the classical inverse mathematics has been completely explained by the relationship between the 12 kinds of logical principles and the 3 kinds of logical principles. A new hierarchy of inverse mathematics is formed by the results of this study. The results of this research are the joint research results of Professor Ishihara and Assistant Professor Takako Nemoto of Hokuriku Advanced University of Science and Technology. This research extends and naturally examines other logical principles. A new theorem is obtained by proving the possibility of an existence theorem and the possibility of a straightforward proof. The existence theorem S corresponds to "S This Proof is a monotone functional interpretation and a proof of mining.

项目成果

Constructive provability versus uniform provability in classical computable mathematics

经典可计算数学中的构造性可证明性与一致可证明性

• 发表时间: 2015
• 作者: Makoto Fujiwara;Hajime Ishihara and Takako Nemoto;Makoto Fujiwara;Makoto Fujiwara;Makoto Fujiwara;Makoto Fujiwara;Makoto Fujiwara;Makoto Fujiwara;藤原 誠;Makoto Fujiwara
• 通讯作者: Makoto Fujiwara

Note on total and partial functions in second-order arithmetic

二阶算术中的全函数和偏函数的注释

• 发表时间: 2015
• 期刊: 京都大学数理解析研究所講究録
• 作者: 坪井祐司;山本博之;山口元樹;野中葉;篠崎香織;Makoto Fujiwara and Ulrich Kohlenbach;Makoto Fujiwara and Takashi Sato
• 通讯作者: Makoto Fujiwara and Takashi Sato

存在定理の構成的証明可能性について

论存在定理的构造性可证明性

• 发表时间: 2015
• 作者: Makoto Fujiwara;Hajime Ishihara and Takako Nemoto;Makoto Fujiwara;Makoto Fujiwara;Makoto Fujiwara;Makoto Fujiwara;Makoto Fujiwara;Makoto Fujiwara;藤原 誠;Makoto Fujiwara;藤原 誠
• 通讯作者: 藤原 誠

Intuitionistic provability versus uniform provability in RCA

RCA 中的直观可证明性与一致可证明性

• DOI: 10.1007/978-3-319-20028-6_19
• 发表时间: 2015
• 期刊: Lecture Notes in Computer Science
• 作者: 坪井祐司;山本博之;山口元樹;野中葉;篠崎香織;Makoto Fujiwara and Ulrich Kohlenbach;Makoto Fujiwara and Takashi Sato;Makoto Fujiwara
• 通讯作者: Makoto Fujiwara

Some principles weaker than Markov’s principle

一些比马尔可夫原理弱的原理

• DOI: 10.1007/s00153-015-0444-9
• 发表时间: 2015
• 期刊: Archive for Mathematical Logic
• 影响因子: 0.3
• 作者: Makoto Fujiwara;Hajime Ishihara and Takako Nemoto
• 通讯作者: Hajime Ishihara and Takako Nemoto