| 研究課題/領域番号 |
14J04387
|
|---|
| 研究機関 | 東北大学 |
|---|
研究代表者 |
藤原 誠 東北大学, 理学研究科, 特別研究員(DC2)
|
|---|
| 研究期間 (年度) |
2014-04-25 – 2016-03-31
|
| キーワード | 数学基礎論 / 逆数学 / 構成的数学 / 直観主義論理 / 存在定理 |
|---|
| 研究実績の概要 |
存在定理の一様証明可能性と直観主義証明可能性に関する理論的解析と実験的解析の両方に取り組み，その両者において以下の成果を得た．
理論的解析においては，自身らの既存の結果をさらに拡張し，前提が純全称的で帰結がΓ2に属するΠ2型論理式として形式化される任意の存在定理Sに対し，Sの一様版がRCAの弱外延性保存的高階拡大WRCAω上ACAの一様版を導出するならば，Sは非構成的関数存在公理WKLを含む直観主義高階算術体系iWKLω+にBar帰納法BIを加えた体系で証明できないことを示した．さらに，「存在定理SがRCAで一様証明可能である」ことの厳密な形式化を与え，比較的単純な形のΠ12論理式として形式化される任意の存在定理Sに対して，SがRCAで一様証明可能であることと直観主義証明可能であることが同値であることを示した．
一方，実験的解析においては，2×2実行列のジョルダン分解可能性及びΠ01最小値原理の一様証明可能性を解析し，これらの一様版がWRCAω上ACAの一様版を導出することを示した．さらに，これらの主張は，前提が純全称的で帰結がΓ2に属するΠ2型論理式として形式化されることを確かめた．これにより，理論的解析における上記の結果が適用でき，2×2実行列のジョルダン分解可能性及びΠ01最小値原理が上記の直観主義高階算術体系で証明できないことが判明した．しかし，直観主義算術体系上これらの主張と同値となる論理原理や非構成的関数存在公理の解明には未だ至っていない．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
これまでの研究により，存在定理の一様証明可能性と直観主義証明可能性の関係性に関する既存の結果を拡張する結果及び関連する興味深い結果が得られている．しかし，具体的な存在定理に対して直観主義高階算術体系上同値となる論理原理や非構成的関数存在公理を特定するには至っていないため，当初の計画からはやや遅れていると言えよう．
|
| 今後の研究の推進方策 |
本研究の目標は，RCAで非一様証明可能な存在定理に対して直観主義高階算術体系上同値となる論理原理を特定すること，及びRCAで証明できない存在定理に対して直観主義高階算術体系上同値となる論理原理や非構成的関数存在公理を特定することであった．これまでのところ，具体的ないくつかの存在定理が直観主義高階算術体系上比較的強い論理原理や非構成的関数存在公理から証明不可能であることは示せているものの，同値となる論理原理や構成的関数存在公理の特定には未だ至っていない．特に，直観主義高階算術体系上で具体的な存在定理から論理原理や構成的関数存在公理を導く方向の結果は未だ得られていない．そのため，今後は直観主義高階算術上で論理原理の階層の更なる解析を行う．これは，考察している無限鳩ノ巣原理やWWKL等の存在定理が既知の論理原理とは同値にならない可能性が考えられるためである．一方で，平行して，これらの存在定理から何かしらの論理原理や構成的関数存在公理が導出されることを示すことを目指す．そのために構成的逆数学における既存の証明法を参考にする．
|
